more robustness in Isar proof reconstruction (cf. bug report by Ondrej)
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Feb 07 18:24:31 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Feb 07 18:39:24 2013 +0100
@@ -201,9 +201,7 @@
fun step_name_ord p =
let val q = pairself fst p in
- (* The "unprefix" part is to cope with remote Vampire's output. The proper
- solution would be to perform a topological sort, e.g. using the nice
- "Graph" functor. *)
+ (* The "unprefix" part is to cope with remote Vampire's output. *)
case pairself (Int.fromString
o perhaps (try (unprefix vampire_fact_prefix))) q of
(NONE, NONE) => string_ord q
@@ -229,6 +227,8 @@
|| Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
>> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
+val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) >> implode
+
val skip_term =
let
fun skip _ accum [] = (accum, [])
@@ -264,9 +264,13 @@
(Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
--| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
-- parse_dependencies --| $$ "]" --| $$ ")") x
+and skip_introduced x =
+ (Scan.this_string "introduced" |-- $$ "(" |-- skip_term --| $$ ")") x
and parse_source x =
(parse_file_source >> File_Source
|| parse_inference_source >> Inference_Source
+ || skip_introduced >> K dummy_inference (* for Vampire *)
+ || scan_nat >> (fn s => Inference_Source ("", [s])) (* for E *)
|| skip_term >> K dummy_inference) x
fun list_app (f, args) =
@@ -508,7 +512,7 @@
| atp_proof_from_tstplike_proof problem tstp =
tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof problem
- |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *)
+ |> sort (step_name_ord o pairself step_name)
fun clean_up_dependencies _ [] = []
| clean_up_dependencies seen
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Thu Feb 07 18:24:31 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Thu Feb 07 18:39:24 2013 +0100
@@ -39,7 +39,8 @@
val string_of_ref_graph : ref_graph -> string
val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent
val direct_graph : direct_sequent list -> direct_graph
- val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof
+ val redirect_graph :
+ atom list -> atom list -> atom -> ref_graph -> direct_proof
val succedent_of_cases : (clause * direct_inference list) list -> clause
val string_of_direct_proof : direct_proof -> string
end;
@@ -147,19 +148,11 @@
| zones_of n (bs :: bss) =
(fold (subtract atom_eq) bss) bs :: zones_of (n - 1) (bss @ [bs])
-fun redirect_graph axioms tainted ref_graph =
+fun redirect_graph axioms tainted bot ref_graph =
let
- val bot =
- case Atom_Graph.maximals ref_graph of
- [bot] => bot
- | bots =>
- raise Fail ("Malformed refutation graph with " ^
- string_of_int (length bots) ^ " maximal nodes (" ^
- commas_quote (map Atom.string_of bots) ^ ")")
val seqs =
map (redirect_sequent tainted bot) (sequents_of_ref_graph ref_graph)
val direct_graph = direct_graph seqs
-
fun redirect c proved seqs =
if null seqs then
[]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 07 18:24:31 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Feb 07 18:39:24 2013 +0100
@@ -131,6 +131,7 @@
val is_typed_helper_name =
String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
+
fun is_typed_helper_used_in_atp_proof atp_proof =
is_axiom_used_in_proof is_typed_helper_name atp_proof
@@ -677,6 +678,7 @@
val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
val axioms = axioms_of_ref_graph ref_graph conjs
val tainted = tainted_atoms_of_ref_graph ref_graph conjs
+ val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
val steps =
Symtab.empty
|> fold (fn Definition_Step _ => I (* FIXME *)
@@ -742,7 +744,7 @@
map (isar_step_of_direct_inf outer) infs
val (isar_proof, (preplay_fail, preplay_time)) =
ref_graph
- |> redirect_graph axioms tainted
+ |> redirect_graph axioms tainted bot
|> map (isar_step_of_direct_inf true)
|> append assms
|> (if not preplay andalso isar_shrink <= 1.0 then