--- a/src/Pure/pattern.ML Tue Apr 21 17:25:19 1998 +0200
+++ b/src/Pure/pattern.ML Wed Apr 22 14:04:35 1998 +0200
@@ -24,9 +24,13 @@
val eta_contract_atom : term -> term
val match : type_sig -> term * term
-> (indexname*typ)list * (indexname*term)list
+ val first_order_match : type_sig -> term * term
+ -> (indexname*typ)list * (indexname*term)list
val matches : type_sig -> term * term -> bool
val matches_subterm : type_sig -> term * term -> bool
val unify : sg * env * (term * term)list -> env
+ val first_order : term -> bool
+ val pattern : term -> bool
exception Unif
exception MATCH
exception Pattern
@@ -279,48 +283,6 @@
| eta_contract2 t = eta_contract_atom t;
-(* Pattern matching *)
-exception MATCH;
-
-(*First-order matching; term_match tsig (pattern, object)
- 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! *)
-fun fomatch tsig (pat,obj) =
- let fun typ_match args = (Type.typ_match tsig args)
- handle Type.TYPE_MATCH => raise MATCH;
- fun mtch (tyinsts,insts) = fn
- (Var(ixn,T), t) =>
- if loose_bvar(t,0) then raise MATCH
- else (case assoc_string_int(insts,ixn) of
- None => (typ_match (tyinsts, (T, fastype_of t)),
- (ixn,t)::insts)
- | Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
- | (Free (a,T), Free (b,U)) =>
- if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH
- | (Const (a,T), Const (b,U)) =>
- if a=b then (typ_match (tyinsts,(T,U)), insts) else raise MATCH
- | (Bound i, Bound j) =>
- if i=j then (tyinsts,insts) else raise MATCH
- | (Abs(_,T,t), Abs(_,U,u)) =>
- 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;
-
-
-fun match_bind(itms,binders,ixn,is,t) =
- let val js = loose_bnos t
- in if null is
- then if null js then (ixn,t)::itms else raise MATCH
- else if js subset_int is
- then let val t' = if downto0(is,length binders - 1) then t
- else mapbnd (idx is) t
- in (ixn, mkabs(binders,is,t')) :: itms end
- else raise MATCH
- end;
-
(*Tests whether 2 terms are alpha/eta-convertible and have same type.
Note that Consts and Vars may have more than one type.*)
fun t aeconv u = aconv_aux (eta_contract_atom t, eta_contract_atom u)
@@ -333,59 +295,106 @@
| aconv_aux _ = false;
+(*** Matching ***)
+
+exception MATCH;
+
+fun typ_match tsig args = (Type.typ_match tsig args)
+ handle Type.TYPE_MATCH => raise MATCH;
+
+(*First-order matching;
+ fomatch tsig (pattern, object) 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.
+ Object is eta-contracted on the fly (by eta-expanding the pattern).
+ Precondition: the pattern is already eta-contracted!
+ Note: types are matched on the fly *)
+fun fomatch tsig =
+ let
+ fun mtch (instsp as (tyinsts,insts)) = fn
+ (Var(ixn,T), t) =>
+ if loose_bvar(t,0) then raise MATCH
+ else (case assoc_string_int(insts,ixn) of
+ None => (typ_match tsig (tyinsts, (T, fastype_of t)),
+ (ixn,t)::insts)
+ | Some u => if t aeconv u then instsp else raise MATCH)
+ | (Free (a,T), Free (b,U)) =>
+ if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
+ | (Const (a,T), Const (b,U)) =>
+ if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
+ | (Bound i, Bound j) => if i=j then instsp else raise MATCH
+ | (Abs(_,T,t), Abs(_,U,u)) =>
+ mtch (typ_match tsig (tyinsts,(T,U)),insts) (t,u)
+ | (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u)
+ | (t, Abs(_,U,u)) => mtch instsp ((incr t)$(Bound 0), u)
+ | _ => raise MATCH
+ in mtch end;
+
+fun first_order_match tsig = fomatch tsig ([],[]);
+
+(* Matching of higher-order patterns *)
+
+fun match_bind(itms,binders,ixn,is,t) =
+ let val js = loose_bnos t
+ in if null is
+ then if null js then (ixn,t)::itms else raise MATCH
+ else if js subset_int is
+ then let val t' = if downto0(is,length binders - 1) then t
+ else mapbnd (idx is) t
+ in (ixn, mkabs(binders,is,t')) :: itms end
+ else raise MATCH
+ end;
+
fun match tsg (po as (pat,obj)) =
let
-
-fun typ_match args = Type.typ_match tsg args
- handle Type.TYPE_MATCH => raise MATCH;
-
-(* Pre: pat and obj have same type *)
-fun mtch binders (env as (iTs,itms),(pat,obj)) =
- case pat of
- Abs(ns,Ts,ts) =>
- (case obj of
- Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
- | _ => let val Tt = typ_subst_TVars iTs Ts
- in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
- | _ => (case obj of
- Abs(nt,Tt,tt) =>
- mtch((nt,Tt)::binders)(env,((incr pat)$Bound(0),tt))
- | _ => cases(binders,env,pat,obj))
+ (* Pre: pat and obj have same type *)
+ fun mtch binders (env as (iTs,itms),(pat,obj)) =
+ case pat of
+ Abs(ns,Ts,ts) =>
+ (case obj of
+ Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
+ | _ => let val Tt = typ_subst_TVars iTs Ts
+ in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
+ | _ => (case obj of
+ Abs(nt,Tt,tt) =>
+ mtch((nt,Tt)::binders)(env,((incr pat)$Bound(0),tt))
+ | _ => cases(binders,env,pat,obj))
-and cases(binders,env as (iTs,itms),pat,obj) =
- let val (ph,pargs) = strip_comb pat
- fun rigrig1(iTs,oargs) =
- foldl (mtch binders) ((iTs,itms), pargs~~oargs)
- fun rigrig2((a,Ta),(b,Tb),oargs) =
- if a<> b then raise MATCH
- else rigrig1(typ_match(iTs,(Ta,Tb)), oargs)
- in case ph of
- Var(ixn,_) =>
- let val is = ints_of pargs
- in case assoc_string_int(itms,ixn) of
- None => (iTs,match_bind(itms,binders,ixn,is,obj))
- | Some u => if obj aeconv (red u is []) then env
- else raise MATCH
- end
- | _ =>
- let val (oh,oargs) = strip_comb obj
- in case (ph,oh) of
- (Const c,Const d) => rigrig2(c,d,oargs)
- | (Free f,Free g) => rigrig2(f,g,oargs)
- | (Bound i,Bound j) => if i<>j then raise MATCH
- else rigrig1(iTs,oargs)
- | (Abs _, _) => raise Pattern
- | (_, Abs _) => raise Pattern
- | _ => raise MATCH
- end
- end;
+ and cases(binders,env as (iTs,itms),pat,obj) =
+ let val (ph,pargs) = strip_comb pat
+ fun rigrig1(iTs,oargs) =
+ foldl (mtch binders) ((iTs,itms), pargs~~oargs)
+ fun rigrig2((a,Ta),(b,Tb),oargs) =
+ if a<> b then raise MATCH
+ else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
+ in case ph of
+ Var(ixn,_) =>
+ let val is = ints_of pargs
+ in case assoc_string_int(itms,ixn) of
+ None => (iTs,match_bind(itms,binders,ixn,is,obj))
+ | Some u => if obj aeconv (red u is []) then env
+ else raise MATCH
+ end
+ | _ =>
+ let val (oh,oargs) = strip_comb obj
+ in case (ph,oh) of
+ (Const c,Const d) => rigrig2(c,d,oargs)
+ | (Free f,Free g) => rigrig2(f,g,oargs)
+ | (Bound i,Bound j) => if i<>j then raise MATCH
+ else rigrig1(iTs,oargs)
+ | (Abs _, _) => raise Pattern
+ | (_, Abs _) => raise Pattern
+ | _ => raise MATCH
+ end
+ end;
-val pT = fastype_of pat
-and oT = fastype_of obj
-val iTs = typ_match ([],(pT,oT))
+ val pT = fastype_of pat
+ and oT = fastype_of obj
+ val iTs = typ_match tsg ([],(pT,oT))
+ val insts2 = (iTs,[])
-in mtch [] ((iTs,[]), po)
- handle Pattern => fomatch tsg po
+in mtch [] (insts2, po)
+ handle Pattern => fomatch tsg insts2 po
end;
(*Predicate: does the pattern match the object?*)
@@ -402,4 +411,17 @@
| _ => false
in msub([],obj) end;
+fun first_order(Abs(_,_,t)) = first_order t
+ | first_order(t $ u) = first_order t andalso first_order u andalso
+ not(is_Var t)
+ | first_order _ = true;
+
+fun pattern(Abs(_,_,t)) = pattern t
+ | pattern(t) = let val (head,args) = strip_comb t
+ in if is_Var head
+ then let val _ = ints_of args in true end
+ handle Pattern => false
+ else forall pattern args
+ end;
+
end;
--- a/src/Pure/thm.ML Tue Apr 21 17:25:19 1998 +0200
+++ b/src/Pure/thm.ML Wed Apr 22 14:04:35 1998 +0200
@@ -1479,7 +1479,7 @@
(* basic components *)
-type rrule = {thm: thm, lhs: term, perm: bool};
+type rrule = {thm: thm, lhs: term, elhs: term, fo: bool, perm: bool};
type cong = {thm: thm, lhs: term};
type simproc =
{name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
@@ -1570,10 +1570,16 @@
(* add_simps *)
+fun mk_rrule2{thm,lhs,perm} =
+ let val elhs = Pattern.eta_contract lhs
+ val fo = Pattern.first_order elhs orelse not(Pattern.pattern elhs)
+ in {thm=thm,lhs=lhs,elhs=elhs,fo=fo,perm=perm} end
+
fun insert_rrule(mss as Mss {rules,...},
- rrule as {thm = thm, lhs = lhs, perm = perm}) =
+ rrule as {thm,lhs,perm}) =
(trace_thm false "Adding rewrite rule:" thm;
- let val rules' = Net.insert_term ((lhs, rrule), rules, eq_rrule)
+ let val rrule2 as {elhs,...} = mk_rrule2 rrule
+ val rules' = Net.insert_term ((elhs, rrule2), rules, eq_rrule)
in upd_rules(mss,rules') end
handle Net.INSERT =>
(prthm true "Ignoring duplicate rewrite rule:" thm; mss));
@@ -1660,7 +1666,9 @@
else let val Mss{mk_rews={mk_sym,...},...} = mss
in case mk_sym thm of
None => []
- | Some thm' => rrule_eq_True(thm',rhs,lhs,mss,thm)
+ | Some thm' =>
+ let val (_,_,lhs',rhs',_) = decomp_simp thm'
+ in rrule_eq_True(thm',lhs',rhs',mss,thm) end
end
else rrule_eq_True(thm,lhs,rhs,mss,thm)
end;
@@ -1688,13 +1696,13 @@
(* del_simps *)
fun del_rrule(mss as Mss {rules,...},
- rrule as {thm = thm, lhs = lhs, perm = perm}) =
- (upd_rules(mss, Net.delete_term ((lhs, rrule), rules, eq_rrule))
+ rrule as {thm, elhs, ...}) =
+ (upd_rules(mss, Net.delete_term ((elhs, rrule), rules, eq_rrule))
handle Net.DELETE =>
(prthm true "Rewrite rule not in simpset:" thm; mss));
fun del_simps(mss,thms) =
- orient_comb_simps del_rrule (mk_rrule mss) (mss,thms);
+ orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule mss) (mss,thms);
(* add_congs *)
@@ -1834,6 +1842,10 @@
| renAbs(t) = t
in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
+fun incr_insts i (in1:(indexname*typ)list,in2:(indexname*term)list) =
+ let fun incr ((a,n),x) = ((a,n+i),x)
+ in (map incr in1, map incr in2) end;
+
fun add_insts_sorts ((iTs, is), Ss) =
add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss));
@@ -1844,7 +1856,7 @@
let val (_,prems,lhs,rhs,_) = decomp_simp thm
in if rewrite_rule_extra_vars prems lhs rhs
then (prthm true "Extra vars on rhs:" thm; [])
- else [{thm = thm, lhs = lhs, perm = false}]
+ else [mk_rrule2{thm = thm, lhs = lhs, perm = false}]
end;
@@ -1867,17 +1879,18 @@
let
val signt = Sign.deref sign_reft;
val tsigt = Sign.tsig_of signt;
- fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...}, lhs, perm} =
+ fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...},
+ lhs, elhs, fo, perm} =
let
val _ = if Sign.subsig (Sign.deref sign_ref, signt) then ()
else (trace_thm true "Rewrite rule from different theory:" thm;
raise Pattern.MATCH);
val rprop = if maxt = ~1 then prop
else Logic.incr_indexes([],maxt+1) prop;
- val rlhs = if maxt = ~1 then lhs
- else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
- val insts = Pattern.match tsigt (rlhs,t);
- val prop' = ren_inst(insts,rprop,rlhs,t);
+ val insts = if fo then Pattern.first_order_match tsigt (elhs,t)
+ else Pattern.match tsigt (elhs,t);
+ val insts = if maxt = ~1 then insts else incr_insts (maxt+1) insts
+ val prop' = ren_inst(insts,rprop,lhs,t);
val hyps' = union_term(hyps,hypst);
val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
val unconditional = (Logic.count_prems(prop',0) = 0);
@@ -1906,7 +1919,7 @@
in case opt of None => rews rrules | some => some end;
fun sort_rrules rrs = let
- fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of
+ fun is_simple({thm as Thm{prop,...}, ...}:rrule) = case prop of
Const("==",_) $ _ $ _ => true
| _ => false
fun sort [] (re1,re2) = re1 @ re2
@@ -1928,8 +1941,7 @@
| some => some)))
else proc_rews eta_t ps;
in case t of
- Abs (_, _, body) $ u =>
- Some (subst_bound (u, body), etc)
+ Abs (_, _, body) $ u => Some (subst_bound (u, body), etc)
| _ => (case rews (sort_rrules (Net.match_term rules t)) of
None => proc_rews (Pattern.eta_contract t)
(Net.match_term procs t)
@@ -2045,7 +2057,7 @@
and mut_impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) =
let
- fun uncond({thm,lhs,...}:rrule) =
+ fun uncond({thm,lhs,perm}) =
if nprems_of thm = 0 then Some lhs else None
val (lhss1,mss1) =