split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)

--- a/src/HOL/Tools/Mirabelle/Mirabelle.thy	Fri Aug 21 09:49:10 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Mirabelle.thy	Fri Aug 21 13:21:19 2009 +0200
@@ -3,10 +3,23 @@
 *)
 
 theory Mirabelle
-imports Plain
+imports Pure
 uses "Tools/mirabelle.ML"
 begin
 
+(* no multithreading, no parallel proofs *)
+ML {* Multithreading.max_threads := 1 *}
+ML {* Goal.parallel_proofs := 0 *}
+
+ML {* Toplevel.add_hook Mirabelle.step_hook *}
+
 setup Mirabelle.setup
 
+ML {*
+signature MIRABELLE_ACTION =
+sig
+  val invoke : (string * string) list -> theory -> theory
 end
+*}
+
+end

--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Fri Aug 21 09:49:10 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Fri Aug 21 13:21:19 2009 +0200
@@ -5,9 +5,7 @@
 signature MIRABELLE =
 sig
   type action
-  type settings
-  val register : string -> action -> theory -> theory
-  val invoke : string -> settings -> theory -> theory
+  val register : string * action -> theory -> theory
 
   val timeout : int Config.T
   val verbose : bool Config.T
@@ -15,37 +13,34 @@
   val end_line : int Config.T
   val set_logfile : string -> theory -> theory
 
-  val setup : theory -> theory
-
-  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
-    unit
-
   val goal_thm_of : Proof.state -> thm
   val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
   val theorems_in_proof_term : Thm.thm -> Thm.thm list
-  val theorems_of_sucessful_proof : Toplevel.state -> Thm.thm list
-  val get_setting : settings -> string * string -> string
-  val get_int_setting : settings -> string * int -> int
-
-(* FIXME  val refute_action : action *)
-  val quickcheck_action : action
-  val arith_action : action
-  val sledgehammer_action : action
-  val metis_action : action
+  val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
+  val get_setting : (string * string) list -> string * string -> string
+  val get_int_setting : (string * string) list -> string * int -> int
 end
 
 
 
-structure Mirabelle (*: MIRABELLE*) =
+signature MIRABELLE_EXT =
+sig
+  include MIRABELLE
+  val setup : theory -> theory
+  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
+    unit
+end
+
+
+
+structure Mirabelle : MIRABELLE_EXT =
 struct
 
 (* Mirabelle core *)
 
-type settings = (string * string) list
-type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option
-type action = settings -> invoked
+type action = {pre: Proof.state, post: Toplevel.state option} -> string option
 
-structure Registered = TheoryDataFun
+structure Actions = TheoryDataFun
 (
   type T = action Symtab.table
   val empty = Symtab.empty
@@ -54,26 +49,7 @@
   fun merge _ = Symtab.merge (K true)
 )
 
-fun register name act = Registered.map (Symtab.update_new (name, act))
-
-
-structure Invoked = TheoryDataFun
-(
-  type T = (string * invoked) list
-  val empty = []
-  val copy = I
-  val extend = I
-  fun merge _ = Library.merge (K true)
-)
-
-fun invoke name sts thy = 
-  let 
-    val act = 
-      (case Symtab.lookup (Registered.get thy) name of
-        SOME act => act
-      | NONE => error ("The invoked action " ^ quote name ^ 
-          " is not registered."))
-  in Invoked.map (cons (name, act sts)) thy end
+val register = Actions.map o Symtab.update_new
 
 val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
 val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
@@ -81,7 +57,7 @@
 val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
 val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
 
-val setup_config = setup1 #> setup2 #> setup3 #> setup4 #> setup5
+val setup = setup1 #> setup2 #> setup3 #> setup4 #> setup5
 
 fun set_logfile name =
   let val _ = File.write (Path.explode name) ""   (* erase file content *)
@@ -104,8 +80,8 @@
 fun capture_exns verb f x =
   (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg)
 
-fun apply_action (c as (verb, _)) st (name, invoked) =
-  Option.map (pair name) (capture_exns verb (with_time_limit c invoked) st)
+fun apply_action (c as (verb, _)) st (name, action) =
+  Option.map (pair name) (capture_exns verb (with_time_limit c action) st)
 
 fun in_range _ _ NONE = true
   | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
@@ -140,7 +116,8 @@
     val secs = Time.fromSeconds (Config.get_thy thy timeout)
     val st = {pre=pre, post=post}
   in
-    Invoked.get thy
+    Actions.get thy
+    |> Symtab.dest
     |> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
     |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
   end
@@ -213,108 +190,4 @@
   | SOME NONE => error ("bad option: " ^ key)
   | NONE => default)
 
-
-
-(* Mirabelle actions *)
-
-(* FIXME
-fun refute_action settings {pre=st, ...} = 
-  let
-    val params   = [("minsize", "2") (*"maxsize", "2"*)]
-    val subgoal = 0
-    val thy     = Proof.theory_of st
-    val thm = goal_thm_of st
-
-    val _ = Refute.refute_subgoal thy parms thm subgoal
-  in
-    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
-    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
-
-    val r =
-      if Substring.isSubstring "model found" writ_log
-      then
-        if Substring.isSubstring "spurious" warn_log
-        then SOME "potential counterexample"
-        else SOME "real counterexample (bug?)"
-      else
-        if Substring.isSubstring "time limit" writ_log
-        then SOME "no counterexample (time out)"
-        else if Substring.isSubstring "Search terminated" writ_log
-        then SOME "no counterexample (normal termination)"
-        else SOME "no counterexample (unknown)"
-  in r end
-*)
-
-fun quickcheck_action settings {pre=st, ...} =
-  let
-    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
-    val args = filter has_valid_key settings
-  in
-    (case Quickcheck.quickcheck args 1 st of
-      NONE => SOME "no counterexample"
-    | SOME _ => SOME "counterexample found")
-  end
-
-
-fun arith_action _ {pre=st, ...} = 
-  if can_apply Arith_Data.arith_tac st
-  then SOME "succeeded"
-  else NONE
-
-
-fun sledgehammer_action settings {pre=st, ...} =
-  let
-    val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
-    val thy = Proof.theory_of st
- 
-    val prover = the (AtpManager.get_prover prover_name thy)
-    val timeout = AtpManager.get_timeout () 
-
-    val (success, message) =
-      let
-        val (success, message, _, _, _) =
-          prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
-      in (success, message) end
-      handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
-           | ERROR msg => (false, "error: " ^ msg)
-  in
-    if success
-    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
-    else NONE
-  end
-
-
-fun metis_action settings {pre, post} =
-  let
-    val thms = theorems_of_sucessful_proof post
-    val names = map Thm.get_name thms
-
-    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
-
-    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
-  in
-    (if can_apply metis pre then "succeeded" else "failed")
-    |> suffix (" (" ^ commas names ^ ")")
-    |> SOME
-  end
-
-
-
-(* Mirabelle setup *)
-
-val setup =
-  setup_config #>
-(* FIXME  register "refute" refute_action #> *)
-  register "quickcheck" quickcheck_action #>
-  register "arith" arith_action #>
-  register "sledgehammer" sledgehammer_action #>
-  register "metis" metis_action (* #> FIXME:
-  Context.theory_map (Specification.add_theorem_hook theorem_hook) *)
-
 end
-
-val _ = Toplevel.add_hook Mirabelle.step_hook
-
-(* no multithreading, no parallel proofs *)
-val _ = Multithreading.max_threads := 1
-val _ = Goal.parallel_proofs := 0

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML	Fri Aug 21 13:21:19 2009 +0200
@@ -0,0 +1,15 @@
+(* Title:  mirabelle_arith.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Arith : MIRABELLE_ACTION =
+struct
+
+fun arith_action {pre=st, ...} =
+  if Mirabelle.can_apply Arith_Data.arith_tac st
+  then SOME "succeeded"
+  else NONE
+
+fun invoke _ = Mirabelle.register ("arith", arith_action)
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML	Fri Aug 21 13:21:19 2009 +0200
@@ -0,0 +1,24 @@
+(* Title:  mirabelle_metis.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Metis : MIRABELLE_ACTION =
+struct
+
+fun metis_action {pre, post} =
+  let
+    val thms = Mirabelle.theorems_of_sucessful_proof post
+    val names = map Thm.get_name thms
+
+    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
+
+    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
+  in
+    (if Mirabelle.can_apply metis pre then "succeeded" else "failed")
+    |> suffix (" (" ^ commas names ^ ")")
+    |> SOME
+  end
+
+fun invoke _ = Mirabelle.register ("metis", metis_action)
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Aug 21 13:21:19 2009 +0200
@@ -0,0 +1,19 @@
+(* Title:  mirabelle_quickcheck.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
+struct
+
+fun quickcheck_action args {pre=st, ...} =
+  let
+    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
+  in
+    (case Quickcheck.quickcheck (filter has_valid_key args) 1 st of
+      NONE => SOME "no counterexample"
+    | SOME _ => SOME "counterexample found")
+  end
+
+fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML	Fri Aug 21 13:21:19 2009 +0200
@@ -0,0 +1,36 @@
+(* Title:  mirabelle_refute.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Refute : MIRABELLE_ACTION =
+struct
+
+
+fun refute_action args {pre=st, ...} = 
+  let
+    val subgoal = 0
+    val thy     = Proof.theory_of st
+    val thm = goal_thm_of st
+
+    val _ = Refute.refute_subgoal thy args thm subgoal
+  in
+    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
+    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
+
+    val r =
+      if Substring.isSubstring "model found" writ_log
+      then
+        if Substring.isSubstring "spurious" warn_log
+        then SOME "potential counterexample"
+        else SOME "real counterexample (bug?)"
+      else
+        if Substring.isSubstring "time limit" writ_log
+        then SOME "no counterexample (time out)"
+        else if Substring.isSubstring "Search terminated" writ_log
+        then SOME "no counterexample (normal termination)"
+        else SOME "no counterexample (unknown)"
+  in r end
+
+fun invoke args = Mirabelle.register ("refute", refute_action args)
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 21 13:21:19 2009 +0200
@@ -0,0 +1,31 @@
+(* Title:  mirabelle_sledgehammer.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
+struct
+
+fun sledgehammer_action {pre=st, ...} =
+  let
+    val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
+    val thy = Proof.theory_of st
+ 
+    val prover = the (AtpManager.get_prover prover_name thy)
+    val timeout = AtpManager.get_timeout () 
+
+    val (success, message) =
+      let
+        val (success, message, _, _, _) =
+          prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
+      in (success, message) end
+      handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
+           | ERROR msg => (false, "error: " ^ msg)
+  in
+    if success
+    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
+    else NONE
+  end
+
+fun invoke _ = Mirabelle.register ("sledgehammer", sledgehammer_action)
+
+end

--- a/src/HOL/Tools/Mirabelle/etc/settings	Fri Aug 21 09:49:10 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/etc/settings	Fri Aug 21 13:21:19 2009 +0200
@@ -1,6 +1,7 @@
 MIRABELLE_HOME="$COMPONENT"
 
 MIRABELLE_LOGIC=HOL
+MIRABELLE_THEORY=Main
 MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
 MIRABELLE_TIMEOUT=30
 MIRABELLE_VERBOSE=false

--- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle	Fri Aug 21 09:49:10 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle	Fri Aug 21 13:21:19 2009 +0200
@@ -7,14 +7,21 @@
 
 PRG="$(basename "$0")"
 
+function action_names() {
+  TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
+  ACTION_NAMES=`find $TOOLS | sed 's/.*mirabelle_\(.*\)\.ML/\1/'`
+}
+
 function usage() {
   out="$MIRABELLE_OUTPUT_PATH"
   timeout="$MIRABELLE_TIMEOUT"
+  action_names
   echo
   echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
   echo
   echo "  Options are:"
   echo "    -L LOGIC     parent logic to use (default $ISABELLE_LOGIC)"
+  echo "    -T THEORY    parent theory to use (default $MIRABELLE_THEORY)"
   echo "    -O DIR       output directory for test data (default $out)"
   echo "    -v           be verbose"
   echo "    -t TIMEOUT   timeout for each action in seconds (default $timeout)"
@@ -23,7 +30,11 @@
   echo "  at all proof steps in the given theory files."
   echo
   echo "  ACTIONS is a colon-separated list of actions, where each action is"
-  echo "  either NAME or NAME[KEY=VALUE,...,KEY=VALUE]."
+  echo "  either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
+  for NAME in $ACTION_NAMES
+  do
+    echo "    $NAME"
+  done
   echo
   echo "  FILES is a space-separated list of theory files, where each file is"
   echo "  either NAME.thy or NAME.thy[START:END] and START and END are numbers"
@@ -37,12 +48,15 @@
 
 # options
 
-while getopts "L:O:vt:" OPT
+while getopts "L:T:O:vt:" OPT
 do
   case "$OPT" in
     L)
       MIRABELLE_LOGIC="$OPTARG"
       ;;
+    T)
+      MIRABELLE_THEORY="$OPTARG"
+      ;;
     O)
       MIRABELLE_OUTPUT_PATH="$OPTARG"
       ;;

--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Fri Aug 21 09:49:10 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Fri Aug 21 13:21:19 2009 +0200
@@ -11,6 +11,7 @@
 my $isabelle_home = $ENV{'ISABELLE_HOME'};
 my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
 my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
+my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
 my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
 my $verbose = $ENV{'MIRABELLE_VERBOSE'};
 my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
@@ -41,11 +42,23 @@
 my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
 my $log_file = $output_path . "/" . $thy_name . ".log";
 
+my @action_files;
+foreach (split(/:/, $actions)) {
+  if (m/([^[]*)/) {
+    push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
+  }
+}
+my $tools = "";
+if ($#action_files >= 0) {
+  $tools = "uses " . join(" ", @action_files);
+}
+
 open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
 
 print SETUP_FILE <<END;
 theory "$setup_thy_name"
-imports "$mirabelle_thy"
+imports "$mirabelle_thy" "$mirabelle_theory"
+$tools
 begin
 
 setup {* 
@@ -61,7 +74,8 @@
 foreach (split(/:/, $actions)) {
   if (m/([^[]*)(?:\[(.*)\])?/) {
     my ($name, $settings_str) = ($1, $2 || "");
-    print SETUP_FILE "setup {* Mirabelle.invoke \"$name\" [";
+    $name =~ s/^([a-z])/\U$1/;
+    print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
     my $sep = "";
     foreach (split(/,/, $settings_str)) {
       if (m/\s*(.*)\s*=\s*(.*)\s*/) {