lib: add @{inline_tactic} and @{inline_method} ML antiquotations

This resurrects a useful part of the removed TacticAPI theory, with a
much more generic implementation.

lib/ROOT

@@ -51,6 +51,7 @@ session Lib (lib) = Word_Lib +
     MonadicRewrite
     HaskellLemmaBucket
     "ml-helpers/TermPatternAntiquote"
+    "ml-helpers/TacticAntiquotation"
     "subgoal_focus/Subgoal_Methods"
     Insulin
     ExtraCorres
@@ -155,6 +156,7 @@ session LibTest (lib) = Refine +
     Trace_Schematic_Insts_Test
     Local_Method_Tests
     Qualify_Test
+    "ml-helpers/TacticAntiquotation_Test"
   (* use virtual memory function as an example, only makes sense on ARM: *)
   theories [condition = "L4V_ARCH_IS_ARM"]
     Corres_Test

lib/ml-helpers/TacticAntiquotation.thy

@@ -0,0 +1,82 @@
+(*
+ * Copyright 2018, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+
+ * @TAG(DATA61_BSD)
+ *)
+
+(*
+ * This provides the ML antiquotations @{inline_tactic} and @{inline_method}.
+ * They take a string containing Isabelle method text and give you an ML
+ * Tactical.tactic or Method.method, respectively.
+ *
+ * See TacticAntiquotation_Test for examples.
+ *)
+
+theory TacticAntiquotation
+imports
+  Main
+begin
+
+ML \<open>
+structure TacticAntiquotation = struct
+
+(* Basically clagged from Pure/ML/ml_thms.ML *)
+
+structure Data = Proof_Data
+(
+  type T = (string * Method.text) list;
+  fun init _ = [];
+);
+
+fun method_binding kind method_text ctxt =
+  let
+    val initial = null (Data.get ctxt);
+    val (name, ctxt') = ML_Context.variant kind ctxt;
+    val ctxt'' = Data.map (cons (name, method_text)) ctxt';
+
+    fun decl final_ctxt = let
+      val method_text_ref = ML_Context.struct_name ctxt ^ "." ^ name;
+      (* XXX: it seems that we need to re-evaluate the method text every time
+       *      the method is run, otherwise Isabelle complains about a context
+       *      mismatch. Figure out how to avoid this *)
+      val method_val =
+            "(fn facts => fn st => Method.evaluate " ^ method_text_ref ^
+              (* XXX: is this the correct way to get dynamic context? *)
+              " (Context.the_local_context ()) facts st)";
+      val ml_body =
+            if kind = "inline_method"
+            then method_val
+            else "(fn st => Method.NO_CONTEXT_TACTIC " ^
+                   (* XXX: as above *)
+                   "(Context.the_local_context ()) (" ^ method_val ^ " []) st)";
+      in
+        if initial then
+          let
+            val binds = Data.get final_ctxt |> map fst;
+            val ml_env = "val [" ^ commas binds ^ "] = " ^
+                           "TacticAntiquotation.Data.get ML_context |> map snd;\n";
+          in (ml_env, ml_body) end
+        else ("", ml_body)
+      end;
+  in (decl, ctxt'') end;
+
+end
+\<close>
+
+setup \<open>
+  ML_Antiquotation.declaration
+        \<^binding>\<open>inline_tactic\<close>
+        Method.text_closure (K (TacticAntiquotation.method_binding "inline_tactic"))
+  #>
+  ML_Antiquotation.declaration
+        \<^binding>\<open>inline_method\<close>
+        Method.text_closure (K (TacticAntiquotation.method_binding "inline_method"))
+\<close>
+
+end

lib/ml-helpers/TacticAntiquotation_Test.thy

@@ -0,0 +1,72 @@
+(*
+ * Copyright 2018, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+
+ * @TAG(DATA61_BSD)
+ *)
+
+(* Basic tests for the @{inline_tactic} and @{inline_method} antiquotations. *)
+
+theory TacticAntiquotation_Test
+imports
+  Lib.TacticAntiquotation
+begin
+
+text \<open>Simple tests.\<close>
+
+text \<open>Example proof.\<close>
+lemma
+  fixes fib :: "nat \<Rightarrow> nat"
+  shows
+  "\<lbrakk> fib 0 = 0;
+     fib (Suc 0) = Suc 0;
+     \<forall>n. fib (Suc (Suc n)) = fib n + fib (Suc n)
+   \<rbrakk> \<Longrightarrow> fib n < 2^n"
+  apply (induct n rule: less_induct)
+  apply (rename_tac n, case_tac n)
+   apply fastforce
+  apply (rename_tac n, case_tac n)
+   apply (clarsimp simp only:, simp)
+  apply (clarsimp simp add: mult_2)
+  apply (rule add_less_le_mono)
+   apply (metis trans_less_add2 lessI less_trans)
+  apply (fastforce simp only: mult_2[symmetric] power_Suc[symmetric]
+                   intro: less_imp_le)
+  done
+
+text \<open>Let's uglify this proof\<dots>\<close>
+
+(* Test that we can save a tactic and call it in another context.
+ * (For this to work, the antiquoter has to dynamically parse and eval
+ *  the method text each time the tactic is run) *)
+ML \<open>
+val stored_tactic = @{inline_tactic "rename_tac n, case_tac n"};
+val stored_method = @{inline_method "rule add_less_le_mono"};
+\<close>
+
+lemma
+  fixes fib :: "nat \<Rightarrow> nat"
+  shows
+  "\<lbrakk> fib 0 = 0;
+     fib (Suc 0) = Suc 0;
+     \<forall>n. fib (Suc (Suc n)) = fib n + fib (Suc n)
+   \<rbrakk> \<Longrightarrow> fib n < 2^n"
+  apply (tactic \<open>@{inline_tactic "induct n rule: less_induct"}\<close>)
+  apply (tactic \<open>stored_tactic\<close>)
+   apply (tactic \<open>@{inline_tactic fastforce}\<close>)
+  apply (tactic \<open>stored_tactic\<close>)
+   apply (tactic \<open>@{inline_tactic "clarsimp simp only:"} THEN @{inline_tactic "simp"}\<close>)
+  apply (tactic \<open>Method.NO_CONTEXT_TACTIC @{context}
+                    (@{inline_method "clarsimp simp add: mult_2"} [])\<close>)
+  apply (tactic \<open>Method.NO_CONTEXT_TACTIC @{context} (stored_method [])\<close>)
+   apply (tactic \<open>@{inline_tactic "metis trans_less_add2 lessI less_trans"}\<close>)
+  apply (tactic \<open>@{inline_tactic "fastforce simp only: mult_2[symmetric] power_Suc[symmetric]
+                                            intro: less_imp_le"}\<close>)
+  done
+
+end