support for ML special forms: modified evaluation similar to Scheme;
authorwenzelm
Fri, 09 Apr 2021 22:06:59 +0200
changeset 73806 2f6855142a8c
parent 73805 a2c589d5e1e4
child 73807 53c148e39819
support for ML special forms: modified evaluation similar to Scheme;
NEWS
etc/symbols
src/HOL/Library/Countable.thy
src/HOL/Tools/Qelim/cooper.ML
src/Pure/General/antiquote.ML
src/Pure/ML/ml_antiquotation.ML
src/Pure/ML/ml_antiquotations.ML
--- a/NEWS	Fri Apr 09 21:07:11 2021 +0200
+++ b/NEWS	Fri Apr 09 22:06:59 2021 +0200
@@ -88,6 +88,10 @@
 
 *** ML ***
 
+* ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on
+the given ML expression, in contrast to functions "try" and "can" that
+modify application of a function.
+
 * External bash processes are always managed by Isabelle/Scala, in
 contrast to Isabelle2021 where this was only done for macOS on Apple
 Silicon.
--- a/etc/symbols	Fri Apr 09 21:07:11 2021 +0200
+++ b/etc/symbols	Fri Apr 09 22:06:59 2021 +0200
@@ -442,6 +442,7 @@
 \<^action>              code: 0x00261b  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
 \<^assert>
 \<^binding>             argument: cartouche
+\<^can>                 argument: cartouche
 \<^class>               argument: cartouche
 \<^class_syntax>        argument: cartouche
 \<^command_keyword>     argument: cartouche
@@ -480,6 +481,7 @@
 \<^theory>              argument: cartouche
 \<^theory_context>      argument: cartouche
 \<^tool>                argument: cartouche
+\<^try>                 argument: cartouche
 \<^typ>                 argument: cartouche
 \<^type_abbrev>         argument: cartouche
 \<^type_name>           argument: cartouche
--- a/src/HOL/Library/Countable.thy	Fri Apr 09 21:07:11 2021 +0200
+++ b/src/HOL/Library/Countable.thy	Fri Apr 09 22:06:59 2021 +0200
@@ -204,7 +204,7 @@
 
 ML \<open>
 fun countable_datatype_tac ctxt st =
-  (case try (fn () => HEADGOAL (old_countable_datatype_tac ctxt) st) () of
+  (case \<^try>\<open>HEADGOAL (old_countable_datatype_tac ctxt) st\<close> of
     SOME res => res
   | NONE => BNF_LFP_Countable.countable_datatype_tac ctxt st);
 
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Apr 09 21:07:11 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Apr 09 22:06:59 2021 +0200
@@ -739,8 +739,7 @@
     in
       if ntac then no_tac
       else
-        (case try (fn () =>
-            Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
+        (case \<^try>\<open>Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))\<close> of
           NONE => no_tac
         | SOME r => resolve_tac ctxt [r] i)
     end)
--- a/src/Pure/General/antiquote.ML	Fri Apr 09 21:07:11 2021 +0200
+++ b/src/Pure/General/antiquote.ML	Fri Apr 09 22:06:59 2021 +0200
@@ -9,6 +9,7 @@
   type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}
   type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
   datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
+  val the_text: 'a antiquote -> 'a
   type text_antiquote = Symbol_Pos.T list antiquote
   val text_antiquote_range: text_antiquote -> Position.range
   val text_range: text_antiquote list -> Position.range
@@ -32,6 +33,11 @@
 type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list};
 datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq;
 
+fun bad_text pos = error ("Unexpected antiquotation" ^ Position.here pos);
+fun the_text (Text x) = x
+  | the_text (Control {range, ...}) = bad_text (#1 range)
+  | the_text (Antiq {range, ...}) = bad_text (#1 range);
+
 type text_antiquote = Symbol_Pos.T list antiquote;
 
 fun text_antiquote_range (Text ss) = Symbol_Pos.range ss
--- a/src/Pure/ML/ml_antiquotation.ML	Fri Apr 09 21:07:11 2021 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Fri Apr 09 22:06:59 2021 +0200
@@ -18,6 +18,7 @@
   val inline_embedded: binding -> string context_parser -> theory -> theory
   val value: binding -> string context_parser -> theory -> theory
   val value_embedded: binding -> string context_parser -> theory -> theory
+  val special_form: binding -> string -> theory -> theory
 end;
 
 structure ML_Antiquotation: ML_ANTIQUOTATION =
@@ -63,6 +64,26 @@
 end;
 
 
+(* ML special form *)
+
+fun special_form binding operator =
+  ML_Context.add_antiquotation binding true
+    (fn _ => fn src => fn ctxt =>
+      let
+        val (s, _) = Token.syntax (Scan.lift Args.embedded_input) src ctxt;
+        val tokenize = ML_Lex.tokenize_range Position.no_range;
+        val tokenize_range = ML_Lex.tokenize_range (Input.range_of s);
+        fun decl (_: Proof.context) =
+          let
+            val expr = ML_Lex.read_source s |> map Antiquote.the_text;
+            val ml =
+              tokenize "let val expr = (fn () => " @ expr @ tokenize ");" @
+              tokenize " val " @ tokenize_range "result" @
+              tokenize (" = " ^ operator ^ " expr; in result end")
+          in ([], ml) end;
+      in (decl, ctxt) end);
+
+
 (* basic antiquotations *)
 
 val _ = Theory.setup
--- a/src/Pure/ML/ml_antiquotations.ML	Fri Apr 09 21:07:11 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Fri Apr 09 22:06:59 2021 +0200
@@ -180,6 +180,13 @@
         in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
 
 
+(* special forms *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.special_form \<^binding>\<open>try\<close> "() |> Basics.try" #>
+  ML_Antiquotation.special_form \<^binding>\<open>can\<close> "() |> Basics.can");
+
+
 (* basic combinators *)
 
 local