# HG changeset patch # User wenzelm # Date 869589943 -7200 # Node ID 2c833cb21f8d490aad2ccfae39983263aa9ea06e # Parent e8c8d76810a6aa00a656dfc5998abc9331cd2e8c added dest_mss, merge_mss; fixed matching of simproc lhss; diff -r e8c8d76810a6 -r 2c833cb21f8d src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Jul 22 17:52:47 1997 +0200 +++ b/src/Pure/thm.ML Tue Jul 22 18:45:43 1997 +0200 @@ -140,18 +140,21 @@ int -> thm -> thm Sequence.seq (*meta simplification*) + exception SIMPLIFIER of string * thm type meta_simpset - exception SIMPLIFIER of string * thm + val dest_mss : meta_simpset -> + {simps: thm list, congs: thm list, procs: (string * cterm list) list} val empty_mss : meta_simpset + val merge_mss : meta_simpset * meta_simpset -> meta_simpset val add_simps : meta_simpset * thm list -> meta_simpset val del_simps : meta_simpset * thm list -> meta_simpset val mss_of : thm list -> meta_simpset val add_congs : meta_simpset * thm list -> meta_simpset val del_congs : meta_simpset * thm list -> meta_simpset val add_simprocs : meta_simpset * - (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset + (string * cterm list * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset val del_simprocs : meta_simpset * - (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset + (string * cterm list * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset 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 @@ -164,7 +167,7 @@ val invoke_oracle : theory * Sign.sg * exn -> thm end; -structure Thm : THM = +structure Thm: THM = struct (*** Certified terms and types ***) @@ -1443,12 +1446,20 @@ type rrule = {thm: thm, lhs: term, perm: bool}; type cong = {thm: thm, lhs: term}; -type simproc = (Sign.sg -> term -> thm option) * stamp; +type simproc = {name: string, proc: Sign.sg -> term -> thm option, lhs: cterm, id: stamp}; -fun eq_rrule ({thm = Thm{prop = p1, ...}, ...}: rrule, +fun eq_rrule ({thm = Thm {prop = p1, ...}, ...}: rrule, {thm = Thm {prop = p2, ...}, ...}: rrule) = p1 aconv p2; -val eq_simproc = eq_snd; +fun eq_cong ({thm = Thm {prop = p1, ...}, ...}: cong, + {thm = Thm {prop = p2, ...}, ...}: cong) = p1 aconv p2; + +fun eq_prem (Thm {prop = p1, ...}, Thm {prop = p2, ...}) = p1 aconv p2; + +fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2); + +fun mk_simproc (name, proc, lhs, id) = + {name = name, proc = proc, lhs = lhs, id = id}; (* datatype mss *) @@ -1487,6 +1498,33 @@ (** simpset operations **) +(* dest_mss *) + +fun dest_mss (Mss {rules, congs, procs, ...}) = + {simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules), + congs = map (fn (_, {thm, ...}) => thm) congs, + procs = + map (fn (_, {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs) + |> partition_eq eq_snd + |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))}; + + +(* 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, ...}) = + mk_mss + (Net.merge (rules1, rules2, eq_rrule), + generic_merge (eq_cong o pairself snd) I I congs1 congs2, + Net.merge (procs1, procs2, eq_simproc), + merge_lists bounds1 bounds2, + generic_merge eq_prem I I prems1 prems2, + mk_rews, termless); + + (* mk_rrule *) fun vperm (Var _, Var _) = true @@ -1599,25 +1637,31 @@ (* add_simprocs *) -fun add_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, - (sign, lhs, proc, id)) = - (trace_term "Adding simplification procedure for:" sign lhs; +fun add_proc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, + (name, lhs as Cterm {sign, t, ...}, proc, id)) = + (trace_term ("Adding simplification procedure " ^ name ^ " for:") sign t; mk_mss (rules, congs, - Net.insert_term ((lhs, (proc, id)), procs, eq_simproc) handle Net.INSERT => - (trace_warning "ignored duplicate"; procs), + Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc) + handle Net.INSERT => (trace_warning "ignored duplicate"; procs), bounds, prems, mk_rews, termless)); +fun add_simproc (mss, (name, lhss, proc, id)) = + foldl add_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss); + val add_simprocs = foldl add_simproc; (* del_simprocs *) -fun del_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, - (sign:Sign.sg, lhs, proc, id)) = +fun del_proc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, + (name, lhs as Cterm {t, ...}, proc, id)) = mk_mss (rules, congs, - Net.delete_term ((lhs, (proc, id)), procs, eq_simproc) handle Net.DELETE => - (trace_warning "simplification procedure not in simpset"; procs), - bounds, prems, mk_rews, termless); + Net.delete_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc) + handle Net.DELETE => (trace_warning "simplification procedure not in simpset"; procs), + bounds, prems, mk_rews, termless); + +fun del_simproc (mss, (name, lhss, proc, id)) = + foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss); val del_simprocs = foldl del_simproc; @@ -1711,12 +1755,14 @@ (1) beta reduction (2) unconditional rewrite rules (3) conditional rewrite rules - (4) simplification procedures (* FIXME (un-)conditional !! *) + (4) simplification procedures *) fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, ...}) (shypst,hypst,maxt,t,ders) = - let fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} = + let + val tsigt = #tsig(Sign.rep_sg signt); + fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} = let val unit = if Sign.subsig(sign,signt) then () else (trace_thm_warning "rewrite rule from different theory" thm; @@ -1725,7 +1771,7 @@ 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 (#tsig(Sign.rep_sg signt)) (rlhs,t) + val insts = Pattern.match tsigt (rlhs,t); val prop' = ren_inst(insts,rprop,rlhs,t); val hyps' = union_term(hyps,hypst); val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst)); @@ -1734,7 +1780,7 @@ t = prop', T = propT, maxidx = maxidx'} - val der' = infer_derivs (RewriteC ct', [der]) (* FIXME fix!? *) + val der' = infer_derivs (RewriteC ct', [der]); val thm' = Thm{sign = signt, der = der', shyps = shyps', @@ -1756,6 +1802,7 @@ | rews (rrule :: rrules) = let val opt = rew rrule handle Pattern.MATCH => None 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 Const("==",_) $ _ $ _ => true @@ -1767,18 +1814,20 @@ in sort rrs ([],[]) end - fun proc_rews _ [] = None - | proc_rews eta_t ((f, _) :: fs) = - (case f signt eta_t of - None => proc_rews eta_t fs - | Some raw_thm => - (trace_thm "Proved rewrite rule: " raw_thm; - (case rews (mk_procrule raw_thm) of - None => proc_rews eta_t fs - | some => some))); + fun proc_rews _ ([]:simproc list) = None + | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) = + if Pattern.matches tsigt (plhs, t) then + (case proc signt eta_t of + None => proc_rews eta_t ps + | Some raw_thm => + (trace_thm ("Procedure" ^ name ^ " proved rewrite rule:") raw_thm; + (case rews (mk_procrule raw_thm) of + None => proc_rews eta_t ps + | some => some))) + else proc_rews eta_t ps; in (case t of - Abs (_, _, body) $ u => (* FIXME bug!? (because of beta/eta overlap) *) + Abs (_, _, body) $ u => Some (shypst, hypst, maxt, subst_bound (u, body), ders) | _ => (case rews (sort_rrules (Net.match_term rules t)) of @@ -1809,7 +1858,7 @@ T = propT, maxidx = maxidx'} val thm' = Thm{sign = signt, - der = infer_derivs (CongC ct', [der]), (* FIXME fix!? *) + der = infer_derivs (CongC ct', [der]), shyps = shyps', hyps = union_term(hyps,hypst), prop = prop',