# HG changeset patch # User wenzelm # Date 1132406465 -3600 # Node ID dbdcf366db53ab054cfaead2b08d11523c69d4c0 # Parent 9edbeda7e39af4b9d1c0b12c9d1aa92372fa160d simpset: added reorient field, set_reorient; diff -r 9edbeda7e39a -r dbdcf366db53 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Sat Nov 19 14:21:04 2005 +0100 +++ b/src/Pure/meta_simplifier.ML Sat Nov 19 14:21:05 2005 +0100 @@ -35,7 +35,8 @@ {mk: thm -> thm list, mk_cong: thm -> thm, mk_sym: thm -> thm option, - mk_eq_True: thm -> thm option}, + mk_eq_True: thm -> thm option, + reorient: theory -> term list -> term -> term -> bool}, termless: term * term -> bool, subgoal_tac: simpset -> int -> tactic, loop_tacs: (string * (simpset -> int -> tactic)) list, @@ -89,6 +90,7 @@ val context: Context.proof -> simpset -> simpset val theory_context: theory -> simpset -> simpset val debug_bounds: bool ref + val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset val set_solvers: solver list -> simpset -> simpset val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> cterm -> thm @@ -163,7 +165,8 @@ {mk: thm -> thm list, mk_cong: thm -> thm, mk_sym: thm -> thm option, - mk_eq_True: thm -> thm option}; + mk_eq_True: thm -> thm option, + reorient: theory -> term list -> term -> term -> bool}; datatype simpset = Simpset of @@ -313,47 +316,6 @@ end; -(* empty simpsets *) - -fun init_ss mk_rews termless subgoal_tac solvers = - make_simpset ((Net.empty, [], (0, []), NONE), - (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers)); - -val basic_mk_rews: mk_rews = - {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], - mk_cong = I, - mk_sym = SOME o Drule.symmetric_fun, - mk_eq_True = K NONE}; - -val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []); - - -(* merge simpsets *) (*NOTE: ignores some fields of 2nd simpset*) - -fun merge_ss (ss1, ss2) = - let - val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, context = _}, - {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, - loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; - val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, context = _}, - {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, - loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; - - val rules' = Net.merge eq_rrule (rules1, rules2); - val prems' = gen_merge_lists Drule.eq_thm_prop prems1 prems2; - val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; - val congs' = gen_merge_lists (eq_cong o pairself #2) congs1 congs2; - val weak' = merge_lists weak1 weak2; - val procs' = Net.merge eq_proc (procs1, procs2); - val loop_tacs' = merge_alists loop_tacs1 loop_tacs2; - val unsafe_solvers' = merge_solvers unsafe_solvers1 unsafe_solvers2; - val solvers' = merge_solvers solvers1 solvers2; - in - make_simpset ((rules', prems', bounds', NONE), ((congs', weak'), procs', - mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'))) - end; - - (* simprocs *) exception SIMPROC_FAIL of string * exn; @@ -400,13 +362,6 @@ theory_context thy ss); -(* clear_ss *) - -fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) = - init_ss mk_rews termless subgoal_tac solvers - |> inherit_context ss; - - (* addsimps *) fun mk_rrule2 {thm, name, lhs, elhs, perm} = @@ -442,7 +397,7 @@ not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems))); (*simple test for looping rewrite rules and stupid orientations*) -fun reorient thy prems lhs rhs = +fun default_reorient thy prems lhs rhs = rewrite_rule_extra_vars prems lhs rhs orelse is_Var (head_of lhs) @@ -511,19 +466,20 @@ end; fun orient_rrule ss (thm, name) = - let val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm in + let + val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm; + val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss; + in if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] else if reorient thy prems lhs rhs then if reorient thy prems rhs lhs then mk_eq_True ss (thm, name) else - let val Simpset (_, {mk_rews = {mk_sym, ...}, ...}) = ss in - (case mk_sym thm of - NONE => [] - | SOME thm' => - let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm' - in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end) - end + (case mk_sym thm of + NONE => [] + | SOME thm' => + let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm' + in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end) else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm) end; @@ -658,26 +614,31 @@ local -fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True}, +fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient}, termless, subgoal_tac, loop_tacs, solvers) => - let val (mk', mk_cong', mk_sym', mk_eq_True') = f (mk, mk_cong, mk_sym, mk_eq_True) in - (congs, procs, {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'}, - termless, subgoal_tac, loop_tacs, solvers) - end); + let + val (mk', mk_cong', mk_sym', mk_eq_True', reorient') = + f (mk, mk_cong, mk_sym, mk_eq_True, reorient); + val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True', + reorient = reorient'}; + in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end); in -fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True) => - (mk, mk_cong, mk_sym, mk_eq_True)); +fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => + (mk, mk_cong, mk_sym, mk_eq_True, reorient)); -fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True) => - (mk, mk_cong, mk_sym, mk_eq_True)); +fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) => + (mk, mk_cong, mk_sym, mk_eq_True, reorient)); -fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True) => - (mk, mk_cong, mk_sym, mk_eq_True)); +fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) => + (mk, mk_cong, mk_sym, mk_eq_True, reorient)); -fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _) => - (mk, mk_cong, mk_sym, mk_eq_True)); +fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) => + (mk, mk_cong, mk_sym, mk_eq_True, reorient)); + +fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) => + (mk, mk_cong, mk_sym, mk_eq_True, reorient)); end; @@ -738,6 +699,52 @@ subgoal_tac, loop_tacs, (solvers, solvers))); +(* empty *) + +fun init_ss mk_rews termless subgoal_tac solvers = + make_simpset ((Net.empty, [], (0, []), NONE), + (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers)); + +fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) = + init_ss mk_rews termless subgoal_tac solvers + |> inherit_context ss; + +val basic_mk_rews: mk_rews = + {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], + mk_cong = I, + mk_sym = SOME o Drule.symmetric_fun, + mk_eq_True = K NONE, + reorient = default_reorient}; + +val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []); + + +(* merge *) (*NOTE: ignores some fields of 2nd simpset*) + +fun merge_ss (ss1, ss2) = + let + val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, context = _}, + {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, + loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; + val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, context = _}, + {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, + loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; + + val rules' = Net.merge eq_rrule (rules1, rules2); + val prems' = gen_merge_lists Drule.eq_thm_prop prems1 prems2; + val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; + val congs' = gen_merge_lists (eq_cong o pairself #2) congs1 congs2; + val weak' = merge_lists weak1 weak2; + val procs' = Net.merge eq_proc (procs1, procs2); + val loop_tacs' = merge_alists loop_tacs1 loop_tacs2; + val unsafe_solvers' = merge_solvers unsafe_solvers1 unsafe_solvers2; + val solvers' = merge_solvers solvers1 solvers2; + in + make_simpset ((rules', prems', bounds', NONE), ((congs', weak'), procs', + mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'))) + end; + + (** rewriting **)