Moved head_norm and fastype from unify.ML to envir.ML

--- a/src/Pure/envir.ML	Fri Nov 16 23:02:58 2001 +0100
+++ b/src/Pure/envir.ML	Mon Nov 19 17:32:49 2001 +0100
@@ -27,6 +27,8 @@
   val norm_type_same: env -> typ -> typ
   val norm_types_same: env -> typ list -> typ list
   val beta_norm: term -> term
+  val head_norm: env -> term -> term
+  val fastype: env -> typ list -> term -> typ
 end;
 
 structure Envir : ENVIR =
@@ -161,4 +163,42 @@
   if Vartab.is_empty iTs then raise SAME else normTs iTs;
 
 
+(*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
+          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))
+      | hnorm (f $ t) = (case hnorm f of
+          Abs (_, _, body) => head_norm env (subst_bound (t, body))
+        | nf => nf $ t)
+	  | hnorm _ =  raise SAME
+  in hnorm t handle SAME => t end;
+
+
+(*finds type of term without checking that combinations are consistent
+  Ts holds types of bound variables*)
+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
+		   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
+      | fast Ts (Bound i) =
+	(nth_elem (i, Ts)
+  	 handle LIST _=> raise TERM ("fastype: Bound", [Bound i]))
+      | fast Ts (Var (_, T)) = T 
+      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
+in fast end;
+
 end;

--- a/src/Pure/unify.ML	Fri Nov 16 23:02:58 2001 +0100
+++ b/src/Pure/unify.ML	Mon Nov 19 17:32:49 2001 +0100
@@ -63,59 +63,7 @@
 
 fun strip_type env T = (binder_types env T, body_type env T);
 
-
-(*Put a term into head normal form for unification.
-  Operands need not be in normal form.  Does eta-expansions on the head,
-  which involves renumbering (thus copying) the args.  To avoid this 
-  inefficiency, avoid partial application:  if an atom is applied to
-  any arguments at all, apply it to its full number of arguments.
-  For
-    rbinder = [(x1,T),...,(xm,Tm)]		(user's var names preserved!)
-    args  =   [arg1,...,argn]
-  the value of 
-      (xm,...,x1)(head(arg1,...,argn))  remains invariant.
-*)
-
-local exception SAME
-in
-  fun head_norm (env,t) : term =
-    let fun hnorm (Var (v,T)) = 
-	      (case Envir.lookup (env,v) 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))
-	  | hnorm (f $ t) =
-	      (case hnorm f of
-		 Abs(_,_,body) =>
-		   head_norm (env, subst_bound (t, body))
-	       | nf => nf $ t)
-	  | hnorm _ =  raise SAME
-    in  hnorm t  handle SAME=> t  end
-end;
-
-
-(*finds type of term without checking that combinations are consistent
-  rbinder holds types of bound variables*)
-fun fastype (Envir.Envir{iTs,...}) =
-let val funerr = "fastype: expected function type";
-    fun fast(rbinder, f$u) =
-	(case (fast (rbinder, f)) of
-	   Type("fun",[_,T]) => T
-	 | TVar(ixn,_) =>
-		(case Vartab.lookup (iTs,ixn) of
-		   Some(Type("fun",[_,T])) => T
-		 | _ => raise TERM(funerr, [f$u]))
-	 | _ => raise TERM(funerr, [f$u]))
-      | fast (rbinder, Const (_,T)) = T
-      | fast (rbinder, Free (_,T)) = T
-      | fast (rbinder, Bound i) =
-	(#2 (nth_elem (i,rbinder))
-  	 handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
-      | fast (rbinder, Var (_,T)) = T 
-      | fast (rbinder, Abs (_,T,u)) =  T --> fast (("",T) :: rbinder, u)
-in fast end;
+fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
 
 
 (*Eta normal form*)
@@ -289,8 +237,8 @@
 
 fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
      new_dpair (rbinder,
-		eta_norm env (rbinder, head_norm(env,t)),
-	  	eta_norm env (rbinder, head_norm(env,u)), env);
+		eta_norm env (rbinder, Envir.head_norm env t),
+	  	eta_norm env (rbinder, Envir.head_norm env u), env);
 
 
 
@@ -390,7 +338,7 @@
 let (*Produce copies of uarg and cons them in front of uargs*)
     fun copycons uarg (uargs, (env, dpairs)) =
 	Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
-	    (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
+	    (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
 		 (env, dpairs)));
 	(*Produce sequence of all possible ways of copying the arg list*)
     fun copyargs [] = Seq.cons( ([],ed), Seq.empty)