# HG changeset patch # User nipkow # Date 907777057 -7200 # Node ID 75b513db9a3a17a1f7b4cf68bd1f056524269487 # Parent 5b56804edf85c90383cc7900387b67f895c8b359 Tuned simplifier not to re-normalized already normalized terms. diff -r 5b56804edf85 -r 75b513db9a3a src/Pure/thm.ML --- a/src/Pure/thm.ML Wed Oct 07 17:51:11 1998 +0200 +++ b/src/Pure/thm.ML Wed Oct 07 18:17:37 1998 +0200 @@ -1509,7 +1509,9 @@ (* A "mss" contains data needed during conversion: rules: discrimination net of rewrite rules; - congs: association list of congruence rules; + congs: association list of congruence rules and + a flag iff all of the congruences are 'full'. + A congruence is 'full' if it enforces normalization of all arguments. procs: discrimination net of simplification procedures (functions that prove rewrite rules on the fly); bounds: names of bound variables already used @@ -1524,7 +1526,7 @@ datatype meta_simpset = Mss of { rules: rrule Net.net, - congs: (string * cong) list, + congs: (string * cong) list * bool, procs: simproc Net.net, bounds: string list, prems: thm list, @@ -1542,7 +1544,8 @@ val empty_mss = let val mk_rews = {mk = K [], mk_sym = K None, mk_eq_True = K None} - in mk_mss (Net.empty, [], Net.empty, [], [], mk_rews, Term.termless) end; + in mk_mss (Net.empty, ([],true), Net.empty, [], [], mk_rews, Term.termless) + end; @@ -1552,7 +1555,7 @@ fun dest_mss (Mss {rules, congs, procs, ...}) = {simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules), - congs = map (fn (_, {thm, ...}) => thm) congs, + congs = map (fn (_, {thm, ...}) => thm) (fst congs), procs = map (fn (_, {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs) |> partition_eq eq_snd @@ -1562,13 +1565,14 @@ (* merge_mss *) (*NOTE: ignores mk_rews and termless of 2nd mss*) fun merge_mss - (Mss {rules = rules1, congs = congs1, procs = procs1, bounds = bounds1, - prems = prems1, mk_rews, termless}, - Mss {rules = rules2, congs = congs2, procs = procs2, bounds = bounds2, - prems = prems2, ...}) = + (Mss {rules = rules1, congs = (congs1,full1), procs = procs1, + bounds = bounds1, prems = prems1, mk_rews, termless}, + Mss {rules = rules2, congs = (congs2,full2), procs = procs2, + bounds = bounds2, prems = prems2, ...}) = mk_mss (Net.merge (rules1, rules2, eq_rrule), - generic_merge (eq_cong o pairself snd) I I congs1 congs2, + (generic_merge (eq_cong o pairself snd) I I congs1 congs2, + full1 andalso full2), Net.merge (procs1, procs2, eq_simproc), merge_lists bounds1 bounds2, generic_merge eq_prem I I prems1 prems2, @@ -1713,6 +1717,33 @@ (* add_congs *) +(*FIXME -> term.ML *) +fun is_Bound (Bound _) = true +fun is_Bound _ = false; + +fun is_full_cong_prems [] varpairs = null varpairs + | is_full_cong_prems (p::prems) varpairs = + (case Logic.strip_assums_concl p of + Const("==",_) $ lhs $ rhs => + let val (x,xs) = strip_comb lhs and (y,ys) = strip_comb rhs + in is_Var x andalso forall is_Bound xs andalso + null(findrep(xs)) andalso xs=ys andalso + (x,y) mem varpairs andalso + is_full_cong_prems (p::prems) (varpairs\(x,y)) + end + | _ => false); + +fun is_full_cong (Thm{prop,...}) = +let val prems = Logic.strip_imp_prems prop + and concl = Logic.strip_imp_concl prop + val (lhs,rhs) = Logic.dest_equals concl + val (f,xs) = strip_comb lhs + and (g,ys) = strip_comb rhs +in + f=g andalso null(findrep(xs@ys)) andalso length xs = length ys andalso + is_full_cong_prems prems (xs ~~ ys) +end + fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) = let val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ => @@ -1720,9 +1751,11 @@ (* val lhs = Pattern.eta_contract lhs; *) val (a, _) = dest_Const (head_of lhs) handle TERM _ => raise SIMPLIFIER ("Congruence must start with a constant", thm); + val (alist,full) = congs + val full2 = full andalso is_full_cong thm in - mk_mss (rules, (a, {lhs = lhs, thm = thm}) :: congs, procs, bounds, - prems, mk_rews, termless) + mk_mss (rules, ((a, {lhs = lhs, thm = thm}) :: alist, full2), + procs, bounds, prems, mk_rews, termless) end; val (op add_congs) = foldl add_cong; @@ -1737,9 +1770,11 @@ (* val lhs = Pattern.eta_contract lhs; *) val (a, _) = dest_Const (head_of lhs) handle TERM _ => raise SIMPLIFIER ("Congruence must start with a constant", thm); + val (alist,full) = congs + val alist2 = filter (fn (x,_)=> x<>a) alist + val full2 = forall (fn(_,{thm,...}) => is_full_cong thm) alist2 in - mk_mss (rules, filter (fn (x,_)=> x<>a) congs, procs, bounds, - prems, mk_rews, termless) + mk_mss (rules, (alist2,full2), procs, bounds, prems, mk_rews, termless) end; val (op del_congs) = foldl del_cong; @@ -1830,7 +1865,8 @@ type termrec = (Sign.sg_ref * term list) * term; type conv = meta_simpset -> termrec -> termrec; -fun check_conv (thm as Thm{shyps,hyps,prop,sign_ref,der,...}, prop0, ders) = +fun check_conv + (thm as Thm{shyps,hyps,prop,sign_ref,der,...}, prop0, ders) = let fun err() = (trace_thm false "Proved wrong thm (Check subgoaler?)" thm; trace_term false "Should have proved:" (Sign.deref sign_ref) prop0; None) @@ -1873,6 +1909,15 @@ (* conversion to apply the meta simpset to a term *) +(* Since the rewriting strategy is bottom-up, we avoid re-normalizing already + normalized terms by carrying around the rhs of the rewrite rule just + applied. This is called the `skeleton'. It is decomposed in parallel + with the term. Once a Var is encountered, the corresponding term is + already in normal form. + skel0 is a dummy skeleton that is to enforce complete normalization. +*) +val skel0 = Bound 0; + (* we try in order: (1) beta reduction @@ -1885,7 +1930,7 @@ *) fun rewritec (prover,sign_reft,maxt) - (mss as Mss{rules, procs, termless, prems, ...}) + (mss as Mss{rules, procs, termless, prems, congs, ...}) (t:term,etc as (shypst,hypst,ders)) = let val signt = Sign.deref sign_reft; @@ -1916,12 +1961,18 @@ if perm andalso not(termless(rhs',lhs')) then None else (trace_thm false "Applying instance of rewrite rule:" thm; if unconditional - then (trace_thm false "Rewriting:" thm'; - Some(rhs', (shyps', hyps', der'::ders))) + then (trace_thm false "Rewriting:" thm'; + let val (_,rhs) = Logic.dest_equals prop + in Some((rhs', (shyps', hyps', der'::ders)), + if snd congs then rhs else skel0) + (* use rhs as depth-limit only if all congs are full *) + end) else (trace_thm false "Trying to rewrite:" thm'; case prover mss thm' of None => (trace_thm false "FAILED" thm'; None) - | Some(thm2) => check_conv(thm2,prop',ders))) + | Some(thm2) => + (case check_conv(thm2,prop',ders) of + None => None | Some trec => Some(trec,skel0)))) end fun rews [] = None @@ -1952,7 +2003,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),skel0) | _ => (case rews (sort_rrules (Net.match_term rules t)) of None => proc_rews (Pattern.eta_contract t) (Net.match_term procs t) @@ -1999,29 +2050,33 @@ fun bottomc ((simprem,useprem,mutsimp),prover,sign_ref,maxidx) = let - fun botc fail mss trec = - (case subc mss trec of + fun botc fail skel mss trec = + if is_Var skel then if fail then None else Some(trec) + else + (case subc skel mss trec of some as Some(trec1) => (case rewritec (prover,sign_ref,maxidx) mss trec1 of - Some(trec2) => botc false mss trec2 + Some(trec2,skel2) => botc false skel2 mss trec2 | None => some) | None => (case rewritec (prover,sign_ref,maxidx) mss trec of - Some(trec2) => botc false mss trec2 + Some(trec2,skel2) => botc false skel2 mss trec2 | None => if fail then None else Some(trec))) - and try_botc mss trec = (case botc true mss trec of - Some(trec1) => trec1 - | None => trec) + and try_botc mss trec = + (case botc true skel0 mss trec of + Some(trec1) => trec1 | None => trec) - and subc (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) + and subc skel + (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) (trec as (t0:term,etc:sort list*term list * rule mtree list)) = (case t0 of Abs(a,T,t) => let val b = variant bounds a val v = Free("." ^ b,T) val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless) - in case botc true mss' (subst_bound(v,t),etc) of + val skel' = case skel of Abs(_,_,sk) => sk | _ => skel0 + in case botc true skel' mss' (subst_bound(v,t),etc) of Some(t',etc') => Some(Abs(a, T, abstract_over(v,t')), etc') | None => None end @@ -2029,25 +2084,30 @@ Const("==>",_)$s => Some(impc(s,u,mss,etc)) | Abs(_,_,body) => let val trec = (subst_bound(u,body), etc) - in case subc mss trec of + in case subc skel0 mss trec of None => Some(trec) | trec => trec end | _ => let fun appc() = - (case botc true mss (t,etc) of + let val (tskel,uskel) = + case skel of tskel$uskel => (tskel,uskel) + | _ => (skel0,skel0) + in + (case botc true tskel mss (t,etc) of Some(t1,etc1) => - (case botc true mss (u,etc1) of + (case botc true uskel mss (u,etc1) of Some(u1,etc2) => Some(t1$u1, etc2) | None => Some(t1$u, etc1)) | None => - (case botc true mss (u,etc) of + (case botc true uskel mss (u,etc) of Some(u1,etc1) => Some(t$u1, etc1) | None => None)) + end val (h,ts) = strip_comb t in case h of Const(a,_) => - (case assoc_string(congs,a) of + (case assoc_string(fst congs,a) of None => appc() | Some(cong) => (congc (prover mss,sign_ref,maxidx) cong trec @@ -2092,9 +2152,9 @@ let val trec = disch1 trec2 in case rewritec (prover,sign_ref,maxidx) mss trec of None => (None,trec) - | Some(Const("==>",_)$prem$conc,etc) => + | Some((Const("==>",_)$prem$conc,etc),_) => mut_impc(prems,prem,conc,mss,etc) - | Some(trec') => (None,trec') + | Some(trec',_) => (None,trec') end fun simpconc() =