src/Pure/pattern.ML
changeset 13998 75a399c2781f
parent 13891 ae9a2a433388
child 14643 130076a81b84
     1.1 --- a/src/Pure/pattern.ML	Sat May 10 20:52:18 2003 +0200
     1.2 +++ b/src/Pure/pattern.ML	Sat May 10 20:53:02 2003 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4    val trace_unify_fail  : bool ref
     1.5    val aeconv            : term * term -> bool
     1.6    val eta_contract      : term -> term
     1.7 +  val eta_long          : typ list -> term -> term
     1.8    val beta_eta_contract : term -> term
     1.9    val eta_contract_atom : term -> term
    1.10    val match             : type_sig -> term * term
    1.11 @@ -328,6 +329,19 @@
    1.12  and eta_contract2 (f$t) = f $ eta_contract_atom t
    1.13    | eta_contract2 t     = eta_contract_atom t;
    1.14  
    1.15 +(* put a term into eta long beta normal form *)
    1.16 +fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
    1.17 +  | eta_long Ts t = (case strip_comb t of
    1.18 +      (Abs _, _) => eta_long Ts (Envir.beta_norm t)
    1.19 +    | (u, ts) => 
    1.20 +      let
    1.21 +        val Us = binder_types (fastype_of1 (Ts, t));
    1.22 +        val i = length Us
    1.23 +      in list_abs (map (pair "x") Us,
    1.24 +        list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
    1.25 +          (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
    1.26 +      end);
    1.27 +
    1.28  
    1.29  (*Tests whether 2 terms are alpha/eta-convertible and have same type.
    1.30    Note that Consts and Vars may have more than one type.*)