# HG changeset patch # User wenzelm # Date 1635176244 -7200 # Node ID d4829a7333e221812d2f4ee3fbd0399307a43f85 # Parent 0b43d42cfde7ed82223062278cc22c9ee7a59628 clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs; diff -r 0b43d42cfde7 -r d4829a7333e2 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Mon Oct 25 17:26:27 2021 +0200 +++ b/src/Pure/ML/ml_antiquotations.ML Mon Oct 25 17:37:24 2021 +0200 @@ -243,14 +243,14 @@ val instT = TVars.make (#1 insts); val instantiateT = Term_Subst.instantiateT instT; val inst = Vars.make ((map o apfst o apsnd) instantiateT (#2 insts)); - in Term_Subst.instantiate (instT, inst) end; + in Term_Subst.instantiate_beta (instT, inst) end; fun instantiate_cterm (cinsts: cinsts) = let val cinstT = TVars.make (#1 cinsts); val instantiateT = Term_Subst.instantiateT (TVars.map (K Thm.typ_of) cinstT); val cinst = Vars.make ((map o apfst o apsnd) instantiateT (#2 cinsts)); - in Thm.instantiate_cterm (cinstT, cinst) end; + in Thm.instantiate_beta_cterm (cinstT, cinst) end; local diff -r 0b43d42cfde7 -r d4829a7333e2 src/Pure/term.ML --- a/src/Pure/term.ML Mon Oct 25 17:26:27 2021 +0200 +++ b/src/Pure/term.ML Mon Oct 25 17:37:24 2021 +0200 @@ -124,6 +124,7 @@ val a_itselfT: typ val argument_type_of: term -> int -> typ val abs: string * typ -> term -> term + val args_of: term -> term list val add_tvar_namesT: typ -> indexname list -> indexname list val add_tvar_names: term -> indexname list -> indexname list val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list @@ -423,6 +424,10 @@ | stripc x = x in stripc(u,[]) end; +fun args_of u = + let fun args (f $ x) xs = args f (x :: xs) + | args _ xs = xs + in args u [] end; (*maps f(t1,...,tn) to f , which is never a combination*) fun head_of (f$t) = head_of f diff -r 0b43d42cfde7 -r d4829a7333e2 src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Mon Oct 25 17:26:27 2021 +0200 +++ b/src/Pure/term_subst.ML Mon Oct 25 17:37:24 2021 +0200 @@ -20,10 +20,14 @@ 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 instantiate_beta_maxidx: (typ * int) TVars.table * (term * int) Vars.table -> + term -> int -> term * int val instantiateT_same: typ TVars.table -> typ Same.operation val instantiate_same: typ TVars.table * term Vars.table -> term Same.operation + val instantiate_beta_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 instantiate_beta: 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 @@ -171,9 +175,50 @@ end | subst (Bound _) = raise Same.SAME | subst (Abs (x, T, t)) = - (Abs (x, substT T, Same.commit subst t) + (Abs (x, substT T, subst_commit t) handle Same.SAME => Abs (x, T, subst t)) - | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u); + | subst (t $ u) = (subst t $ subst_commit u handle Same.SAME => t $ subst u) + and subst_commit t = Same.commit subst t; + in subst tm end; + +(*version with local beta reduction*) +fun inst_beta_same maxidx (instT, inst) tm = + let + fun maxify i = if i > ! maxidx then maxidx := i else (); + + val substT = instT_same maxidx instT; + + fun expand_head t = + (case Term.head_of t of + Var ((x, i), T) => + let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in + (case Vars.lookup inst ((x, i), T') of + SOME (u, j) => (maxify j; SOME u) + | NONE => (maxify i; if same then NONE else SOME (Var ((x, i), T')))) + end + | _ => NONE); + + fun subst t = + (case expand_head t of + NONE => + (case t of + Const (c, T) => Const (c, substT T) + | Free (x, T) => Free (x, substT T) + | Var _ => raise Same.SAME + | Bound _ => raise Same.SAME + | Abs (x, T, b) => + (Abs (x, substT T, subst_commit b) + handle Same.SAME => Abs (x, T, subst b)) + | _ $ _ => subst_comb t) + | SOME (u as Abs _) => Term.betapplys (u, map subst_commit (Term.args_of t)) + | SOME u => subst_head u t) + and subst_comb (t $ u) = (subst_comb t $ subst_commit u handle Same.SAME => t $ subst u) + | subst_comb (Var _) = raise Same.SAME + | subst_comb t = subst t + and subst_head h (t $ u) = subst_head h t $ subst_commit u + | subst_head h _ = h + and subst_commit t = Same.commit subst t; + in subst tm end; in @@ -186,6 +231,11 @@ let val maxidx = Unsynchronized.ref i in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end; +fun instantiate_beta_maxidx insts tm i = + let val maxidx = Unsynchronized.ref i + in (Same.commit (inst_beta_same maxidx insts) tm, ! maxidx) end; + + fun instantiateT_same instT ty = if TVars.is_empty instT then raise Same.SAME else instT_same (Unsynchronized.ref ~1) (no_indexesT instT) ty; @@ -194,9 +244,17 @@ 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 instantiate_beta_same (instT, inst) tm = + if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME + else inst_beta_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; +fun instantiate_beta inst tm = Same.commit (instantiate_beta_same inst) tm; + end; diff -r 0b43d42cfde7 -r d4829a7333e2 src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Oct 25 17:26:27 2021 +0200 +++ b/src/Pure/thm.ML Mon Oct 25 17:37:24 2021 +0200 @@ -157,7 +157,9 @@ val generalize_cterm: Names.set * Names.set -> int -> cterm -> cterm val generalize_ctyp: Names.set -> int -> ctyp -> ctyp val instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm + val instantiate_beta: ctyp TVars.table * cterm Vars.table -> thm -> thm val instantiate_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm + val instantiate_beta_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm val trivial: cterm -> thm val of_class: ctyp * class -> thm val unconstrainT: thm -> thm @@ -1675,7 +1677,7 @@ (*Left-to-right replacements: ctpairs = [..., (vi, ti), ...]. Instantiates distinct Vars by terms of same type. Does NOT normalize the resulting theorem!*) -fun instantiate (instT, inst) th = +fun gen_instantiate inst_fn (instT, inst) th = if TVars.is_empty instT andalso Vars.is_empty inst then th else let @@ -1684,7 +1686,7 @@ handle CONTEXT (msg, cTs, cts, ths, context) => raise CONTEXT (msg, cTs, cts, th :: ths, context); - val subst = Term_Subst.instantiate_maxidx (instT', inst'); + val subst = inst_fn (instT', inst'); val (prop', maxidx1) = subst prop ~1; val (tpairs', maxidx') = fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1; @@ -1708,19 +1710,25 @@ end handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); -fun instantiate_cterm (instT, inst) ct = +val instantiate = gen_instantiate Term_Subst.instantiate_maxidx; +val instantiate_beta = gen_instantiate Term_Subst.instantiate_beta_maxidx; + +fun gen_instantiate_cterm inst_fn (instT, inst) ct = if TVars.is_empty instT andalso Vars.is_empty inst then ct else let val Cterm {cert, t, T, sorts, ...} = ct; val ((instT', inst'), (cert', sorts')) = prep_insts (instT, inst) (cert, sorts); - val subst = Term_Subst.instantiate_maxidx (instT', inst'); + val subst = inst_fn (instT', inst'); val substT = Term_Subst.instantiateT_maxidx instT'; val (t', maxidx1) = subst t ~1; val (T', maxidx') = substT T maxidx1; in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); +val instantiate_cterm = gen_instantiate_cterm Term_Subst.instantiate_maxidx; +val instantiate_beta_cterm = gen_instantiate_cterm Term_Subst.instantiate_beta_maxidx; + end;