# HG changeset patch # User wenzelm # Date 1139255944 -3600 # Node ID 0eb35519f0f3188778a5512269afb00795262c26 # Parent 6475286609803f5b9d009af689aa5cd81127991b added (beta_)eta_contract (from pattern.ML); added expand_atom; diff -r 647528660980 -r 0eb35519f0f3 src/Pure/envir.ML --- a/src/Pure/envir.ML Mon Feb 06 20:59:03 2006 +0100 +++ b/src/Pure/envir.ML Mon Feb 06 20:59:04 2006 +0100 @@ -31,11 +31,14 @@ val norm_types_same: Type.tyenv -> typ list -> typ list val beta_norm: term -> term val head_norm: env -> term -> term + val eta_contract: term -> term + val beta_eta_contract: term -> term val fastype: env -> typ list -> term -> typ val typ_subst_TVars: Type.tyenv -> typ -> typ val subst_TVars: Type.tyenv -> term -> term val subst_Vars: tenv -> term -> term val subst_vars: Type.tyenv * tenv -> term -> term + val expand_atom: Type.tsig -> typ -> typ * term -> term end; structure Envir : ENVIR = @@ -211,6 +214,32 @@ in hnorm t handle SAME => t end; +(*Eta-contract a term (fully)*) + +fun eta_contract t = + let + exception SAME; + fun eta (Abs (a, T, body)) = + ((case eta body of + body' as (f $ Bound 0) => + if loose_bvar1 (f, 0) then Abs(a, T, body') + else incr_boundvars ~1 f + | body' => Abs (a, T, body')) handle SAME => + (case body of + (f $ Bound 0) => + if loose_bvar1 (f, 0) then raise SAME + else incr_boundvars ~1 f + | _ => raise SAME)) + | eta (f $ t) = + (let val f' = eta f + in f' $ etah t end handle SAME => f $ eta t) + | eta _ = raise SAME + and etah t = (eta t handle SAME => t) + in etah t end; + +val beta_eta_contract = eta_contract o beta_norm; + + (*finds type of term without checking that combinations are consistent Ts holds types of bound variables*) fun fastype (Envir {iTs, ...}) = @@ -246,7 +275,7 @@ (*Substitute for Vars in a term *) fun subst_Vars itms t = if Vartab.is_empty itms then t else - let fun subst (v as Var ixnT) = getOpt (lookup' (itms, ixnT), v) + let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT)) | subst (Abs (a, T, t)) = Abs (a, T, subst t) | subst (f $ t) = subst f $ subst t | subst t = t @@ -265,4 +294,11 @@ | subst (f $ t) = subst f $ subst t in subst end; + +(* expand_atom *) + +fun expand_atom tsig T (U, u) = + subst_TVars (Type.typ_match tsig (U, T) Vartab.empty) u + handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]); + end;