refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
authorwenzelm
Thu Aug 30 21:23:04 2012 +0200 (2012-08-30)
changeset 490128686c36fa27d
parent 49011 9c68e43502ce
child 49013 1266b51f9bbc
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Aug 30 19:18:49 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 30 21:23:04 2012 +0200
     1.3 @@ -265,7 +265,7 @@
     1.4  (* global endings *)
     1.5  
     1.6  fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
     1.7 -val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof;
     1.8 +val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof;
     1.9  val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
    1.10  val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
    1.11  val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
     2.1 --- a/src/Pure/Isar/proof.ML	Thu Aug 30 19:18:49 2012 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Thu Aug 30 21:23:04 2012 +0200
     2.3 @@ -1137,19 +1137,21 @@
     2.4  
     2.5  local
     2.6  
     2.7 -fun future_terminal_proof proof1 proof2 meths int state =
     2.8 -  if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
     2.9 -  then proof1 meths state
    2.10 -  else snd (proof2 (fn state' =>
    2.11 -    Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state);
    2.12 +fun future_terminal_proof n proof1 proof2 meths int state =
    2.13 +  if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int)
    2.14 +    andalso not (is_relevant state)
    2.15 +  then
    2.16 +    snd (proof2 (fn state' =>
    2.17 +      Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state)
    2.18 +  else proof1 meths state;
    2.19  
    2.20  in
    2.21  
    2.22  fun local_future_terminal_proof x =
    2.23 -  future_terminal_proof local_terminal_proof local_future_proof x;
    2.24 +  future_terminal_proof 2 local_terminal_proof local_future_proof x;
    2.25  
    2.26  fun global_future_terminal_proof x =
    2.27 -  future_terminal_proof global_terminal_proof global_future_proof x;
    2.28 +  future_terminal_proof 3 global_terminal_proof global_future_proof x;
    2.29  
    2.30  end;
    2.31  
     3.1 --- a/src/Pure/Isar/toplevel.ML	Thu Aug 30 19:18:49 2012 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Aug 30 21:23:04 2012 +0200
     3.3 @@ -53,9 +53,10 @@
     3.4    val ignored: Position.T -> transition
     3.5    val malformed: Position.T -> string -> transition
     3.6    val is_malformed: transition -> bool
     3.7 -  val theory: (theory -> theory) -> transition -> transition
     3.8 +  val join_recent_proofs: state -> unit
     3.9    val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
    3.10    val theory': (bool -> theory -> theory) -> transition -> transition
    3.11 +  val theory: (theory -> theory) -> transition -> transition
    3.12    val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
    3.13    val end_local_theory: transition -> transition
    3.14    val open_target: (generic_theory -> local_theory) -> transition -> transition
    3.15 @@ -422,15 +423,21 @@
    3.16  val unknown_context = imperative (fn () => warning "Unknown context");
    3.17  
    3.18  
    3.19 -(* theory transitions *)
    3.20 +(* forked proofs *)
    3.21 +
    3.22 +val begin_proofs_thy = Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
    3.23 +val begin_proofs = Context.mapping begin_proofs_thy (Local_Theory.raw_theory begin_proofs_thy);
    3.24  
    3.25 -val global_theory_group =
    3.26 -  Sign.new_group #>
    3.27 -  Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
    3.28 +fun join_recent_proofs st =
    3.29 +  (case try proof_of st of
    3.30 +    SOME prf => Proof.join_recent_proofs prf
    3.31 +  | NONE =>
    3.32 +      (case try theory_of st of
    3.33 +        SOME thy => Thm.join_recent_proofs thy
    3.34 +      | NONE => ()));
    3.35  
    3.36 -val local_theory_group =
    3.37 -  Local_Theory.new_group #>
    3.38 -  Local_Theory.raw_theory (Context.theory_map Thm.begin_proofs #> Theory.checkpoint);
    3.39 +
    3.40 +(* theory transitions *)
    3.41  
    3.42  fun generic_theory f = transaction (fn _ =>
    3.43    (fn Theory (gthy, _) => Theory (f gthy, NONE)
    3.44 @@ -439,7 +446,8 @@
    3.45  fun theory' f = transaction (fn int =>
    3.46    (fn Theory (Context.Theory thy, _) =>
    3.47        let val thy' = thy
    3.48 -        |> global_theory_group
    3.49 +        |> Sign.new_group
    3.50 +        |> Theory.checkpoint
    3.51          |> f int
    3.52          |> Sign.reset_group;
    3.53        in Theory (Context.Theory thy', NONE) end
    3.54 @@ -478,9 +486,11 @@
    3.55  fun local_theory_presentation loc f = present_transaction (fn int =>
    3.56    (fn Theory (gthy, _) =>
    3.57          let
    3.58 -          val (finish, lthy) = loc_begin loc gthy;
    3.59 +          val (finish, lthy) = gthy
    3.60 +            |> begin_proofs
    3.61 +            |> loc_begin loc;
    3.62            val lthy' = lthy
    3.63 -            |> local_theory_group
    3.64 +            |> Local_Theory.new_group
    3.65              |> f int
    3.66              |> Local_Theory.reset_group;
    3.67          in Theory (finish lthy', SOME lthy') end
    3.68 @@ -534,15 +544,19 @@
    3.69  
    3.70  fun local_theory_to_proof' loc f = begin_proof
    3.71    (fn int => fn gthy =>
    3.72 -    let val (finish, lthy) = loc_begin loc gthy
    3.73 -    in (finish o Local_Theory.reset_group, f int (local_theory_group lthy)) end);
    3.74 +    let val (finish, lthy) = gthy
    3.75 +      |> begin_proofs
    3.76 +      |> loc_begin loc;
    3.77 +    in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
    3.78  
    3.79  fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
    3.80  
    3.81  fun theory_to_proof f = begin_proof
    3.82    (fn _ => fn gthy =>
    3.83      (Context.Theory o Sign.reset_group o Proof_Context.theory_of,
    3.84 -      (case gthy of Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF)));
    3.85 +      (case begin_proofs gthy of
    3.86 +        Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))
    3.87 +      | _ => raise UNDEF)));
    3.88  
    3.89  end;
    3.90  
    3.91 @@ -552,12 +566,12 @@
    3.92      | _ => raise UNDEF));
    3.93  
    3.94  val present_proof = present_transaction (fn _ =>
    3.95 -  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
    3.96 +  (fn Proof (prf, x) => Proof (Proof_Node.apply Proof.begin_proofs prf, x)
    3.97      | skip as SkipProof _ => skip
    3.98      | _ => raise UNDEF));
    3.99  
   3.100  fun proofs' f = transaction (fn int =>
   3.101 -  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
   3.102 +  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int o Proof.begin_proofs) prf, x)
   3.103      | skip as SkipProof _ => skip
   3.104      | _ => raise UNDEF));
   3.105  
     4.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 30 19:18:49 2012 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 30 21:23:04 2012 +0200
     4.3 @@ -362,10 +362,7 @@
     4.4  fun stable_command exec =
     4.5    (case Exn.capture Command.memo_result exec of
     4.6      Exn.Exn exn => not (Exn.is_interrupt exn)
     4.7 -  | Exn.Res ((st, _), _) =>
     4.8 -      (case try Toplevel.theory_of st of
     4.9 -        NONE => true
    4.10 -      | SOME thy => is_some (Exn.get_res (Exn.capture Thm.join_recent_proofs thy))));
    4.11 +  | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st)));
    4.12  
    4.13  fun make_required nodes =
    4.14    let
     5.1 --- a/src/Pure/goal.ML	Thu Aug 30 19:18:49 2012 +0200
     5.2 +++ b/src/Pure/goal.ML	Thu Aug 30 21:23:04 2012 +0200
     5.3 @@ -26,8 +26,9 @@
     5.4    val norm_result: thm -> thm
     5.5    val fork_name: string -> (unit -> 'a) -> 'a future
     5.6    val fork: (unit -> 'a) -> 'a future
     5.7 +  val future_enabled_level: int -> bool
     5.8    val future_enabled: unit -> bool
     5.9 -  val local_future_enabled: unit -> bool
    5.10 +  val future_enabled_nested: int -> bool
    5.11    val future_result: Proof.context -> thm future -> term -> thm
    5.12    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    5.13    val prove_multi: Proof.context -> string list -> term list -> term list ->
    5.14 @@ -155,12 +156,14 @@
    5.15  val parallel_proofs = Unsynchronized.ref 1;
    5.16  val parallel_proofs_threshold = Unsynchronized.ref 50;
    5.17  
    5.18 -fun future_enabled () =
    5.19 -  Multithreading.enabled () andalso ! parallel_proofs >= 1 andalso
    5.20 +fun future_enabled_level n =
    5.21 +  Multithreading.enabled () andalso ! parallel_proofs >= n andalso
    5.22    is_some (Future.worker_task ());
    5.23  
    5.24 -fun local_future_enabled () =
    5.25 -  future_enabled () andalso ! parallel_proofs >= 2 andalso
    5.26 +fun future_enabled () = future_enabled_level 1;
    5.27 +
    5.28 +fun future_enabled_nested n =
    5.29 +  future_enabled_level n andalso
    5.30    Synchronized.value forked_proofs <
    5.31      ! parallel_proofs_threshold * Multithreading.max_threads_value ();
    5.32