# HG changeset patch
# User haftmann
# Date 1747851223 -7200
# Node ID d374a7eb121abbda1cc198ff6b9702ff49a17a9a
# Parent  e153ab596247086bbb79739d0669b618a2a213aa
provide modern interface for solvers

diff -r e153ab596247 -r d374a7eb121a src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Wed May 21 20:13:43 2025 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed May 21 20:13:43 2025 +0200
@@ -955,10 +955,14 @@
   @{define_ML_type solver} \\
   @{define_ML Simplifier.mk_solver: "string ->
   (Proof.context -> int -> tactic) -> solver"} \\
-  @{define_ML_infix setSolver: "Proof.context * solver -> Proof.context"} \\
-  @{define_ML_infix addSolver: "Proof.context * solver -> Proof.context"} \\
-  @{define_ML_infix setSSolver: "Proof.context * solver -> Proof.context"} \\
-  @{define_ML_infix addSSolver: "Proof.context * solver -> Proof.context"} \\
+  @{define_ML Simplifier.set_safe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.add_safe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.set_unsafe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.add_unsafe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
   \end{mldecls}
 
   A solver is a tactic that attempts to solve a subgoal after simplification.
@@ -989,14 +993,14 @@
   \<^descr> \<^ML>\<open>Simplifier.mk_solver\<close>~\<open>name tac\<close> turns \<open>tac\<close> into a solver; the
   \<open>name\<close> is only attached as a comment and has no further significance.
 
-  \<^descr> \<open>ctxt setSSolver solver\<close> installs \<open>solver\<close> as the safe solver of \<open>ctxt\<close>.
+  \<^descr> \<^ML>\<open>Simplifier.set_safe_solver\<close>~\<open>solver ctxt\<close> installs \<open>solver\<close> as the safe solver of \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt addSSolver solver\<close> adds \<open>solver\<close> as an additional safe solver; it
+  \<^descr> \<^ML>\<open>Simplifier.add_safe_solver\<close>~\<open>solver ctxt\<close> adds \<open>solver\<close> as an additional safe solver; it
   will be tried after the solvers which had already been present in \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt setSolver solver\<close> installs \<open>solver\<close> as the unsafe solver of \<open>ctxt\<close>.
+  \<^descr> \<^ML>\<open>Simplifier.set_unsafe_solver\<close>~\<open>solver ctxt\<close> installs \<open>solver\<close> as the unsafe solver of \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt addSolver solver\<close> adds \<open>solver\<close> as an additional unsafe solver; it
+  \<^descr> \<^ML>\<open>Simplifier.add_unsafe_solver\<close>~\<open>solver ctxt\<close> adds \<open>solver\<close> as an additional unsafe solver; it
   will be tried after the solvers which had already been present in \<open>ctxt\<close>.
 
 
diff -r e153ab596247 -r d374a7eb121a src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed May 21 20:13:43 2025 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed May 21 20:13:43 2025 +0200
@@ -108,6 +108,10 @@
   val del_loop: string -> Proof.context -> Proof.context
   val solvers: Proof.context -> solver list * solver list
   val solver: Proof.context -> solver -> int -> tactic
+  val set_safe_solver: solver -> Proof.context -> Proof.context
+  val add_safe_solver: solver -> Proof.context -> Proof.context
+  val set_unsafe_solver: solver -> Proof.context -> Proof.context
+  val add_unsafe_solver: solver -> Proof.context -> Proof.context
   val set_solvers: solver list -> Proof.context -> Proof.context
   val default_mk_sym: Proof.context -> thm -> thm option
   val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->
@@ -893,22 +897,30 @@
 
 fun ctxt delloop name = ctxt |> del_loop name;
 
-fun ctxt setSSolver solver = ctxt |> map_simpset2
+fun set_safe_solver solver = map_simpset2
   (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
     (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
 
-fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord,
+fun ctxt setSSolver solver = ctxt |> set_safe_solver solver;
+
+fun add_safe_solver solver = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
 
-fun ctxt setSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord,
+fun ctxt addSSolver solver = ctxt |> add_safe_solver solver;
+
+fun set_unsafe_solver solver = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, ([solver], solvers)));
 
-fun ctxt addSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord,
+fun ctxt setSolver solver = ctxt |> set_unsafe_solver solver;
+
+fun add_unsafe_solver solver = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
 
+fun ctxt addSolver solver = ctxt |> add_unsafe_solver solver;
+
 fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (solvers, solvers)));