--- 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 **)