# HG changeset patch
# User wenzelm
# Date 1697833145 -7200
# Node ID 62616d8422c5cd955a1277cf75f948ca6ae9f3f1
# Parent  d4e9d6b7f48d5455841fa4d64a11ad3462825bdb
added ML antiquotation "simproc_setup";

diff -r d4e9d6b7f48d -r 62616d8422c5 NEWS
--- a/NEWS	Fri Oct 20 16:40:41 2023 +0200
+++ b/NEWS	Fri Oct 20 22:19:05 2023 +0200
@@ -31,6 +31,15 @@
 the current thread attributes (normally interruptible). Various examples
 occur in the Isabelle sources (.ML and .thy files).
 
+* ML antiquotation "simproc_setup" inlines an invocation of
+Simplifier.simproc_setup, using the same concrete syntax as the
+corresponding Isar command. This allows to introduce a new simproc
+conveniently within an ML module, and refer directly to its ML value.
+For example, the simproc "Record.eq" is defined in
+~~/src/HOL/Tools/record.ML as follows:
+
+  val eq_simproc = \<^simproc_setup>\<open>eq ("r = s") = \<open>K eq_proc\<close>\<close>;
+
 * Isabelle/ML explicitly rejects 'handle' with catch-all patterns.
 INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or
 as last resort declare [[ML_catch_all]] within the theory context.
diff -r d4e9d6b7f48d -r 62616d8422c5 etc/symbols
--- a/etc/symbols	Fri Oct 20 16:40:41 2023 +0200
+++ b/etc/symbols	Fri Oct 20 22:19:05 2023 +0200
@@ -478,6 +478,7 @@
 \<^scala_type>          argument: cartouche
 \<^session>             argument: cartouche
 \<^simproc>             argument: cartouche
+\<^simproc_setup>       argument: cartouche
 \<^sort>                argument: cartouche
 \<^syntax_const>        argument: cartouche
 \<^system_option>       argument: cartouche
diff -r d4e9d6b7f48d -r 62616d8422c5 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Fri Oct 20 16:40:41 2023 +0200
+++ b/lib/texinputs/isabellesym.sty	Fri Oct 20 22:19:05 2023 +0200
@@ -467,6 +467,7 @@
 \newcommand{\isactrlscalaUNDERSCOREobject}{\isakeywordcontrol{scala{\isacharunderscore}object}}
 \newcommand{\isactrlscalaUNDERSCOREtype}{\isakeywordcontrol{scala{\isacharunderscore}type}}
 \newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
+\newcommand{\isactrlsimprocUNDERSCOREsetup}{\isakeywordcontrol{simproc{\isacharunderscore}setup}}
 \newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
 \newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}
 \newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}}
diff -r d4e9d6b7f48d -r 62616d8422c5 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Oct 20 16:40:41 2023 +0200
+++ b/src/HOL/Tools/record.ML	Fri Oct 20 22:19:05 2023 +0200
@@ -1115,10 +1115,7 @@
     | _ => NONE)
   end;
 
-val simproc =
-  Simplifier.simproc_setup
-   {passive = false, name = \<^binding>\<open>select_update\<close>, lhss = ["x::'a::{}"],
-     proc = K select_update_proc};
+val simproc = \<^simproc_setup>\<open>select_update ("x::'a::{}") = \<open>K select_update_proc\<close>\<close>
 
 fun get_upd_acc_cong_thm upd acc thy ss =
   let
@@ -1283,9 +1280,7 @@
     else NONE
   end;
 
-val upd_simproc =
-  Simplifier.simproc_setup
-    {passive = false, name = \<^binding>\<open>update\<close>, lhss = ["x::'a::{}"], proc = K upd_proc};
+val upd_simproc = \<^simproc_setup>\<open>update ("x::'a::{}") = \<open>K upd_proc\<close>\<close>
 
 end;
 
@@ -1316,9 +1311,7 @@
           | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
   | _ => NONE);
 
-val eq_simproc =
-  Simplifier.simproc_setup
-    {passive = false, name = \<^binding>\<open>eq\<close>, lhss = ["r = s"], proc = K eq_proc};
+val eq_simproc = \<^simproc_setup>\<open>eq ("r = s") = \<open>K eq_proc\<close>\<close>;
 
 
 (* split_simproc *)
@@ -1395,9 +1388,7 @@
     | _ => NONE)
   end;
 
-val ex_sel_eq_simproc =
-  Simplifier.simproc_setup
-    {passive = true, name = \<^binding>\<open>ex_sel_eq\<close>, lhss = ["Ex t"], proc = K ex_sel_eq_proc};
+val ex_sel_eq_simproc = \<^simproc_setup>\<open>passive ex_sel_eq ("Ex t") = \<open>K ex_sel_eq_proc\<close>\<close>;
 
 
 (* split_simp_tac *)
diff -r d4e9d6b7f48d -r 62616d8422c5 src/Pure/ex/Def.thy
--- a/src/Pure/ex/Def.thy	Fri Oct 20 16:40:41 2023 +0200
+++ b/src/Pure/ex/Def.thy	Fri Oct 20 22:19:05 2023 +0200
@@ -65,9 +65,7 @@
 
 (* simproc setup *)
 
-val _ =
-  Simplifier.simproc_setup
-    {passive = false, name = \<^binding>\<open>expand_def\<close>, lhss = ["x::'a"], proc = K get_def};
+val _ = \<^simproc_setup>\<open>expand_def ("x::'a") = \<open>K get_def\<close>\<close>;
 
 
 (* Isar command *)
diff -r d4e9d6b7f48d -r 62616d8422c5 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Oct 20 16:40:41 2023 +0200
+++ b/src/Pure/simplifier.ML	Fri Oct 20 22:19:05 2023 +0200
@@ -41,9 +41,9 @@
     {lhss: term list, proc: morphism -> proc} -> simproc
   val define_simproc: {passive: bool, name: binding, lhss: term list, proc: morphism -> proc} ->
     local_theory -> simproc * local_theory
-  val define_simproc_cmd: {passive: bool, name: binding, lhss: string list, proc: morphism -> proc} ->
-    local_theory -> simproc * local_theory
   val simproc_setup:
+    {passive: bool, name: binding, lhss: term list, proc: morphism -> proc} -> simproc
+  val simproc_setup_cmd:
     {passive: bool, name: binding, lhss: string list, proc: morphism -> proc} -> simproc
   val simproc_setup_command: (local_theory -> local_theory) parser
   val pretty_simpset: bool -> Proof.context -> Pretty.T
@@ -134,12 +134,10 @@
       {lhss = lhss', proc = Morphism.entity proc}
   end;
 
-local
-
-fun def_simproc prep {passive, name, lhss, proc} lthy =
+fun define_simproc {passive, name, lhss, proc} lthy =
   let
     val simproc0 =
-      make_simproc lthy (Local_Theory.full_name lthy name) {lhss = prep lthy lhss, proc = proc};
+      make_simproc lthy (Local_Theory.full_name lthy name) {lhss = lhss, proc = proc};
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of name}
       (fn phi => fn context =>
@@ -154,15 +152,16 @@
     |> pair simproc0
   end;
 
-in
 
-val define_simproc = def_simproc Syntax.check_terms;
-val define_simproc_cmd = def_simproc Syntax.read_terms;
+(* simproc_setup with concrete syntax *)
 
-end;
+val simproc_setup =
+  Named_Target.setup_result Raw_Simplifier.transform_simproc o define_simproc;
 
-
-(* implicit simproc_setup *)
+fun simproc_setup_cmd {passive, name, lhss, proc} =
+  Named_Target.setup_result Raw_Simplifier.transform_simproc (fn lthy =>
+    lthy |> define_simproc
+      {passive = passive, name = name, lhss = Syntax.read_terms lthy lhss, proc = proc});
 
 val simproc_setup_parser =
   Scan.optional (Parse.$$$ "passive" >> K true) false --
@@ -171,22 +170,37 @@
     (Parse.$$$ "=" |-- Parse.ML_source)
   >> (fn (((a, b), c), d) => {passive = a, name = b, lhss = c, proc = d});
 
-fun simproc_setup_ml {name, passive, lhss, proc} =
-  ML_Lex.read
-    ("{passive = " ^ Bool.toString passive ^
-     ", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^
-     ", lhss = " ^ ML_Syntax.print_strings lhss ^
-     ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read ")}";
+val _ = Theory.setup
+  (ML_Context.add_antiquotation_embedded \<^binding>\<open>simproc_setup\<close>
+    (fn _ => fn input => fn ctxt =>
+      let
+        val ml = ML_Lex.tokenize_no_range;
+
+        val {passive, name, lhss, proc} = input
+          |> Parse.read_embedded ctxt (Thy_Header.get_keywords' ctxt) simproc_setup_parser;
+        val lhss' = Syntax.read_terms ctxt lhss;
 
-fun simproc_setup args =
-  Named_Target.setup_result Raw_Simplifier.transform_simproc
-    (define_simproc_cmd args);
+        val (decl, ctxt') = ML_Context.read_antiquotes proc ctxt;
+        fun decl' ctxt'' =
+          let
+            val (ml_env, ml_body) = decl ctxt'';
+            val ml_body' =
+              ml "Simplifier.simproc_setup {passive = " @ ml (Bool.toString passive) @
+              ml ", name = " @ ml (ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name)) @
+              ml ", lhss = " @ ml (ML_Syntax.print_list ML_Syntax.print_term lhss') @
+              ml ", proc = (" @ ml_body @ ml ")}";
+          in (ml_env, ml_body') end;
+      in (decl', ctxt') end));
 
 val simproc_setup_command =
-  simproc_setup_parser >> (fn args =>
+  simproc_setup_parser >> (fn {passive, name, lhss, proc} =>
     Context.proof_map
-      (ML_Context.expression (Input.pos_of (#proc args))
-        (ML_Lex.read "Simplifier.simproc_setup " @ simproc_setup_ml args)));
+      (ML_Context.expression (Input.pos_of proc)
+        (ML_Lex.read
+          ("Simplifier.simproc_setup_cmd {passive = " ^ Bool.toString passive ^
+           ", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^
+           ", lhss = " ^ ML_Syntax.print_strings lhss ^
+           ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read ")}")));