# 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>\eq ("r = s") = \K eq_proc\\; + * Isabelle/ML explicitly rejects 'handle' with catch-all patterns. INCOMPATIBILITY, better use \<^try>\...\ 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>\select_update\, lhss = ["x::'a::{}"], - proc = K select_update_proc}; +val simproc = \<^simproc_setup>\select_update ("x::'a::{}") = \K select_update_proc\\ 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>\update\, lhss = ["x::'a::{}"], proc = K upd_proc}; +val upd_simproc = \<^simproc_setup>\update ("x::'a::{}") = \K upd_proc\\ end; @@ -1316,9 +1311,7 @@ | SOME thm => SOME (thm RS @{thm Eq_TrueI}))) | _ => NONE); -val eq_simproc = - Simplifier.simproc_setup - {passive = false, name = \<^binding>\eq\, lhss = ["r = s"], proc = K eq_proc}; +val eq_simproc = \<^simproc_setup>\eq ("r = s") = \K eq_proc\\; (* split_simproc *) @@ -1395,9 +1388,7 @@ | _ => NONE) end; -val ex_sel_eq_simproc = - Simplifier.simproc_setup - {passive = true, name = \<^binding>\ex_sel_eq\, lhss = ["Ex t"], proc = K ex_sel_eq_proc}; +val ex_sel_eq_simproc = \<^simproc_setup>\passive ex_sel_eq ("Ex t") = \K ex_sel_eq_proc\\; (* 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>\expand_def\, lhss = ["x::'a"], proc = K get_def}; +val _ = \<^simproc_setup>\expand_def ("x::'a") = \K get_def\\; (* 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>\simproc_setup\ + (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 ")}")));