added (beta_)eta_contract (from pattern.ML);
authorwenzelm
Mon Feb 06 20:59:04 2006 +0100 (2006-02-06)
changeset 189370eb35519f0f3
parent 18936 647528660980
child 18938 b401ee1cda14
added (beta_)eta_contract (from pattern.ML);
added expand_atom;
src/Pure/envir.ML
     1.1 --- a/src/Pure/envir.ML	Mon Feb 06 20:59:03 2006 +0100
     1.2 +++ b/src/Pure/envir.ML	Mon Feb 06 20:59:04 2006 +0100
     1.3 @@ -31,11 +31,14 @@
     1.4    val norm_types_same: Type.tyenv -> typ list -> typ list
     1.5    val beta_norm: term -> term
     1.6    val head_norm: env -> term -> term
     1.7 +  val eta_contract: term -> term
     1.8 +  val beta_eta_contract: term -> term
     1.9    val fastype: env -> typ list -> term -> typ
    1.10    val typ_subst_TVars: Type.tyenv -> typ -> typ
    1.11    val subst_TVars: Type.tyenv -> term -> term
    1.12    val subst_Vars: tenv -> term -> term
    1.13    val subst_vars: Type.tyenv * tenv -> term -> term
    1.14 +  val expand_atom: Type.tsig -> typ -> typ * term -> term
    1.15  end;
    1.16  
    1.17  structure Envir : ENVIR =
    1.18 @@ -211,6 +214,32 @@
    1.19    in hnorm t handle SAME => t end;
    1.20  
    1.21  
    1.22 +(*Eta-contract a term (fully)*)
    1.23 +
    1.24 +fun eta_contract t =
    1.25 +  let
    1.26 +    exception SAME;
    1.27 +    fun eta (Abs (a, T, body)) =
    1.28 +      ((case eta body of
    1.29 +          body' as (f $ Bound 0) =>
    1.30 +            if loose_bvar1 (f, 0) then Abs(a, T, body')
    1.31 +            else incr_boundvars ~1 f
    1.32 +        | body' => Abs (a, T, body')) handle SAME =>
    1.33 +       (case body of
    1.34 +          (f $ Bound 0) =>
    1.35 +            if loose_bvar1 (f, 0) then raise SAME
    1.36 +            else incr_boundvars ~1 f
    1.37 +        | _ => raise SAME))
    1.38 +      | eta (f $ t) =
    1.39 +          (let val f' = eta f
    1.40 +           in f' $ etah t end handle SAME => f $ eta t)
    1.41 +      | eta _ = raise SAME
    1.42 +    and etah t = (eta t handle SAME => t)
    1.43 +  in etah t end;
    1.44 +
    1.45 +val beta_eta_contract = eta_contract o beta_norm;
    1.46 +
    1.47 +
    1.48  (*finds type of term without checking that combinations are consistent
    1.49    Ts holds types of bound variables*)
    1.50  fun fastype (Envir {iTs, ...}) =
    1.51 @@ -246,7 +275,7 @@
    1.52  
    1.53  (*Substitute for Vars in a term *)
    1.54  fun subst_Vars itms t = if Vartab.is_empty itms then t else
    1.55 -  let fun subst (v as Var ixnT) = getOpt (lookup' (itms, ixnT), v)
    1.56 +  let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT))
    1.57          | subst (Abs (a, T, t)) = Abs (a, T, subst t)
    1.58          | subst (f $ t) = subst f $ subst t
    1.59          | subst t = t
    1.60 @@ -265,4 +294,11 @@
    1.61          | subst (f $ t) = subst f $ subst t
    1.62    in subst end;
    1.63  
    1.64 +
    1.65 +(* expand_atom *)
    1.66 +
    1.67 +fun expand_atom tsig T (U, u) =
    1.68 +  subst_TVars (Type.typ_match tsig (U, T) Vartab.empty) u
    1.69 +  handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
    1.70 +
    1.71  end;