# HG changeset patch # User paulson # Date 857552685 -3600 # Node ID 9453616d4b803e077b4f8eac54907b2f62ebdda3 # Parent ddc6cf6b62e930c25cad65e7bce146dec7a15748 Declares eta_contract_atom; fixed comment; some tidying diff -r ddc6cf6b62e9 -r 9453616d4b80 src/Pure/pattern.ML --- a/src/Pure/pattern.ML Wed Mar 05 10:03:30 1997 +0100 +++ b/src/Pure/pattern.ML Wed Mar 05 10:04:45 1997 +0100 @@ -17,11 +17,12 @@ type type_sig type sg type env - val eta_contract: term -> term - val match: type_sig -> term * term - -> (indexname*typ)list * (indexname*term)list - val matches: type_sig -> term * term -> bool - val unify: sg * env * (term * term)list -> env + val eta_contract : term -> term + val eta_contract_atom : term -> term + val match : type_sig -> term * term + -> (indexname*typ)list * (indexname*term)list + val matches : type_sig -> term * term -> bool + val unify : sg * env * (term * term)list -> env exception Unif exception MATCH exception Pattern @@ -221,7 +222,7 @@ foldl (unif []) (env,tus)); -(*Perform eta-contractions upon a term*) +(*Eta-contract a term (fully)*) fun eta_contract (Abs(a,T,body)) = (case eta_contract body of body' as (f $ Bound 0) => @@ -232,6 +233,18 @@ | eta_contract t = t; +(*Eta-contract a term from outside: just enough to reduce it to an atom*) +fun eta_contract_atom (t0 as Abs(a, T, body)) = + (case eta_contract2 body of + body' as (f $ Bound 0) => + if (0 mem_int loose_bnos f) then Abs(a,T,body') + else eta_contract_atom (incr_boundvars ~1 f) + | _ => t0) + | eta_contract_atom t = t +and eta_contract2 (f$t) = f $ eta_contract_atom t + | eta_contract2 t = eta_contract_atom t; + + (* Pattern matching *) exception MATCH; @@ -239,8 +252,7 @@ returns a (tyvar,typ)list and (var,term)list. The pattern and object may have variables in common. Instantiation does not affect the object, so matching ?a with ?a+1 works. - A Const does not match a Free of the same name! - Does not notice eta-equality, thus f does not match %(x)f(x) *) + A Const does not match a Free of the same name! *) fun fomatch tsig (pat,obj) = let fun typ_match args = (Type.typ_match tsig args) handle Type.TYPE_MATCH => raise MATCH; @@ -261,7 +273,7 @@ mtch (typ_match (tyinsts,(T,U)),insts) (t,u) | (f$t, g$u) => mtch (mtch (tyinsts,insts) (f,g)) (t, u) | _ => raise MATCH - in mtch([],[]) (eta_contract pat,eta_contract obj) end; + in mtch([],[]) (eta_contract pat, eta_contract obj) end; fun match_bind(itms,binders,ixn,is,t) =