some support for registering forked proofs within Proof.state, using its bottom context;
authorwenzelm
Thu Aug 30 19:18:49 2012 +0200 (2012-08-30 ago)
changeset 490119c68e43502ce
parent 49010 72808e956879
child 49012 8686c36fa27d
some support for registering forked proofs within Proof.state, using its bottom context;
tuned signature;
src/Pure/General/stack.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
src/Pure/global_theory.ML
src/Pure/more_thm.ML
     1.1 --- a/src/Pure/General/stack.ML	Thu Aug 30 16:39:50 2012 +0200
     1.2 +++ b/src/Pure/General/stack.ML	Thu Aug 30 19:18:49 2012 +0200
     1.3 @@ -10,7 +10,9 @@
     1.4    val level: 'a T -> int
     1.5    val init: 'a -> 'a T
     1.6    val top: 'a T -> 'a
     1.7 +  val bottom: 'a T -> 'a
     1.8    val map_top: ('a -> 'a) -> 'a T -> 'a T
     1.9 +  val map_bottom: ('a -> 'a) -> 'a T -> 'a T
    1.10    val map_all: ('a -> 'a) -> 'a T -> 'a T
    1.11    val push: 'a T -> 'a T
    1.12    val pop: 'a T -> 'a T      (*exception List.Empty*)
    1.13 @@ -27,8 +29,16 @@
    1.14  
    1.15  fun top (x, _) = x;
    1.16  
    1.17 +fun bottom (x, []) = x
    1.18 +  | bottom (_, xs) = List.last xs;
    1.19 +
    1.20  fun map_top f (x, xs) = (f x, xs);
    1.21  
    1.22 +fun map_bottom f (x, []) = (f x, [])
    1.23 +  | map_bottom f (x, rest) =
    1.24 +      let val (ys, z) = split_last rest
    1.25 +      in (x, ys @ [f z]) end;
    1.26 +
    1.27  fun map_all f (x, xs) = (f x, map f xs);
    1.28  
    1.29  fun push (x, xs) = (x, x :: xs);
     2.1 --- a/src/Pure/Isar/proof.ML	Thu Aug 30 16:39:50 2012 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Thu Aug 30 19:18:49 2012 +0200
     2.3 @@ -111,6 +111,9 @@
     2.4      (Thm.binding * (term * term list) list) list -> bool -> state -> state
     2.5    val show_cmd: Method.text option -> (thm list list -> state -> state) ->
     2.6      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
     2.7 +  val begin_proofs: state -> state
     2.8 +  val register_proofs: thm list -> state -> state
     2.9 +  val join_recent_proofs: state -> unit
    2.10    val schematic_goal: state -> bool
    2.11    val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
    2.12    val global_future_proof: (state -> ('a * Proof.context) future) -> state -> 'a future * context
    2.13 @@ -168,8 +171,11 @@
    2.14  fun init ctxt =
    2.15    State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
    2.16  
    2.17 -fun current (State st) = Stack.top st |> (fn Node node => node);
    2.18 -fun map_current f (State st) = State (Stack.map_top (map_node f) st);
    2.19 +fun top (State st) = Stack.top st |> (fn Node node => node);
    2.20 +fun bottom (State st) = Stack.bottom st |> (fn Node node => node);
    2.21 +
    2.22 +fun map_top f (State st) = State (Stack.map_top (map_node f) st);
    2.23 +fun map_bottom f (State st) = State (Stack.map_bottom (map_node f) st);
    2.24  fun map_all f (State st) = State (Stack.map_all (map_node f) st);
    2.25  
    2.26  
    2.27 @@ -195,18 +201,21 @@
    2.28  
    2.29  (* context *)
    2.30  
    2.31 -val context_of = #context o current;
    2.32 +val context_of = #context o top;
    2.33  val theory_of = Proof_Context.theory_of o context_of;
    2.34  
    2.35  fun map_node_context f =
    2.36    map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
    2.37  
    2.38  fun map_context f =
    2.39 -  map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
    2.40 +  map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
    2.41  
    2.42  fun map_context_result f state =
    2.43    f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
    2.44  
    2.45 +fun map_context_bottom f =
    2.46 +  map_bottom (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
    2.47 +
    2.48  fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
    2.49  
    2.50  fun propagate_ml_env state = map_contexts
    2.51 @@ -218,7 +227,7 @@
    2.52  
    2.53  (* facts *)
    2.54  
    2.55 -val get_facts = #facts o current;
    2.56 +val get_facts = #facts o top;
    2.57  
    2.58  fun the_facts state =
    2.59    (case get_facts state of SOME facts => facts
    2.60 @@ -229,7 +238,7 @@
    2.61    | _ => error "Single theorem expected");
    2.62  
    2.63  fun put_facts facts =
    2.64 -  map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
    2.65 +  map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
    2.66    put_thms true (Auto_Bind.thisN, facts);
    2.67  
    2.68  val set_facts = put_facts o SOME;
    2.69 @@ -249,8 +258,8 @@
    2.70  
    2.71  (* mode *)
    2.72  
    2.73 -val get_mode = #mode o current;
    2.74 -fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
    2.75 +val get_mode = #mode o top;
    2.76 +fun put_mode mode = map_top (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
    2.77  
    2.78  val mode_name = (fn Forward => "state" | Chain => "chain" | Backward => "prove");
    2.79  
    2.80 @@ -274,7 +283,7 @@
    2.81  (* current goal *)
    2.82  
    2.83  fun current_goal state =
    2.84 -  (case current state of
    2.85 +  (case top state of
    2.86      {context, goal = SOME (Goal goal), ...} => (context, goal)
    2.87    | _ => error "No current goal");
    2.88  
    2.89 @@ -285,7 +294,7 @@
    2.90      else state
    2.91    end;
    2.92  
    2.93 -fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
    2.94 +fun put_goal goal = map_top (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
    2.95  
    2.96  val set_goal = put_goal o SOME;
    2.97  val reset_goal = put_goal NONE;
    2.98 @@ -338,7 +347,7 @@
    2.99  
   2.100  fun pretty_state nr state =
   2.101    let
   2.102 -    val {context = ctxt, facts, mode, goal = _} = current state;
   2.103 +    val {context = ctxt, facts, mode, goal = _} = top state;
   2.104      val verbose = Config.get ctxt Proof_Context.verbose;
   2.105  
   2.106      fun levels_up 0 = ""
   2.107 @@ -1051,6 +1060,14 @@
   2.108  
   2.109  (** future proofs **)
   2.110  
   2.111 +(* forked proofs *)
   2.112 +
   2.113 +val begin_proofs = map_context_bottom (Context.proof_map Thm.begin_proofs);
   2.114 +val register_proofs = map_context_bottom o Context.proof_map o Thm.register_proofs;
   2.115 +
   2.116 +val join_recent_proofs = Thm.join_local_proofs o #context o bottom;
   2.117 +
   2.118 +
   2.119  (* relevant proof states *)
   2.120  
   2.121  fun is_schematic t =
     3.1 --- a/src/Pure/Isar/toplevel.ML	Thu Aug 30 16:39:50 2012 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Aug 30 19:18:49 2012 +0200
     3.3 @@ -426,11 +426,11 @@
     3.4  
     3.5  val global_theory_group =
     3.6    Sign.new_group #>
     3.7 -  Thm.begin_recent_proofs #> Theory.checkpoint;
     3.8 +  Context.theory_map Thm.begin_proofs #> Theory.checkpoint;
     3.9  
    3.10  val local_theory_group =
    3.11    Local_Theory.new_group #>
    3.12 -  Local_Theory.raw_theory (Thm.begin_recent_proofs #> Theory.checkpoint);
    3.13 +  Local_Theory.raw_theory (Context.theory_map Thm.begin_proofs #> Theory.checkpoint);
    3.14  
    3.15  fun generic_theory f = transaction (fn _ =>
    3.16    (fn Theory (gthy, _) => Theory (f gthy, NONE)
     4.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 30 16:39:50 2012 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 30 19:18:49 2012 +0200
     4.3 @@ -357,7 +357,7 @@
     4.4    is_some (Exn.get_res (Exn.capture (fn () =>
     4.5      fst (fst (Command.memo_result (the (get_result node))))
     4.6      |> Toplevel.end_theory Position.none
     4.7 -    |> Thm.join_all_proofs) ()));
     4.8 +    |> Thm.join_theory_proofs) ()));
     4.9  
    4.10  fun stable_command exec =
    4.11    (case Exn.capture Command.memo_result exec of
     5.1 --- a/src/Pure/Thy/thy_info.ML	Thu Aug 30 16:39:50 2012 +0200
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Aug 30 19:18:49 2012 +0200
     5.3 @@ -176,7 +176,7 @@
     5.4  local
     5.5  
     5.6  fun finish_thy ((thy, present, commit): result) =
     5.7 -  (Thm.join_all_proofs thy; Future.join present; commit (); thy);
     5.8 +  (Thm.join_theory_proofs thy; Future.join present; commit (); thy);
     5.9  
    5.10  val schedule_seq =
    5.11    Graph.schedule (fn deps => fn (_, task) =>
     6.1 --- a/src/Pure/global_theory.ML	Thu Aug 30 16:39:50 2012 +0200
     6.2 +++ b/src/Pure/global_theory.ML	Thu Aug 30 19:18:49 2012 +0200
     6.3 @@ -124,7 +124,7 @@
     6.4  
     6.5  (* enter_thms *)
     6.6  
     6.7 -fun register_proofs thms thy = (thms, Thm.register_proofs thms thy);
     6.8 +fun register_proofs thms thy = (thms, Context.theory_map (Thm.register_proofs thms) thy);
     6.9  
    6.10  fun enter_thms pre_name post_name app_att (b, thms) thy =
    6.11    if Binding.is_empty b
     7.1 --- a/src/Pure/more_thm.ML	Thu Aug 30 16:39:50 2012 +0200
     7.2 +++ b/src/Pure/more_thm.ML	Thu Aug 30 19:18:49 2012 +0200
     7.3 @@ -95,10 +95,11 @@
     7.4    val legacy_get_kind: thm -> string
     7.5    val kind_rule: string -> thm -> thm
     7.6    val kind: string -> attribute
     7.7 -  val register_proofs: thm list -> theory -> theory
     7.8 -  val begin_recent_proofs: theory -> theory
     7.9 +  val register_proofs: thm list -> Context.generic -> Context.generic
    7.10 +  val begin_proofs: Context.generic -> Context.generic
    7.11 +  val join_local_proofs: Proof.context -> unit
    7.12    val join_recent_proofs: theory -> unit
    7.13 -  val join_all_proofs: theory -> unit
    7.14 +  val join_theory_proofs: theory -> unit
    7.15  end;
    7.16  
    7.17  structure Thm: THM =
    7.18 @@ -470,7 +471,7 @@
    7.19  fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
    7.20  
    7.21  
    7.22 -(* forked proofs within the context *)
    7.23 +(* forked proofs *)
    7.24  
    7.25  type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
    7.26  
    7.27 @@ -482,19 +483,20 @@
    7.28  
    7.29  fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
    7.30  
    7.31 -structure Proofs = Theory_Data
    7.32 +structure Proofs = Generic_Data
    7.33  (
    7.34 -  type T = proofs * proofs;  (*recent proofs, all proofs of theory node*)
    7.35 +  type T = proofs * proofs;  (*recent proofs since last begin, all proofs of theory node*)
    7.36    val empty = (empty_proofs, empty_proofs);
    7.37    fun extend _ = empty;
    7.38    fun merge _ = empty;
    7.39  );
    7.40  
    7.41 +val begin_proofs = Proofs.map (apfst (K empty_proofs));
    7.42  val register_proofs = Proofs.map o pairself o add_proofs;
    7.43 -val begin_recent_proofs = Proofs.map (apfst (K empty_proofs));
    7.44  
    7.45 -val join_recent_proofs = force_proofs o #1 o Proofs.get;
    7.46 -val join_all_proofs = force_proofs o #2 o Proofs.get;
    7.47 +val join_local_proofs = force_proofs o #1 o Proofs.get o Context.Proof;
    7.48 +val join_recent_proofs = force_proofs o #1 o Proofs.get o Context.Theory;
    7.49 +val join_theory_proofs = force_proofs o #2 o Proofs.get o Context.Theory;
    7.50  
    7.51  
    7.52  open Thm;