# HG changeset patch # User nipkow # Date 888676803 -3600 # Node ID 6328d427a3396160ab4b02b415352d6b37f661d7 # Parent b7c4e4ade1aa7257037c1e638e492e29bed12349 Tried to reorganize rewriter a little. More to be done. diff -r b7c4e4ade1aa -r 6328d427a339 src/Pure/logic.ML --- a/src/Pure/logic.ML Fri Feb 27 11:21:28 1998 +0100 +++ b/src/Pure/logic.ML Sat Feb 28 15:40:03 1998 +0100 @@ -324,11 +324,11 @@ orelse (null prems andalso Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs)) - orelse +(* orelse (case lhs of (f as Free _) $ (Var _) => exists (fn p => f occs p) prems orelse (null prems andalso f occs rhs) - | _ => false); + | _ => false)*); (*the condition "null prems" in the last cases is necessary because conditional rewrites with extra variables in the conditions may terminate although the rhs is an instance of the lhs. Example: diff -r b7c4e4ade1aa -r 6328d427a339 src/Pure/pattern.ML --- a/src/Pure/pattern.ML Fri Feb 27 11:21:28 1998 +0100 +++ b/src/Pure/pattern.ML Sat Feb 28 15:40:03 1998 +0100 @@ -25,6 +25,7 @@ val 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 exception Unif exception MATCH @@ -390,4 +391,15 @@ (*Predicate: does the pattern match the object?*) fun matches tsig po = (match tsig po; true) handle MATCH => false; +(* Does pat match a subterm of obj? *) +fun matches_subterm tsig (pat,obj) = + let fun msub(bounds,obj) = matches tsig (pat,obj) orelse + case obj of + Abs(x,T,t) => let val y = variant bounds x + val f = Free(":" ^ y,T) + in msub(x::bounds,subst_bound(f,t)) end + | s$t => msub(bounds,s) orelse msub(bounds,t) + | _ => false + in msub([],obj) end; + end; diff -r b7c4e4ade1aa -r 6328d427a339 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Feb 27 11:21:28 1998 +0100 +++ b/src/Pure/thm.ML Sat Feb 28 15:40:03 1998 +0100 @@ -164,7 +164,7 @@ val add_prems : meta_simpset * thm list -> meta_simpset val prems_of_mss : meta_simpset -> thm list val set_mk_rews : meta_simpset * (thm -> thm list) -> meta_simpset - val mk_rews_of_mss : meta_simpset -> thm -> thm list +(* val mk_rews_of_mss : meta_simpset -> thm -> thm list *) val set_termless : meta_simpset * (term * term -> bool) -> meta_simpset val trace_simp : bool ref val rewrite_cterm : bool * bool -> meta_simpset -> @@ -1575,33 +1575,39 @@ (* add_simps *) -fun add_simp - (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, - thm as Thm {sign_ref, prop, ...}) = - (case mk_rrule thm of +fun add_simp1(mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, + thm as Thm {sign_ref, prop, ...}) = + case mk_rrule thm of None => mss | Some (rrule as {lhs, ...}) => (trace_thm false "Adding rewrite rule:" thm; - mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule) handle Net.INSERT => - (prtm true "ignoring duplicate rewrite rule" (Sign.deref sign_ref) prop; rules), - congs, procs, bounds, prems, mk_rews, termless))); + mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule), + congs, procs, bounds, prems, mk_rews, termless) + handle Net.INSERT => + (prtm true "ignoring duplicate rewrite rule" (Sign.deref sign_ref) prop; + mss)); + +fun add_simp(mss as Mss{mk_rews,...},thm) = foldl add_simp1 (mss, mk_rews thm); val add_simps = foldl add_simp; -fun mss_of thms = add_simps (empty_mss, thms); +fun mss_of thms = foldl add_simp1 (empty_mss, thms); (* del_simps *) -fun del_simp - (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, - thm as Thm {sign_ref, prop, ...}) = - (case mk_rrule thm of +fun del_simp1(mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, + thm as Thm {sign_ref, prop, ...}) = + case mk_rrule thm of None => mss | Some (rrule as {lhs, ...}) => - mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule) handle Net.DELETE => - (prtm true "rewrite rule not in simpset" (Sign.deref sign_ref) prop; rules), - congs, procs, bounds, prems, mk_rews, termless)); + (mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule), + congs, procs, bounds, prems, mk_rews, termless) + handle Net.DELETE => + (prtm true "rewrite rule not in simpset" (Sign.deref sign_ref) prop; + mss)); + +fun del_simp(mss as Mss{mk_rews,...},thm) = foldl del_simp1 (mss, mk_rews thm); val del_simps = foldl del_simp; @@ -1951,7 +1957,7 @@ end) | _ => None) - and impc(shyps, hyps, s, u, mss as Mss{mk_rews,...}, ders) = + and impc(shyps, hyps, s, u, mss, ders) = let val (shyps1,hyps1,s1,ders1) = if simprem then try_botc mss (shyps,hyps,s,ders) else (shyps,hyps,s,ders); @@ -1963,7 +1969,7 @@ (Sign.deref sign_ref) s1; mss) else let val thm = assume (Cterm{sign_ref=sign_ref, t=s1, T=propT, maxidx= ~1}) - in add_simps(add_prems(mss,[thm]), mk_rews thm) end + in add_simp(add_prems(mss,[thm]), thm) end val (shyps2,hyps2,u1,ders2) = try_botc mss1 (shyps1,hyps1,u,ders1) val hyps3 = if gen_mem (op aconv) (s1, hyps1) then hyps2 else hyps2\s1