src/Pure/envir.ML

 (*  Title:      Pure/envir.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1988  University of Cambridge
 
-Environments.  They don't take account that typ is part of variable
-name.  Therefore we check elsewhere that two variables with same names
-and different types cannot occur.
+Environments.  The type of a term variable / sort of a type variable is
+part of its name. The lookup function must apply type substitutions,
+since they may change the identity of a variable.
 *)
 
 signature ENVIR =
 sig
-  datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
-  val type_env: env -> typ Vartab.table
+  type tenv
+  datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
+  val type_env: env -> Type.tyenv
   exception SAME
   val genvars: string -> env * typ list -> env * term list
   val genvar: string -> env * typ -> env * term
-  val lookup: env * indexname -> term option
-  val update: (indexname * term) * env -> env
+  val lookup: env * (indexname * typ) -> term option
+  val lookup': (Type.tyenv * tenv) * (indexname * typ) -> term option
+  val update: ((indexname * typ) * term) * env -> env
   val empty: int -> env
   val is_empty: env -> bool
   val above: int * env -> bool
-  val vupdate: (indexname * term) * env -> env
-  val alist_of: env -> (indexname * term) list
+  val vupdate: ((indexname * typ) * term) * env -> env
+  val alist_of: env -> (indexname * (typ * term)) list
   val norm_term: env -> term -> term
   val norm_term_same: env -> term -> term
-  val norm_type: typ Vartab.table -> typ -> typ
-  val norm_type_same: typ Vartab.table -> typ -> typ
-  val norm_types_same: typ Vartab.table -> typ list -> typ list
+  val norm_type: Type.tyenv -> typ -> typ
+  val norm_type_same: Type.tyenv -> typ -> typ
+  val norm_types_same: Type.tyenv -> typ list -> typ list
   val beta_norm: term -> term
   val head_norm: env -> term -> term
   val fastype: env -> typ list -> term -> typ
+  val typ_subst_TVars: Type.tyenv -> typ -> typ
+  val subst_TVars: Type.tyenv -> term -> term
+  val subst_Vars: tenv -> term -> term
+  val subst_vars: Type.tyenv * tenv -> term -> term
 end;
 
 structure Envir : ENVIR =
 struct
 
 (*updating can destroy environment in 2 ways!!
    (1) variables out of range   (2) circular assignments
 *)
+type tenv = (typ * term) Vartab.table
+
 datatype env = Envir of
-    {maxidx: int,               (*maximum index of vars*)
-     asol: term Vartab.table,   (*table of assignments to Vars*)
-     iTs: typ Vartab.table}     (*table of assignments to TVars*)
+    {maxidx: int,      (*maximum index of vars*)
+     asol: tenv,       (*table of assignments to Vars*)
+     iTs: Type.tyenv}  (*table of assignments to TVars*)
 
 fun type_env (Envir {iTs, ...}) = iTs;
 
 (*Generate a list of distinct variables.
   Increments index to make them distinct from ALL present variables. *)

 (*Generate a variable.*)
 fun genvar name (env,T) : env * term =
   let val (env',[v]) = genvars name (env,[T])
   in  (env',v)  end;
 
-fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
-
-fun update ((xname, t), Envir{maxidx, asol, iTs}) =
-  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs};
+(* de-reference TVars. When dealing with environments produced by *)
+(* matching instead of unification, there is no need to chase     *)
+(* assigned TVars. In this case, set b to false.                  *)
+fun devar b iTs (T as TVar vT) = (case Type.lookup (iTs, vT) of
+      NONE => T
+    | SOME T' => if b then devar true iTs T' else T')
+  | devar b iTs T = T;
+
+fun eq_type b iTs (T, T') =
+  (case (devar b iTs T, devar b iTs T') of
+     (Type (s, Ts), Type (s', Ts')) =>
+       s = s' andalso ListPair.all (eq_type b iTs) (Ts, Ts')
+   | (U, U') => U = U');
+
+fun var_clash ixn T T' = raise TYPE ("Variable " ^
+  quote (Syntax.string_of_vname ixn) ^ " has two distinct types",
+  [T', T], []);
+
+fun gen_lookup f asol (xname, T) =
+  (case Vartab.lookup (asol, xname) of
+     NONE => NONE
+   | SOME (U, t) => if f (T, U) then SOME t
+       else var_clash xname T U);
+
+(* version ignoring type substitutions *)
+fun lookup1 asol = gen_lookup op = asol;
+
+fun gen_lookup2 b (iTs, asol) =
+  if Vartab.is_empty iTs then lookup1 asol
+  else gen_lookup (eq_type b iTs) asol;
+
+fun lookup2 env = gen_lookup2 true env;
+
+fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
+
+(* version for matching algorithms, does not chase TVars *)
+fun lookup' (env, p) = gen_lookup2 false env p;
+
+fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
+  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname, (T, t)), asol), iTs=iTs};
 
 (*The empty environment.  New variables will start with the given index+1.*)
 fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
 
 (*Test for empty environment*)

    | (SOME (_, i), NONE) => i > lim
    | (NONE, SOME (_, i')) => i' > lim
    | (SOME (_, i), SOME (_, i')) => i > lim andalso i' > lim);
 
 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
-fun vupdate((a,t), env) = case t of
-      Var(name',T) =>
-        if a=name' then env     (*cycle!*)
+fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
+      Var (nT as (name', T)) =>
+        if a = name' then env     (*cycle!*)
         else if xless(a, name')  then
-           (case lookup(env,name') of  (*if already assigned, chase*)
-                NONE => update((name', Var(a,T)), env)
-              | SOME u => vupdate((a,u), env))
-        else update((a,t), env)
-    | _ => update((a,t), env);
+           (case lookup (env, nT) of  (*if already assigned, chase*)
+                NONE => update ((nT, Var (a, T)), env)
+              | SOME u => vupdate ((aU, u), env))
+        else update ((aU, t), env)
+    | _ => update ((aU, t), env);
 
 
 (*Convert environment to alist*)
 fun alist_of (Envir{asol,...}) = Vartab.dest asol;
 

 
 (*raised when norm has no effect on a term, to do sharing instead of copying*)
 exception SAME;
 
 fun norm_term1 same (asol,t) : term =
-  let fun norm (Var (w,T)) =
-            (case Vartab.lookup (asol, w) of
+  let fun norm (Var wT) =
+            (case lookup1 asol wT of
                 SOME u => (norm u handle SAME => u)
               | NONE   => raise SAME)
         | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
         | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
         | norm (f $ t) =

       and normh t = norm t handle SAME => t
   in (if same then norm else normh) t end
 
 fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
   | normT iTs (TFree _) = raise SAME
-  | normT iTs (TVar(v, _)) = (case Vartab.lookup (iTs, v) of
+  | normT iTs (TVar vS) = (case Type.lookup (iTs, vS) of
           SOME U => normTh iTs U
         | NONE => raise SAME)
 and normTh iTs T = ((normT iTs T) handle SAME => T)
 and normTs iTs [] = raise SAME
   | normTs iTs (T :: Ts) =

 
 fun norm_term2 same (asol, iTs, t) : term =
   let fun norm (Const (a, T)) = Const(a, normT iTs T)
         | norm (Free (a, T)) = Free(a, normT iTs T)
         | norm (Var (w, T)) =
-            (case Vartab.lookup (asol, w) of
+            (case lookup2 (iTs, asol) (w, T) of
                 SOME u => normh u
               | NONE   => Var(w, normT iTs T))
         | norm (Abs (a, T, body)) =
                (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
         | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))

 
 (*Put a term into head normal form for unification.*)
 
 fun head_norm env t =
   let
-    fun hnorm (Var (v, T)) = (case lookup (env, v) of
+    fun hnorm (Var vT) = (case lookup (env, vT) of
           SOME u => head_norm env u
         | NONE => raise SAME)
       | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
       | hnorm (Abs (_, _, body) $ t) =
           head_norm env (subst_bound (t, body))

 fun fastype (Envir {iTs, ...}) =
 let val funerr = "fastype: expected function type";
     fun fast Ts (f $ u) =
 	(case fast Ts f of
 	   Type ("fun", [_, T]) => T
-	 | TVar(ixn, _) =>
-		(case Vartab.lookup (iTs, ixn) of
+	 | TVar ixnS =>
+		(case Type.lookup (iTs, ixnS) of
 		   SOME (Type ("fun", [_, T])) => T
 		 | _ => raise TERM (funerr, [f $ u]))
 	 | _ => raise TERM (funerr, [f $ u]))
       | fast Ts (Const (_, T)) = T
       | fast Ts (Free (_, T)) = T

   	 handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
       | fast Ts (Var (_, T)) = T 
       | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
 in fast end;
 
+
+(*Substitute for type Vars in a type*)
+fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else
+  let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
+        | subst(T as TFree _) = T
+        | subst(T as TVar ixnS) =
+            (case Type.lookup (iTs, ixnS) of NONE => T | SOME(U) => U)
+  in subst T end;
+
+(*Substitute for type Vars in a term*)
+val subst_TVars = map_term_types o typ_subst_TVars;
+
+(*Substitute for Vars in a term *)
+fun subst_Vars itms t = if Vartab.is_empty itms then t else
+  let fun subst (v as Var ixnT) = getOpt (lookup1 itms ixnT, v)
+        | subst (Abs (a, T, t)) = Abs (a, T, subst t)
+        | subst (f $ t) = subst f $ subst t
+        | subst t = t
+  in subst t end;
+
+(*Substitute for type/term Vars in a term *)
+fun subst_vars (env as (iTs, itms)) =
+  if Vartab.is_empty iTs then subst_Vars itms else
+  let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T)
+        | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T)
+        | subst (Var (ixn, T)) = (case lookup' (env, (ixn, T)) of
+            NONE   => Var (ixn, typ_subst_TVars iTs T)
+          | SOME t => t)
+        | subst (b as Bound _) = b
+        | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
+        | subst (f $ t) = subst f $ subst t
+  in subst end;
+
 end;