# HG changeset patch # User wenzelm # Date 1721597492 -7200 # Node ID 0b8922e351a3eeb7b7ed5ca5d3f1ff324410aa03 # Parent e23aab2df03c7f47cf795587569ec4f86075495e clarified export: replaced Proofterm.standard_vars by ZTerm.standard_vars; diff -r e23aab2df03c -r 0b8922e351a3 src/Pure/Build/export_theory.ML --- 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, _)) = diff -r e23aab2df03c -r 0b8922e351a3 src/Pure/proofterm.ML --- 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, diff -r e23aab2df03c -r 0b8922e351a3 src/Pure/zterm.ML --- 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;