Add term_ and value_ ML antiquotations

examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy

@@ -404,6 +404,17 @@ a referentiable meta-object of class \<^theory_text>\<open>cid\<close> is create
 The SML-code is type-checked and executed 
 in the context of the SML toplevel of the Isabelle system as in the corresponding 
 \<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
+Additionally, ML antiquotations were added to check and evaluate terms with
+term antiquotations:
+\<^item> \<^theory_text>\<open>@{term_ \<open>term\<close> }\<close> parses and type-checks \<open>term\<close> with term antiquotations,
+  for instance \<^theory_text>\<open>@{term_ \<open>@{cenelec-term \<open>FT\<close>}\<close>}\<close> will parse and check
+  that \<open>FT\<close> is indeed an instance of the class \<^typ>\<open>cenelec_term\<close>,
+\<^item> \<^theory_text>\<open>@{value_ \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close> with term antiquotations,
+  for instance \<^theory_text>\<open>@{value_ \<open>mcc @{cenelec-term \<open>FT\<close>}\<close>}\<close>
+  will print the value of the \<^const>\<open>mcc\<close> attribute of the instance \<open>FT\<close>.
+  \<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator:
+  \<open>@{value_ [nbe] \<open>mcc @{cenelec-term \<open>FT\<close>}\<close>}\<close> forces \<open>value_\<close> to evaluate
+  the term using normalization by evaluation (see @{cite "wenzel:isabelle-isar:2020"}).
 \<close>
 
 (*<*)
@@ -435,7 +446,6 @@ Note unspecified attribute values were represented by free fresh variables which
 to choose either the normalization-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
 the \<^theory_text>\<open>auto\<close> method. A failure of these strategies will be reported and regarded as non-validation
 of this meta-object. The latter leads to a failure of the entire command.
-
 \<close>
 
 (*<*)

src/DOF/Isa_DOF.thy

@@ -1405,11 +1405,12 @@ fun value_select name ctxt =
   then default_value ctxt
   else Name_Space.get (Evaluators.get (Proof_Context.theory_of ctxt)) name ctxt;
 
-fun value_select' name ctxt =
-  if name = ""
+fun value_select' raw_name ctxt =
+  if raw_name = ""
   then (DOF_core.elaborate_term ctxt) #> default_value ctxt
   else (DOF_core.elaborate_term ctxt)
-       #> Name_Space.get (Evaluators.get (Proof_Context.theory_of ctxt)) name ctxt;
+       #> (let val name = intern_evaluator (Proof_Context.theory_of ctxt) raw_name in
+           Name_Space.get (Evaluators.get (Proof_Context.theory_of ctxt)) name ctxt end);
 
 val value = value_select' ""
 
@@ -1902,14 +1903,22 @@ val _ =
 local 
   fun pretty_term_style ctxt (style: term -> term, t) =
       Document_Output.pretty_term ctxt (style (DOF_core.check_term ctxt t));
+  fun print_term ctxt t = ML_Syntax.print_term (DOF_core.check_term (Context.proof_of ctxt) t)
 in
 val _ = Theory.setup
   (Document_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value_\<close>
     (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
     (fn ctxt => fn ((name, style), t) =>
       Document_Output.pretty_term ctxt (style (value_select' name ctxt t)))
+  #> ML_Antiquotation.inline_embedded \<^binding>\<open>value_\<close>
+      ((Scan.lift opt_evaluator -- Args.term)
+      #> (fn ((name, t),(ctxt, ts)) =>
+           (((value_select' name (Context.proof_of ctxt) t)
+             |> (ML_Syntax.atomic o (print_term ctxt))), (ctxt, ts))))
   #> Document_Output.antiquotation_pretty_source_embedded \<^binding>\<open>term_\<close> 
-             (Term_Style.parse -- Args.term) pretty_term_style)
+             (Term_Style.parse -- Args.term) pretty_term_style
+  #> ML_Antiquotation.inline_embedded \<^binding>\<open>term_\<close>
+       (fn (ctxt, ts) => (Args.term >> (ML_Syntax.atomic o (print_term ctxt))) (ctxt, ts)))
 end
 
 (* setup evaluators  *)

src/tests/TermAntiquotations.thy

@@ -118,5 +118,17 @@ We can print the term @{term_ \<open>r @{F \<open>xcv4\<close>}\<close>} with \<
 or get the value of the \<^const>\<open>F.r\<close> attribute of @{docitem \<open>xcv4\<close>} with \<open>@{value_ \<open>r @{F \<open>xcv4\<close>}\<close>}\<close>
 \<close>
 
+text\<open>There also are \<^theory_text>\<open>term_\<close> and \<^theory_text>\<open>value_\<close> ML antiquotations:
+\<^ML>\<open>@{term_ \<open>r @{F \<open>xcv4\<close>}\<close>}\<close> will return the ML representation of the term \<^term_>\<open>r @{F \<open>xcv4\<close>}\<close>,
+and \<^ML>\<open>@{value_ \<open>r @{F \<open>xcv4\<close>}\<close>}\<close> will return the ML representation
+of the value of the \<^const>\<open>F.r\<close> attribute of @{docitem \<open>xcv4\<close>}.
+\<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator:
+\<close>
+
+ML\<open>
+val t = @{term_ \<open>r @{F \<open>xcv4\<close>}\<close>}
+val tt = @{value_ [nbe] \<open>r @{F \<open>xcv4\<close>}\<close>}
+\<close>
+
 end