author blanchet Wed, 18 Apr 2012 22:16:05 +0200 changeset 47557 32f35b3d9e42 parent 47556 45250c34ee1a child 47558 55b42f9af99d
started integrating Nik's parser into TPTP command-line tools
```--- 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
```
```--- 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

-  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
+
+  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"),