--- a/src/HOL/Tools/SMT/z3_proof.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/HOL/Tools/SMT/z3_proof.ML Sun Dec 31 19:24:37 2023 +0100
@@ -210,7 +210,7 @@
fun substTs_same subst =
let val applyT = Same.function (AList.lookup (op =) subst)
- in Term_Subst.map_atypsT_same applyT end
+ in Term.map_atyps_same applyT end
fun subst_types ctxt env bounds t =
let
@@ -226,7 +226,7 @@
val patTs = map snd (Term.strip_qnt_vars \<^const_name>\<open>Pure.all\<close> t')
val objTs = map objT_of bounds
val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
- in Term_Subst.map_types (substTs_same subst) t' end
+ in Term.map_types (substTs_same subst) t' end
fun eq_quant (\<^const_name>\<open>HOL.All\<close>, _) (\<^const_name>\<open>HOL.All\<close>, _) = true
| eq_quant (\<^const_name>\<open>HOL.Ex\<close>, _) (\<^const_name>\<open>HOL.Ex\<close>, _) = true
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Dec 31 19:24:37 2023 +0100
@@ -74,7 +74,7 @@
| alternative _ NONE NONE = NONE
fun varify_nonfixed_terms_global nonfixeds tm =
- tm |> Term_Subst.map_aterms
+ tm |> Term.map_aterms
(fn Free (x, T) => if member (op =) nonfixeds x then Var ((x, 0), T) else raise Same.SAME
| Var (xi, _) => raise TERM (Logic.bad_schematic xi, [tm])
| _ => raise Same.SAME)
--- a/src/Pure/Proof/extraction.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/Proof/extraction.ML Sun Dec 31 19:24:37 2023 +0100
@@ -390,7 +390,7 @@
val cs = maps (fn T => map (pair T) S) Ts;
val constraints' = map Logic.mk_of_class cs;
val typ_map = Type.strip_sorts o
- Term_Subst.map_atypsT (fn U =>
+ Term.map_atyps (fn U =>
if member (op =) atyps U
then #typ_operation ucontext {strip_sorts = false} U
else raise Same.SAME);
--- a/src/Pure/envir.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/envir.ML Sun Dec 31 19:24:37 2023 +0100
@@ -341,14 +341,14 @@
local
-fun subst_type0 tyenv = Term_Subst.map_atypsT_same
+fun subst_type0 tyenv = Term.map_atyps_same
(fn TVar v =>
(case Type.lookup tyenv v of
SOME U => U
| NONE => raise Same.SAME)
| _ => raise Same.SAME);
-fun subst_term1 tenv = Term_Subst.map_aterms_same
+fun subst_term1 tenv = Term.map_aterms_same
(fn Var v =>
(case lookup1 tenv v of
SOME u => u
@@ -381,7 +381,7 @@
fun subst_term_types_same tyenv =
if Vartab.is_empty tyenv then Same.same
- else Term_Subst.map_types_same (subst_type0 tyenv);
+ else Term.map_types_same (subst_type0 tyenv);
fun subst_term_same (tyenv, tenv) =
if Vartab.is_empty tenv then subst_term_types_same tyenv
--- a/src/Pure/logic.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/logic.ML Sun Dec 31 19:24:37 2023 +0100
@@ -388,7 +388,7 @@
SOME T' => T' |> strip_sorts ? Type.strip_sorts
| NONE => raise TYPE ("Dangling type variable ", [T], [prop]))));
- val typ_operation = Term_Subst.map_atypsT_same o atyp_operation;
+ val typ_operation = Term.map_atyps_same o atyp_operation;
val constraints =
constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
@@ -402,7 +402,7 @@
constraints = constraints,
outer_constraints = outer_constraints};
val prop' = prop
- |> Term_Subst.map_types (typ_operation {strip_sorts = true})
+ |> Term.map_types (typ_operation {strip_sorts = true})
|> curry list_implies (map #2 constraints);
in (ucontext, prop') end;
@@ -447,7 +447,7 @@
| rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
fun incr_tvar_same 0 = Same.same
- | incr_tvar_same inc = Term_Subst.map_atypsT_same
+ | incr_tvar_same inc = Term.map_atyps_same
(fn TVar ((a, i), S) => TVar ((a, i + inc), S)
| _ => raise Same.SAME);
@@ -612,12 +612,12 @@
fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
fun varifyT_global_same ty = ty
- |> Term_Subst.map_atypsT_same
+ |> Term.map_atyps_same
(fn TFree (a, S) => TVar ((a, 0), S)
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
fun unvarifyT_global_same ty = ty
- |> Term_Subst.map_atypsT_same
+ |> Term.map_atyps_same
(fn TVar ((a, 0), S) => TFree (a, S)
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
| TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
@@ -626,22 +626,22 @@
val unvarifyT_global = Same.commit unvarifyT_global_same;
fun varify_types_global tm =
- Term_Subst.map_types varifyT_global_same tm
+ Term.map_types varifyT_global_same tm
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
fun unvarify_types_global tm =
- Term_Subst.map_types unvarifyT_global_same tm
+ Term.map_types unvarifyT_global_same tm
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
fun varify_global tm = tm
- |> Term_Subst.map_aterms
+ |> Term.map_aterms
(fn Free (x, T) => Var ((x, 0), T)
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
| _ => raise Same.SAME)
|> varify_types_global;
fun unvarify_global tm = tm
- |> Term_Subst.map_aterms
+ |> Term.map_aterms
(fn Var ((x, 0), T) => Free (x, T)
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
| Free (x, _) => raise TERM (bad_fixed x, [tm])
--- a/src/Pure/proofterm.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/proofterm.ML Sun Dec 31 19:24:37 2023 +0100
@@ -552,7 +552,7 @@
in proof end;
fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => PClass (typ T, c));
-fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
+fun map_proof_types_same typ = map_proof_terms_same (Term.map_types_same typ) typ;
fun map_proof_terms f g =
Same.commit (map_proof_terms_same (Same.function_eq (op =) f) (Same.function_eq (op =) g));
@@ -925,7 +925,7 @@
let
val tab = TFrees.make names;
val typ =
- Term_Subst.map_atypsT_same
+ Term.map_atyps_same
(fn TFree v =>
(case TFrees.lookup tab v of
NONE => raise Same.SAME
@@ -1118,7 +1118,7 @@
let val T' = Same.commit typ_sort T
in the_single (of_sort_proof algebra sorts_proof hyps (T', [c])) end;
in
- Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ class)
+ Same.commit (map_proof_same (Term.map_types_same typ) typ class)
#> fold_rev (implies_intr_proof o #2) (#constraints ucontext)
end;
@@ -1613,7 +1613,7 @@
fun subst_same A =
(case AList.lookup (op =) inst A of SOME T => T | NONE => raise Same.SAME);
val subst_type_same =
- Term_Subst.map_atypsT_same
+ Term.map_atyps_same
(fn TVar ((a, i), S) => subst_same (TVar ((a, i - shift), S)) | A => subst_same A);
in Same.commit (map_proof_types_same subst_type_same) prf end;
@@ -2240,7 +2240,7 @@
val proof2 =
if unconstrain then
proof_combt' (head,
- (Same.commit o Same.map o Same.map_option o Term_Subst.map_types_same)
+ (Same.commit o Same.map o Same.map_option o Term.map_types_same)
(typ_operation {strip_sorts = true}) args)
else
proof_combP (proof_combt' (head, args),
--- a/src/Pure/term.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/term.ML Sun Dec 31 19:24:37 2023 +0100
@@ -68,11 +68,11 @@
val head_of: term -> term
val size_of_term: term -> int
val size_of_typ: typ -> int
- val map_atyps: (typ -> typ) -> typ -> typ
- val map_aterms: (term -> term) -> term -> term
- val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
- val map_type_tfree: (string * sort -> typ) -> typ -> typ
- val map_types: (typ -> typ) -> term -> term
+ val map_atyps: typ Same.operation -> typ -> typ
+ val map_aterms: term Same.operation -> term -> term
+ val map_types: typ Same.operation -> term -> term
+ val map_type_tvar: (indexname * sort, typ) Same.function -> typ -> typ
+ val map_type_tfree: (string * sort, typ) Same.function -> typ -> typ
val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
@@ -122,6 +122,9 @@
signature TERM =
sig
include BASIC_TERM
+ val map_atyps_same: typ Same.operation -> typ Same.operation
+ val map_aterms_same: term Same.operation -> term Same.operation
+ val map_types_same: typ Same.operation -> term Same.operation
val aT: sort -> typ
val itselfT: typ -> typ
val a_itselfT: typ
@@ -449,25 +452,44 @@
| add_size _ n = n + 1;
in add_size ty 0 end;
-fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
- | map_atyps f T = f T;
+
+(* map types and terms *)
+
+fun map_atyps_same f =
+ let
+ fun typ (Type (a, Ts)) = Type (a, Same.map typ Ts)
+ | typ T = f T;
+ in typ end;
-fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
- | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
- | map_aterms f t = f t;
-
-fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
-fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
+fun map_aterms_same f =
+ let
+ fun term (Abs (x, T, t)) = Abs (x, T, term t)
+ | term (t $ u) =
+ (term t $ Same.commit term u
+ handle Same.SAME => t $ term u)
+ | term a = f a;
+ in term end;
-fun map_types f =
+fun map_types_same f =
let
- fun map_aux (Const (a, T)) = Const (a, f T)
- | map_aux (Free (a, T)) = Free (a, f T)
- | map_aux (Var (v, T)) = Var (v, f T)
- | map_aux (Bound i) = Bound i
- | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
- | map_aux (t $ u) = map_aux t $ map_aux u;
- in map_aux end;
+ fun term (Const (a, T)) = Const (a, f T)
+ | term (Free (a, T)) = Free (a, f T)
+ | term (Var (xi, T)) = Var (xi, f T)
+ | term (Bound _) = raise Same.SAME
+ | term (Abs (x, T, t)) =
+ (Abs (x, f T, Same.commit term t)
+ handle Same.SAME => Abs (x, T, term t))
+ | term (t $ u) =
+ (term t $ Same.commit term u
+ handle Same.SAME => t $ term u);
+ in term end;
+
+val map_atyps = Same.commit o map_atyps_same;
+val map_aterms = Same.commit o map_aterms_same;
+val map_types = Same.commit o map_types_same;
+
+fun map_type_tvar f = map_atyps (fn TVar x => f x | _ => raise Same.SAME);
+fun map_type_tfree f = map_atyps (fn TFree x => f x | _ => raise Same.SAME);
(* fold types and terms *)
--- a/src/Pure/term_subst.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/term_subst.ML Sun Dec 31 19:24:37 2023 +0100
@@ -6,12 +6,6 @@
signature TERM_SUBST =
sig
- val map_atypsT_same: typ Same.operation -> typ Same.operation
- val map_types_same: typ Same.operation -> term Same.operation
- val map_aterms_same: term Same.operation -> term Same.operation
- val map_atypsT: typ Same.operation -> typ -> typ
- val map_types: typ Same.operation -> term -> term
- val map_aterms: term Same.operation -> term -> term
val generalizeT_same: Names.set -> int -> typ Same.operation
val generalize_same: Names.set * Names.set -> int -> term Same.operation
val generalizeT: Names.set -> int -> typ -> typ
@@ -39,38 +33,6 @@
structure Term_Subst: TERM_SUBST =
struct
-(* generic mapping *)
-
-fun map_atypsT_same f =
- let
- fun typ (Type (a, Ts)) = Type (a, Same.map typ Ts)
- | typ T = f T;
- in typ end;
-
-fun map_types_same f =
- let
- fun term (Const (a, T)) = Const (a, f T)
- | term (Free (a, T)) = Free (a, f T)
- | term (Var (v, T)) = Var (v, f T)
- | term (Bound _) = raise Same.SAME
- | term (Abs (x, T, t)) =
- (Abs (x, f T, Same.commit term t)
- handle Same.SAME => Abs (x, T, term t))
- | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u);
- in term end;
-
-fun map_aterms_same f =
- let
- fun term (Abs (x, T, t)) = Abs (x, T, term t)
- | term (t $ u) = (term t $ Same.commit term u handle Same.SAME => t $ term u)
- | term a = f a;
- in term end;
-
-val map_atypsT = Same.commit o map_atypsT_same;
-val map_types = Same.commit o map_types_same;
-val map_aterms = Same.commit o map_aterms_same;
-
-
(* generalization of fixed variables *)
fun generalizeT_same tfrees idx ty =
--- a/src/Pure/thm.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/thm.ML Sun Dec 31 19:24:37 2023 +0100
@@ -1102,7 +1102,7 @@
(ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
val zproof' = ZTerm.map_proof_types map_ztyp zproof;
- val proof' = Proofterm.map_proof_types (Term_Subst.map_atypsT_same map_atyp) proof;
+ val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;
in
Thm (make_deriv promises oracles thms zboxes zproof' proof',
{cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
--- a/src/Pure/type_infer.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/type_infer.ML Sun Dec 31 19:24:37 2023 +0100
@@ -48,7 +48,7 @@
fun anyT S = TFree ("'_dummy_", S);
val paramify_vars =
- Term_Subst.map_atypsT (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME);
+ Term.map_atyps (fn TVar ((x, i), S) => param i (x, S) | _ => raise Same.SAME);