tuned/modernized subst: Same.operation;
authorwenzelm
Fri Jul 17 22:54:11 2009 +0200 (2009-07-17)
changeset 3203470c0bcd0adfb
parent 32033 f92df23c3305
child 32035 8e77b6a250d5
tuned/modernized subst: Same.operation;
renamed typ_subst_TVars to subst_type;
renamed subst_TVars to subst_term_types;
renamed subst_vars to subst_term;
removed unused subst_Vars (covered by subst_term);
src/Pure/envir.ML
     1.1 --- a/src/Pure/envir.ML	Fri Jul 17 22:51:18 2009 +0200
     1.2 +++ b/src/Pure/envir.ML	Fri Jul 17 22:54:11 2009 +0200
     1.3 @@ -34,10 +34,12 @@
     1.4    val eta_contract: term -> term
     1.5    val beta_eta_contract: term -> term
     1.6    val fastype: env -> typ list -> term -> typ
     1.7 -  val typ_subst_TVars: Type.tyenv -> typ -> typ
     1.8 -  val subst_TVars: Type.tyenv -> term -> term
     1.9 -  val subst_Vars: tenv -> term -> term
    1.10 -  val subst_vars: Type.tyenv * tenv -> term -> term
    1.11 +  val subst_type_same: Type.tyenv -> typ Same.operation
    1.12 +  val subst_term_types_same: Type.tyenv -> term Same.operation
    1.13 +  val subst_term_same: Type.tyenv * tenv -> term Same.operation
    1.14 +  val subst_type: Type.tyenv -> typ -> typ
    1.15 +  val subst_term_types: Type.tyenv -> term -> term
    1.16 +  val subst_term: Type.tyenv * tenv -> term -> term
    1.17    val expand_atom: typ -> typ * term -> term
    1.18    val expand_term: (term -> (typ * term) option) -> term -> term
    1.19    val expand_term_frees: ((string * typ) * term) list -> term -> term
    1.20 @@ -296,51 +298,68 @@
    1.21    in fast end;
    1.22  
    1.23  
    1.24 -(*Substitute for type Vars in a type*)
    1.25 -fun typ_subst_TVars tyenv T =
    1.26 -  if Vartab.is_empty tyenv then T
    1.27 -  else
    1.28 -    let
    1.29 -      fun subst (Type (a, Ts)) = Type (a, map subst Ts)
    1.30 -        | subst (T as TFree _) = T
    1.31 -        | subst (T as TVar v) = (case Type.lookup tyenv v of NONE => T | SOME U => U);
    1.32 -    in subst T end;
    1.33 +
    1.34 +(** plain substitution -- without variable chasing **)
    1.35 +
    1.36 +local
    1.37  
    1.38 -(*Substitute for type Vars in a term*)
    1.39 -val subst_TVars = map_types o typ_subst_TVars;
    1.40 +fun subst_type0 tyenv = Term_Subst.map_atypsT_same
    1.41 +  (fn TVar v =>
    1.42 +        (case Type.lookup tyenv v of
    1.43 +          SOME U => U
    1.44 +        | NONE => raise Same.SAME)
    1.45 +    | _ => raise Same.SAME);
    1.46 +
    1.47 +fun subst_term1 tenv = Term_Subst.map_aterms_same
    1.48 +  (fn Var v =>
    1.49 +        (case lookup' (tenv, v) of
    1.50 +          SOME u => u
    1.51 +        | NONE => raise Same.SAME)
    1.52 +    | _ => raise Same.SAME);
    1.53  
    1.54 -(*Substitute for Vars in a term *)
    1.55 -fun subst_Vars tenv tm =
    1.56 -  if Vartab.is_empty tenv then tm
    1.57 -  else
    1.58 -    let
    1.59 -      fun subst (t as Var v) = the_default t (lookup' (tenv, v))
    1.60 -        | subst (Abs (a, T, t)) = Abs (a, T, subst t)
    1.61 -        | subst (t $ u) = subst t $ subst u
    1.62 -        | subst t = t;
    1.63 -    in subst tm end;
    1.64 +fun subst_term2 tenv tyenv : term Same.operation =
    1.65 +  let
    1.66 +    val substT = subst_type0 tyenv;
    1.67 +    fun subst (Const (a, T)) = Const (a, substT T)
    1.68 +      | subst (Free (a, T)) = Free (a, substT T)
    1.69 +      | subst (Var (xi, T)) =
    1.70 +          (case lookup' (tenv, (xi, T)) of
    1.71 +            SOME u => u
    1.72 +          | NONE => Var (xi, substT T))
    1.73 +      | subst (Bound _) = raise Same.SAME
    1.74 +      | subst (Abs (a, T, t)) =
    1.75 +          (Abs (a, substT T, Same.commit subst t)
    1.76 +            handle Same.SAME => Abs (a, T, subst t))
    1.77 +      | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
    1.78 +  in subst end;
    1.79 +
    1.80 +in
    1.81  
    1.82 -(*Substitute for type/term Vars in a term *)
    1.83 -fun subst_vars (tyenv, tenv) =
    1.84 -  if Vartab.is_empty tyenv then subst_Vars tenv
    1.85 -  else
    1.86 -    let
    1.87 -      fun subst (Const (a, T)) = Const (a, typ_subst_TVars tyenv T)
    1.88 -        | subst (Free (a, T)) = Free (a, typ_subst_TVars tyenv T)
    1.89 -        | subst (Var (xi, T)) =
    1.90 -            (case lookup' (tenv, (xi, T)) of
    1.91 -              NONE => Var (xi, typ_subst_TVars tyenv T)
    1.92 -            | SOME t => t)
    1.93 -        | subst (t as Bound _) = t
    1.94 -        | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars tyenv T, subst t)
    1.95 -        | subst (t $ u) = subst t $ subst u;
    1.96 -    in subst end;
    1.97 +fun subst_type_same tyenv T =
    1.98 +  if Vartab.is_empty tyenv then raise Same.SAME
    1.99 +  else subst_type0 tyenv T;
   1.100 +
   1.101 +fun subst_term_types_same tyenv t =
   1.102 +  if Vartab.is_empty tyenv then raise Same.SAME
   1.103 +  else Term_Subst.map_types_same (subst_type0 tyenv) t;
   1.104 +
   1.105 +fun subst_term_same (tyenv, tenv) =
   1.106 +  if Vartab.is_empty tenv then subst_term_types_same tyenv
   1.107 +  else if Vartab.is_empty tyenv then subst_term1 tenv
   1.108 +  else subst_term2 tenv tyenv;
   1.109 +
   1.110 +fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
   1.111 +fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
   1.112 +fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
   1.113 +
   1.114 +end;
   1.115  
   1.116  
   1.117 -(* expand defined atoms -- with local beta reduction *)
   1.118 +
   1.119 +(** expand defined atoms -- with local beta reduction **)
   1.120  
   1.121  fun expand_atom T (U, u) =
   1.122 -  subst_TVars (Type.raw_match (U, T) Vartab.empty) u
   1.123 +  subst_term_types (Type.raw_match (U, T) Vartab.empty) u
   1.124      handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
   1.125  
   1.126  fun expand_term get =