--- 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
--- 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;
--- 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
--- 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;