--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Sep 03 18:57:33 2021 +0200
@@ -45,7 +45,7 @@
('a -> thm -> 'b Seq.seq) -> 'a -> thm -> 'b Seq.seq
val try_dest_Trueprop : term -> term
- val type_devar : ((indexname * sort) * typ) list -> term -> term
+ val type_devar : typ Term_Subst.TVars.table -> term -> term
val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm
val batter_tac : Proof.context -> int -> tactic
@@ -545,7 +545,7 @@
end)
(*Instantiate type variables in a term, based on a type environment*)
-fun type_devar (tyenv : ((indexname * sort) * typ) list) (t : term) : term =
+fun type_devar tyenv (t : term) : term =
case t of
Const (s, ty) => Const (s, Term_Subst.instantiateT tyenv ty)
| Free (s, ty) => Free (s, Term_Subst.instantiateT tyenv ty)
@@ -573,7 +573,7 @@
val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing
val typeval_env =
- map (apfst dest_TVar) type_pairing
+ Term_Subst.TVars.table (map (apfst dest_TVar) type_pairing)
(*valuation of term variables*)
val termval =
map (apfst (dest_Var o type_devar typeval_env)) term_pairing
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 03 18:57:33 2021 +0200
@@ -78,8 +78,8 @@
val (instT, lthy2) = lthy1
|> Variable.declare_names fixed_crel
|> Variable.importT_inst (param_rel_subst :: args_subst)
- val args_fixed = (map (Term_Subst.instantiate (instT, []))) args_subst
- val param_rel_fixed = Term_Subst.instantiate (instT, []) param_rel_subst
+ val args_fixed = (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty))) args_subst
+ val param_rel_fixed = Term_Subst.instantiate (instT, Term_Subst.Vars.empty) param_rel_subst
val rty = (domain_type o fastype_of) param_rel_fixed
val relcomp_op = Const (\<^const_name>\<open>relcompp\<close>,
(rty --> rty' --> HOLogic.boolT) -->
@@ -295,7 +295,7 @@
let
val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
- in (tvars ~~ map TFree tfrees, ctxt') end
+ in (Term_Subst.TVars.table (tvars ~~ map TFree tfrees), ctxt') end
fun import_inst_exclude exclude ts ctxt =
let
@@ -304,7 +304,7 @@
val vars = map (apsnd (Term_Subst.instantiateT instT))
(rev (subtract op= exclude (fold Term.add_vars ts [])))
val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
- val inst = vars ~~ map Free (xs ~~ map #2 vars)
+ val inst = Term_Subst.Vars.table (vars ~~ map Free (xs ~~ map #2 vars))
in ((instT, inst), ctxt'') end
fun import_terms_exclude exclude ts ctxt =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 03 18:57:33 2021 +0200
@@ -1072,7 +1072,10 @@
" (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
" and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
" in " ^ Thm.string_of_thm ctxt' th)
- in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end
+ in
+ Vartab.fold (fn (xi, (S, T)) => Term_Subst.TVars.add ((xi, S), T))
+ subst Term_Subst.TVars.empty
+ end
fun instantiate_typ th =
let
val (pred', _) = strip_intro_concl th
@@ -1080,7 +1083,10 @@
if not (fst (dest_Const pred) = fst (dest_Const pred')) then
raise Fail "Trying to instantiate another predicate"
else ()
- in Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt')) (subst_of (pred', pred)), []) th end
+ val instT =
+ Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T))
+ (subst_of (pred', pred)) [];
+ in Thm.instantiate (instT, []) th end
fun instantiate_ho_args th =
let
val (_, args') =
@@ -1088,7 +1094,7 @@
val ho_args' = map dest_Var (ho_args_of_typ T args')
in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end
val outp_pred =
- Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
+ Term_Subst.instantiate (subst_of (inp_pred, pred), Term_Subst.Vars.empty) inp_pred
val ((_, ths'), ctxt1) =
Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
in
--- a/src/Pure/Isar/expression.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/Isar/expression.ML Fri Sep 03 18:57:33 2021 +0200
@@ -190,7 +190,8 @@
(type_parms ~~ map Logic.dest_type type_parms'')
|> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
val cert_inst =
- ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'')
+ ((map #1 params ~~
+ map (Term_Subst.instantiateT_frees (Term_Subst.TFrees.table instT)) parm_types) ~~ insts'')
|> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
in
(Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
--- a/src/Pure/Isar/generic_target.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML Fri Sep 03 18:57:33 2021 +0200
@@ -317,14 +317,17 @@
chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
|>> map Logic.dest_type;
- val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
- val inst =
+ val instT =
+ fold2 (fn a => fn b => (case a of TVar v => Term_Subst.TVars.add (v, b) | _ => I))
+ tvars tfrees Term_Subst.TVars.empty;
+ val cinstT = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) instT [];
+ val cinst =
map_filter
(fn (Var (xi, T), t) =>
SOME ((xi, Term_Subst.instantiateT instT T),
Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t))
| _ => NONE) (vars ~~ frees);
- val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result;
+ val result' = Thm.instantiate (cinstT, cinst) result;
(*import assumes/defines*)
val result'' =
--- a/src/Pure/Isar/subgoal.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML Fri Sep 03 18:57:33 2021 +0200
@@ -55,8 +55,8 @@
else ([], goal);
val text = asms @ (if do_concl then [concl] else []);
- val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
- val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst);
+ val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
+ val schematic_terms = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
val schematics = (schematic_types, schematic_terms);
val asms' = map (Thm.instantiate_cterm schematics) asms;
--- a/src/Pure/Tools/rule_insts.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML Fri Sep 03 18:57:33 2021 +0200
@@ -119,7 +119,8 @@
|> Proof_Context.add_fixes_cmd raw_fixes;
(*explicit type instantiations*)
- val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);
+ val instT1 =
+ Term_Subst.instantiateT (Term_Subst.TVars.table (map (read_type ctxt1 tvars) type_insts));
val vars1 = map (apsnd instT1) vars;
(*term instantiations*)
@@ -128,10 +129,12 @@
val ((ts, inferred), ctxt2) = read_terms ss Ts ctxt1;
(*implicit type instantiations*)
- val instT2 = Term_Subst.instantiateT inferred;
+ val instT2 = Term_Subst.instantiateT (Term_Subst.TVars.table inferred);
val vars2 = map (apsnd instT2) vars1;
val inst2 =
- Term_Subst.instantiate ([], map2 (fn (xi, _) => fn t => ((xi, Term.fastype_of t), t)) xs ts)
+ Term_Subst.instantiate (Term_Subst.TVars.empty,
+ fold2 (fn (xi, _) => fn t => Term_Subst.Vars.add ((xi, Term.fastype_of t), t))
+ xs ts Term_Subst.Vars.empty)
#> Envir.beta_norm;
val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
--- a/src/Pure/consts.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/consts.ML Fri Sep 03 18:57:33 2021 +0200
@@ -225,9 +225,11 @@
fun instance consts (c, Ts) =
let
val declT = type_scheme consts c;
- val vars = map Term.dest_TVar (typargs consts (c, declT));
- val inst = vars ~~ Ts handle ListPair.UnequalLengths =>
- raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
+ val args = typargs consts (c, declT);
+ val inst =
+ fold2 (fn a => fn T => Term_Subst.TVars.add (Term.dest_TVar a, T))
+ args Ts Term_Subst.TVars.empty
+ handle ListPair.UnequalLengths => raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
in declT |> Term_Subst.instantiateT inst end;
fun dummy_types consts =
--- a/src/Pure/drule.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/drule.ML Fri Sep 03 18:57:33 2021 +0200
@@ -214,11 +214,15 @@
val tvars = fold Thm.add_tvars ths [];
fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars);
- val instT' = map (fn (v, TVar (b, _)) => (v, Thm.rename_tvar b (the_tvar v))) instT;
+ val instT' =
+ (instT, []) |-> Term_Subst.TVars.fold (fn (v, TVar (b, _)) =>
+ cons (v, Thm.rename_tvar b (the_tvar v)));
val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths [];
fun the_var v = the (find_first (fn ct => v = dest_Var (Thm.term_of ct)) vars);
- val inst' = map (fn (v, Var (b, _)) => (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v)))) inst;
+ val inst' =
+ (inst, []) |-> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
+ cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v))));
in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end;
val zero_var_indexes = singleton zero_var_indexes_list;
--- a/src/Pure/more_thm.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/more_thm.ML Fri Sep 03 18:57:33 2021 +0200
@@ -467,8 +467,9 @@
handle TERM (msg, _) => raise THM (msg, 0, [th]);
val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
+ val instantiateT = Term_Subst.instantiateT (Term_Subst.TVars.table instT);
val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
- let val T' = Term_Subst.instantiateT instT T
+ let val T' = instantiateT T
in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end);
in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end;
--- a/src/Pure/morphism.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/morphism.ML Fri Sep 03 18:57:33 2021 +0200
@@ -137,12 +137,18 @@
fun instantiate_frees_morphism ([], []) = identity
| instantiate_frees_morphism (cinstT, cinst) =
let
- val instT = map (apsnd Thm.typ_of) cinstT;
- val inst = map (apsnd Thm.term_of) cinst;
+ val instT =
+ fold (fn (v, cT) => Term_Subst.TFrees.add (v, Thm.typ_of cT))
+ cinstT Term_Subst.TFrees.empty;
+ val inst =
+ fold (fn (v, ct) => Term_Subst.Frees.add (v, Thm.term_of ct))
+ cinst Term_Subst.Frees.empty;
in
morphism "instantiate_frees"
{binding = [],
- typ = if null instT then [] else [Term_Subst.instantiateT_frees instT],
+ typ =
+ if Term_Subst.TFrees.is_empty instT then []
+ else [Term_Subst.instantiateT_frees instT],
term = [Term_Subst.instantiate_frees (instT, inst)],
fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
end;
@@ -150,12 +156,18 @@
fun instantiate_morphism ([], []) = identity
| instantiate_morphism (cinstT, cinst) =
let
- val instT = map (apsnd Thm.typ_of) cinstT;
- val inst = map (apsnd Thm.term_of) cinst;
+ val instT =
+ fold (fn (v, cT) => Term_Subst.TVars.add (v, Thm.typ_of cT))
+ cinstT Term_Subst.TVars.empty;
+ val inst =
+ fold (fn (v, ct) => Term_Subst.Vars.add (v, Thm.term_of ct))
+ cinst Term_Subst.Vars.empty;
in
morphism "instantiate"
{binding = [],
- typ = if null instT then [] else [Term_Subst.instantiateT instT],
+ typ =
+ if Term_Subst.TVars.is_empty instT then []
+ else [Term_Subst.instantiateT instT],
term = [Term_Subst.instantiate (instT, inst)],
fact = [map (Thm.instantiate (cinstT, cinst))]}
end;
--- a/src/Pure/proofterm.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/proofterm.ML Fri Sep 03 18:57:33 2021 +0200
@@ -114,8 +114,7 @@
val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
val permute_prems_proof: term list -> int -> int -> proof -> proof
val generalize_proof: Symtab.set * Symtab.set -> int -> term -> proof -> proof
- val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
- -> proof -> proof
+ val instantiate: typ Term_Subst.TVars.table * term Term_Subst.Vars.table -> proof -> proof
val lift_proof: term -> int -> term -> proof -> proof
val incr_indexes: int -> proof -> proof
val assumption_proof: term list -> term -> int -> proof -> proof
@@ -672,18 +671,25 @@
(* substitutions *)
-fun del_conflicting_tvars envT T = Term_Subst.instantiateT
- (map_filter (fn ixnS as (_, S) =>
- (Type.lookup envT ixnS; NONE) handle TYPE _ =>
- SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvarsT T [])) T;
+fun del_conflicting_tvars envT T =
+ let
+ val instT =
+ map_filter (fn ixnS as (_, S) =>
+ (Type.lookup envT ixnS; NONE) handle TYPE _ =>
+ SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvarsT T [])
+ in Term_Subst.instantiateT (Term_Subst.TVars.table instT) T end;
-fun del_conflicting_vars env t = Term_Subst.instantiate
- (map_filter (fn ixnS as (_, S) =>
- (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
- SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvars t []),
- map_filter (fn (ixnT as (_, T)) =>
- (Envir.lookup env ixnT; NONE) handle TYPE _ =>
- SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
+fun del_conflicting_vars env t =
+ let
+ val instT =
+ map_filter (fn ixnS as (_, S) =>
+ (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
+ SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvars t []);
+ val inst =
+ map_filter (fn (ixnT as (_, T)) =>
+ (Envir.lookup env ixnT; NONE) handle TYPE _ =>
+ SOME (ixnT, Free ("dummy", T))) (Term.add_vars t []);
+ in Term_Subst.instantiate (Term_Subst.TVars.make instT, Term_Subst.Vars.table inst) t end;
fun norm_proof env =
let
@@ -967,7 +973,7 @@
fun instantiate (instT, inst) =
Same.commit (map_proof_terms_same
- (Term_Subst.instantiate_same (instT, map (apsnd remove_types) inst))
+ (Term_Subst.instantiate_same (instT, Term_Subst.Vars.map (K remove_types) inst))
(Term_Subst.instantiateT_same instT));
--- a/src/Pure/term_subst.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/term_subst.ML Fri Sep 03 18:57:33 2021 +0200
@@ -4,8 +4,31 @@
Efficient type/term substitution.
*)
+signature INST_TABLE =
+sig
+ include TABLE
+ val add: key * 'a -> 'a table -> 'a table
+ val table: (key * 'a) list -> 'a table
+end;
+
+functor Inst_Table(Key: KEY): INST_TABLE =
+struct
+
+structure Tab = Table(Key);
+
+fun add entry = Tab.insert (K true) entry;
+fun table entries = fold add entries Tab.empty;
+
+open Tab;
+
+end;
+
signature TERM_SUBST =
sig
+ structure TFrees: INST_TABLE
+ structure TVars: INST_TABLE
+ structure Frees: INST_TABLE
+ structure Vars: INST_TABLE
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
@@ -13,24 +36,18 @@
val generalize_same: Symtab.set * Symtab.set -> int -> term Same.operation
val generalizeT: Symtab.set -> int -> typ -> typ
val generalize: Symtab.set * Symtab.set -> int -> term -> term
- val instantiateT_maxidx: ((indexname * sort) * (typ * int)) list -> typ -> int -> typ * int
- val instantiate_maxidx:
- ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
+ val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int
+ val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
term -> int -> term * int
- val instantiateT_frees_same: ((string * sort) * typ) list -> typ Same.operation
- val instantiate_frees_same: ((string * sort) * typ) list * ((string * typ) * term) list ->
- term Same.operation
- val instantiateT_frees: ((string * sort) * typ) list -> typ -> typ
- val instantiate_frees: ((string * sort) * typ) list * ((string * typ) * term) list ->
- term -> term
- val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation
- val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
- term Same.operation
- val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
- val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
- term -> term
- val zero_var_indexes_inst: Name.context -> term list ->
- ((indexname * sort) * typ) list * ((indexname * typ) * term) list
+ val instantiateT_frees_same: typ TFrees.table -> typ Same.operation
+ val instantiate_frees_same: typ TFrees.table * term Frees.table -> term Same.operation
+ val instantiateT_frees: typ TFrees.table -> typ -> typ
+ val instantiate_frees: typ TFrees.table * term Frees.table -> term -> term
+ val instantiateT_same: typ TVars.table -> typ Same.operation
+ val instantiate_same: typ TVars.table * term Vars.table -> term Same.operation
+ val instantiateT: typ TVars.table -> typ -> typ
+ val instantiate: typ TVars.table * term Vars.table -> term -> term
+ val zero_var_indexes_inst: Name.context -> term list -> typ TVars.table * term Vars.table
val zero_var_indexes: term -> term
val zero_var_indexes_list: term list -> term list
end;
@@ -38,6 +55,29 @@
structure Term_Subst: TERM_SUBST =
struct
+(* instantiation as table *)
+
+structure TFrees = Inst_Table(
+ type key = string * sort
+ val ord = prod_ord fast_string_ord Term_Ord.sort_ord
+);
+
+structure TVars = Inst_Table(
+ type key = indexname * sort
+ val ord = prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord
+);
+
+structure Frees = Inst_Table(
+ type key = string * typ
+ val ord = prod_ord fast_string_ord Term_Ord.typ_ord
+);
+
+structure Vars = Inst_Table(
+ type key = indexname * typ
+ val ord = prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord
+);
+
+
(* generic mapping *)
fun map_atypsT_same f =
@@ -103,35 +143,37 @@
(* instantiation of free variables (types before terms) *)
-fun instantiateT_frees_same [] _ = raise Same.SAME
- | instantiateT_frees_same instT ty =
- let
- fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts)
- | subst (TFree v) =
- (case AList.lookup (op =) instT v of
- SOME T => T
- | NONE => raise Same.SAME)
- | subst _ = raise Same.SAME;
- in subst ty end;
+fun instantiateT_frees_same instT ty =
+ if TFrees.is_empty instT then raise Same.SAME
+ else
+ let
+ fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts)
+ | subst (TFree v) =
+ (case TFrees.lookup instT v of
+ SOME T => T
+ | NONE => raise Same.SAME)
+ | subst _ = raise Same.SAME;
+ in subst ty end;
-fun instantiate_frees_same ([], []) _ = raise Same.SAME
- | instantiate_frees_same (instT, inst) tm =
- let
- val substT = instantiateT_frees_same instT;
- fun subst (Const (c, T)) = Const (c, substT T)
- | subst (Free (x, T)) =
- let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
- (case AList.lookup (op =) inst (x, T') of
- SOME t => t
- | NONE => if same then raise Same.SAME else Free (x, T'))
- end
- | subst (Var (xi, T)) = Var (xi, substT T)
- | subst (Bound _) = raise Same.SAME
- | subst (Abs (x, T, t)) =
- (Abs (x, substT T, Same.commit subst t)
- handle Same.SAME => Abs (x, T, subst t))
- | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
- in subst tm end;
+fun instantiate_frees_same (instT, inst) tm =
+ if TFrees.is_empty instT andalso Frees.is_empty inst then raise Same.SAME
+ else
+ let
+ val substT = instantiateT_frees_same instT;
+ fun subst (Const (c, T)) = Const (c, substT T)
+ | subst (Free (x, T)) =
+ let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
+ (case Frees.lookup inst (x, T') of
+ SOME t => t
+ | NONE => if same then raise Same.SAME else Free (x, T'))
+ end
+ | subst (Var (xi, T)) = Var (xi, substT T)
+ | subst (Bound _) = raise Same.SAME
+ | subst (Abs (x, T, t)) =
+ (Abs (x, substT T, Same.commit subst t)
+ handle Same.SAME => Abs (x, T, subst t))
+ | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
+ in subst tm end;
fun instantiateT_frees instT ty = Same.commit (instantiateT_frees_same instT) ty;
fun instantiate_frees inst tm = Same.commit (instantiate_frees_same inst) tm;
@@ -141,9 +183,8 @@
local
-fun no_index (x, y) = (x, (y, ~1));
-fun no_indexes1 inst = map no_index inst;
-fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
+fun no_indexesT instT = TVars.map (fn _ => rpair ~1) instT;
+fun no_indexes inst = Vars.map (fn _ => rpair ~1) inst;
fun instT_same maxidx instT ty =
let
@@ -151,7 +192,7 @@
fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
| subst_typ (TVar ((a, i), S)) =
- (case AList.lookup Term.eq_tvar instT ((a, i), S) of
+ (case TVars.lookup instT ((a, i), S) of
SOME (T, j) => (maxify j; T)
| NONE => (maxify i; raise Same.SAME))
| subst_typ _ = raise Same.SAME
@@ -170,7 +211,7 @@
| subst (Free (x, T)) = Free (x, substT T)
| subst (Var ((x, i), T)) =
let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
- (case AList.lookup Term.eq_var inst ((x, i), T') of
+ (case Vars.lookup inst ((x, i), T') of
SOME (t, j) => (maxify j; t)
| NONE => (maxify i; if same then raise Same.SAME else Var ((x, i), T')))
end
@@ -191,11 +232,13 @@
let val maxidx = Unsynchronized.ref i
in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end;
-fun instantiateT_same [] _ = raise Same.SAME
- | instantiateT_same instT ty = instT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty;
+fun instantiateT_same instT ty =
+ if TVars.is_empty instT then raise Same.SAME
+ else instT_same (Unsynchronized.ref ~1) (no_indexesT instT) ty;
-fun instantiate_same ([], []) _ = raise Same.SAME
- | instantiate_same insts tm = inst_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm;
+fun instantiate_same (instT, inst) tm =
+ if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME
+ else inst_same (Unsynchronized.ref ~1) (no_indexesT instT, no_indexes inst) tm;
fun instantiateT instT ty = Same.commit (instantiateT_same instT) ty;
fun instantiate inst tm = Same.commit (instantiate_same inst) tm;
@@ -205,26 +248,20 @@
(* zero var indexes *)
-structure TVars = Table(type key = indexname * sort val ord = Term_Ord.tvar_ord);
-structure Vars = Table(type key = indexname * typ val ord = Term_Ord.var_ord);
-
-fun zero_var_inst 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 ((v, mk ((x', 0), X)) :: inst, used') end;
+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;
fun zero_var_indexes_inst used ts =
let
val (instT, _) =
- TVars.fold (zero_var_inst TVar o #1)
+ (TVars.empty, used) |> TVars.fold (zero_var_inst TVars.add TVar o #1)
((fold o fold_types o fold_atyps) (fn TVar v =>
- TVars.insert (K true) (v, ()) | _ => I) ts TVars.empty)
- ([], used);
+ TVars.add (v, ()) | _ => I) ts TVars.empty);
val (inst, _) =
- Vars.fold (zero_var_inst Var o #1)
+ (Vars.empty, used) |> Vars.fold (zero_var_inst Vars.add Var o #1)
((fold o fold_aterms) (fn Var (xi, T) =>
- Vars.insert (K true) ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty)
- ([], used);
+ Vars.add ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty);
in (instT, inst) end;
fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst Name.context ts)) ts;
--- a/src/Pure/thm.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/thm.ML Fri Sep 03 18:57:33 2021 +0200
@@ -1611,12 +1611,12 @@
val add_instT_sorts = add_sorts (fn Ctyp {sorts, ...} => sorts);
val add_inst_sorts = add_sorts (fn Cterm {sorts, ...} => sorts);
-fun make_instT thy (v as (_, S), Ctyp {T = U, maxidx, ...}) =
- if Sign.of_sort thy (U, S) then (v, (U, maxidx))
+fun add_instT thy (v as (_, S), Ctyp {T = U, maxidx, ...}) =
+ if Sign.of_sort thy (U, S) then Term_Subst.TVars.add (v, (U, maxidx))
else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy S, [U], []);
-fun make_inst thy (v as (_, T), Cterm {t = u, T = U, maxidx, ...}) =
- if T = U then (v, (u, maxidx))
+fun add_inst thy (v as (_, T), Cterm {t = u, T = U, maxidx, ...}) =
+ if T = U then Term_Subst.Vars.add (v, (u, maxidx))
else
let
fun pretty_typing t ty =
@@ -1641,8 +1641,8 @@
|> fold add_instT_sorts instT
|> fold add_inst_sorts inst;
- val instT' = map (make_instT thy') instT;
- val inst' = map (make_inst thy') inst;
+ val instT' = fold (add_instT thy') instT Term_Subst.TVars.empty;
+ val inst' = fold (add_inst thy') inst Term_Subst.Vars.empty;
in ((instT', inst'), (cert', sorts')) end;
in
@@ -1665,10 +1665,13 @@
val thy' = Context.certificate_theory cert';
val constraints' =
- fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) instT' constraints;
+ Term_Subst.TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
+ instT' constraints;
in
Thm (deriv_rule1
- (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
+ (fn d =>
+ Proofterm.instantiate
+ (Term_Subst.TVars.map (K #1) instT', Term_Subst.Vars.map (K #1) inst') d) der,
{cert = cert',
tags = [],
maxidx = maxidx',
--- a/src/Pure/type_infer.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/type_infer.ML Fri Sep 03 18:57:33 2021 +0200
@@ -114,10 +114,10 @@
let
val [a] = Name.invent used Name.aT 1;
val used' = Name.declare a used;
- in (((xi, S), TFree (a, improve_sort S)) :: inst, used') end
+ in (Term_Subst.TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
else (inst, used);
val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
- val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
+ val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) (Term_Subst.TVars.empty, used);
in (map o map_types) (Term_Subst.instantiateT inst) ts end;
end;
--- a/src/Pure/variable.ML Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/variable.ML Fri Sep 03 18:57:33 2021 +0200
@@ -69,9 +69,9 @@
val export: Proof.context -> Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
- val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context
+ val importT_inst: term list -> Proof.context -> typ Term_Subst.TVars.table * Proof.context
val import_inst: bool -> term list -> Proof.context ->
- (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
+ (typ Term_Subst.TVars.table * term Term_Subst.Vars.table) * Proof.context
val importT_terms: term list -> Proof.context -> term list * Proof.context
val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
val importT: thm list -> Proof.context ->
@@ -593,20 +593,25 @@
let
val tvars = rev (fold Term.add_tvars ts []);
val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
- in (tvars ~~ map TFree tfrees, ctxt') end;
+ val instT =
+ fold2 (fn a => fn b => Term_Subst.TVars.add (a, TFree b))
+ tvars tfrees Term_Subst.TVars.empty;
+ in (instT, ctxt') end;
fun import_inst is_open ts ctxt =
let
val ren = Name.clean #> (if is_open then I else Name.internal);
val (instT, ctxt') = importT_inst ts ctxt;
val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts []));
- val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
- val inst = vars ~~ map Free (xs ~~ map #2 vars);
+ val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
+ val inst =
+ fold2 (fn (x, T) => fn y => Term_Subst.Vars.add ((x, T), Free (y, T)))
+ vars ys Term_Subst.Vars.empty;
in ((instT, inst), ctxt'') end;
fun importT_terms ts ctxt =
let val (instT, ctxt') = importT_inst ts ctxt
- in (map (Term_Subst.instantiate (instT, [])) ts, ctxt') end;
+ in (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty)) ts, ctxt') end;
fun import_terms is_open ts ctxt =
let val (inst, ctxt') = import_inst is_open ts ctxt
@@ -615,7 +620,7 @@
fun importT ths ctxt =
let
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
- val instT' = map (apsnd (Thm.ctyp_of ctxt')) instT;
+ val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
val ths' = map (Thm.instantiate (instT', [])) ths;
in ((instT', ths'), ctxt') end;
@@ -628,11 +633,10 @@
fun import is_open ths ctxt =
let
val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
- val insts' =
- (map (apsnd (Thm.ctyp_of ctxt')) instT,
- map (apsnd (Thm.cterm_of ctxt')) inst);
- val ths' = map (Thm.instantiate insts') ths;
- in ((insts', ths'), ctxt') end;
+ val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
+ val inst' = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt' t)) inst [];
+ val ths' = map (Thm.instantiate (instT', inst')) ths;
+ in (((instT', inst'), ths'), ctxt') end;
fun import_vars ctxt th =
let val ((_, [th']), _) = ctxt |> set_body false |> import true [th];