# HG changeset patch
# User nipkow
# Date 1251720611 -7200
# Node ID 4595ff1d1a1a8c4d0327a48868152b78dce7cf95
# Parent  c714141777926ba29633674c25753961a0a988ac# Parent  341c83339aebd6fd411dac0b13c94f77d92ba89a
merged

diff -r 341c83339aeb -r 4595ff1d1a1a src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Aug 31 14:09:42 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Aug 31 14:10:11 2009 +0200
@@ -24,7 +24,7 @@
   type prover = int -> (thm * (string * int)) list option ->
     (thm * (string * int)) list option -> string -> int ->
     Proof.context * (thm list * thm) ->
-    bool * string * string * string vector * (thm * (string * int)) list
+    bool * (string * string list) * string * string vector * (thm * (string * int)) list
   val add_prover: string -> prover -> theory -> theory
   val print_provers: theory -> unit
   val get_prover: string -> theory -> prover option
@@ -305,7 +305,7 @@
 type prover = int -> (thm * (string * int)) list option ->
   (thm * (string * int)) list option -> string -> int ->
   Proof.context * (thm list * thm) ->
-  bool * string * string * string vector * (thm * (string * int)) list
+  bool * (string * string list) * string * string vector * (thm * (string * int)) list
 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
 
@@ -345,7 +345,7 @@
           let
             val _ = register birthtime deadtime (Thread.self (), desc)
             val result =
-              let val (success, message, _, _, _) =
+              let val (success, (message, _), _, _, _) =
                 prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
               in (success, message) end
               handle ResHolClause.TOO_TRIVIAL
diff -r 341c83339aeb -r 4595ff1d1a1a src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Aug 31 14:09:42 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Aug 31 14:10:11 2009 +0200
@@ -89,10 +89,10 @@
     val failure = find_failure proof
     val success = rc = 0 andalso is_none failure
     val message =
-      if is_some failure then "External prover failed."
-      else if rc <> 0 then "External prover failed: " ^ proof
-      else "Try this command: " ^
-        produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)
+      if is_some failure then ("External prover failed.", [])
+      else if rc <> 0 then ("External prover failed: " ^ proof, [])
+      else apfst (fn s => "Try this command: " ^ s)
+        (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno))
     val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
   in (success, message, proof, thm_names, the_filtered_clauses) end;
 
diff -r 341c83339aeb -r 4595ff1d1a1a src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 14:09:42 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 14:10:11 2009 +0200
@@ -5,10 +5,34 @@
 structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
 struct
 
+fun thms_of_name ctxt name =
+  let
+    val lex = OuterKeyword.get_lexicons
+    val get = maps (ProofContext.get_fact ctxt o fst)
+  in
+    Source.of_string name
+    |> Symbol.source {do_recover=false}
+    |> OuterLex.source {do_recover=SOME false} lex Position.start
+    |> OuterLex.source_proper
+    |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
+    |> Source.exhaust
+  end
+
+fun safe init done f x =
+  let
+    val y = init x
+    val z = Exn.capture f y
+    val _ = done y
+  in Exn.release z end
+
+val proverK = "prover"
+val keepK = "keep"
+val metisK = "metis"
+
 fun sledgehammer_action args {pre=st, ...} =
   let
     val prover_name =
-      AList.lookup (op =) args "prover"
+      AList.lookup (op =) args proverK
       |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
 
     val thy = Proof.theory_of st
@@ -16,16 +40,37 @@
     val prover = the (AtpManager.get_prover prover_name thy)
     val timeout = AtpManager.get_timeout () 
 
-    val (success, message) =
+    (* run sledgehammer *)
+    fun init NONE = !AtpWrapper.destdir
+      | init (SOME path) =
+          let
+            (* Warning: we implicitly assume single-threaded execution here! *)
+            val old = !AtpWrapper.destdir
+            val _ = AtpWrapper.destdir := path
+          in old end
+    fun done path = AtpWrapper.destdir := path
+    fun sh _ =
       let
-        val (success, message, _, _, _) =
+        val (success, (message, thm_names), _, _, _) =
           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 (success, message, SOME thm_names) end
+      handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
+           | ERROR msg => (false, "error: " ^ msg, NONE)
+    val (success, message, thm_names) = safe init done sh
+      (AList.lookup (op =) args keepK)
+
+    (* try metis *)
+    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 try (Mirabelle.can_apply (metis thms)) st = SOME true
+      then "success"
+      else "failure")
+    val msg = if not (AList.defined (op =) args metisK) then ""
+      else apply_metis (get_thms (Proof.context_of st) (these thm_names))
   in
     if success
-    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
+    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)
     else NONE
   end
 
diff -r 341c83339aeb -r 4595ff1d1a1a src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 31 14:09:42 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 31 14:10:11 2009 +0200
@@ -26,10 +26,10 @@
 my $thy_file = $ARGV[1];
 my $start_line = "0";
 my $end_line = "~1";
-if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { # FIXME
-  my $thy_file = $1;
-  my $start_line = $2;
-  my $end_line = $3;
+if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
+  $thy_file = $1;
+  $start_line = $2;
+  $end_line = $3;
 }
 my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
 my $new_thy_name = $thy_name . "_Mirabelle";
diff -r 341c83339aeb -r 4595ff1d1a1a src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Mon Aug 31 14:09:42 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Mon Aug 31 14:10:11 2009 +0200
@@ -17,10 +17,10 @@
   (* extracting lemma list*)
   val find_failure: string -> string option
   val lemma_list: bool -> string ->
-    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string
+    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
   (* structured proofs *)
   val structured_proof: string ->
-    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string
+    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
 end;
 
 structure ResReconstruct : RES_RECONSTRUCT =
@@ -554,9 +554,10 @@
 
   fun lemma_list dfg name result =
     let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
-    in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
+    in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
       (if used_conj then ""
-       else "\nWarning: Goal is provable because context is inconsistent.")
+       else "\nWarning: Goal is provable because context is inconsistent."),
+       lemmas)
     end;
 
   (* === Extracting structured Isar-proof === *)
@@ -567,11 +568,11 @@
     val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
     val proofextract = get_proof_extract proof
     val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
-    val one_line_proof = lemma_list false name result
+    val (one_line_proof, lemma_names) = lemma_list false name result
     val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
                 else decode_tstp_file cnfs ctxt goal subgoalno thm_names
     in
-    one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured
+    (one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured, lemma_names)
   end
 
 end;