# HG changeset patch
# User blanchet
# Date 1328441230 -3600
# Node ID 4fd25dadbd94a8034418a7aa4bccc8a317b670d0
# Parent  fd15abc50fc19ff957884d8c94c8f2e86e2c55c2
cleaned up new SPASS parsing

diff -r fd15abc50fc1 -r 4fd25dadbd94 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Feb 05 12:27:10 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun Feb 05 12:27:10 2012 +0100
@@ -115,7 +115,7 @@
     "The prover claims the conjecture is a theorem but did not provide a proof."
   | string_for_failure ProofIncomplete =
     "The prover claims the conjecture is a theorem but provided an incomplete \
-    \proof."
+    \(or unparsable) proof."
   | string_for_failure (UnsoundProof (false, ss)) =
     "The prover found a type-unsound proof " ^ involving ss ^
     "(or, less likely, your axioms are inconsistent). Specify a sound type \
@@ -431,26 +431,30 @@
      -- Scan.repeat parse_decorated_atom
    >> (mk_horn o apfst (op @))) x
 
-fun resolve_spass_num spass_names num =
-  case Int.fromString num of
-    SOME j => if j > 0 andalso j <= Vector.length spass_names then
-                Vector.sub (spass_names, j - 1)
-              else
-                []
-  | NONE => []
+fun resolve_spass_num (SOME names) _ _ = names
+  | resolve_spass_num NONE spass_names num =
+    case Int.fromString num of
+      SOME j => if j > 0 andalso j <= Vector.length spass_names then
+                  Vector.sub (spass_names, j - 1)
+                else
+                  []
+    | NONE => []
 
 val parse_spass_debug =
   Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ","))
                --| $$ ")")
 
-(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. *)
+(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
+           derived from formulae <ident>* *)
 fun parse_spass_line spass_names =
   parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
     -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
     -- parse_horn_clause --| $$ "."
-  >> (fn (((num, rule), deps), u) =>
-         Inference ((num, resolve_spass_num spass_names num), u, rule,
-                    map (swap o `(resolve_spass_num spass_names)) deps))
+    -- Scan.option (Scan.this_string "derived from formulae "
+                    |-- Scan.repeat scan_general_id)
+  >> (fn ((((num, rule), deps), u), names) =>
+         Inference ((num, resolve_spass_num names spass_names num), u, rule,
+                    map (swap o `(resolve_spass_num NONE spass_names)) deps))
 
 (* Syntax: <name> *)
 fun parse_satallax_line x =
diff -r fd15abc50fc1 -r 4fd25dadbd94 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Feb 05 12:27:10 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Feb 05 12:27:10 2012 +0100
@@ -211,9 +211,7 @@
 
 fun used_facts_in_unsound_atp_proof _ _ [] = NONE
   | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
-    let
-      val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
-    in
+    let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
       if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
          not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
         SOME (map fst used_facts)
diff -r fd15abc50fc1 -r 4fd25dadbd94 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun Feb 05 12:27:10 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun Feb 05 12:27:10 2012 +0100
@@ -360,8 +360,9 @@
    required_execs =
      [("SPASS_NEW_HOME", "SPASS"), ("SPASS_NEW_HOME", "tptp2dfg")],
    arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ =>
-     ("-Auto -LR=1 -LT=1 -Isabelle=1 -TimeLimit=" ^
-      string_of_int (to_secs 1 timeout))
+     (* TODO: add: -FPDFGProof -FPFCR *)
+     ("-Auto -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
+     (* TODO: not used yet *)
      |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ",
    proof_delims = #proof_delims spass_config,
    known_failures = #known_failures spass_config,
diff -r fd15abc50fc1 -r 4fd25dadbd94 src/HOL/Tools/ATP/scripts/spass_new
--- a/src/HOL/Tools/ATP/scripts/spass_new	Sun Feb 05 12:27:10 2012 +0100
+++ b/src/HOL/Tools/ATP/scripts/spass_new	Sun Feb 05 12:27:10 2012 +0100
@@ -8,7 +8,7 @@
 name=${@:$(($#)):1}
 
 rm -f "$name.prf"
-"$SPASS_NEW_HOME/SPASS" -FPDFGProof -FPFCR $options "$name"
+"$SPASS_NEW_HOME/SPASS" $options "$name"
 if [ -f "$name.prf" ]
 then
   cat "$name.prf"
diff -r fd15abc50fc1 -r 4fd25dadbd94 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Feb 05 12:27:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Feb 05 12:27:10 2012 +0100
@@ -746,8 +746,11 @@
                        SOME facts =>
                        let
                          val failure =
-                           UnsoundProof (is_type_enc_quasi_sound type_enc,
-                                         facts)
+                           if null facts then
+                             ProofIncomplete
+                           else
+                             UnsoundProof (is_type_enc_quasi_sound type_enc,
+                                           facts)
                        in
                          if debug then
                            (warning (string_for_failure failure); NONE)