--- a/src/HOL/TPTP/atp_problem_import.ML Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Tue Apr 24 09:47:40 2012 +0200
@@ -22,92 +22,6 @@
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})
@@ -129,23 +43,11 @@
|> (fn path =>
path |> not (Path.is_absolute path)
? Path.append (Path.explode "$PWD"))
+ val ((_, _, problem), thy) =
+ TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
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
+ (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem,
+ map get_tptp_formula problem, thy)
end
(** Isabelle (combination of provers) **)
@@ -157,8 +59,9 @@
fun nitpick_tptp_file timeout file_name =
let
- val (falsify, ts) = read_tptp_file @{theory} file_name
- val state = Proof.init @{context}
+ val (falsify, ts, thy) = read_tptp_file @{theory} file_name
+ val ctxt = Proof_Context.init_global thy
+ val state = Proof.init ctxt
val params =
[("card", "1\<emdash>100"),
("box", "false"),
@@ -173,7 +76,7 @@
("format", "1000"),
("max_potential", "0"),
("timeout", string_of_int timeout)]
- |> Nitpick_Isar.default_params @{theory}
+ |> Nitpick_Isar.default_params thy
val i = 1
val n = 1
val step = 0
@@ -196,11 +99,13 @@
fun refute_tptp_file timeout file_name =
let
- val (falsify, ts) = read_tptp_file @{theory} file_name
+ val (falsify, ts, thy) = read_tptp_file @{theory} file_name
+ val ctxt = Proof_Context.init_global thy
val params =
- [("maxtime", string_of_int timeout)]
+ [("maxtime", string_of_int timeout),
+ ("maxvars", "100000")]
in
- Refute.refute_term @{context} params ts @{prop False}
+ Refute.refute_term ctxt params ts @{prop False}
|> print_szs_from_outcome falsify
end