src/Pure/unify.ML
changeset 12231 4a25f04bea61
parent 8406 a217b0cd304d
child 12262 11ff5f47df6e
     1.1 --- a/src/Pure/unify.ML	Fri Nov 16 23:02:58 2001 +0100
     1.2 +++ b/src/Pure/unify.ML	Mon Nov 19 17:32:49 2001 +0100
     1.3 @@ -63,59 +63,7 @@
     1.4  
     1.5  fun strip_type env T = (binder_types env T, body_type env T);
     1.6  
     1.7 -
     1.8 -(*Put a term into head normal form for unification.
     1.9 -  Operands need not be in normal form.  Does eta-expansions on the head,
    1.10 -  which involves renumbering (thus copying) the args.  To avoid this 
    1.11 -  inefficiency, avoid partial application:  if an atom is applied to
    1.12 -  any arguments at all, apply it to its full number of arguments.
    1.13 -  For
    1.14 -    rbinder = [(x1,T),...,(xm,Tm)]		(user's var names preserved!)
    1.15 -    args  =   [arg1,...,argn]
    1.16 -  the value of 
    1.17 -      (xm,...,x1)(head(arg1,...,argn))  remains invariant.
    1.18 -*)
    1.19 -
    1.20 -local exception SAME
    1.21 -in
    1.22 -  fun head_norm (env,t) : term =
    1.23 -    let fun hnorm (Var (v,T)) = 
    1.24 -	      (case Envir.lookup (env,v) of
    1.25 -		  Some u => head_norm (env, u)
    1.26 -		| None   => raise SAME)
    1.27 -	  | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
    1.28 -	  | hnorm (Abs(_,_,body) $ t) =
    1.29 -	      head_norm (env, subst_bound (t, body))
    1.30 -	  | hnorm (f $ t) =
    1.31 -	      (case hnorm f of
    1.32 -		 Abs(_,_,body) =>
    1.33 -		   head_norm (env, subst_bound (t, body))
    1.34 -	       | nf => nf $ t)
    1.35 -	  | hnorm _ =  raise SAME
    1.36 -    in  hnorm t  handle SAME=> t  end
    1.37 -end;
    1.38 -
    1.39 -
    1.40 -(*finds type of term without checking that combinations are consistent
    1.41 -  rbinder holds types of bound variables*)
    1.42 -fun fastype (Envir.Envir{iTs,...}) =
    1.43 -let val funerr = "fastype: expected function type";
    1.44 -    fun fast(rbinder, f$u) =
    1.45 -	(case (fast (rbinder, f)) of
    1.46 -	   Type("fun",[_,T]) => T
    1.47 -	 | TVar(ixn,_) =>
    1.48 -		(case Vartab.lookup (iTs,ixn) of
    1.49 -		   Some(Type("fun",[_,T])) => T
    1.50 -		 | _ => raise TERM(funerr, [f$u]))
    1.51 -	 | _ => raise TERM(funerr, [f$u]))
    1.52 -      | fast (rbinder, Const (_,T)) = T
    1.53 -      | fast (rbinder, Free (_,T)) = T
    1.54 -      | fast (rbinder, Bound i) =
    1.55 -	(#2 (nth_elem (i,rbinder))
    1.56 -  	 handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
    1.57 -      | fast (rbinder, Var (_,T)) = T 
    1.58 -      | fast (rbinder, Abs (_,T,u)) =  T --> fast (("",T) :: rbinder, u)
    1.59 -in fast end;
    1.60 +fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
    1.61  
    1.62  
    1.63  (*Eta normal form*)
    1.64 @@ -289,8 +237,8 @@
    1.65  
    1.66  fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
    1.67       new_dpair (rbinder,
    1.68 -		eta_norm env (rbinder, head_norm(env,t)),
    1.69 -	  	eta_norm env (rbinder, head_norm(env,u)), env);
    1.70 +		eta_norm env (rbinder, Envir.head_norm env t),
    1.71 +	  	eta_norm env (rbinder, Envir.head_norm env u), env);
    1.72  
    1.73  
    1.74  
    1.75 @@ -390,7 +338,7 @@
    1.76  let (*Produce copies of uarg and cons them in front of uargs*)
    1.77      fun copycons uarg (uargs, (env, dpairs)) =
    1.78  	Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
    1.79 -	    (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
    1.80 +	    (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
    1.81  		 (env, dpairs)));
    1.82  	(*Produce sequence of all possible ways of copying the arg list*)
    1.83      fun copyargs [] = Seq.cons( ([],ed), Seq.empty)