tuned/modernized Envir.subst_XXX;
authorwenzelm
Fri Jul 17 23:11:40 2009 +0200 (2009-07-17)
changeset 320358e77b6a250d5
parent 32034 70c0bcd0adfb
child 32046 3b12e03e4178
tuned/modernized Envir.subst_XXX;
src/HOL/Library/reflection.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Function/context_tree.ML
src/HOL/Tools/Function/fundef_datatype.ML
src/HOL/Tools/Function/pattern_split.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/thry.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOLCF/Tools/adm_tac.ML
src/Pure/Isar/overloading.ML
src/Pure/Proof/extraction.ML
src/Pure/defs.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
src/Tools/Compute_Oracle/linker.ML
src/Tools/coherent.ML
     1.1 --- a/src/HOL/Library/reflection.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -205,8 +205,8 @@
     1.4              val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
     1.5              val rhs_P = subst_free subst rhs
     1.6              val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty)
     1.7 -            val sbst = Envir.subst_vars (tyenv, tmenv)
     1.8 -            val sbsT = Envir.typ_subst_TVars tyenv
     1.9 +            val sbst = Envir.subst_term (tyenv, tmenv)
    1.10 +            val sbsT = Envir.subst_type tyenv
    1.11              val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
    1.12                                 (Vartab.dest tyenv)
    1.13              val tml = Vartab.dest tmenv
     2.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 17 22:54:11 2009 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 17 23:11:40 2009 +0200
     2.3 @@ -342,7 +342,7 @@
     2.4                   val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
     2.5                     (Vartab.empty, Vartab.empty);
     2.6                   val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
     2.7 -                   (map (Envir.subst_vars env) vs ~~
     2.8 +                   (map (Envir.subst_term env) vs ~~
     2.9                      map (fold_rev (NominalDatatype.mk_perm [])
    2.10                        (rev pis' @ pis)) params' @ [z])) ihyp;
    2.11                   fun mk_pi th =
     3.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 17 22:54:11 2009 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 17 23:11:40 2009 +0200
     3.3 @@ -147,7 +147,7 @@
     3.4    let val env = Pattern.first_order_match thy (p, prop_of th)
     3.5      (Vartab.empty, Vartab.empty)
     3.6    in Thm.instantiate ([],
     3.7 -    map (Envir.subst_vars env #> cterm_of thy) vs ~~ cts) th
     3.8 +    map (Envir.subst_term env #> cterm_of thy) vs ~~ cts) th
     3.9    end;
    3.10  
    3.11  fun prove_strong_ind s avoids ctxt =
     4.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Fri Jul 17 22:54:11 2009 +0200
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Fri Jul 17 23:11:40 2009 +0200
     4.3 @@ -293,7 +293,7 @@
     4.4    end;
     4.5  
     4.6  fun make_case tab ctxt = gen_make_case
     4.7 -  (match_type (ProofContext.theory_of ctxt)) Envir.subst_TVars fastype_of tab ctxt;
     4.8 +  (match_type (ProofContext.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt;
     4.9  val make_case_untyped = gen_make_case (K (K Vartab.empty))
    4.10    (K (Term.map_types (K dummyT))) (K dummyT);
    4.11  
     5.1 --- a/src/HOL/Tools/Function/context_tree.ML	Fri Jul 17 22:54:11 2009 +0200
     5.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Fri Jul 17 23:11:40 2009 +0200
     5.3 @@ -116,8 +116,9 @@
     5.4         val (c, subs) = (concl_of r, prems_of r)
     5.5  
     5.6         val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
     5.7 -       val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
     5.8 -       val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
     5.9 +       val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs
    5.10 +       val inst = map (fn v =>
    5.11 +        (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c [])
    5.12       in
    5.13     (cterm_instantiate inst r, dep, branches)
    5.14       end
     6.1 --- a/src/HOL/Tools/Function/fundef_datatype.ML	Fri Jul 17 22:54:11 2009 +0200
     6.2 +++ b/src/HOL/Tools/Function/fundef_datatype.ML	Fri Jul 17 23:11:40 2009 +0200
     6.3 @@ -102,7 +102,8 @@
     6.4  
     6.5  
     6.6  fun inst_constrs_of thy (T as Type (name, _)) =
     6.7 -        map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
     6.8 +        map (fn (Cn,CT) =>
     6.9 +              Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    6.10              (the (Datatype.get_constrs thy name))
    6.11    | inst_constrs_of thy _ = raise Match
    6.12  
     7.1 --- a/src/HOL/Tools/Function/pattern_split.ML	Fri Jul 17 22:54:11 2009 +0200
     7.2 +++ b/src/HOL/Tools/Function/pattern_split.ML	Fri Jul 17 23:11:40 2009 +0200
     7.3 @@ -39,7 +39,8 @@
     7.4           
     7.5  (* This is copied from "fundef_datatype.ML" *)
     7.6  fun inst_constrs_of thy (T as Type (name, _)) =
     7.7 -    map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
     7.8 +    map (fn (Cn,CT) =>
     7.9 +          Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    7.10          (the (Datatype.get_constrs thy name))
    7.11    | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
    7.12                              
     8.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Fri Jul 17 22:54:11 2009 +0200
     8.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Fri Jul 17 23:11:40 2009 +0200
     8.3 @@ -129,8 +129,8 @@
     8.4            | _ => error "not a valid case thm";
     8.5        val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
     8.6          (Vartab.dest type_insts);
     8.7 -      val cPv = ctermify (Envir.subst_TVars type_insts Pv);
     8.8 -      val cDv = ctermify (Envir.subst_TVars type_insts Dv);
     8.9 +      val cPv = ctermify (Envir.subst_term_types type_insts Pv);
    8.10 +      val cDv = ctermify (Envir.subst_term_types type_insts Dv);
    8.11      in
    8.12        (beta_eta_contract
    8.13           (case_thm
     9.1 --- a/src/HOL/Tools/TFL/thry.ML	Fri Jul 17 22:54:11 2009 +0200
     9.2 +++ b/src/HOL/Tools/TFL/thry.ML	Fri Jul 17 23:11:40 2009 +0200
     9.3 @@ -35,7 +35,7 @@
     9.4  fun match_term thry pat ob =
     9.5    let
     9.6      val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
     9.7 -    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
     9.8 +    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t)
     9.9    in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
    9.10    end;
    9.11  
    10.1 --- a/src/HOL/Tools/inductive.ML	Fri Jul 17 22:54:11 2009 +0200
    10.2 +++ b/src/HOL/Tools/inductive.ML	Fri Jul 17 23:11:40 2009 +0200
    10.3 @@ -922,7 +922,7 @@
    10.4          val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
    10.5            (Vartab.empty, Vartab.empty);
    10.6        in
    10.7 -        map (Envir.subst_vars tab) vars
    10.8 +        map (Envir.subst_term tab) vars
    10.9        end
   10.10    in
   10.11      map (mtch o apsnd prop_of) (cases ~~ intros)
    11.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Jul 17 22:54:11 2009 +0200
    11.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Jul 17 23:11:40 2009 +0200
    11.3 @@ -324,7 +324,7 @@
    11.4  fun to_pred_proc thy rules t = case lookup_rule thy I rules t of
    11.5      NONE => NONE
    11.6    | SOME (lhs, rhs) =>
    11.7 -      SOME (Envir.subst_vars
    11.8 +      SOME (Envir.subst_term
    11.9          (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rhs);
   11.10  
   11.11  fun to_pred thms ctxt thm =
    12.1 --- a/src/HOLCF/Tools/adm_tac.ML	Fri Jul 17 22:54:11 2009 +0200
    12.2 +++ b/src/HOLCF/Tools/adm_tac.ML	Fri Jul 17 23:11:40 2009 +0200
    12.3 @@ -117,8 +117,8 @@
    12.4      val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye;
    12.5      val ctye = map (fn (ixn, (S, T)) =>
    12.6        (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye');
    12.7 -    val tv = cterm_of thy (Var (("t", j), Envir.typ_subst_TVars tye' tT));
    12.8 -    val Pv = cterm_of thy (Var (("P", j), Envir.typ_subst_TVars tye' PT));
    12.9 +    val tv = cterm_of thy (Var (("t", j), Envir.subst_type tye' tT));
   12.10 +    val Pv = cterm_of thy (Var (("P", j), Envir.subst_type tye' PT));
   12.11      val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
   12.12    in rule' end;
   12.13  
    13.1 --- a/src/Pure/Isar/overloading.ML	Fri Jul 17 22:54:11 2009 +0200
    13.2 +++ b/src/Pure/Isar/overloading.ML	Fri Jul 17 23:11:40 2009 +0200
    13.3 @@ -76,7 +76,7 @@
    13.4            | _ => I)
    13.5        | accumulate_improvements _ = I;
    13.6      val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
    13.7 -    val ts' = (map o map_types) (Envir.typ_subst_TVars improvements) ts;
    13.8 +    val ts' = (map o map_types) (Envir.subst_type improvements) ts;
    13.9      fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty)
   13.10           of SOME (ty', t') =>
   13.11                if Type.typ_instance tsig (ty, ty')
    14.1 --- a/src/Pure/Proof/extraction.ML	Fri Jul 17 22:54:11 2009 +0200
    14.2 +++ b/src/Pure/Proof/extraction.ML	Fri Jul 17 23:11:40 2009 +0200
    14.3 @@ -103,7 +103,7 @@
    14.4            fun ren t = the_default t (Term.rename_abs tm1 tm t);
    14.5            val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
    14.6            val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
    14.7 -          val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
    14.8 +          val prems' = map (pairself (Envir.subst_term env o inc o ren)) prems;
    14.9            val env' = Envir.Envir
   14.10              {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
   14.11               tenv = tenv, tyenv = Tenv};
    15.1 --- a/src/Pure/defs.ML	Fri Jul 17 22:54:11 2009 +0200
    15.2 +++ b/src/Pure/defs.ML	Fri Jul 17 23:11:40 2009 +0200
    15.3 @@ -46,7 +46,7 @@
    15.4        handle Type.TUNIFY => true);
    15.5  
    15.6  fun match_args (Ts, Us) =
    15.7 -  Option.map Envir.typ_subst_TVars
    15.8 +  Option.map Envir.subst_type
    15.9      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
   15.10  
   15.11  
    16.1 --- a/src/Pure/pattern.ML	Fri Jul 17 22:54:11 2009 +0200
    16.2 +++ b/src/Pure/pattern.ML	Fri Jul 17 23:11:40 2009 +0200
    16.3 @@ -354,7 +354,7 @@
    16.4        Abs(ns,Ts,ts) =>
    16.5          (case obj of
    16.6             Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env
    16.7 -         | _ => let val Tt = Envir.typ_subst_TVars iTs Ts
    16.8 +         | _ => let val Tt = Envir.subst_type iTs Ts
    16.9                  in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end)
   16.10      | _ => (case obj of
   16.11                Abs(nt,Tt,tt) =>
   16.12 @@ -428,7 +428,7 @@
   16.13  
   16.14  fun match_rew thy tm (tm1, tm2) =
   16.15    let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
   16.16 -    SOME (Envir.subst_vars (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
   16.17 +    SOME (Envir.subst_term (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
   16.18        handle MATCH => NONE
   16.19    end;
   16.20  
    17.1 --- a/src/Pure/proofterm.ML	Fri Jul 17 22:54:11 2009 +0200
    17.2 +++ b/src/Pure/proofterm.ML	Fri Jul 17 23:11:40 2009 +0200
    17.3 @@ -1087,7 +1087,7 @@
    17.4  
    17.5  fun prf_subst (pinst, (tyinsts, insts)) =
    17.6    let
    17.7 -    val substT = Envir.typ_subst_TVars tyinsts;
    17.8 +    val substT = Envir.subst_type tyinsts;
    17.9  
   17.10      fun subst' lev (t as Var (ixn, _)) = (case AList.lookup (op =) insts ixn of
   17.11            NONE => t
    18.1 --- a/src/Pure/thm.ML	Fri Jul 17 22:54:11 2009 +0200
    18.2 +++ b/src/Pure/thm.ML	Fri Jul 17 23:11:40 2009 +0200
    18.3 @@ -317,7 +317,7 @@
    18.4        (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts},
    18.5         Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts});
    18.6      fun mk_ctinst ((x, i), (T, t)) =
    18.7 -      let val T = Envir.typ_subst_TVars Tinsts T in
    18.8 +      let val T = Envir.subst_type Tinsts T in
    18.9          (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy,
   18.10            maxidx = i, sorts = sorts},
   18.11           Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts})
   18.12 @@ -1467,7 +1467,7 @@
   18.13  fun norm_term_skip env 0 t = Envir.norm_term env t
   18.14    | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
   18.15        let
   18.16 -        val T' = Envir.typ_subst_TVars (Envir.type_env env) T
   18.17 +        val T' = Envir.subst_type (Envir.type_env env) T
   18.18          (*Must instantiate types of parameters because they are flattened;
   18.19            this could be a NEW parameter*)
   18.20        in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
    19.1 --- a/src/Tools/Compute_Oracle/linker.ML	Fri Jul 17 22:54:11 2009 +0200
    19.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Fri Jul 17 23:11:40 2009 +0200
    19.3 @@ -341,7 +341,7 @@
    19.4  	    let
    19.5  		val (newsubsts, instances) = Linker.add_instances thy instances monocs
    19.6  		val _ = if not (null newsubsts) then changed := true else ()
    19.7 -		val newpats = map (fn subst => Envir.subst_TVars subst p) newsubsts
    19.8 +		val newpats = map (fn subst => Envir.subst_term_types subst p) newsubsts
    19.9  	    in
   19.10  		PolyPattern (p, instances, instancepats@newpats)
   19.11  	    end 
    20.1 --- a/src/Tools/coherent.ML	Fri Jul 17 22:54:11 2009 +0200
    20.2 +++ b/src/Tools/coherent.ML	Fri Jul 17 23:11:40 2009 +0200
    20.3 @@ -131,7 +131,7 @@
    20.4    let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
    20.5      valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
    20.6        let val cs' = map (fn (Ts, ts) =>
    20.7 -        (map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs
    20.8 +        (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
    20.9        in
   20.10          inst_extra_vars ctxt dom cs' |>
   20.11            Seq.map_filter (fn (inst, cs'') =>
   20.12 @@ -184,7 +184,7 @@
   20.13              (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
   20.14                 (Vartab.dest tye),
   20.15            map (fn (ixn, (T, t)) =>
   20.16 -            (Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)),
   20.17 +            (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
   20.18               Thm.cterm_of thy t)) (Vartab.dest env) @
   20.19            map (fn (ixnT, t) =>
   20.20              (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)