--- a/src/Pure/Build/export_theory.ML Sun Jul 21 22:34:25 2024 +0200
+++ b/src/Pure/Build/export_theory.ML Sun Jul 21 23:31:32 2024 +0200
@@ -65,17 +65,6 @@
in ([], triple int string int (ass, delim, pri)) end];
-(* free variables: not declared in the context *)
-
-val is_free = not oo Name.is_declared;
-
-fun add_frees used =
- fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I);
-
-fun add_tfrees used =
- (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
-
-
(* locales *)
fun locale_content thy loc =
@@ -149,6 +138,22 @@
val enabled = export_enabled context;
+ (* recode *)
+
+ val thy_cache = perhaps ZTerm.init_cache thy;
+
+ val ztyp_of = ZTerm.ztyp_cache thy_cache;
+ val zterm_of = ZTerm.zterm_of thy_cache;
+ val zproof_of = Proofterm.proof_to_zproof thy_cache;
+
+ val encode_ztyp = ZTerm.encode_ztyp;
+ val encode_zterm = ZTerm.encode_zterm {typed_vars = true};
+ val encode_term = encode_zterm o zterm_of;
+
+ val encode_standard_zterm = ZTerm.encode_zterm {typed_vars = false};
+ val encode_standard_zproof = ZTerm.encode_zproof {typed_vars = false};
+
+
(* strict parents *)
val parents = Theory.parents_of thy;
@@ -228,11 +233,9 @@
(* consts *)
- val encode_term = Term_XML.Encode.term consts;
-
val encode_const =
let open XML.Encode Term_XML.Encode
- in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) bool))) end;
+ in pair encode_syntax (pair (list string) (pair typ (pair (option encode_zterm) bool))) end;
val _ =
export_entities "consts" Sign.const_space (#constants (Consts.dest consts))
@@ -242,7 +245,8 @@
val syntax = get_syntax_const thy_ctxt c;
val U = Logic.unvarifyT_global T;
val U0 = Term.strip_sortsT U;
- val trim_abbrev = Proofterm.standard_vars_term Name.context #> Term.strip_sorts;
+ fun trim_abbrev t =
+ ZTerm.standard_vars Name.context (zterm_of t, NONE) |> #prop |> ZTerm.strip_sorts;
val abbrev' = Option.map trim_abbrev abbrev;
val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
@@ -253,19 +257,21 @@
fun standard_prop used extra_shyps raw_prop raw_proof =
let
- val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof);
- val args = rev (add_frees used prop []);
- val typargs = rev (add_tfrees used prop []);
- val used_typargs = fold (Name.declare o #1) typargs used;
+ val {typargs, args, prop, proof} =
+ ZTerm.standard_vars used (zterm_of raw_prop, Option.map zproof_of raw_proof);
+ val is_free = not o Name.is_declared used;
+ val args' = args |> filter (is_free o #1);
+ val typargs' = typargs |> filter (is_free o #1);
+ val used_typargs = fold (Name.declare o #1) typargs' used;
val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
- in ((sorts @ typargs, args, prop), proof) end;
+ in ((sorts @ typargs', args', prop), proof) end;
fun standard_prop_of thm =
standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
val encode_prop =
let open XML.Encode Term_XML.Encode
- in triple (list (pair string sort)) (list (pair string typ)) encode_term end;
+ in triple (list (pair string sort)) (list (pair string encode_ztyp)) encode_zterm end;
fun encode_axiom used prop =
encode_prop (#1 (standard_prop used [] prop NONE));
@@ -308,10 +314,8 @@
val _ = Thm.expose_proofs thy [thm];
in
(prop, deps, proof) |>
- let
- open XML.Encode Term_XML.Encode;
- val encode_proof = Proofterm.encode_standard_proof thy;
- in triple encode_prop (list Thm_Name.encode) encode_proof end
+ let open XML.Encode Term_XML.Encode
+ in triple encode_prop (list Thm_Name.encode) encode_standard_zproof end
end;
fun export_thm (thm_id, (thm_name, _)) =
--- a/src/Pure/proofterm.ML Sun Jul 21 22:34:25 2024 +0200
+++ b/src/Pure/proofterm.ML Sun Jul 21 23:31:32 2024 +0200
@@ -174,11 +174,6 @@
val expand_name_empty: thm_header -> Thm_Name.P option
val expand_proof: theory -> (thm_header -> Thm_Name.P option) -> proof -> proof
- val standard_vars: Name.context -> term * proof option -> term * proof option
- val standard_vars_term: Name.context -> term -> term
- val add_standard_vars: proof -> (string * typ) list -> (string * typ) list
- val add_standard_vars_term: term -> (string * typ) list -> (string * typ) list
-
val export_enabled: unit -> bool
val export_standard_enabled: unit -> bool
val export_proof_boxes_required: theory -> bool
@@ -2034,107 +2029,6 @@
(** theorems **)
-(* standardization of variables for export: only frees and named bounds *)
-
-local
-
-val declare_frees_term = Term.declare_term_frees;
-val declare_frees_term' = fn SOME t => declare_frees_term t | NONE => I;
-val declare_frees_proof = fold_proof_terms declare_frees_term;
-
-fun variant_term bs (Abs (x, T, t)) =
- let
- val x' = #1 (Name.variant x (declare_frees_term t bs));
- val t' = variant_term (Name.declare x' bs) t;
- in Abs (x', T, t') end
- | variant_term bs (t $ u) = variant_term bs t $ variant_term bs u
- | variant_term _ t = t;
-
-fun variant_proof bs (Abst (x, T, prf)) =
- let
- val x' = #1 (Name.variant x (declare_frees_proof prf bs));
- val prf' = variant_proof (Name.declare x' bs) prf;
- in Abst (x', T, prf') end
- | variant_proof bs (AbsP (x, t, prf)) =
- let
- val x' = #1 (Name.variant x (declare_frees_term' t (declare_frees_proof prf bs)));
- val t' = Option.map (variant_term bs) t;
- val prf' = variant_proof (Name.declare x' bs) prf;
- in AbsP (x', t', prf') end
- | variant_proof bs (prf % t) = variant_proof bs prf % Option.map (variant_term bs) t
- | variant_proof bs (prf1 %% prf2) = variant_proof bs prf1 %% variant_proof bs prf2
- | variant_proof bs (Hyp t) = Hyp (variant_term bs t)
- | variant_proof _ prf = prf;
-
-val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
-fun used_frees_term t = fold_types used_frees_type t #> declare_frees_term t;
-val used_frees_proof = fold_proof_terms_types used_frees_term used_frees_type;
-
-val unvarify_type = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
-val unvarify_term = map_types unvarify_type o Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t);
-val unvarify_proof = map_proof_terms unvarify_term unvarify_type;
-
-fun hidden_types prop proof =
- let
- val visible = (fold_types o fold_atyps) (insert (op =)) prop [];
- val add_hiddenT = fold_atyps (fn T => not (member (op =) visible T) ? insert (op =) T);
- in rev (fold_proof_terms_types (fold_types add_hiddenT) add_hiddenT proof []) end;
-
-fun standard_hidden_types prop proof =
- let
- val hidden = hidden_types prop proof;
- val idx = Term.maxidx_term prop (maxidx_proof proof ~1) + 1;
- fun smash T =
- if member (op =) hidden T then
- (case Type.sort_of_atyp T of
- [] => dummyT
- | S => TVar (("'", idx), S))
- else T;
- val smashT = map_atyps smash;
- in map_proof_terms (map_types smashT) smashT proof end;
-
-fun standard_hidden_terms prop proof =
- let
- fun add_unless excluded x =
- ((is_Free x orelse is_Var x) andalso not (member (op =) excluded x)) ? insert (op =) x;
- val visible = fold_aterms (add_unless []) prop [];
- val hidden = fold_proof_terms (fold_aterms (add_unless visible)) proof [];
- val dummy_term = Term.map_aterms (fn x =>
- if member (op =) hidden x then Term.dummy_pattern (Term.fastype_of x) else x);
- in proof |> not (null hidden) ? map_proof_terms dummy_term I end;
-
-in
-
-fun standard_vars used (term, opt_proof) =
- let
- val proofs = opt_proof
- |> Option.map (standard_hidden_types term #> standard_hidden_terms term) |> the_list;
- val proof_terms = rev (fold (fold_proof_terms_types cons (cons o Logic.mk_type)) proofs []);
- val used' = used
- |> used_frees_term term
- |> fold used_frees_proof proofs;
- val inst = Term_Subst.zero_var_indexes_inst used' (term :: proof_terms);
- val term' = term |> Term_Subst.instantiate inst |> unvarify_term |> variant_term Name.context;
- val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof Name.context);
- in (term', try hd proofs') end;
-
-fun standard_vars_term used t = #1 (standard_vars used (t, NONE));
-
-val add_standard_vars_term = fold_aterms
- (fn Free (x, T) =>
- (fn env =>
- (case AList.lookup (op =) env x of
- NONE => (x, T) :: env
- | SOME T' =>
- if T = T' then env
- else raise TYPE ("standard_vars_env: type conflict for variable " ^ quote x, [T, T'], [])))
- | _ => I);
-
-val add_standard_vars = fold_proof_terms add_standard_vars_term;
-
-end;
-
-
(* PThm nodes *)
fun prune_body body =
@@ -2165,19 +2059,19 @@
local
-fun export_proof thy i prop prf =
+fun export_proof thy i prop0 proof0 =
let
- val (prop', SOME prf') = standard_vars Name.context (prop, SOME (no_thm_names prf));
- val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
- val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev;
-
- val xml = (typargs, (args, (prop', prf'))) |>
+ val {typargs, args, prop, proof} =
+ ZTerm.standard_vars Name.context
+ (ZTerm.zterm_of thy prop0, SOME (proof_to_zproof thy (no_thm_names proof0)));
+ val xml = (typargs, (args, (prop, the proof))) |>
let
open XML.Encode Term_XML.Encode;
- val encode_vars = list (pair string typ);
- val encode_term = encode_standard_term thy;
- val encode_proof = encode_standard_proof thy;
- in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
+ val encode_tfrees = list (pair string sort);
+ val encode_frees = list (pair string ZTerm.encode_ztyp);
+ val encode_term = ZTerm.encode_zterm {typed_vars = false};
+ val encode_proof = ZTerm.encode_zproof {typed_vars = false};
+ in pair encode_tfrees (pair encode_frees (pair encode_term encode_proof)) end;
in
Export.export_params (Context.Theory thy)
{theory_name = Context.theory_long_name thy,
--- a/src/Pure/zterm.ML Sun Jul 21 22:34:25 2024 +0200
+++ b/src/Pure/zterm.ML Sun Jul 21 23:31:32 2024 +0200
@@ -312,12 +312,16 @@
val ztyp_dummy: ztyp
val typ_of_tvar: indexname * sort -> typ
val typ_of: ztyp -> typ
+ val init_cache: theory -> theory option
+ val exit_cache: theory -> theory option
val reset_cache: theory -> theory
val check_cache: theory -> {ztyp: int, typ: int} option
val ztyp_cache: theory -> typ -> ztyp
val typ_cache: theory -> ztyp -> typ
val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
val zterm_of: theory -> term -> zterm
+ val zterm_dummy_pattern: ztyp -> zterm
+ val zterm_type: ztyp -> zterm
val term_of: theory -> zterm -> term
val beta_norm_term_same: zterm Same.operation
val beta_norm_proof_same: zproof Same.operation
@@ -376,6 +380,8 @@
val encode_ztyp: ztyp XML.Encode.T
val encode_zterm: {typed_vars: bool} -> zterm XML.Encode.T
val encode_zproof: {typed_vars: bool} -> zproof XML.Encode.T
+ val standard_vars: Name.context -> zterm * zproof option ->
+ {typargs: (string * sort) list, args: (string * ztyp) list, prop: zterm, proof: zproof option}
end;
structure ZTerm: ZTERM =
@@ -697,6 +703,8 @@
fun make_ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
fun make_typ_cache () = ZTypes.unsynchronized_cache typ_of;
+in
+
fun init_cache thy =
if is_some (Data.get thy) then NONE
else SOME (Data.put (SOME (make_ztyp_cache (), make_typ_cache ())) thy);
@@ -706,8 +714,6 @@
SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); SOME (Data.put NONE thy))
| NONE => NONE);
-in
-
val _ = Theory.setup (Theory.at_begin init_cache #> Theory.at_end exit_cache);
fun reset_cache thy =
@@ -757,6 +763,9 @@
val zterm_of = #zterm o zterm_cache;
+fun zterm_dummy_pattern T = ZConst1 ("Pure.dummy_pattern", T);
+fun zterm_type T = ZConst1 ("Pure.type", T);
+
fun term_of thy =
let
val instance = Consts.instance (Sign.consts_of thy);
@@ -1502,4 +1511,143 @@
end;
+
+(* standardization of variables for export: only frees and named bounds *)
+
+local
+
+fun declare_frees_term t = fold_vars (fn ((x, ~1), _) => Name.declare x | _ => I) t;
+val declare_frees_proof = fold_proof {hyps = true} (K I) declare_frees_term;
+
+val (variant_abs_term, variant_abs_proof) =
+ let
+ fun term bs (ZAbs (x, T, t)) =
+ let
+ val x' = #1 (Name.variant x (declare_frees_term t bs));
+ val bs' = Name.declare x' bs;
+ in ZAbs (x', T, Same.commit_if (x <> x') (term bs') t) end
+ | term bs (ZApp (t, u)) =
+ (ZApp (term bs t, Same.commit (term bs) u)
+ handle Same.SAME => ZApp (t, term bs u))
+ | term _ _ = raise Same.SAME;
+
+ fun proof bs (ZAbst (x, T, p)) =
+ let
+ val x' = #1 (Name.variant x (declare_frees_proof p bs));
+ val bs' = Name.declare x' bs;
+ in ZAbst (x', T, Same.commit_if (x <> x') (proof bs') p) end
+ | proof bs (ZAbsp (x, t, p)) =
+ let
+ val x' = #1 (Name.variant x (declare_frees_term t (declare_frees_proof p bs)));
+ val (t', term_eq) = Same.commit_id (term bs) t;
+ val bs' = Name.declare x' bs;
+ in ZAbsp (x', t', Same.commit_if (x <> x' orelse not term_eq) (proof bs') p) end
+ | proof bs (ZAppt (p, t)) =
+ (ZAppt (proof bs p, Same.commit (term bs) t)
+ handle Same.SAME => ZAppt (p, term bs t))
+ | proof bs (ZAppp (p, q)) =
+ (ZAppp (proof bs p, Same.commit (proof bs) q)
+ handle Same.SAME => ZAppp (p, proof bs q))
+ | proof bs (ZHyp t) = ZHyp (term bs t)
+ | proof _ _ = raise Same.SAME;
+ in (term Name.context, proof Name.context) end;
+
+val used_frees_type = fold_tvars (fn ((a, ~1), _) => Name.declare a | _ => I);
+fun used_frees_term t = fold_types used_frees_type t #> declare_frees_term t;
+val used_frees_proof = fold_proof {hyps = true} used_frees_type used_frees_term;
+
+fun hidden_types prop proof =
+ let
+ val visible = (fold_types o fold_tvars) (insert (op =)) prop [];
+ val add_hiddenT = fold_tvars (fn v => not (member (op =) visible v) ? insert (op =) v);
+ in rev (fold_proof {hyps = true} add_hiddenT (fold_types add_hiddenT) proof []) end;
+
+fun standard_hidden_types prop proof =
+ let
+ val hidden = hidden_types prop proof;
+ val idx = maxidx_term prop (maxidx_proof proof ~1) + 1;
+ fun zvar (v as (_, S)) =
+ if not (member (op =) hidden v) then raise Same.SAME
+ else if null S then ztyp_dummy
+ else ZTVar (("'", idx), S);
+ val typ = map_tvars_same zvar;
+ in proof |> not (null hidden) ? map_proof {hyps = true} typ (map_types typ) end;
+
+fun standard_hidden_terms prop proof =
+ let
+ fun add_unless excluded (ZVar v) = not (member (op =) excluded v) ? insert (op =) v
+ | add_unless _ _ = I;
+ val visible = fold_aterms (add_unless []) prop [];
+ val hidden = fold_proof {hyps = true} (K I) (fold_aterms (add_unless visible)) proof [];
+ fun var (v as (_, T)) =
+ if member (op =) hidden v then zterm_dummy_pattern T else raise Same.SAME;
+ val term = map_vars_same var;
+ in proof |> not (null hidden) ? map_proof {hyps = true} Same.same term end;
+
+fun standard_inst add mk (v as ((x, i), T)) (inst, used) =
+ let
+ val (x', used') = Name.variant_bound x used;
+ val inst' = if x = x' andalso i = ~1 then inst else add (v, mk ((x', ~1), T)) inst;
+ in (inst', used') end;
+
+fun standard_inst_type used prf =
+ let
+ val add_tvars = fold_tvars (fn v => ZTVars.add (v, ()));
+ val (instT, _) =
+ (ZTVars.empty, used) |> ZTVars.fold (standard_inst ZTVars.add ZTVar o #1)
+ (TVars.build (prf |> fold_proof {hyps = true} add_tvars (fold_types add_tvars)));
+ in instantiate_type_same instT end;
+
+fun standard_inst_term used inst_type prf =
+ let
+ val add_vars = fold_vars (fn (x, T) => ZVars.add ((x, Same.commit inst_type T), ()));
+ val (inst, _) =
+ (ZVars.empty, used) |> ZVars.fold (standard_inst ZVars.add ZVar o #1)
+ (ZVars.build (prf |> fold_proof {hyps = true} (K I) add_vars));
+ in instantiate_term_same inst_type inst end;
+
+val typargs_type = fold_tvars (fn ((a, ~1), S) => TFrees.add_set (a, S) | _ => I);
+val typargs_term = fold_types typargs_type;
+val typargs_proof = fold_proof {hyps = true} typargs_type typargs_term;
+
+val add_standard_vars_term = fold_aterms
+ (fn ZVar ((x, ~1), T) =>
+ (fn env =>
+ (case AList.lookup (op =) env x of
+ NONE => (x, T) :: env
+ | SOME T' =>
+ if T = T' then env
+ else
+ raise TYPE ("standard_vars_env: type conflict for variable " ^ quote x,
+ [typ_of T, typ_of T'], [])))
+ | _ => I);
+
+val add_standard_vars = fold_proof {hyps = true} (K I) add_standard_vars_term;
+
+in
+
+fun standard_vars used (prop, opt_prf) =
+ let
+ val prf = the_default ZNop opt_prf
+ |> standard_hidden_types prop
+ |> standard_hidden_terms prop;
+ val prop_prf = ZAppp (ZHyp prop, prf);
+
+ val used' = used |> used_frees_proof prop_prf;
+ val inst_type = standard_inst_type used' prop_prf;
+ val inst_term = standard_inst_term used' inst_type prop_prf;
+ val inst_proof = map_proof_same {hyps = true} inst_type inst_term;
+
+ val prop' = prop |> Same.commit (Same.compose variant_abs_term inst_term);
+ val opt_proof' =
+ if is_none opt_prf then NONE
+ else SOME (prf |> Same.commit (Same.compose variant_abs_proof inst_proof));
+ val proofs' = the_list opt_proof';
+
+ val args = build_rev (add_standard_vars_term prop' #> fold add_standard_vars proofs');
+ val typargs = TFrees.list_set (TFrees.build (typargs_term prop' #> fold typargs_proof proofs'));
+ in {typargs = typargs, args = args, prop = prop', proof = opt_proof'} end;
+
end;
+
+end;