Moved head_norm and fastype from unify.ML to envir.ML
authorberghofe
Mon Nov 19 17:32:49 2001 +0100 (2001-11-19)
changeset 122314a25f04bea61
parent 12230 b06cc3834ee5
child 12232 ff75ed08b3fb
Moved head_norm and fastype from unify.ML to envir.ML
src/Pure/envir.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/envir.ML	Fri Nov 16 23:02:58 2001 +0100
     1.2 +++ b/src/Pure/envir.ML	Mon Nov 19 17:32:49 2001 +0100
     1.3 @@ -27,6 +27,8 @@
     1.4    val norm_type_same: env -> typ -> typ
     1.5    val norm_types_same: env -> typ list -> typ list
     1.6    val beta_norm: term -> term
     1.7 +  val head_norm: env -> term -> term
     1.8 +  val fastype: env -> typ list -> term -> typ
     1.9  end;
    1.10  
    1.11  structure Envir : ENVIR =
    1.12 @@ -161,4 +163,42 @@
    1.13    if Vartab.is_empty iTs then raise SAME else normTs iTs;
    1.14  
    1.15  
    1.16 +(*Put a term into head normal form for unification.*)
    1.17 +
    1.18 +fun head_norm env t =
    1.19 +  let
    1.20 +    fun hnorm (Var (v, T)) = (case lookup (env, v) of
    1.21 +          Some u => head_norm env u
    1.22 +        | None => raise SAME)
    1.23 +      | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
    1.24 +      | hnorm (Abs (_, _, body) $ t) =
    1.25 +          head_norm env (subst_bound (t, body))
    1.26 +      | hnorm (f $ t) = (case hnorm f of
    1.27 +          Abs (_, _, body) => head_norm env (subst_bound (t, body))
    1.28 +        | nf => nf $ t)
    1.29 +	  | hnorm _ =  raise SAME
    1.30 +  in hnorm t handle SAME => t end;
    1.31 +
    1.32 +
    1.33 +(*finds type of term without checking that combinations are consistent
    1.34 +  Ts holds types of bound variables*)
    1.35 +fun fastype (Envir {iTs, ...}) =
    1.36 +let val funerr = "fastype: expected function type";
    1.37 +    fun fast Ts (f $ u) =
    1.38 +	(case fast Ts f of
    1.39 +	   Type ("fun", [_, T]) => T
    1.40 +	 | TVar(ixn, _) =>
    1.41 +		(case Vartab.lookup (iTs, ixn) of
    1.42 +		   Some (Type ("fun", [_, T])) => T
    1.43 +		 | _ => raise TERM (funerr, [f $ u]))
    1.44 +	 | _ => raise TERM (funerr, [f $ u]))
    1.45 +      | fast Ts (Const (_, T)) = T
    1.46 +      | fast Ts (Free (_, T)) = T
    1.47 +      | fast Ts (Bound i) =
    1.48 +	(nth_elem (i, Ts)
    1.49 +  	 handle LIST _=> raise TERM ("fastype: Bound", [Bound i]))
    1.50 +      | fast Ts (Var (_, T)) = T 
    1.51 +      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
    1.52 +in fast end;
    1.53 +
    1.54  end;
     2.1 --- a/src/Pure/unify.ML	Fri Nov 16 23:02:58 2001 +0100
     2.2 +++ b/src/Pure/unify.ML	Mon Nov 19 17:32:49 2001 +0100
     2.3 @@ -63,59 +63,7 @@
     2.4  
     2.5  fun strip_type env T = (binder_types env T, body_type env T);
     2.6  
     2.7 -
     2.8 -(*Put a term into head normal form for unification.
     2.9 -  Operands need not be in normal form.  Does eta-expansions on the head,
    2.10 -  which involves renumbering (thus copying) the args.  To avoid this 
    2.11 -  inefficiency, avoid partial application:  if an atom is applied to
    2.12 -  any arguments at all, apply it to its full number of arguments.
    2.13 -  For
    2.14 -    rbinder = [(x1,T),...,(xm,Tm)]		(user's var names preserved!)
    2.15 -    args  =   [arg1,...,argn]
    2.16 -  the value of 
    2.17 -      (xm,...,x1)(head(arg1,...,argn))  remains invariant.
    2.18 -*)
    2.19 -
    2.20 -local exception SAME
    2.21 -in
    2.22 -  fun head_norm (env,t) : term =
    2.23 -    let fun hnorm (Var (v,T)) = 
    2.24 -	      (case Envir.lookup (env,v) of
    2.25 -		  Some u => head_norm (env, u)
    2.26 -		| None   => raise SAME)
    2.27 -	  | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
    2.28 -	  | hnorm (Abs(_,_,body) $ t) =
    2.29 -	      head_norm (env, subst_bound (t, body))
    2.30 -	  | hnorm (f $ t) =
    2.31 -	      (case hnorm f of
    2.32 -		 Abs(_,_,body) =>
    2.33 -		   head_norm (env, subst_bound (t, body))
    2.34 -	       | nf => nf $ t)
    2.35 -	  | hnorm _ =  raise SAME
    2.36 -    in  hnorm t  handle SAME=> t  end
    2.37 -end;
    2.38 -
    2.39 -
    2.40 -(*finds type of term without checking that combinations are consistent
    2.41 -  rbinder holds types of bound variables*)
    2.42 -fun fastype (Envir.Envir{iTs,...}) =
    2.43 -let val funerr = "fastype: expected function type";
    2.44 -    fun fast(rbinder, f$u) =
    2.45 -	(case (fast (rbinder, f)) of
    2.46 -	   Type("fun",[_,T]) => T
    2.47 -	 | TVar(ixn,_) =>
    2.48 -		(case Vartab.lookup (iTs,ixn) of
    2.49 -		   Some(Type("fun",[_,T])) => T
    2.50 -		 | _ => raise TERM(funerr, [f$u]))
    2.51 -	 | _ => raise TERM(funerr, [f$u]))
    2.52 -      | fast (rbinder, Const (_,T)) = T
    2.53 -      | fast (rbinder, Free (_,T)) = T
    2.54 -      | fast (rbinder, Bound i) =
    2.55 -	(#2 (nth_elem (i,rbinder))
    2.56 -  	 handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
    2.57 -      | fast (rbinder, Var (_,T)) = T 
    2.58 -      | fast (rbinder, Abs (_,T,u)) =  T --> fast (("",T) :: rbinder, u)
    2.59 -in fast end;
    2.60 +fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
    2.61  
    2.62  
    2.63  (*Eta normal form*)
    2.64 @@ -289,8 +237,8 @@
    2.65  
    2.66  fun head_norm_dpair (env, (rbinder,t,u)) : dpair * Envir.env =
    2.67       new_dpair (rbinder,
    2.68 -		eta_norm env (rbinder, head_norm(env,t)),
    2.69 -	  	eta_norm env (rbinder, head_norm(env,u)), env);
    2.70 +		eta_norm env (rbinder, Envir.head_norm env t),
    2.71 +	  	eta_norm env (rbinder, Envir.head_norm env u), env);
    2.72  
    2.73  
    2.74  
    2.75 @@ -390,7 +338,7 @@
    2.76  let (*Produce copies of uarg and cons them in front of uargs*)
    2.77      fun copycons uarg (uargs, (env, dpairs)) =
    2.78  	Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
    2.79 -	    (mc (rbinder, targs,eta_norm env (rbinder,head_norm(env,uarg)),
    2.80 +	    (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
    2.81  		 (env, dpairs)));
    2.82  	(*Produce sequence of all possible ways of copying the arg list*)
    2.83      fun copyargs [] = Seq.cons( ([],ed), Seq.empty)