# HG changeset patch
# User blanchet
# Date 1360258764 -3600
# Node ID 63d71b24732385dff6b087e4fa1b436ab333c6a5
# Parent  b0d9ff6b4b4f479c6dfef0e40532b4099f4099c6
more robustness in Isar proof reconstruction (cf. bug report by Ondrej)

diff -r b0d9ff6b4b4f -r 63d71b247323 src/HOL/Tools/ATP/atp_proof.ML
--- 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
diff -r b0d9ff6b4b4f -r 63d71b247323 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- 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
         []
diff -r b0d9ff6b4b4f -r 63d71b247323 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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