discontinued complicated/unreliable notion of recent proofs within context;
authorwenzelm
Sat Sep 01 19:43:18 2012 +0200 (2012-09-01 ago)
changeset 490627e31dfd99ce7
parent 49061 7449b804073b
child 49063 f93443defa6c
discontinued complicated/unreliable notion of recent proofs within context;
src/Pure/Isar/local_theory.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/toplevel.ML
src/Pure/global_theory.ML
src/Pure/more_thm.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Sat Sep 01 19:27:28 2012 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Sep 01 19:43:18 2012 +0200
     1.3 @@ -30,8 +30,6 @@
     1.4    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     1.5    val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     1.6    val background_theory: (theory -> theory) -> local_theory -> local_theory
     1.7 -  val begin_proofs: local_theory -> local_theory
     1.8 -  val register_proofs: thm list -> local_theory -> local_theory
     1.9    val target_of: local_theory -> Proof.context
    1.10    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    1.11    val target_morphism: local_theory -> morphism
    1.12 @@ -192,12 +190,6 @@
    1.13  fun background_theory f = #2 o background_theory_result (f #> pair ());
    1.14  
    1.15  
    1.16 -(* forked proofs *)
    1.17 -
    1.18 -val begin_proofs = background_theory (Context.theory_map Thm.begin_proofs);
    1.19 -val register_proofs = background_theory o Thm.register_proofs_thy;
    1.20 -
    1.21 -
    1.22  (* target contexts *)
    1.23  
    1.24  val target_of = #target o get_last_lthy;
     2.1 --- a/src/Pure/Isar/proof.ML	Sat Sep 01 19:27:28 2012 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Sat Sep 01 19:43:18 2012 +0200
     2.3 @@ -21,9 +21,6 @@
     2.4    val propagate_ml_env: state -> state
     2.5    val bind_terms: (indexname * term option) list -> state -> state
     2.6    val put_thms: bool -> string * thm list option -> 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 the_facts: state -> thm list
    2.11    val the_fact: state -> thm
    2.12    val set_facts: thm list -> state -> state
    2.13 @@ -225,14 +222,6 @@
    2.14  val put_thms = map_context oo Proof_Context.put_thms;
    2.15  
    2.16  
    2.17 -(* forked proofs *)
    2.18 -
    2.19 -val begin_proofs = map_context_bottom (Context.proof_map Thm.begin_proofs);
    2.20 -val register_proofs = map_context_bottom o Context.proof_map o Thm.register_proofs;
    2.21 -
    2.22 -val join_recent_proofs = Thm.join_local_proofs o #context o bottom;
    2.23 -
    2.24 -
    2.25  (* facts *)
    2.26  
    2.27  val get_facts = #facts o top;
    2.28 @@ -966,7 +955,7 @@
    2.29  fun local_qeds txt =
    2.30    end_proof false txt
    2.31    #> Seq.map (generic_qed Proof_Context.auto_bind_facts #->
    2.32 -    (fn ((after_qed, _), results) => register_proofs (flat results) #> after_qed results));
    2.33 +    (fn ((after_qed, _), results) => after_qed results));
    2.34  
    2.35  fun local_qed txt = local_qeds txt #> check_finish;
    2.36  
     3.1 --- a/src/Pure/Isar/specification.ML	Sat Sep 01 19:27:28 2012 +0200
     3.2 +++ b/src/Pure/Isar/specification.ML	Sat Sep 01 19:43:18 2012 +0200
     3.3 @@ -395,8 +395,7 @@
     3.4        let
     3.5          val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results;
     3.6          val (res, lthy') =
     3.7 -          if forall (Attrib.is_empty_binding o fst) stmt
     3.8 -          then (map (pair "") results', Local_Theory.register_proofs (flat results) lthy)
     3.9 +          if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
    3.10            else
    3.11              Local_Theory.notes_kind kind
    3.12                (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
     4.1 --- a/src/Pure/Isar/toplevel.ML	Sat Sep 01 19:27:28 2012 +0200
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Sep 01 19:43:18 2012 +0200
     4.3 @@ -53,7 +53,6 @@
     4.4    val ignored: Position.T -> transition
     4.5    val malformed: Position.T -> string -> transition
     4.6    val is_malformed: transition -> bool
     4.7 -  val join_recent_proofs: state -> unit
     4.8    val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
     4.9    val theory': (bool -> theory -> theory) -> transition -> transition
    4.10    val theory: (theory -> theory) -> transition -> transition
    4.11 @@ -423,21 +422,6 @@
    4.12  val unknown_context = imperative (fn () => warning "Unknown context");
    4.13  
    4.14  
    4.15 -(* forked proofs *)
    4.16 -
    4.17 -val begin_proofs =
    4.18 -  Context.mapping (Context.theory_map Thm.begin_proofs #> Theory.checkpoint)
    4.19 -    Local_Theory.begin_proofs;
    4.20 -
    4.21 -fun join_recent_proofs st =
    4.22 -  (case try proof_of st of
    4.23 -    SOME prf => Proof.join_recent_proofs prf
    4.24 -  | NONE =>
    4.25 -      (case try theory_of st of
    4.26 -        SOME thy => Thm.join_recent_proofs thy
    4.27 -      | NONE => ()));
    4.28 -
    4.29 -
    4.30  (* theory transitions *)
    4.31  
    4.32  fun generic_theory f = transaction (fn _ =>
    4.33 @@ -487,9 +471,7 @@
    4.34  fun local_theory_presentation loc f = present_transaction (fn int =>
    4.35    (fn Theory (gthy, _) =>
    4.36          let
    4.37 -          val (finish, lthy) = gthy
    4.38 -            |> begin_proofs
    4.39 -            |> loc_begin loc;
    4.40 +          val (finish, lthy) = loc_begin loc gthy;
    4.41            val lthy' = lthy
    4.42              |> Local_Theory.new_group
    4.43              |> f int
    4.44 @@ -545,9 +527,7 @@
    4.45  
    4.46  fun local_theory_to_proof' loc f = begin_proof
    4.47    (fn int => fn gthy =>
    4.48 -    let val (finish, lthy) = gthy
    4.49 -      |> begin_proofs
    4.50 -      |> loc_begin loc;
    4.51 +    let val (finish, lthy) = loc_begin loc gthy
    4.52      in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
    4.53  
    4.54  fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
    4.55 @@ -555,7 +535,7 @@
    4.56  fun theory_to_proof f = begin_proof
    4.57    (fn _ => fn gthy =>
    4.58      (Context.Theory o Sign.reset_group o Proof_Context.theory_of,
    4.59 -      (case begin_proofs gthy of
    4.60 +      (case gthy of
    4.61          Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))
    4.62        | _ => raise UNDEF)));
    4.63  
    4.64 @@ -567,12 +547,12 @@
    4.65      | _ => raise UNDEF));
    4.66  
    4.67  val present_proof = present_transaction (fn _ =>
    4.68 -  (fn Proof (prf, x) => Proof (Proof_Node.apply Proof.begin_proofs prf, x)
    4.69 +  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
    4.70      | skip as SkipProof _ => skip
    4.71      | _ => raise UNDEF));
    4.72  
    4.73  fun proofs' f = transaction (fn int =>
    4.74 -  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int o Proof.begin_proofs) prf, x)
    4.75 +  (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
    4.76      | skip as SkipProof _ => skip
    4.77      | _ => raise UNDEF));
    4.78  
     5.1 --- a/src/Pure/global_theory.ML	Sat Sep 01 19:27:28 2012 +0200
     5.2 +++ b/src/Pure/global_theory.ML	Sat Sep 01 19:43:18 2012 +0200
     5.3 @@ -124,7 +124,7 @@
     5.4  
     5.5  (* enter_thms *)
     5.6  
     5.7 -fun register_proofs thms thy = (thms, Thm.register_proofs_thy thms thy);
     5.8 +fun register_proofs thms thy = (thms, Thm.register_proofs thms thy);
     5.9  
    5.10  fun enter_thms pre_name post_name app_att (b, thms) thy =
    5.11    if Binding.is_empty b
     6.1 --- a/src/Pure/more_thm.ML	Sat Sep 01 19:27:28 2012 +0200
     6.2 +++ b/src/Pure/more_thm.ML	Sat Sep 01 19:43:18 2012 +0200
     6.3 @@ -95,11 +95,7 @@
     6.4    val legacy_get_kind: thm -> string
     6.5    val kind_rule: string -> thm -> thm
     6.6    val kind: string -> attribute
     6.7 -  val register_proofs: thm list -> Context.generic -> Context.generic
     6.8 -  val register_proofs_thy: thm list -> theory -> theory
     6.9 -  val begin_proofs: Context.generic -> Context.generic
    6.10 -  val join_local_proofs: Proof.context -> unit
    6.11 -  val join_recent_proofs: theory -> unit
    6.12 +  val register_proofs: thm list -> theory -> theory
    6.13    val join_theory_proofs: theory -> unit
    6.14  end;
    6.15  
    6.16 @@ -474,31 +470,16 @@
    6.17  
    6.18  (* forked proofs *)
    6.19  
    6.20 -type proofs = thm list * unit lazy;  (*accumulated thms, persistent join*)
    6.21 -
    6.22 -val empty_proofs: proofs = ([], Lazy.value ());
    6.23 -
    6.24 -fun add_proofs more_thms ((thms, _): proofs) =
    6.25 -  let val thms' = fold cons more_thms thms
    6.26 -  in (thms', Lazy.lazy (fn () => Thm.join_proofs (rev thms'))) end;
    6.27 -
    6.28 -fun force_proofs ((_, prfs): proofs) = Lazy.force prfs;
    6.29 -
    6.30 -structure Proofs = Generic_Data
    6.31 +structure Proofs = Theory_Data
    6.32  (
    6.33 -  type T = proofs * proofs;  (*recent proofs since last begin, all proofs of theory node*)
    6.34 -  val empty = (empty_proofs, empty_proofs);
    6.35 +  type T = thm list;
    6.36 +  val empty = [];
    6.37    fun extend _ = empty;
    6.38    fun merge _ = empty;
    6.39  );
    6.40  
    6.41 -val begin_proofs = Proofs.map (apfst (K empty_proofs));
    6.42 -val register_proofs = Proofs.map o pairself o add_proofs;
    6.43 -val register_proofs_thy = Context.theory_map o register_proofs;
    6.44 -
    6.45 -val join_local_proofs = force_proofs o #1 o Proofs.get o Context.Proof;
    6.46 -val join_recent_proofs = force_proofs o #1 o Proofs.get o Context.Theory;
    6.47 -val join_theory_proofs = force_proofs o #2 o Proofs.get o Context.Theory;
    6.48 +fun register_proofs more_thms = Proofs.map (fn thms => fold cons more_thms thms);
    6.49 +val join_theory_proofs = Thm.join_proofs o rev o Proofs.get;
    6.50  
    6.51  
    6.52  open Thm;