src/Pure/envir.ML
changeset 12231 4a25f04bea61
parent 11513 2f6fe5b01521
child 12496 0a9bd5034e05
     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;