present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
authorwenzelm
Sat Mar 26 21:45:29 2011 +0100 (2011-03-26 ago)
changeset 42129c17508a61f49
parent 42128 eb84d28961a9
child 42130 e10e2cce85c8
child 42137 6803f2fd15c1
present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Mar 26 21:28:04 2011 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Mar 26 21:45:29 2011 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4    type isar
     1.5    val isar: TextIO.instream -> bool -> isar
     1.6    val prepare_command: Position.T -> string -> Toplevel.transition
     1.7 -  val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> (unit -> unit) * theory
     1.8 +  val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> theory * unit future
     1.9  end;
    1.10  
    1.11  structure Outer_Syntax: OUTER_SYNTAX =
    1.12 @@ -288,11 +288,16 @@
    1.13      val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion atoms);
    1.14      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    1.15  
    1.16 -    fun after_load () =
    1.17 -      Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
    1.18 -      |> Buffer.content
    1.19 -      |> Present.theory_output name;
    1.20 -  in (after_load, thy) end;
    1.21 +    val present =
    1.22 +      singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
    1.23 +        deps = map Future.task_of results, pri = 0})
    1.24 +      (fn () =>
    1.25 +        Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup
    1.26 +          (maps Future.join results) toks
    1.27 +        |> Buffer.content
    1.28 +        |> Present.theory_output name);
    1.29 +
    1.30 +  in (thy, present) end;
    1.31  
    1.32  end;
    1.33  
     2.1 --- a/src/Pure/Isar/toplevel.ML	Sat Mar 26 21:28:04 2011 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Mar 26 21:45:29 2011 +0100
     2.3 @@ -89,7 +89,8 @@
     2.4    val add_hook: (transition -> state -> state -> unit) -> unit
     2.5    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     2.6    val command: transition -> state -> state
     2.7 -  val excursion: (transition * transition list) list -> (transition * state) list lazy * theory
     2.8 +  val excursion:
     2.9 +    (transition * transition list) list -> (transition * state) list future list * theory
    2.10  end;
    2.11  
    2.12  structure Toplevel: TOPLEVEL =
    2.13 @@ -655,7 +656,7 @@
    2.14        Proof.is_relevant (proof_of st')
    2.15      then
    2.16        let val (states, st'') = fold_map command_result proof_trs st'
    2.17 -      in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end
    2.18 +      in (Future.value ((tr, st') :: (proof_trs ~~ states)), st'') end
    2.19      else
    2.20        let
    2.21          val (body_trs, end_tr) = split_last proof_trs;
    2.22 @@ -679,8 +680,8 @@
    2.23            (case States.get (presentation_context_of st'') of
    2.24              NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
    2.25            | SOME states => states);
    2.26 -        val result = Lazy.lazy
    2.27 -          (fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]);
    2.28 +        val result = states
    2.29 +          |> Future.map (fn sts => (tr, st') :: (body_trs ~~ sts) @ [(end_tr, st'')]);
    2.30  
    2.31        in (result, st'') end
    2.32    end;
    2.33 @@ -691,6 +692,6 @@
    2.34      val immediate = not (Goal.future_enabled ());
    2.35      val (results, end_state) = fold_map (proof_result immediate) input toplevel;
    2.36      val thy = end_theory end_pos end_state;
    2.37 -  in (Lazy.lazy (fn () => maps Lazy.force results), thy) end;
    2.38 +  in (results, thy) end;
    2.39  
    2.40  end;
     3.1 --- a/src/Pure/Thy/thy_info.ML	Sat Mar 26 21:28:04 2011 +0100
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Mar 26 21:45:29 2011 +0100
     3.3 @@ -155,7 +155,7 @@
     3.4  (* scheduling loader tasks *)
     3.5  
     3.6  datatype task =
     3.7 -  Task of string list * (theory list -> (theory * (unit -> unit))) |
     3.8 +  Task of string list * (theory list -> (theory * unit future * (unit -> unit))) |
     3.9    Finished of theory;
    3.10  
    3.11  fun task_finished (Task _) = false
    3.12 @@ -168,8 +168,9 @@
    3.13      (case Graph.get_node task_graph name of
    3.14        Task (parents, body) =>
    3.15          let
    3.16 -          val (thy, after_load) = body (map (the o Symtab.lookup tab) parents);
    3.17 -          val _ = after_load ();
    3.18 +          val (thy, present, commit) = body (map (the o Symtab.lookup tab) parents);
    3.19 +          val _ = Future.join present;
    3.20 +          val _ = commit ();
    3.21          in Symtab.update (name, thy) tab end
    3.22      | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
    3.23  
    3.24 @@ -194,13 +195,14 @@
    3.25                    | bad => error (loader_msg ("failed to load " ^ quote name ^
    3.26                        " (unresolved " ^ commas_quote bad ^ ")") [])));
    3.27            in Symtab.update (name, future) tab end
    3.28 -      | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
    3.29 +      | Finished thy => Symtab.update (name, Future.value (thy, Future.value (), I)) tab));
    3.30      val _ =
    3.31        tasks |> maps (fn name =>
    3.32          let
    3.33 -          val (thy, after_load) = Future.join (the (Symtab.lookup futures name));
    3.34 +          val (thy, present, commit) = Future.join (the (Symtab.lookup futures name));
    3.35            val _ = Global_Theory.join_proofs thy;
    3.36 -          val _ = after_load ();
    3.37 +          val _ = Future.join present;
    3.38 +          val _ = commit ();
    3.39          in [] end handle exn => [Exn.Exn exn])
    3.40        |> rev |> Exn.release_all;
    3.41    in () end) ();
    3.42 @@ -237,17 +239,15 @@
    3.43        Thy_Load.begin_theory dir name imports parent_thys uses
    3.44        |> Present.begin_theory update_time dir uses;
    3.45  
    3.46 -    val (after_load, theory) = Outer_Syntax.load_thy name init pos text;
    3.47 +    val (theory, present) = Outer_Syntax.load_thy name init pos text;
    3.48  
    3.49      val parents = map Context.theory_name parent_thys;
    3.50 -    fun after_load' () =
    3.51 -     (after_load ();
    3.52 +    fun commit () =
    3.53        NAMED_CRITICAL "Thy_Info" (fn () =>
    3.54         (map get_theory parents;
    3.55          change_thys (new_entry name parents (SOME deps, SOME theory));
    3.56 -        perform Update name)));
    3.57 -
    3.58 -  in (theory, after_load') end;
    3.59 +        perform Update name));
    3.60 +  in (theory, present, commit) end;
    3.61  
    3.62  fun check_deps dir name =
    3.63    (case lookup_deps name of
    3.64 @@ -255,7 +255,7 @@
    3.65    | NONE =>
    3.66        let val {master, text, imports, ...} = Thy_Load.check_thy dir name
    3.67        in (false, SOME (make_deps master imports, text), imports) end
    3.68 -  | SOME (SOME {master, imports}) =>
    3.69 +  | SOME (SOME {master, ...}) =>
    3.70        let
    3.71          val {master = master', text = text', imports = imports', ...} = Thy_Load.check_thy dir name;
    3.72          val deps' = SOME (make_deps master' imports', text');