tuned eta_contract;
authorwenzelm
Thu Sep 21 19:05:01 2006 +0200 (2006-09-21)
changeset 20670115262dd18e2
parent 20669 52ba40872033
child 20671 2aa8269a868e
tuned eta_contract;
src/Pure/envir.ML
     1.1 --- a/src/Pure/envir.ML	Thu Sep 21 19:04:55 2006 +0200
     1.2 +++ b/src/Pure/envir.ML	Thu Sep 21 19:05:01 2006 +0200
     1.3 @@ -207,7 +207,7 @@
     1.4        | hnorm (f $ t) = (case hnorm f of
     1.5            Abs (_, _, body) => head_norm env (subst_bound (t, body))
     1.6          | nf => nf $ t)
     1.7 -	  | hnorm _ =  raise SAME
     1.8 +          | hnorm _ =  raise SAME
     1.9    in hnorm t handle SAME => t end;
    1.10  
    1.11  
    1.12 @@ -215,23 +215,26 @@
    1.13  
    1.14  fun eta_contract t =
    1.15    let
    1.16 -    exception SAME;
    1.17 +    fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise SAME
    1.18 +      | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
    1.19 +      | decr lev (t $ u) = (decr lev t $ decrh lev u handle SAME => t $ decr lev u)
    1.20 +      | decr _ _ = raise SAME
    1.21 +    and decrh lev t = (decr lev t handle SAME => t);
    1.22 +
    1.23      fun eta (Abs (a, T, body)) =
    1.24 -      ((case eta body of
    1.25 -          body' as (f $ Bound 0) =>
    1.26 -            if loose_bvar1 (f, 0) then Abs(a, T, body')
    1.27 -            else incr_boundvars ~1 f
    1.28 -        | body' => Abs (a, T, body')) handle SAME =>
    1.29 -       (case body of
    1.30 -          (f $ Bound 0) =>
    1.31 -            if loose_bvar1 (f, 0) then raise SAME
    1.32 -            else incr_boundvars ~1 f
    1.33 -        | _ => raise SAME))
    1.34 -      | eta (f $ t) =
    1.35 -          (let val f' = eta f
    1.36 -           in f' $ etah t end handle SAME => f $ eta t)
    1.37 +        ((case eta body of
    1.38 +            body' as (f $ Bound 0) =>
    1.39 +              if loose_bvar1 (f, 0) then Abs (a, T, body')
    1.40 +              else decrh 0 f
    1.41 +         | body' => Abs (a, T, body')) handle SAME =>
    1.42 +            (case body of
    1.43 +              f $ Bound 0 =>
    1.44 +                if loose_bvar1 (f, 0) then raise SAME
    1.45 +                else decrh 0 f
    1.46 +            | _ => raise SAME))
    1.47 +      | eta (t $ u) = (eta t $ etah u handle SAME => t $ eta u)
    1.48        | eta _ = raise SAME
    1.49 -    and etah t = (eta t handle SAME => t)
    1.50 +    and etah t = (eta t handle SAME => t);
    1.51    in etah t end;
    1.52  
    1.53  val beta_eta_contract = eta_contract o beta_norm;
    1.54 @@ -242,19 +245,19 @@
    1.55  fun fastype (Envir {iTs, ...}) =
    1.56  let val funerr = "fastype: expected function type";
    1.57      fun fast Ts (f $ u) =
    1.58 -	(case fast Ts f of
    1.59 -	   Type ("fun", [_, T]) => T
    1.60 -	 | TVar ixnS =>
    1.61 -		(case Type.lookup (iTs, ixnS) of
    1.62 -		   SOME (Type ("fun", [_, T])) => T
    1.63 -		 | _ => raise TERM (funerr, [f $ u]))
    1.64 -	 | _ => raise TERM (funerr, [f $ u]))
    1.65 +        (case fast Ts f of
    1.66 +           Type ("fun", [_, T]) => T
    1.67 +         | TVar ixnS =>
    1.68 +                (case Type.lookup (iTs, ixnS) of
    1.69 +                   SOME (Type ("fun", [_, T])) => T
    1.70 +                 | _ => raise TERM (funerr, [f $ u]))
    1.71 +         | _ => raise TERM (funerr, [f $ u]))
    1.72        | fast Ts (Const (_, T)) = T
    1.73        | fast Ts (Free (_, T)) = T
    1.74        | fast Ts (Bound i) =
    1.75 -	(List.nth (Ts, i)
    1.76 -  	 handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
    1.77 -      | fast Ts (Var (_, T)) = T 
    1.78 +        (List.nth (Ts, i)
    1.79 +         handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
    1.80 +      | fast Ts (Var (_, T)) = T
    1.81        | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
    1.82  in fast end;
    1.83