--- 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) **)