(* Title: HOL/TPTP/TPTP_Parser_Test.thy Author: Nik Sultana, Cambridge University Computer Laboratory
Some tests for the TPTP interface. Some of the tests rely on the Isabelle environment variable $TPTP, which should point to the TPTP-vX.Y.Z directory.
*)
theory TPTP_Parser_Test imports TPTP_Test TPTP_Parser_Example begin
section "Problem-name parsing tests"
ML \<open> local open TPTP_Syntax; open TPTP_Problem_Name;
val name_tests =
[("HWV041_4.p",
Standard {suffix = Problem ((4, NONE), "p"), prob_form = TFF, prob_domain = "HWV", prob_number = 41}),
("LCL617^1.p",
Standard {suffix = Problem ((1, NONE), "p"), prob_form = THF, prob_domain = "LCL", prob_number = 617}),
("LCL831-1.p",
Standard {suffix = Problem ((1, NONE), "p"), prob_form = CNF, prob_domain = "LCL", prob_number = 831}),
("HWV045=1.p",
Standard {suffix = Problem ((1, NONE), "p"), prob_form = TFF_with_arithmetic, prob_domain = "HWV", prob_number = 45}),
("LCL655+1.010.p",
Standard {suffix = Problem ((1, SOME 10), "p"), prob_form = FOF, prob_domain = "LCL", prob_number = 655}),
("OTH123.p",
Nonstandard "OTH123.p"),
("other",
Nonstandard "other"),
("AAA000\194\1630.axiom",
Nonstandard "AAA000\194\1630.axiom"),
("AAA000\194\1630.p",
Nonstandard "AAA000\194\1630.p"),
("AAA000.0.p",
Nonstandard "AAA000.0.p"),
("AAA000\194\1630.what",
Nonstandard "AAA000\194\1630.what"),
("",
Nonstandard "")]; in
val _ = map (fn (str, res) =>
@{assert}(TPTP_Problem_Name.parse_problem_name str = res)) name_tests end
(*test against all TPTP problems*) fun problem_names () =
map (Path.file_name #>
TPTP_Problem_Name.parse_problem_name #>
TPTP_Problem_Name.mangle_problem_name)
(TPTP_Syntax.get_file_list tptp_probs_dir) \<close>
ML \<open> open TPTP_Syntax;
@{assert}
((TPTP_Parser.parse_expression "" "thf(x,axiom,^ [X] : ^ [Y] : f @ g)."
|> payloads_of |> hd)
=
Fmla (Interpreted_ExtraLogic Apply,
[Quant (Lambda, [("X", NONE)],
Quant (Lambda, [("Y", NONE)],
Atom (THF_Atom_term (Term_Func (Uninterpreted "f", []))))),
Atom (THF_Atom_term (Term_Func (Uninterpreted "g", [])))])
) \<close>
text"Parse a specific problem."
ML \<open>
map TPTP_Parser.parse_file
["$TPTP/Problems/FLD/FLD051-1.p", "$TPTP/Problems/FLD/FLD005-3.p", "$TPTP/Problems/SWV/SWV567-1.015.p", "$TPTP/Problems/SWV/SWV546-1.010.p"] \<close>
ML \<open>
parser_test @{context} (situate "DAT/DAT001=1.p");
parser_test @{context} (situate "ALG/ALG001^5.p");
parser_test @{context} (situate "NUM/NUM021^1.p");
parser_test @{context} (situate "SYN/SYN000^1.p") \<close>
text"Run the parser over all problems."
ML \<open> if test_all @{context} then
(report @{context} "Testing parser";
S timed_test parser_test @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
else () \<close>
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
