# HG changeset patch # User wenzelm # Date 1703190954 -3600 # Node ID d300a8f02b84df3de992367feaa2ffc770ebc433 # Parent 992c494bda25a8d91979f1570cffecaee937eb16 clarified zproof storage: per-theory table in anticipation of session exports; diff -r 992c494bda25 -r d300a8f02b84 src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Dec 21 21:03:02 2023 +0100 +++ b/src/Pure/thm.ML Thu Dec 21 21:35:54 2023 +0100 @@ -173,7 +173,8 @@ val varifyT_global: thm -> thm val legacy_freezeT: thm -> thm val plain_prop_of: thm -> term - val get_zproof: theory -> serial -> {prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof} option + val get_zproof: theory -> serial -> + {thm_name: Thm_Name.T, pos: Position.T, prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof} option val store_zproof: Thm_Name.T * Position.T -> thm -> theory -> thm * theory val dest_state: thm * int -> (term * term) list * term list * term * term val lift_rule: cterm -> thm -> thm @@ -942,16 +943,19 @@ (* data *) +type stored_zproof = + {thm_name: Thm_Name.T, pos: Position.T, prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof}; + structure Data = Theory_Data ( type T = - {prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof} Inttab.table * (*stored thms: zproof*) + stored_zproof Inttab.table * (*stored thms: zproof*) unit Name_Space.table * (*oracles: authentic derivation names*) classes; (*type classes within the logic*) val empty : T = (Inttab.empty, Name_Space.empty_table Markup.oracleN, empty_classes); - fun merge ((zproofs1, oracles1, sorts1), (zproofs2, oracles2, sorts2)) : T = - (Inttab.merge (K true) (zproofs1, zproofs2), + fun merge ((_, oracles1, sorts1), (_, oracles2, sorts2)) : T = + (Inttab.empty, Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2)); ); @@ -972,6 +976,11 @@ fun map_classrels f = map_classes (fn (classrels, arities) => (f classrels, arities)); fun map_arities f = map_classes (fn (classrels, arities) => (classrels, f arities)); +val _ = + (Theory.setup o Theory.at_begin) (fn thy => + if Inttab.is_empty (get_zproofs thy) then NONE + else SOME (map_zproofs (K Inttab.empty) thy)); + (* type classes *) @@ -2074,16 +2083,17 @@ val get_zproof = Inttab.lookup o get_zproofs; -fun store_zproof name thm thy = +fun store_zproof (name, pos) thm thy = let val Thm (Deriv {promises, body = PBody body}, args as {hyps, prop, ...}) = thm; val {oracles, thms, zboxes, zproof, proof} = body; val _ = null promises orelse raise THM ("store_zproof: theorem may not use promises", 0, [thm]); - val ((i, (zprop, zprf)), zproof') = ZTerm.thm_proof thy name hyps prop zproof; + val ((i, (zprop, zprf)), zproof') = ZTerm.thm_proof thy (name, pos) hyps prop zproof; val thy' = thy - |> map_zproofs (Inttab.update (i, {prop = zprop, zboxes = zboxes, zproof = zprf})); + |> (map_zproofs o Inttab.update) + (i, {thm_name = name, pos = pos, prop = zprop, zboxes = zboxes, zproof = zprf}); val der' = make_deriv promises oracles thms [] zproof' proof; in (Thm (der', args), thy') end;