# HG changeset patch
# User blanchet
# Date 1292508737 -3600
# Node ID 1393514094d78b3707597ac20432f0670c4a0d79
# Parent  bf00e0a578e8ae01f78c18a9a60461a9f9d60482
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)

diff -r bf00e0a578e8 -r 1393514094d7 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -100,11 +100,12 @@
   | string_for_failure prover NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail prover
   | string_for_failure prover MalformedInput =
-    "The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \
-    \developers."
+    "The " ^ prover ^ " problem is malformed. Please report this to the \
+    \Isabelle developers."
   | string_for_failure prover MalformedOutput =
     "The " ^ prover ^ " output is malformed."
-  | string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted."
+  | string_for_failure prover Interrupted =
+    "The " ^ prover ^ " was interrupted."
   | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
   | string_for_failure prover InternalError =
     "An internal " ^ prover ^ " error occurred."
@@ -216,9 +217,9 @@
 
 fun parse_term x =
   (scan_general_id
-    -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
-                      --| $$ ")") []
-    --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
+     -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
+                       --| $$ ")") []
+     --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
    >> ATerm) x
 and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
 
@@ -253,6 +254,8 @@
   Scan.optional ($$ "," |-- parse_annotation false
                  --| Scan.option ($$ "," |-- parse_annotations false)) []
 
+val vampire_unknown_fact = "unknown"
+
 (* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
    The <num> could be an identifier, but we assume integers. *)
 val parse_tstp_line =
@@ -263,7 +266,8 @@
           let
             val (name, deps) =
               case deps of
-                ["file", _, s] => ((num, SOME s), [])
+                ["file", _, s] =>
+                ((num, if s = vampire_unknown_fact then NONE else SOME s), [])
               | _ => ((num, NONE), deps)
           in
             case role of
@@ -282,12 +286,15 @@
 
 val parse_vampire_braced_stuff =
   $$ "{" -- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) -- $$ "}"
-  -- Scan.option ($$ "(" |-- parse_vampire_detritus --| $$ ")")
+val parse_vampire_parenthesized_detritus =
+  $$ "(" |-- parse_vampire_detritus --| $$ ")"
 
 (* Syntax: <num>. <formula> <annotation> *)
 val parse_vampire_line =
   scan_general_id --| $$ "." -- parse_formula
-    --| Scan.option parse_vampire_braced_stuff -- parse_annotation true
+    --| Scan.option parse_vampire_braced_stuff
+    --| Scan.option parse_vampire_parenthesized_detritus
+    -- parse_annotation true
   >> (fn ((num, phi), deps) =>
          Inference ((num, NONE), phi, map (rpair NONE) deps))
 
diff -r bf00e0a578e8 -r 1393514094d7 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -153,8 +153,9 @@
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
    arguments = fn complete => fn timeout =>
-     ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
-      " --thanks Andrei --input_file")
+     (* This would work too but it's less tested: "--proof tptp " ^ *)
+     "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
+     " --thanks \"Andrei and Krystof\" --input_file"
      |> not complete ? prefix "--sos on ",
    has_incomplete_mode = true,
    proof_delims =
diff -r bf00e0a578e8 -r 1393514094d7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -144,6 +144,8 @@
       "\nTo minimize the number of lemmas, try this: " ^
       Markup.markup Markup.sendback command ^ "."
 
+val vampire_fact_prefix = "f" (* grrr... *)
+
 fun resolve_fact fact_names ((_, SOME s)) =
     (case strip_prefix_and_unascii fact_prefix s of
        SOME s' => (case find_first_in_list_vector fact_names s' of
@@ -151,7 +153,7 @@
                    | NONE => [])
      | NONE => [])
   | resolve_fact fact_names (num, NONE) =
-    case Int.fromString num of
+    case Int.fromString (perhaps (try (unprefix vampire_fact_prefix)) num) of
       SOME j =>
       if j > 0 andalso j <= Vector.length fact_names then
         Vector.sub (fact_names, j - 1)