--- 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.
--- 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
--- 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}}
--- 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 *)
--- 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 *)
--- 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 ")}")));