# HG changeset patch # User wenzelm # Date 1572875809 -3600 # Node ID d32ed8927a428a272533794a362dc69392133949 # Parent c85efa2be6191bd46496a9b1c0f5fe9ecce01801 more robust expose_proofs corresponding to register_proofs/consolidate_theory; expose_proofs of class algebra more aggresively, to ensure early export within original theory/session context; diff -r c85efa2be619 -r d32ed8927a42 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Sun Nov 03 20:38:08 2019 +0100 +++ b/src/Pure/Isar/class_declaration.ML Mon Nov 04 14:56:49 2019 +0100 @@ -84,7 +84,6 @@ in Goal.prove_sorry_global thy [] [] (Thm.prop_of thm'') (fn {context = ctxt, ...} => ALLGOALS (Proof_Context.fact_tac ctxt [thm''])) - |> tap (Thm.expose_proof thy) end; val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class)); @@ -103,9 +102,7 @@ REPEAT (SOMEGOAL (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs) ORELSE' assume_tac ctxt)); - val of_class = - Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context) - |> tap (Thm.expose_proof thy); + val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context); in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end; diff -r c85efa2be619 -r d32ed8927a42 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sun Nov 03 20:38:08 2019 +0100 +++ b/src/Pure/Isar/element.ML Mon Nov 04 14:56:49 2019 +0100 @@ -275,7 +275,7 @@ Witness (t, Goal.prove ctxt [] [] (mark_witness t) (fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac) - |> Thm.expose_derivation \<^here>); + |> Thm.close_derivation \<^here>); local @@ -290,7 +290,7 @@ (map o map) (fn prop => (mark_witness prop, [])) wit_propss @ [map (rpair []) eq_props]; fun after_qed' thmss = - let val (wits, eqs) = split_last ((map o map) (Thm.expose_derivation \<^here>) thmss); + let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here>) thmss); in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end; in proof after_qed' propss #> refine_witness end; @@ -324,7 +324,7 @@ fun conclude_witness ctxt (Witness (_, th)) = Goal.conclude th |> Raw_Simplifier.norm_hhf_protect ctxt - |> Thm.expose_derivation \<^here>; + |> Thm.close_derivation \<^here>; fun pretty_witness ctxt witn = let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in diff -r c85efa2be619 -r d32ed8927a42 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sun Nov 03 20:38:08 2019 +0100 +++ b/src/Pure/Isar/expression.ML Mon Nov 04 14:56:49 2019 +0100 @@ -720,8 +720,7 @@ compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN compose_tac defs_ctxt (false, - Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1) - |> tap (Thm.expose_proof defs_thy); + Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1); val conjuncts = (Drule.equal_elim_rule2 OF diff -r c85efa2be619 -r d32ed8927a42 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sun Nov 03 20:38:08 2019 +0100 +++ b/src/Pure/Thy/export_theory.ML Mon Nov 04 14:56:49 2019 +0100 @@ -275,9 +275,7 @@ else MinProof; val (prop, SOME proof) = standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0); - val _ = - if Proofterm.export_proof_boxes_required thy - then Proofterm.export_proof_boxes [proof] else (); + val _ = Thm.expose_proofs thy [thm]; in (prop, deps, proof) |> let diff -r c85efa2be619 -r d32ed8927a42 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Sun Nov 03 20:38:08 2019 +0100 +++ b/src/Pure/global_theory.ML Mon Nov 04 14:56:49 2019 +0100 @@ -288,11 +288,7 @@ fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy); fun apply_facts name_flags1 name_flags2 (b, facts) thy = - if Binding.is_empty b then - let - val (thms, thy') = app_facts facts thy; - val _ = Thm.expose_proofs thy' thms; - in register_proofs thms thy' end + if Binding.is_empty b then app_facts facts thy |-> register_proofs else let val name_pos = bind_name thy b; diff -r c85efa2be619 -r d32ed8927a42 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sun Nov 03 20:38:08 2019 +0100 +++ b/src/Pure/more_thm.ML Mon Nov 04 14:56:49 2019 +0100 @@ -682,9 +682,13 @@ (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths); fun consolidate_theory thy = - rev (Proofs.get thy) - |> maps (map (Thm.transfer thy) o Lazy.force) - |> Thm.consolidate; + let + val thms = + rev (Proofs.get thy) + |> maps (map (Thm.transfer thy) o Lazy.force); + val _ = Thm.consolidate thms; + val _ = Thm.expose_proofs thy thms; + in () end; diff -r c85efa2be619 -r d32ed8927a42 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Sun Nov 03 20:38:08 2019 +0100 +++ b/src/Pure/proofterm.ML Mon Nov 04 14:56:49 2019 +0100 @@ -46,7 +46,6 @@ val thm_node_body: thm_node -> proof_body future val thm_node_thms: thm_node -> thm list val join_thms: thm list -> proof_body list - val consolidate: proof_body list -> unit val make_thm: thm_header -> thm_body -> thm val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a val fold_body_thms: @@ -176,7 +175,7 @@ val export_enabled: unit -> bool val export_standard_enabled: unit -> bool val export_proof_boxes_required: theory -> bool - val export_proof_boxes: proof list -> unit + val export_proof_boxes: proof_body list -> unit val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body val thm_proof: theory -> (class * class -> proof) -> (string * class list list * class -> proof) -> string * Position.T -> sort list -> @@ -223,10 +222,10 @@ thms: (serial * thm_node) Ord_List.T, proof: proof} and thm_body = - Thm_Body of {export_proof: unit lazy, open_proof: proof -> proof, body: proof_body future} + Thm_Body of {open_proof: proof -> proof, body: proof_body future} and thm_node = Thm_Node of {theory_name: string, name: string, prop: term, - body: proof_body future, consolidate: unit lazy}; + body: proof_body future, export: unit lazy, consolidate: unit lazy}; type oracle = string * term option; val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord); @@ -246,11 +245,7 @@ fun thm_header serial pos theory_name name prop types : thm_header = {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types}; -val no_export_proof = Lazy.value (); - -fun thm_body body = - Thm_Body {export_proof = no_export_proof, open_proof = I, body = Future.value body}; -fun thm_body_export_proof (Thm_Body {export_proof, ...}) = export_proof; +fun thm_body body = Thm_Body {open_proof = I, body = Future.value body}; fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body; fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body); @@ -260,24 +255,33 @@ val thm_node_prop = #prop o rep_thm_node; val thm_node_body = #body o rep_thm_node; val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms); +val thm_node_export = #export o rep_thm_node; val thm_node_consolidate = #consolidate o rep_thm_node; fun join_thms (thms: thm list) = Future.joins (map (thm_node_body o #2) thms); -val consolidate = +val consolidate_bodies = maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms) #> Lazy.consolidate #> map Lazy.force #> ignore; -fun make_thm_node theory_name name prop body = - Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body, - consolidate = +fun make_thm_node theory_name name prop body export = + let + val body' = body + |> Options.default_bool "prune_proofs" ? (Future.map o map_proof_of) (K MinProof); + val consolidate = Lazy.lazy_name "Proofterm.make_thm_node" (fn () => - let val PBody {thms, ...} = Future.join body - in consolidate (join_thms thms) end)}; + let val PBody {thms, ...} = Future.join body' + in consolidate_bodies (join_thms thms) end); + in + Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body', + export = export, consolidate = consolidate} + end; + +val no_export = Lazy.value (); fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) = - (serial, make_thm_node theory_name name prop body); + (serial, make_thm_node theory_name name prop body no_export); (* proof atoms *) @@ -339,10 +343,10 @@ | no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf) | no_body_proofs (prf % t) = no_body_proofs prf % t | no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2 - | no_body_proofs (PThm (header, Thm_Body {export_proof, open_proof, body})) = + | no_body_proofs (PThm (header, Thm_Body {open_proof, body})) = let val body' = Future.value (no_proof_body (join_proof body)); - val thm_body' = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'}; + val thm_body' = Thm_Body {open_proof = open_proof, body = body'}; in PThm (header, thm_body') end | no_body_proofs a = a; @@ -443,7 +447,7 @@ let val (a, (b, (c, (d, e)))) = pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x - in (a, make_thm_node b c d (Future.value e)) end; + in (a, make_thm_node b c d (Future.value e) no_export) end; in @@ -1959,7 +1963,7 @@ fun fulfill_norm_proof thy ps body0 = let - val _ = consolidate (map #2 ps @ [body0]); + val _ = consolidate_bodies (map #2 ps @ [body0]); val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0; val oracles = unions_oracles @@ -2097,24 +2101,19 @@ Context.theory_name thy = Context.PureN orelse (export_enabled () andalso not (export_standard_enabled ())); -fun export_proof_boxes proofs = +fun export_proof_boxes bodies = let - fun export_boxes (AbsP (_, _, prf)) = export_boxes prf - | export_boxes (Abst (_, _, prf)) = export_boxes prf - | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2 - | export_boxes (prf % _) = export_boxes prf - | export_boxes (PThm ({serial = i, ...}, thm_body)) = - (fn boxes => - if Inttab.defined boxes i then boxes - else - let - val prf' = thm_body_proof_raw thm_body; - val export = thm_body_export_proof thm_body; - val boxes' = Inttab.update (i, export) boxes; - in export_boxes prf' boxes' end) - | export_boxes _ = I; - val boxes = (proofs, Inttab.empty) |-> fold export_boxes |> Inttab.dest; - in List.app (Lazy.force o #2) boxes end; + fun export_thm (i, thm_node) boxes = + if Inttab.defined boxes i then boxes + else + boxes + |> Inttab.update (i, thm_node_export thm_node) + |> fold export_thm (thm_node_thms thm_node); + + fun export_body (PBody {thms, ...}) = fold export_thm thms; + + val exports = (bodies, Inttab.empty) |-> fold export_body |> Inttab.dest; + in List.app (Lazy.force o #2) exports end; local @@ -2160,18 +2159,6 @@ strict = false} xml end; -fun export thy i prop prf = - if export_enabled () then - let - val _ = export_proof_boxes [prf]; - val _ = export_proof thy i prop prf; - in () end - else (); - -fun prune proof = - if Options.default_bool "prune_proofs" then MinProof - else proof; - fun prepare_thm_proof unconstrain thy classrel_proof arity_proof (name, pos) shyps hyps concl promises body = let @@ -2188,15 +2175,12 @@ (PBody {oracles = oracles0, thms = thms0, proof = if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof}); - fun publish i = map_proof_of (rew_proof thy #> tap (export thy i prop1) #> prune); - val open_proof = not named ? rew_proof thy; - fun new_prf () = let val i = serial (); val unconstrainT = unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext; - val postproc = map_proof_of unconstrainT #> named ? publish i; + val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy); in (i, fulfill_proof_future thy promises postproc body0) end; val (i, body') = @@ -2207,25 +2191,27 @@ let val Thm_Body {body = body', ...} = thm_body'; val i = if a = "" andalso named then serial () else ser; - in (i, body' |> ser <> i ? Future.map (publish i)) end + in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end else new_prf () | _ => new_prf ()); - val export_proof = - if named orelse not (export_enabled ()) then no_export_proof - else + val open_proof = not named ? rew_proof thy; + + val export = + if export_enabled () then Lazy.lazy (fn () => join_proof body' |> open_proof |> export_proof thy i prop1 handle exn => if Exn.is_interrupt exn then raise Fail ("Interrupt: potential resource problems while exporting proof " ^ string_of_int i) - else Exn.reraise exn); + else Exn.reraise exn) + else no_export; val theory_name = Context.theory_long_name thy; - val thm = (i, make_thm_node theory_name name prop1 body'); + val thm = (i, make_thm_node theory_name name prop1 body' export); val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE; - val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'}; + val thm_body = Thm_Body {open_proof = open_proof, body = body'}; val head = PThm (header, thm_body); val proof = if unconstrain then diff -r c85efa2be619 -r d32ed8927a42 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Nov 03 20:38:08 2019 +0100 +++ b/src/Pure/thm.ML Mon Nov 04 14:56:49 2019 +0100 @@ -113,7 +113,6 @@ val expand_name: thm -> Proofterm.thm_header -> string option val name_derivation: string * Position.T -> thm -> thm val close_derivation: Position.T -> thm -> thm - val expose_derivation: Position.T -> thm -> thm val trim_context: thm -> thm val axiom: theory -> string -> thm val all_axioms_of: theory -> (string * thm) list @@ -765,7 +764,7 @@ fun expose_proofs thy thms = if Proofterm.export_proof_boxes_required thy then - Proofterm.export_proof_boxes (map (proof_of o transfer thy) thms) + Proofterm.export_proof_boxes (proof_bodies_of (map (transfer thy) thms)) else (); fun expose_proof thy = expose_proofs thy o single; @@ -1044,10 +1043,6 @@ if not (null (tpairs_of thm)) orelse derivation_closed thm then thm else name_derivation ("", pos) thm); -fun expose_derivation pos thm = - close_derivation pos thm - |> tap (expose_proof (theory_of_thm thm)); - val trim_context = solve_constraints #> trim_context_thm; @@ -2253,7 +2248,8 @@ |> (map_classrels o Symreltab.update) ((c1, c2), (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) |> standard_tvars - |> expose_derivation \<^here> + |> close_derivation \<^here> + |> tap (expose_proof thy2) |> trim_context)); val proven = is_classrel thy1; @@ -2286,7 +2282,8 @@ val th1 = (th RS the_classrel thy (c, c1)) |> standard_tvars - |> expose_derivation \<^here> + |> close_derivation \<^here> + |> tap (expose_proof thy) |> trim_context; in SOME ((t, Ss, c1), (th1, thy_name, ser)) end); val finished' = finished andalso null completions;