--- a/src/Pure/Build/export_theory.ML Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/Build/export_theory.ML Mon Jul 22 20:13:46 2024 +0100
@@ -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/General/same.ML Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/General/same.ML Mon Jul 22 20:13:46 2024 +0100
@@ -12,6 +12,7 @@
type 'a operation = ('a, 'a) function (*exception SAME*)
val same: ('a, 'b) function
val commit: 'a operation -> 'a -> 'a
+ val commit_if: bool -> 'a operation -> 'a -> 'a
val commit_id: 'a operation -> 'a -> 'a * bool
val catch: ('a, 'b) function -> 'a -> 'b option
val compose: 'a operation -> 'a operation -> 'a operation
@@ -31,6 +32,7 @@
fun same _ = raise SAME;
fun commit f x = f x handle SAME => x;
+fun commit_if b f x = if b then commit f x else f x;
fun commit_id f x = (f x, false) handle SAME => (x, true);
fun catch f x = SOME (f x) handle SAME => NONE;
--- a/src/Pure/name.ML Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/name.ML Mon Jul 22 20:13:46 2024 +0100
@@ -26,11 +26,13 @@
val build_context: (context -> context) -> context
val make_context: string list -> context
val declare: string -> context -> context
+ val declare_renamed: string * string -> context -> context
val is_declared: context -> string -> bool
val invent: context -> string -> int -> string list
val invent_names: context -> string -> 'a list -> (string * 'a) list
val invent_list: string list -> string -> int -> string list
val variant: string -> context -> string * context
+ val variant_bound: string -> context -> string * context
val variant_list: string list -> string list -> string list
val enforce_case: bool -> string -> string
val desymbolize: bool option -> string -> string
@@ -101,6 +103,9 @@
fun declare_renaming (x, x') (Context tab) =
Context (Symtab.update (clean x, SOME (clean x')) tab);
+fun declare_renamed (x, x') =
+ clean x <> clean x' ? declare_renaming (x, x') #> declare x';
+
fun is_declared (Context tab) = Symtab.defined tab;
fun declared (Context tab) = Symtab.lookup tab;
@@ -144,12 +149,12 @@
let
val x0 = Symbol.bump_init x;
val x' = vary x0;
- val ctxt' = ctxt
- |> x0 <> x' ? declare_renaming (x0, x')
- |> declare x';
+ val ctxt' = ctxt |> declare_renamed (x0, x');
in (x', ctxt') end;
in (x' ^ replicate_string n "_", ctxt') end;
+fun variant_bound name = variant (if is_bound name then "u" else name);
+
fun variant_list used names = #1 (make_context used |> fold_map variant names);
--- a/src/Pure/proofterm.ML Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/proofterm.ML Mon Jul 22 20:13:46 2024 +0100
@@ -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
@@ -397,7 +392,7 @@
| zproof (PAxm (a, prop, SOME Ts)) = zproof_const (ZAxiom a) prop Ts
| zproof (PClass (T, c)) = OFCLASSp (ztyp T, c)
| zproof (Oracle (a, prop, SOME Ts)) = zproof_const (ZOracle a) prop Ts
- | zproof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
+ | zproof (PThm ({serial, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
let val proof_name =
ZThm {theory_name = theory_name, thm_name = thm_name, serial = serial};
in zproof_const proof_name prop Ts end;
@@ -2034,110 +2029,6 @@
(** theorems **)
-(* standardization of variables for export: only frees and named bounds *)
-
-local
-
-val declare_names_term = Term.declare_term_frees;
-val declare_names_term' = fn SOME t => declare_names_term t | NONE => I;
-val declare_names_proof = fold_proof_terms declare_names_term;
-
-fun variant names bs x =
- #1 (Name.variant x (fold Name.declare bs names));
-
-fun variant_term bs (Abs (x, T, t)) =
- let
- val x' = variant (declare_names_term t Name.context) bs x;
- val t' = variant_term (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' = variant (declare_names_proof prf Name.context) bs x;
- val prf' = variant_proof (x' :: bs) prf;
- in Abst (x', T, prf') end
- | variant_proof bs (AbsP (x, t, prf)) =
- let
- val x' = variant (declare_names_term' t (declare_names_proof prf Name.context)) bs x;
- val t' = Option.map (variant_term bs) t;
- val prf' = variant_proof (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 #> Term.declare_term_frees t;
-val used_frees_proof = fold_proof_terms_types used_frees_term used_frees_type;
-
-val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
-val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT;
-val unvarify_proof = map_proof_terms unvarify unvarifyT;
-
-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 term proof =
- let
- val hidden = hidden_types term proof;
- val idx = Term.maxidx_term term (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 term 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 []) term [];
- 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_frees = used
- |> used_frees_term term
- |> fold used_frees_proof proofs;
- val inst = Term_Subst.zero_var_indexes_inst used_frees (term :: proof_terms);
- val term' = term |> Term_Subst.instantiate inst |> unvarify |> variant_term [];
- val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof []);
- 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 =
@@ -2168,19 +2059,19 @@
local
-fun export_proof thy i prop prf =
+fun export_proof thy i prop0 proof0 =
let
- val (prop', SOME prf') = (prop, SOME prf) |> standard_vars Name.context;
- 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', no_thm_names 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/term_subst.ML Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/term_subst.ML Mon Jul 22 20:13:46 2024 +0100
@@ -230,8 +230,10 @@
(* zero var indexes *)
fun zero_var_inst ins mk (v as ((x, i), X)) (inst, used) =
- let val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used
- in if x = x' andalso i = 0 then (inst, used') else (ins (v, mk ((x', 0), X)) inst, used') end;
+ let
+ val (x', used') = Name.variant_bound x used;
+ val inst' = if x = x' andalso i = 0 then inst else ins (v, mk ((x', 0), X)) inst;
+ in (inst', used') end;
fun zero_var_indexes_inst used ts =
let
--- a/src/Pure/zterm.ML Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Pure/zterm.ML Mon Jul 22 20:13:46 2024 +0100
@@ -52,6 +52,53 @@
| fold_types _ _ = I;
+(* map *)
+
+fun map_tvars_same f =
+ let
+ fun typ (ZTVar v) = f v
+ | typ (ZFun (T, U)) =
+ (ZFun (typ T, Same.commit typ U)
+ handle Same.SAME => ZFun (T, typ U))
+ | typ ZProp = raise Same.SAME
+ | typ (ZType0 _) = raise Same.SAME
+ | typ (ZType1 (a, T)) = ZType1 (a, typ T)
+ | typ (ZType (a, Ts)) = ZType (a, Same.map typ Ts);
+ in typ end;
+
+fun map_aterms_same f =
+ let
+ fun term (ZAbs (x, T, t)) = ZAbs (x, T, term t)
+ | term (ZApp (t, u)) =
+ (ZApp (term t, Same.commit term u)
+ handle Same.SAME => ZApp (t, term u))
+ | term a = f a;
+ in term end;
+
+fun map_vars_same f = map_aterms_same (fn ZVar v => f v | _ => raise Same.SAME);
+
+fun map_types_same f =
+ let
+ fun term (ZVar (xi, T)) = ZVar (xi, f T)
+ | term (ZBound _) = raise Same.SAME
+ | term (ZConst0 _) = raise Same.SAME
+ | term (ZConst1 (c, T)) = ZConst1 (c, f T)
+ | term (ZConst (c, Ts)) = ZConst (c, Same.map f Ts)
+ | term (ZAbs (x, T, t)) =
+ (ZAbs (x, f T, Same.commit term t)
+ handle Same.SAME => ZAbs (x, T, term t))
+ | term (ZApp (t, u)) =
+ (ZApp (term t, Same.commit term u)
+ handle Same.SAME => ZApp (t, term u))
+ | term (OFCLASS (T, c)) = OFCLASS (f T, c);
+ in term end;
+
+val map_tvars = Same.commit o map_tvars_same;
+val map_aterms = Same.commit o map_aterms_same;
+val map_vars = Same.commit o map_vars_same;
+val map_types = Same.commit o map_types_same;
+
+
(* type ordering *)
local
@@ -224,6 +271,10 @@
val fold_aterms: (zterm -> 'a -> 'a) -> zterm -> 'a -> 'a
val fold_vars: (indexname * ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
+ val map_tvars: (indexname * sort -> ztyp) -> ztyp -> ztyp
+ val map_aterms: (zterm -> zterm) -> zterm -> zterm
+ val map_vars: (indexname * ztyp -> zterm) -> zterm -> zterm
+ val map_types: (ztyp -> ztyp) -> zterm -> zterm
val ztyp_ord: ztyp ord
val fast_zterm_ord: zterm ord
val aconv_zterm: zterm * zterm -> bool
@@ -231,6 +282,8 @@
val ZAbsps: zterm list -> zproof -> zproof
val ZAppts: zproof * zterm list -> zproof
val ZAppps: zproof * zproof list -> zproof
+ val strip_sortsT: ztyp -> ztyp
+ val strip_sorts: zterm -> zterm
val incr_bv_same: int -> int -> zterm Same.operation
val incr_proof_bv_same: int -> int -> int -> int -> zproof Same.operation
val incr_bv: int -> int -> zterm -> zterm
@@ -247,19 +300,28 @@
val subst_term_same:
ztyp Same.operation -> (indexname * ztyp, zterm) Same.function -> zterm Same.operation
exception BAD_INST of ((indexname * ztyp) * zterm) list
+ val fold_proof: {hyps: bool} -> (ztyp -> 'a -> 'a) -> (zterm -> 'a -> 'a) -> zproof -> 'a -> 'a
+ val fold_proof_types: {hyps: bool} -> (ztyp -> 'a -> 'a) -> zproof -> 'a -> 'a
val map_proof: {hyps: bool} -> ztyp Same.operation -> zterm Same.operation -> zproof -> zproof
val map_proof_types: {hyps: bool} -> ztyp Same.operation -> zproof -> zproof
val map_class_proof: (ztyp * class, zproof) Same.function -> zproof -> zproof
+ val maxidx_type: ztyp -> int -> int
+ val maxidx_term: zterm -> int -> int
+ val maxidx_proof: zproof -> int -> int
val ztyp_of: typ -> ztyp
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
@@ -318,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 =
@@ -345,6 +409,12 @@
fun combound (t, n, k) =
if k > 0 then ZApp (combound (t, n + 1, k - 1), ZBound n) else t;
+val strip_sortsT_same = map_tvars_same (fn (_, []) => raise Same.SAME | (a, _) => ZTVar (a, []));
+val strip_sorts_same = map_types_same strip_sortsT_same;
+
+val strip_sortsT = Same.commit strip_sortsT_same;
+val strip_sorts = Same.commit strip_sorts_same;
+
(* increment bound variables *)
@@ -585,6 +655,17 @@
in Same.commit proof end;
+(* maximum index of variables *)
+
+val maxidx_type = fold_tvars (fn ((_, i), _) => Integer.max i);
+
+fun maxidx_term t =
+ fold_types maxidx_type t #>
+ fold_aterms (fn ZVar ((_, i), _) => Integer.max i | _ => I) t;
+
+val maxidx_proof = fold_proof {hyps = false} maxidx_type maxidx_term;
+
+
(* convert ztyp vs. regular typ *)
fun ztyp_of (TFree (a, S)) = ZTVar ((a, ~1), S)
@@ -622,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);
@@ -631,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 =
@@ -682,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);
@@ -1427,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;
--- a/src/Tools/Haskell/Haskell.thy Mon Jul 22 20:13:38 2024 +0100
+++ b/src/Tools/Haskell/Haskell.thy Mon Jul 22 20:13:46 2024 +0100
@@ -2175,7 +2175,7 @@
Name,
uu, uu_, aT,
clean_index, clean, internal, skolem, is_internal, is_skolem, dest_internal, dest_skolem,
- Context, declare, declare_renaming, is_declared, declared, context, make_context,
+ Context, declare, declare_renamed, is_declared, declared, context, make_context,
variant, variant_list
)
where
@@ -2242,6 +2242,10 @@
declare_renaming (x, x') (Context names) =
Context (Map.insert (clean x) (Just (clean x')) names)
+declare_renamed :: (Name, Name) -> Context -> Context
+declare_renamed (x, x') =
+ (if clean x /= clean x' then declare_renaming (x, x') else id) #> declare x'
+
is_declared :: Context -> Name -> Bool
is_declared (Context names) x = Map.member x names
@@ -2289,9 +2293,7 @@
let
x0 = bump_init x
x' = vary x0
- ctxt' = ctxt
- |> (if x0 /= x' then declare_renaming (x0, x') else id)
- |> declare x'
+ ctxt' = ctxt |> declare_renamed (x0, x')
in (x', ctxt')
in (x' <> Bytes.pack (replicate n underscore), ctxt')