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;
```