# HG changeset patch
# User blanchet
# Date 1334780165 -7200
# Node ID 32f35b3d9e4214a8f17e91aae50e67a1deab3c5d
# Parent  45250c34ee1a375117476810487b046af5a56027
started integrating Nik's parser into TPTP command-line tools

diff -r 45250c34ee1a -r 32f35b3d9e42 src/HOL/TPTP/ATP_Problem_Import.thy
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Apr 18 21:28:49 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Apr 18 22:16:05 2012 +0200
@@ -5,7 +5,7 @@
 header {* ATP Problem Importer *}
 
 theory ATP_Problem_Import
-imports Complex_Main
+imports Complex_Main TPTP_Interpret
 uses ("atp_problem_import.ML")
 begin
 
diff -r 45250c34ee1a -r 32f35b3d9e42 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 18 21:28:49 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 18 22:16:05 2012 +0200
@@ -22,9 +22,10 @@
 open ATP_Proof
 
 
-(** General TPTP parsing **)
+(** Crude TPTP CNF and FOF parsing **)
 
 exception SYNTAX of string
+exception THF of unit
 
 val tptp_explode = raw_explode o strip_spaces_except_between_idents
 
@@ -53,7 +54,8 @@
    || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
    || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
       --| $$ ")" --| $$ "."
-  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
+    >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
+  || Scan.this_string "thf" >> (fn _ => raise THF ())
 
 val parse_problem =
   Scan.repeat parse_include
@@ -104,11 +106,22 @@
 
 fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
 
-fun read_tptp_file file_name =
-  case parse_tptp_problem (File.read (Path.explode file_name)) of
-    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
-  | (phis, []) =>
-    map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula) phis
+fun mk_meta_not P = Logic.mk_implies (P, @{prop False})
+
+fun get_tptp_formula (_, role, _, P, _) =
+  P |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not
+
+fun read_tptp_file thy file_name =
+  let val path = Path.explode file_name in
+    (case parse_tptp_problem (File.read path) of
+       (_, s :: ss) =>
+       raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
+     | (phis, []) =>
+       map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula) phis)
+    handle THF () =>
+    TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
+    |> fst |> #3 |> map get_tptp_formula
+  end
 
 fun print_szs_from_outcome s =
   "% SZS status " ^
@@ -127,11 +140,10 @@
 
 fun nitpick_tptp_file file_name =
   let
-    val ts = read_tptp_file file_name
+    val ts = read_tptp_file @{theory} file_name
     val state = Proof.init @{context}
     val params =
-      [("card iota", "1\<emdash>100"),
-       ("card", "1\<emdash>8"),
+      [("card", "1\<emdash>100"),
        ("box", "false"),
        ("sat_solver", "smart"),
        ("max_threads", "1"),
@@ -160,7 +172,7 @@
 
 fun refute_tptp_file file_name =
   let
-    val ts = read_tptp_file file_name
+    val ts = read_tptp_file @{theory} file_name
     val params =
       [("maxtime", "10000"),
        ("assms", "true"),