# HG changeset patch
# User desharna
# Date 1642848385 -3600
# Node ID f21e7e6172a0175b77aac05950669566d87e126a
# Parent  ef18787842b315ce4379b63fc33e35cbc0ce8e15
renamed run_action to run in Mirabelle.action record

diff -r ef18787842b3 -r f21e7e6172a0 NEWS
--- a/NEWS	Sat Jan 22 11:33:31 2022 +0100
+++ b/NEWS	Sat Jan 22 11:46:25 2022 +0100
@@ -54,6 +54,7 @@
   - Added option "-r INT" to randomize the goals with a given seed before
     selection.
   - Added option "-y" for a dry run.
+  - Renamed run_action to run in Mirabelle.action record. Minor INCOMPATIBILITY.
 
 
 
diff -r ef18787842b3 -r f21e7e6172a0 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Sat Jan 22 11:33:31 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Sat Jan 22 11:46:25 2022 +0100
@@ -13,7 +13,7 @@
      output_dir: Path.T}
   type command =
     {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}
-  type action = {run_action: command -> string, finalize: unit -> string}
+  type action = {run: command -> string, finalize: unit -> string}
   val register_action: string -> (action_context -> string * action) -> unit
 
   (*utility functions*)
@@ -67,9 +67,9 @@
 type action_context =
   {index: int, label: string, name: string, arguments: Properties.T, timeout: Time.time,
    output_dir: Path.T};
-type action = {run_action: command -> string, finalize: unit -> string};
+type action = {run: command -> string, finalize: unit -> string};
 
-val dry_run_action : action = {run_action = K "", finalize = K ""}
+val dry_run_action : action = {run = K "", finalize = K ""}
 
 local
   val actions = Synchronized.var "Mirabelle.actions"
@@ -130,14 +130,14 @@
       ()
   end
 
-fun apply_action ({run_action, ...} : action) context (command as {pos, pre, ...} : command) =
+fun apply_action ({run, ...} : action) context (command as {pos, pre, ...} : command) =
   let
     val thy = Proof.theory_of pre;
     val action_path = make_action_path context;
     val goal_name_path = Path.basic (#name command)
     val line_path = Path.basic (string_of_int (the (Position.line_of pos)));
     val offset_path = Path.basic (string_of_int (the (Position.offset_of pos)));
-    val ({elapsed, ...}, s) = Timing.timing run_action_function (fn () => run_action command);
+    val ({elapsed, ...}, s) = Timing.timing run_action_function (fn () => run command);
     val export_name =
       Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path +
         line_path + offset_path + Path.basic (string_of_int (Time.toMilliseconds elapsed)));
diff -r ef18787842b3 -r f21e7e6172a0 src/HOL/Tools/Mirabelle/mirabelle_arith.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Sat Jan 22 11:33:31 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Sat Jan 22 11:46:25 2022 +0100
@@ -12,11 +12,11 @@
 
 fun make_action ({timeout, ...} : Mirabelle.action_context) =
   let
-    fun run_action ({pre, ...} : Mirabelle.command) =
+    fun run ({pre, ...} : Mirabelle.command) =
       (case Timing.timing (Mirabelle.can_apply timeout Arith_Data.arith_tac) pre of
         ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
       | (_, false) => "failed")
-  in ("", {run_action = run_action, finalize = K ""}) end
+  in ("", {run = run, finalize = K ""}) end
 
 val () = Mirabelle.register_action "arith" make_action
 
diff -r ef18787842b3 -r f21e7e6172a0 src/HOL/Tools/Mirabelle/mirabelle_metis.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML	Sat Jan 22 11:33:31 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML	Sat Jan 22 11:46:25 2022 +0100
@@ -11,7 +11,7 @@
 
 fun make_action ({timeout, ...} : Mirabelle.action_context) =
   let
-    fun run_action ({pre, post, ...} : Mirabelle.command) =
+    fun run ({pre, post, ...} : Mirabelle.command) =
       let
         val thms = Mirabelle.theorems_of_sucessful_proof post;
         val names = map Thm.get_name_hint thms;
@@ -21,7 +21,7 @@
         (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
         |> not (null names) ? suffix (":\n" ^ commas names)
       end
-  in ("", {run_action = run_action, finalize = K ""}) end
+  in ("", {run = run, finalize = K ""}) end
 
 val () = Mirabelle.register_action "metis" make_action
 
diff -r ef18787842b3 -r f21e7e6172a0 src/HOL/Tools/Mirabelle/mirabelle_presburger.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML	Sat Jan 22 11:33:31 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML	Sat Jan 22 11:46:25 2022 +0100
@@ -9,12 +9,11 @@
 
 fun make_action ({timeout, ...} : Mirabelle.action_context) =
   let
-    val _ = Timing.timing
-    fun run_action ({pre, ...} : Mirabelle.command) =
+    fun run ({pre, ...} : Mirabelle.command) =
       (case Timing.timing (Mirabelle.can_apply timeout (Cooper.tac true [] [])) pre of
         ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
       | (_, false) => "failed")
-  in ("", {run_action = run_action, finalize = K ""}) end
+  in ("", {run = run, finalize = K ""}) end
 
 val () = Mirabelle.register_action "presburger" make_action
 
diff -r ef18787842b3 -r f21e7e6172a0 src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML	Sat Jan 22 11:33:31 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML	Sat Jan 22 11:46:25 2022 +0100
@@ -15,11 +15,11 @@
     val quickcheck =
       Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1
 
-    fun run_action ({pre, ...} : Mirabelle.command) =
+    fun run ({pre, ...} : Mirabelle.command) =
       (case Timeout.apply timeout quickcheck pre of
         NONE => "no counterexample"
       | SOME _ => "counterexample found")
-  in ("", {run_action = run_action, finalize = K ""}) end
+  in ("", {run = run, finalize = K ""}) end
 
 val () = Mirabelle.register_action "quickcheck" make_action
 
diff -r ef18787842b3 -r f21e7e6172a0 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Sat Jan 22 11:33:31 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Sat Jan 22 11:46:25 2022 +0100
@@ -464,7 +464,7 @@
 
     val init_msg = "Params for sledgehammer: " ^ Sledgehammer_Prover.string_of_params params
 
-    fun run_action ({theory_index, name, pos, pre, ...} : Mirabelle.command) =
+    fun run ({theory_index, name, pos, pre, ...} : Mirabelle.command) =
       let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
         if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then
           ""
@@ -492,7 +492,7 @@
       end
 
     fun finalize () = log_data (Synchronized.value data)
-  in (init_msg, {run_action = run_action, finalize = finalize}) end
+  in (init_msg, {run = run, finalize = finalize}) end
 
 val () = Mirabelle.register_action "sledgehammer" make_action
 
diff -r ef18787842b3 -r f21e7e6172a0 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML	Sat Jan 22 11:33:31 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML	Sat Jan 22 11:46:25 2022 +0100
@@ -83,7 +83,7 @@
     val num_found_facts = Synchronized.var "num_found_facts" 0
     val num_lost_facts = Synchronized.var "num_lost_facts" 0
 
-    fun run_action ({pos, pre, ...} : Mirabelle.command) =
+    fun run ({pos, pre, ...} : Mirabelle.command) =
       let
         val results =
           (case (Position.line_of pos, Position.offset_of pos) of
@@ -179,7 +179,7 @@
             (Synchronized.value num_lost_facts) ^ "%"
       else
         ""
-  in ("", {run_action = run_action, finalize = finalize}) end
+  in ("", {run = run, finalize = finalize}) end
 
 val () = Mirabelle.register_action "sledgehammer_filter" make_action
 
diff -r ef18787842b3 -r f21e7e6172a0 src/HOL/Tools/Mirabelle/mirabelle_try0.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Sat Jan 22 11:33:31 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Sat Jan 22 11:46:25 2022 +0100
@@ -13,12 +13,12 @@
   let
     val generous_timeout = Time.scale 10.0 timeout
 
-    fun run_action ({pre, ...} : Mirabelle.command) =
+    fun run ({pre, ...} : Mirabelle.command) =
       if Timeout.apply generous_timeout (Try0.try0 (SOME timeout) ([], [], [], [])) pre then
         "succeeded"
       else
         ""
-  in ("", {run_action = run_action, finalize = K ""}) end
+  in ("", {run = run, finalize = K ""}) end
 
 val () = Mirabelle.register_action "try0" make_action