# HG changeset patch
# User blanchet
# Date 1334999749 -7200
# Node ID e33c2be488fe4d9c1e7024d2dd1f246e71a0e2b6
# Parent  9a9218111085403bd94a123fc15af49ef8890296
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures

diff -r 9a9218111085 -r e33c2be488fe src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Sat Apr 21 11:15:49 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Sat Apr 21 11:15:49 2012 +0200
@@ -17,7 +17,100 @@
 structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =
 struct
 
-(** TPTP parsing **)
+open ATP_Util
+open ATP_Problem
+open ATP_Proof
+
+
+(** Crude TPTP CNF and FOF parsing (obsolescent) **)
+
+exception SYNTAX of string
+exception THF of unit
+
+val tptp_explode = raw_explode o strip_spaces_except_between_idents
+
+fun parse_file_path (c :: ss) =
+    if c = "'" orelse c = "\"" then
+      ss |> chop_while (curry (op <>) c) |>> implode ||> tl
+    else
+      raise SYNTAX "invalid file path"
+  | parse_file_path [] = raise SYNTAX "invalid file path"
+
+fun parse_include x =
+  let
+    val (file_name, rest) =
+      (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
+       --| $$ ".") x
+    val path = file_name |> Path.explode
+    val path =
+      path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
+  in ((), (path |> File.read |> tptp_explode) @ rest) end
+
+val parse_cnf_or_fof =
+  (Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |--
+  Scan.many (not_equal ",") |-- $$ "," |--
+  (Scan.this_string "axiom" || Scan.this_string "definition"
+   || Scan.this_string "theorem" || Scan.this_string "lemma"
+   || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
+   || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
+      --| $$ ")" --| $$ "."
+    >> (fn ("conjecture", phi) => (true, AConn (ANot, [phi]))
+         | (_, phi) => (false, phi))
+  || Scan.this_string "thf" >> (fn _ => raise THF ())
+
+val parse_problem =
+  Scan.repeat parse_include
+  |-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include)
+
+val parse_tptp_problem =
+  Scan.finite Symbol.stopper
+      (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
+                  parse_problem))
+  o tptp_explode
+
+val iota_T = @{typ iota}
+val quant_T = @{typ "(iota => bool) => bool"}
+
+fun is_variable s = Char.isUpper (String.sub (s, 0))
+
+fun hol_term_from_fo_term res_T (ATerm (x, us)) =
+  let val ts = map (hol_term_from_fo_term iota_T) us in
+    list_comb ((case x of
+                  "$true" => @{const_name True}
+                | "$false" => @{const_name False}
+                | "=" => @{const_name HOL.eq}
+                | "equal" => @{const_name HOL.eq}
+                | _ => x, map fastype_of ts ---> res_T)
+               |> (if is_variable x then Free else Const), ts)
+  end
+
+fun hol_prop_from_formula phi =
+  case phi of
+    AQuant (_, [], phi') => hol_prop_from_formula phi'
+  | AQuant (q, (x, _) :: xs, phi') =>
+    Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
+           quant_T)
+    $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
+  | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
+  | AConn (c, [u1, u2]) =>
+    pairself hol_prop_from_formula (u1, u2)
+    |> (case c of
+          AAnd => HOLogic.mk_conj
+        | AOr => HOLogic.mk_disj
+        | AImplies => HOLogic.mk_imp
+        | AIff => HOLogic.mk_eq
+        | ANot => raise Fail "binary \"ANot\"")
+  | AConn _ => raise Fail "malformed AConn"
+  | AAtom u => hol_term_from_fo_term @{typ bool} u
+
+fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
+
+fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
+
+
+(** TPTP parsing based on ML-Yacc-generated "TPTP_Parser" **)
+
+fun mk_meta_not P = Logic.mk_implies (P, @{prop False})
 
 (* cf. "close_form" in "refute.ML" *)
 fun close_form t =
@@ -25,21 +118,28 @@
            Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
        (Term.add_vars t []) t
 
-fun mk_meta_not P = Logic.mk_implies (P, @{prop False})
-
 fun get_tptp_formula (_, role, P, _) =
   P |> Logic.varify_global |> close_form
     |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not
 
 fun read_tptp_file thy file_name =
-  let
-    val path = Path.explode file_name
-    val problem =
-      TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
-      |> fst |> #3
-  in
-    (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,
-     map get_tptp_formula problem)
+  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)))
+     | (problem, []) =>
+       (exists fst problem,
+        map (HOLogic.mk_Trueprop o close_hol_prop o hol_prop_from_formula o snd)
+            problem))
+    handle THF () =>
+    let
+      val problem =
+        TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
+        |> fst |> #3
+    in
+      (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,
+       map get_tptp_formula problem)
+    end
   end
 
 (** Isabelle (combination of provers) **)