Mirabelle: added preliminary documentation,
Mirabelle: removed option "verbose",
Mirabelle: actions need to limit their execution time themselves,
sledgehammer: do not report chained facts

--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Tue Sep 01 14:09:59 2009 +0200
@@ -9,12 +9,12 @@
 
   val logfile : string Config.T
   val timeout : int Config.T
-  val verbose : bool Config.T
   val start_line : int Config.T
   val end_line : int Config.T
 
   val goal_thm_of : Proof.state -> thm
-  val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
+  val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
+    Proof.state -> bool
   val theorems_in_proof_term : Thm.thm -> Thm.thm list
   val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
   val get_setting : (string * string) list -> string * string -> string
@@ -38,7 +38,8 @@
 
 (* Mirabelle core *)
 
-type action = {pre: Proof.state, post: Toplevel.state option} -> string option
+type action = Time.time -> {pre: Proof.state, post: Toplevel.state option} ->
+  string option
 
 structure Actions = TheoryDataFun
 (
@@ -53,11 +54,10 @@
 
 val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
 val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
-val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true
-val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
-val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
+val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0
+val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1
 
-val setup = setup1 #> setup2 #> setup3 #> setup4 #> setup5
+val setup = setup1 #> setup2 #> setup3 #> setup4
 
 local
 
@@ -67,17 +67,15 @@
   (* FIXME: with multithreading and parallel proofs enabled, we might need to
      encapsulate this inside a critical section *)
 
-fun verbose_msg verbose msg = if verbose then SOME msg else NONE
-
-fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x
-  handle TimeLimit.TimeOut => verbose_msg verb "time out"
-       | ERROR msg => verbose_msg verb ("error: " ^ msg)
+fun capture_exns f x =
+  let
+    fun f' x = f x
+      handle TimeLimit.TimeOut => SOME "time out"
+           | ERROR msg => SOME ("error: " ^ msg)
+  in (case try f' x of NONE => SOME "exception" | SOME msg => msg) end
 
-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, action) =
-  Option.map (pair name) (capture_exns verb (with_time_limit c action) st)
+fun apply_action timeout st (name, action) =
+  Option.map (pair name) (capture_exns (action timeout) st)
 
 fun in_range _ _ NONE = true
   | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
@@ -104,13 +102,12 @@
     val thy = Proof.theory_of pre
     val pos = Toplevel.pos_of tr
     val name = Toplevel.name_of tr
-    val verb = Config.get_thy thy verbose
-    val secs = Time.fromSeconds (Config.get_thy thy timeout)
+    val timeout = Time.fromSeconds (Config.get_thy thy timeout)
     val st = {pre=pre, post=post}
   in
     Actions.get thy
     |> Symtab.dest
-    |> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
+    |> only_within_range thy pos (map_filter (apply_action timeout st))
     |> (fn [] => () | msgs => log thy (pretty_print pos name msgs))
   end
 
@@ -131,10 +128,12 @@
 
 val goal_thm_of = snd o snd o Proof.get_goal
 
-fun can_apply tac st =
-  let val (ctxt, (facts, goal)) = Proof.get_goal st
+fun can_apply timeout tac st =
+  let
+    val (ctxt, (facts, goal)) = Proof.get_goal st
+    val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
   in
-    (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of
+    (case TimeLimit.timeLimit timeout (Seq.pull o full_tac) goal of
       SOME (thm, _) => true
     | NONE => false)
   end

--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML	Tue Sep 01 14:09:59 2009 +0200
@@ -5,8 +5,8 @@
 structure Mirabelle_Arith : MIRABELLE_ACTION =
 struct
 
-fun arith_action {pre=st, ...} =
-  if Mirabelle.can_apply Arith_Data.arith_tac st
+fun arith_action timeout {pre=st, ...} =
+  if Mirabelle.can_apply timeout Arith_Data.arith_tac st
   then SOME "succeeded"
   else NONE
 

--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML	Tue Sep 01 14:09:59 2009 +0200
@@ -5,7 +5,7 @@
 structure Mirabelle_Metis : MIRABELLE_ACTION =
 struct
 
-fun metis_action {pre, post} =
+fun metis_action timeout {pre, post} =
   let
     val thms = Mirabelle.theorems_of_sucessful_proof post
     val names = map Thm.get_name thms
@@ -14,7 +14,7 @@
 
     fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
   in
-    (if Mirabelle.can_apply metis pre then "succeeded" else "failed")
+    (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
     |> suffix (" (" ^ commas names ^ ")")
     |> SOME
   end

--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML	Tue Sep 01 14:09:59 2009 +0200
@@ -5,11 +5,12 @@
 structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
 struct
 
-fun quickcheck_action args {pre=st, ...} =
+fun quickcheck_action limit args {pre=st, ...} =
   let
     val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
+    val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
   in
-    (case Quickcheck.quickcheck (filter has_valid_key args) 1 st of
+    (case TimeLimit.timeLimit limit quickcheck st of
       NONE => SOME "no counterexample"
     | SOME _ => SOME "counterexample found")
   end

--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML	Tue Sep 01 14:09:59 2009 +0200
@@ -7,13 +7,14 @@
 
 
 (* FIXME:
-fun refute_action args {pre=st, ...} = 
+fun refute_action args timeout {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
+    val refute = Refute.refute_subgoal thy args thm
+    val _ = TimeLimit.timeLimit timeout refute subgoal
   in
     val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
     val warn_log = Substring.full (the (Symtab.lookup tab "warning"))

--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 01 14:09:59 2009 +0200
@@ -29,7 +29,7 @@
 val keepK = "keep"
 val metisK = "metis"
 
-fun sledgehammer_action args {pre=st, ...} =
+fun sledgehammer_action args timeout {pre=st, ...} =
   let
     val prover_name =
       AList.lookup (op =) args proverK
@@ -38,7 +38,7 @@
     val thy = Proof.theory_of st
  
     val prover = the (AtpManager.get_prover prover_name thy)
-    val timeout = AtpManager.get_timeout () 
+    val atp_timeout = AtpManager.get_timeout () 
 
     (* run sledgehammer *)
     fun init NONE = !AtpWrapper.destdir
@@ -51,8 +51,9 @@
     fun done path = AtpWrapper.destdir := path
     fun sh _ =
       let
+        val atp = prover atp_timeout NONE NONE prover_name 1
         val (success, (message, thm_names), _, _, _) =
-          prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
+          TimeLimit.timeLimit timeout atp (Proof.get_goal st)
       in (success, message, SOME thm_names) end
       handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
            | ERROR msg => (false, "error: " ^ msg, NONE)
@@ -63,7 +64,7 @@
     fun get_thms ctxt = maps (thms_of_name ctxt)
     fun metis thms ctxt = MetisTools.metis_tac ctxt thms
     fun apply_metis thms = "\nApplying metis with these theorems: " ^
-     (if Mirabelle.can_apply (metis thms) st
+     (if Mirabelle.can_apply timeout (metis thms) st
       then "success"
       else "failure")
     val msg = if not (AList.defined (op =) args metisK) then ""

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/doc/options.txt	Tue Sep 01 14:09:59 2009 +0200
@@ -0,0 +1,6 @@
+Options for sledgehammer:
+
+  * prover=NAME: name of the external prover to call
+  * keep=PATH: path where to keep temporary files created by sledgehammer 
+  * metis=X: apply metis with the theorems found by sledgehammer (X may be any
+      non-empty string)

--- a/src/HOL/Tools/Mirabelle/etc/settings	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/etc/settings	Tue Sep 01 14:09:59 2009 +0200
@@ -4,6 +4,5 @@
 MIRABELLE_THEORY=Main
 MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
 MIRABELLE_TIMEOUT=30
-MIRABELLE_VERBOSE=false
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"

--- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle	Tue Sep 01 14:09:59 2009 +0200
@@ -25,7 +25,6 @@
   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)"
   echo
   echo "  Apply the given actions (i.e., automated proof tools)"
@@ -47,7 +46,7 @@
 
 # options
 
-while getopts "L:T:O:vt:?" OPT
+while getopts "L:T:O:t:?" OPT
 do
   case "$OPT" in
     L)
@@ -59,9 +58,6 @@
     O)
       MIRABELLE_OUTPUT_PATH="$OPTARG"
       ;;
-    v)
-      MIRABELLE_VERBOSE="true"
-      ;;
     t)
       MIRABELLE_TIMEOUT="$OPTARG"
       ;;

--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Tue Sep 01 14:09:59 2009 +0200
@@ -13,7 +13,6 @@
 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'};
 
 my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
@@ -66,7 +65,6 @@
 setup {* 
   Config.put_thy Mirabelle.logfile "$log_file" #>
   Config.put_thy Mirabelle.timeout $timeout #>
-  Config.put_thy Mirabelle.verbose $verbose #>
   Config.put_thy Mirabelle.start_line $start_line #>
   Config.put_thy Mirabelle.end_line $end_line
 *}

--- a/src/HOL/Tools/res_reconstruct.ML	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Sep 01 14:09:59 2009 +0200
@@ -557,7 +557,7 @@
     in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
       (if used_conj then ""
        else "\nWarning: Goal is provable because context is inconsistent."),
-       lemmas)
+       nochained lemmas)
     end;
 
   (* === Extracting structured Isar-proof === *)