src/Pure/envir.ML
changeset 16652 4ecf94235ec7
parent 15797 a63605582573
child 17224 a78339014063
     1.1 --- a/src/Pure/envir.ML	Fri Jul 01 14:20:01 2005 +0200
     1.2 +++ b/src/Pure/envir.ML	Fri Jul 01 14:22:33 2005 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val genvars: string -> env * typ list -> env * term list
     1.5    val genvar: string -> env * typ -> env * term
     1.6    val lookup: env * (indexname * typ) -> term option
     1.7 -  val lookup': (Type.tyenv * tenv) * (indexname * typ) -> term option
     1.8 +  val lookup': tenv * (indexname * typ) -> term option
     1.9    val update: ((indexname * typ) * term) * env -> env
    1.10    val empty: int -> env
    1.11    val is_empty: env -> bool
    1.12 @@ -68,20 +68,6 @@
    1.13    let val (env',[v]) = genvars name (env,[T])
    1.14    in  (env',v)  end;
    1.15  
    1.16 -(* de-reference TVars. When dealing with environments produced by *)
    1.17 -(* matching instead of unification, there is no need to chase     *)
    1.18 -(* assigned TVars. In this case, set b to false.                  *)
    1.19 -fun devar b iTs (T as TVar vT) = (case Type.lookup (iTs, vT) of
    1.20 -      NONE => T
    1.21 -    | SOME T' => if b then devar true iTs T' else T')
    1.22 -  | devar b iTs T = T;
    1.23 -
    1.24 -fun eq_type b iTs (T, T') =
    1.25 -  (case (devar b iTs T, devar b iTs T') of
    1.26 -     (Type (s, Ts), Type (s', Ts')) =>
    1.27 -       s = s' andalso ListPair.all (eq_type b iTs) (Ts, Ts')
    1.28 -   | (U, U') => U = U');
    1.29 -
    1.30  fun var_clash ixn T T' = raise TYPE ("Variable " ^
    1.31    quote (Syntax.string_of_vname ixn) ^ " has two distinct types",
    1.32    [T', T], []);
    1.33 @@ -92,20 +78,19 @@
    1.34     | SOME (U, t) => if f (T, U) then SOME t
    1.35         else var_clash xname T U);
    1.36  
    1.37 -(* version ignoring type substitutions *)
    1.38 -fun lookup1 asol = gen_lookup op = asol;
    1.39 +(* When dealing with environments produced by matching instead *)
    1.40 +(* of unification, there is no need to chase assigned TVars.   *)
    1.41 +(* In this case, we can simply ignore the type substitution    *)
    1.42 +(* and use = instead of eq_type.                               *)
    1.43  
    1.44 -fun gen_lookup2 b (iTs, asol) =
    1.45 -  if Vartab.is_empty iTs then lookup1 asol
    1.46 -  else gen_lookup (eq_type b iTs) asol;
    1.47 +fun lookup' (asol, p) = gen_lookup op = asol p;
    1.48  
    1.49 -fun lookup2 env = gen_lookup2 true env;
    1.50 +fun lookup2 (iTs, asol) p =
    1.51 +  if Vartab.is_empty iTs then lookup' (asol, p)
    1.52 +  else gen_lookup (Type.eq_type iTs) asol p;
    1.53  
    1.54  fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
    1.55  
    1.56 -(* version for matching algorithms, does not chase TVars *)
    1.57 -fun lookup' (env, p) = gen_lookup2 false env p;
    1.58 -
    1.59  fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
    1.60    Envir{maxidx=maxidx, asol=Vartab.update_new ((xname, (T, t)), asol), iTs=iTs};
    1.61  
    1.62 @@ -148,7 +133,7 @@
    1.63  
    1.64  fun norm_term1 same (asol,t) : term =
    1.65    let fun norm (Var wT) =
    1.66 -            (case lookup1 asol wT of
    1.67 +            (case lookup' (asol, wT) of
    1.68                  SOME u => (norm u handle SAME => u)
    1.69                | NONE   => raise SAME)
    1.70          | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
    1.71 @@ -261,18 +246,18 @@
    1.72  
    1.73  (*Substitute for Vars in a term *)
    1.74  fun subst_Vars itms t = if Vartab.is_empty itms then t else
    1.75 -  let fun subst (v as Var ixnT) = getOpt (lookup1 itms ixnT, v)
    1.76 +  let fun subst (v as Var ixnT) = getOpt (lookup' (itms, ixnT), v)
    1.77          | subst (Abs (a, T, t)) = Abs (a, T, subst t)
    1.78          | subst (f $ t) = subst f $ subst t
    1.79          | subst t = t
    1.80    in subst t end;
    1.81  
    1.82  (*Substitute for type/term Vars in a term *)
    1.83 -fun subst_vars (env as (iTs, itms)) =
    1.84 +fun subst_vars (iTs, itms) =
    1.85    if Vartab.is_empty iTs then subst_Vars itms else
    1.86    let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T)
    1.87          | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T)
    1.88 -        | subst (Var (ixn, T)) = (case lookup' (env, (ixn, T)) of
    1.89 +        | subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of
    1.90              NONE   => Var (ixn, typ_subst_TVars iTs T)
    1.91            | SOME t => t)
    1.92          | subst (b as Bound _) = b