# HG changeset patch
# User blanchet
# Date 1272532944 -7200
# Node ID 36eff5a50babe0362f92761343f4bdd589793d69
# Parent  3c2438efe22463e9392147d02373ee3de7678993
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction

diff -r 3c2438efe224 -r 36eff5a50bab src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 10:55:59 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 11:22:24 2010 +0200
@@ -189,18 +189,20 @@
   parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ " ")
 
 fun parse_horn_clause pool =
-  Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
-  -- Scan.repeat (parse_starred_predicate_term pool)
-  >> (fn ([], []) => [str_leaf "c_False"]
-       | (clauses1, clauses2) => map negate_node clauses1 @ clauses2)
+  Scan.repeat (parse_starred_predicate_term pool) --| $$ "|" --| $$ "|"
+    -- Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
+    -- Scan.repeat (parse_starred_predicate_term pool)
+  >> (fn (([], []), []) => [str_leaf "c_False"]
+       | ((clauses1, clauses2), clauses3) =>
+         map negate_node (clauses1 @ clauses2) @ clauses3)
 
-(* Syntax: <num>[0:<inference><annotations>] ||
-           <cnf_formulas> -> <cnf_formulas>. *)
+(* Syntax: <num>[0:<inference><annotations>]
+   <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
 fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
+|> tap (fn _ => priority ("*** processing " ^ PolyML.makestring num)) (* ### *)
 fun parse_spass_line pool =
   parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-  -- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|"
-  -- parse_horn_clause pool --| $$ "."
+  -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
   >> finish_spass_line
 
 fun parse_line pool = parse_tstp_line pool || parse_spass_line pool