# HG changeset patch # User nipkow # Date 893246675 -7200 # Node ID 8f6dbbd8d497e0c165f227c7dd670dcaba136472 # Parent ef2e8e2a10e13a2d994d2e265d3dea469cc2ec64 Tried to speed up the rewriter by eta-contracting all patterns beforehand and by classifying each pattern as to whether it allows first-order matching. diff -r ef2e8e2a10e1 -r 8f6dbbd8d497 src/Pure/pattern.ML --- 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; diff -r ef2e8e2a10e1 -r 8f6dbbd8d497 src/Pure/thm.ML --- 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) =