# HG changeset patch
# User boehmes
# Date 1251576115 -7200
# Node ID 6084b36a195f993b84ee79c57bedc38be454b3c9
# Parent  d84edd022efe1a9641afbbc00a9e848b85e329d0# Parent  375db037f4d26660a8b8ec9a78586b34b83c3613
merged

diff -r 375db037f4d2 -r 6084b36a195f src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sat Aug 29 22:01:55 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 375db037f4d2 -r 6084b36a195f src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sat Aug 29 22:01:55 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 375db037f4d2 -r 6084b36a195f src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Aug 29 22:01:55 2009 +0200
@@ -5,6 +5,32 @@
 structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
 struct
 
+local
+val valid = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
+  member (op =) (explode "_.")
+val name = Scan.many1 valid >> (rpair Position.none o implode)
+
+val digit = (fn
+  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
+  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
+  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
+fun join d n = 10 * n + d
+val number = Scan.repeat1 (Scan.some digit) >> (fn ds => fold join ds 0)
+val interval = Scan.option (Scan.$$ "(" |-- number --| Scan.$$ ")" >>
+  (single o Facts.Single))
+
+val fact_ref = name -- interval >> Facts.Named
+
+in
+
+fun thm_of_name ctxt s =
+  (case try (Scan.read Symbol.stopper fact_ref) (explode s) of
+    SOME (SOME r) => ProofContext.get_fact ctxt r
+  | _ => [])
+
+end
+
+
 fun sledgehammer_action args {pre=st, ...} =
   let
     val prover_name =
@@ -16,16 +42,25 @@
     val prover = the (AtpManager.get_prover prover_name thy)
     val timeout = AtpManager.get_timeout () 
 
-    val (success, message) =
+    (* run sledgehammer *)
+    val (success, message, thm_names) =
       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)
+
+    (* try metis *)
+    val thms = maps (thm_of_name (Proof.context_of st)) (these thm_names)
+    fun metis ctxt = MetisTools.metis_tac ctxt thms
+    val msg = if not (AList.defined (op =) args "metis") then "" else
+      if try (Mirabelle.can_apply metis) st = SOME true
+        then "\nMETIS: success"
+        else "\nMETIS: failure"
   in
     if success
-    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
+    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)
     else NONE
   end
 
diff -r 375db037f4d2 -r 6084b36a195f src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Sat Aug 29 22:01:55 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;