merged
authorwenzelm
Mon Mar 04 17:32:10 2013 +0100 (2013-03-04)
changeset 513332cfd028a2fd9
parent 51329 4a3c453f99a1
parent 51332 8707df0b0255
child 51334 fd531bd984d8
merged
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Feb 20 12:04:42 2013 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Mar 04 17:32:10 2013 +0100
     1.3 @@ -1191,7 +1191,7 @@
     1.4  in
     1.5  
     1.6  fun local_future_terminal_proof meths =
     1.7 -  future_terminal_proof 2
     1.8 +  future_terminal_proof 3
     1.9      (local_terminal_proof meths)
    1.10      (local_terminal_proof meths #> context_of) local_done_proof;
    1.11  
     2.1 --- a/src/Pure/Isar/toplevel.ML	Wed Feb 20 12:04:42 2013 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Mar 04 17:32:10 2013 +0100
     2.3 @@ -96,8 +96,9 @@
     2.4    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     2.5    val command_errors: bool -> transition -> state -> Runtime.error list * state option
     2.6    val command_exception: bool -> transition -> state -> state
     2.7 -  val element_result: transition Thy_Syntax.element -> state ->
     2.8 -    (transition * state) list future * state
     2.9 +  type result
    2.10 +  val join_results: result -> (transition * state) list
    2.11 +  val element_result: transition Thy_Syntax.element -> state -> result * state
    2.12  end;
    2.13  
    2.14  structure Toplevel: TOPLEVEL =
    2.15 @@ -705,19 +706,26 @@
    2.16  
    2.17  (* scheduled proof result *)
    2.18  
    2.19 +datatype result =
    2.20 +  Result of transition * state |
    2.21 +  Result_List of result list |
    2.22 +  Result_Future of result future;
    2.23 +
    2.24 +fun join_results (Result x) = [x]
    2.25 +  | join_results (Result_List xs) = maps join_results xs
    2.26 +  | join_results (Result_Future x) = join_results (Future.join x);
    2.27 +
    2.28  local
    2.29  
    2.30  structure Result = Proof_Data
    2.31  (
    2.32 -  type T = (transition * state) list future;
    2.33 -  val empty: T = Future.value [];
    2.34 +  type T = result;
    2.35 +  val empty: T = Result_List [];
    2.36    fun init _ = empty;
    2.37  );
    2.38  
    2.39 -fun done_proof state =
    2.40 -  if can (Proof.assert_bottom true) state
    2.41 -  then Proof.global_done_proof state
    2.42 -  else Proof.context_of (Proof.local_done_proof state);
    2.43 +val get_result = Result.get o Proof.context_of;
    2.44 +val put_result = Proof.map_context o Result.put;
    2.45  
    2.46  fun proof_future_enabled st =
    2.47    (case try proof_of st of
    2.48 @@ -744,46 +752,52 @@
    2.49            (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
    2.50              (fn () => command tr st); st)) ()
    2.51        else command tr st;
    2.52 -  in ((tr, st'), st') end;
    2.53 +  in (Result (tr, st'), st') end;
    2.54  
    2.55  in
    2.56  
    2.57 -fun element_result (Thy_Syntax.Element (tr, NONE)) st =
    2.58 -      let val (result, st') = atom_result tr st
    2.59 -      in (Future.value [result], st') end
    2.60 -  | element_result (Thy_Syntax.Element (head_tr, SOME proof)) st =
    2.61 +fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
    2.62 +  | element_result (Thy_Syntax.Element (head_tr, SOME element_rest)) st =
    2.63        let
    2.64          val (head_result, st') = atom_result head_tr st;
    2.65 -        val (body_elems, end_tr) = proof;
    2.66 -        val body_trs = maps Thy_Syntax.flat_element body_elems;
    2.67 +        val (body_elems, end_tr) = element_rest;
    2.68        in
    2.69          if not (proof_future_enabled st')
    2.70          then
    2.71 -          let val (proof_results, st'') = fold_map atom_result (body_trs @ [end_tr]) st'
    2.72 -          in (Future.value (head_result :: proof_results), st'') end
    2.73 +          let
    2.74 +            val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
    2.75 +            val (proof_results, st'') = fold_map atom_result proof_trs st';
    2.76 +          in (Result_List (head_result :: proof_results), st'') end
    2.77          else
    2.78            let
    2.79              val finish = Context.Theory o Proof_Context.theory_of;
    2.80  
    2.81              val future_proof = Proof.future_proof
    2.82 -              (fn prf =>
    2.83 +              (fn state =>
    2.84                  setmp_thread_position head_tr (fn () =>
    2.85                    Goal.fork_name "Toplevel.future_proof"
    2.86 -                    (priority (Thy_Syntax.Element (empty, SOME proof)))
    2.87 +                    (priority (Thy_Syntax.Element (empty, SOME element_rest)))
    2.88                      (fn () =>
    2.89 -                      let val (result, result_state) =
    2.90 -                        (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    2.91 -                          => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    2.92 -                        |> fold_map atom_result body_trs ||> command end_tr;
    2.93 -                      in (result, presentation_context_of result_state) end)) ())
    2.94 -              #> (fn (result, state') => state' |> done_proof |> Result.put result);
    2.95 +                      let
    2.96 +                        val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
    2.97 +                        val prf' = Proof_Node.apply (K state) prf;
    2.98 +                        val (result, result_state) =
    2.99 +                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
   2.100 +                          |> fold_map element_result body_elems ||> command end_tr;
   2.101 +                      in (Result_List result, presentation_context_of result_state) end)) ())
   2.102 +              #> (fn (res, state') => state' |> put_result (Result_Future res));
   2.103 +
   2.104 +            val forked_proof =
   2.105 +              proof (future_proof #>
   2.106 +                (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o
   2.107 +              end_proof (fn _ => future_proof #>
   2.108 +                (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
   2.109  
   2.110              val st'' = st'
   2.111 -              |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
   2.112 +              |> command (head_tr |> set_print false |> reset_trans |> forked_proof);
   2.113 +            val end_result = Result (end_tr, st'');
   2.114              val result =
   2.115 -              Result.get (presentation_context_of st'')
   2.116 -              |> Future.map (fn body_results => head_result :: body_results @ [(end_tr, st'')]);
   2.117 -
   2.118 +              Result_List [head_result, Result.get (presentation_context_of st''), end_result];
   2.119            in (result, st'') end
   2.120        end;
   2.121  
     3.1 --- a/src/Pure/System/isabelle_process.ML	Wed Feb 20 12:04:42 2013 +0100
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Mar 04 17:32:10 2013 +0100
     3.3 @@ -242,7 +242,7 @@
     3.4          Multithreading.max_threads := Options.int options "threads";
     3.5          if Multithreading.max_threads_value () < 2
     3.6          then Multithreading.max_threads := 2 else ();
     3.7 -        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
     3.8 +        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
     3.9          Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
    3.10          tracing_messages := Options.int options "editor_tracing_messages"
    3.11        end);
     4.1 --- a/src/Pure/Thy/thy_info.ML	Wed Feb 20 12:04:42 2013 +0100
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Mar 04 17:32:10 2013 +0100
     4.3 @@ -164,7 +164,22 @@
     4.4  
     4.5  (* scheduling loader tasks *)
     4.6  
     4.7 -type result = theory * serial * unit future * (unit -> unit);
     4.8 +datatype result =
     4.9 +  Result of {theory: theory, id: serial, present: unit -> unit, commit: unit -> unit, weight: int};
    4.10 +
    4.11 +fun theory_result theory = Result {theory = theory, id = 0, present = I, commit = I, weight = 0};
    4.12 +
    4.13 +fun result_theory (Result {theory, ...}) = theory;
    4.14 +fun result_present (Result {present, ...}) = present;
    4.15 +fun result_commit (Result {commit, ...}) = commit;
    4.16 +fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
    4.17 +
    4.18 +fun join_proofs (Result {theory, id, present, ...}) =
    4.19 +  let
    4.20 +    val result1 = Exn.capture Thm.join_theory_proofs theory;
    4.21 +    val results2 = Future.join_results (Goal.peek_futures id);
    4.22 +  in result1 :: results2 end;
    4.23 +
    4.24  
    4.25  datatype task =
    4.26    Task of string list * (theory list -> result) |
    4.27 @@ -177,24 +192,21 @@
    4.28  
    4.29  local
    4.30  
    4.31 -fun finish_thy ((thy, id, present, commit): result) =
    4.32 -  let
    4.33 -    val result1 = Exn.capture Thm.join_theory_proofs thy;
    4.34 -    val results2 = Future.join_results (Goal.peek_futures id);
    4.35 -    val result3 = Future.join_result present;
    4.36 -    val _ = Par_Exn.release_all (result1 :: results2 @ [result3]);
    4.37 -    val _ = commit ();
    4.38 -  in thy end;
    4.39 -
    4.40  val schedule_seq =
    4.41    String_Graph.schedule (fn deps => fn (_, task) =>
    4.42      (case task of
    4.43 -      Task (parents, body) => finish_thy (body (task_parents deps parents))
    4.44 +      Task (parents, body) =>
    4.45 +        let
    4.46 +          val result = body (task_parents deps parents);
    4.47 +          val _ = Par_Exn.release_all (join_proofs result);
    4.48 +          val _ = result_present result ();
    4.49 +          val _ = result_commit result ();
    4.50 +        in result_theory result end
    4.51      | Finished thy => thy)) #> ignore;
    4.52  
    4.53  val schedule_futures = uninterruptible (fn _ => fn tasks =>
    4.54    let
    4.55 -    val results1 = tasks
    4.56 +    val futures = tasks
    4.57        |> String_Graph.schedule (fn deps => fn (name, task) =>
    4.58          (case task of
    4.59            Task (parents, body) =>
    4.60 @@ -203,17 +215,31 @@
    4.61                  deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
    4.62                (fn () =>
    4.63                  (case filter (not o can Future.join o #2) deps of
    4.64 -                  [] => body (map (#1 o Future.join) (task_parents deps parents))
    4.65 +                  [] => body (map (result_theory o Future.join) (task_parents deps parents))
    4.66                  | bad =>
    4.67                      error (loader_msg ("failed to load " ^ quote name ^
    4.68                        " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
    4.69 -        | Finished thy => Future.value (thy, 0, Future.value (), I)))
    4.70 -      |> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn]);
    4.71 +        | Finished theory => Future.value (theory_result theory)));
    4.72 +
    4.73 +    val results1 = futures
    4.74 +      |> maps (fn future =>
    4.75 +          (case Future.join_result future of
    4.76 +            Exn.Res result => join_proofs result
    4.77 +          | Exn.Exn exn => [Exn.Exn exn]));
    4.78 +
    4.79 +    val results2 = futures
    4.80 +      |> map_filter (Exn.get_res o Future.join_result)
    4.81 +      |> sort result_ord
    4.82 +      |> Par_List.map (fn result => Exn.capture (result_present result) ());
    4.83 +
    4.84 +    (* FIXME more precise commit order (!?) *)
    4.85 +    val results3 = futures
    4.86 +      |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
    4.87  
    4.88      (* FIXME avoid global reset_futures (!??) *)
    4.89 -    val results2 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ()));
    4.90 +    val results4 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ()));
    4.91  
    4.92 -    val _ = Par_Exn.release_all (rev (results2 @ results1));
    4.93 +    val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
    4.94    in () end);
    4.95  
    4.96  in
    4.97 @@ -249,11 +275,11 @@
    4.98  
    4.99      val id = serial ();
   4.100      val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path);
   4.101 -    val (theory, present) =
   4.102 +    val (theory, present, weight) =
   4.103        Thy_Load.load_thy last_timing update_time dir header text_pos text
   4.104          (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
   4.105      fun commit () = update_thy deps theory;
   4.106 -  in (theory, id, present, commit) end;
   4.107 +  in Result {theory = theory, id = id, present = present, commit = commit, weight = weight} end;
   4.108  
   4.109  fun check_deps dir name =
   4.110    (case lookup_deps name of
     5.1 --- a/src/Pure/Thy/thy_load.ML	Wed Feb 20 12:04:42 2013 +0100
     5.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Mar 04 17:32:10 2013 +0100
     5.3 @@ -23,7 +23,7 @@
     5.4    val exec_ml: Path.T -> generic_theory -> generic_theory
     5.5    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     5.6    val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header ->
     5.7 -    Position.T -> string -> theory list -> theory * unit future
     5.8 +    Position.T -> string -> theory list -> theory * (unit -> unit) * int
     5.9    val set_master_path: Path.T -> unit
    5.10    val get_master_path: unit -> Path.T
    5.11  end;
    5.12 @@ -258,19 +258,18 @@
    5.13      val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
    5.14      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    5.15  
    5.16 -    val present =
    5.17 -      Future.flat results |> Future.map (fn res0 =>
    5.18 -        let
    5.19 -          val res = filter_out (Toplevel.is_ignored o #1) res0;
    5.20 -          val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
    5.21 -        in
    5.22 -          Thy_Output.present_thy minor Keyword.command_tags
    5.23 -            (Outer_Syntax.is_markup outer_syntax) res toks
    5.24 -          |> Buffer.content
    5.25 -          |> Present.theory_output name
    5.26 -        end);
    5.27 +    fun present () =
    5.28 +      let
    5.29 +        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
    5.30 +        val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
    5.31 +      in
    5.32 +        Thy_Output.present_thy minor Keyword.command_tags
    5.33 +          (Outer_Syntax.is_markup outer_syntax) res toks
    5.34 +        |> Buffer.content
    5.35 +        |> Present.theory_output name
    5.36 +      end;
    5.37  
    5.38 -  in (thy, present) end;
    5.39 +  in (thy, present, size text) end;
    5.40  
    5.41  
    5.42  (* document antiquotation *)