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