|
46844
|
1 |
(* Title: HOL/TPTP/TPTP_Parser_Test.thy
|
|
|
2 |
Author: Nik Sultana, Cambridge University Computer Laboratory
|
|
|
3 |
|
|
|
4 |
Some tests for the TPTP interface. Some of the tests rely on the Isabelle
|
|
|
5 |
environment variable TPTP_PROBLEMS_PATH, which should point to the
|
|
|
6 |
TPTP-vX.Y.Z/Problems directory.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
theory TPTP_Parser_Test
|
|
47512
|
10 |
imports TPTP_Test (*TPTP_Parser_Example*)
|
|
46844
|
11 |
begin
|
|
|
12 |
|
|
|
13 |
section "Parser tests"
|
|
|
14 |
|
|
|
15 |
ML {*
|
|
|
16 |
TPTP_Parser.parse_expression "" "fof(dt_k4_waybel34, axiom, ~ v3).";
|
|
|
17 |
TPTP_Parser.parse_expression "" "thf(dt_k4_waybel34, axiom, ~ ($true | $false)).";
|
|
|
18 |
TPTP_Parser.parse_expression ""
|
|
|
19 |
"thf(dt_k4_waybel34, axiom, ~ (! [X : $o, Y : ($o > $o)] : ( (X | (Y = Y))))).";
|
|
|
20 |
TPTP_Parser.parse_expression "" "tff(dt_k4_waybel34, axiom, ~ ($true)).";
|
|
|
21 |
payloads_of it;
|
|
|
22 |
*}
|
|
|
23 |
ML {*
|
|
|
24 |
TPTP_Parser.parse_expression "" "thf(bla, type, x : $o).";
|
|
|
25 |
TPTP_Parser.parse_expression ""
|
|
|
26 |
"fof(dt_k4_waybel34, axiom, ~ v3_struct_0(k4_waybel34(A))).";
|
|
|
27 |
TPTP_Parser.parse_expression ""
|
|
|
28 |
"fof(dt_k4_waybel34, axiom, (! [A] : (v1_xboole_0(A) => ( ~ v3_struct_0(k4_waybel34(A)))))).";
|
|
|
29 |
*}
|
|
|
30 |
ML {*
|
|
|
31 |
TPTP_Parser.parse_expression ""
|
|
|
32 |
("fof(dt_k4_waybel34,axiom,(" ^
|
|
|
33 |
"! [A] :" ^
|
|
|
34 |
"( ~ v1_xboole_0(A)" ^
|
|
|
35 |
"=> ( ~ v3_struct_0(k4_waybel34(A))" ^
|
|
|
36 |
"& v2_altcat_1(k4_waybel34(A))" ^
|
|
|
37 |
"& v6_altcat_1(k4_waybel34(A))" ^
|
|
|
38 |
"& v11_altcat_1(k4_waybel34(A))" ^
|
|
|
39 |
"& v12_altcat_1(k4_waybel34(A))" ^
|
|
|
40 |
"& v2_yellow21(k4_waybel34(A))" ^
|
|
|
41 |
"& l2_altcat_1(k4_waybel34(A)) ) ) )).")
|
|
|
42 |
*}
|
|
|
43 |
|
|
|
44 |
ML {*
|
|
|
45 |
open TPTP_Syntax;
|
|
|
46 |
@{assert}
|
|
|
47 |
((TPTP_Parser.parse_expression ""
|
|
|
48 |
"thf(x,axiom,^ [X] : ^ [Y] : f @ g)."
|
|
|
49 |
|> payloads_of |> hd)
|
|
|
50 |
=
|
|
|
51 |
Fmla (Interpreted_ExtraLogic Apply,
|
|
|
52 |
[Quant (Lambda, [("X", NONE)],
|
|
|
53 |
Quant (Lambda, [("Y", NONE)],
|
|
|
54 |
Atom (THF_Atom_term (Term_Func (Uninterpreted "f", []))))),
|
|
|
55 |
Atom (THF_Atom_term (Term_Func (Uninterpreted "g", [])))])
|
|
|
56 |
)
|
|
|
57 |
*}
|
|
|
58 |
|
|
|
59 |
|
|
|
60 |
text "Parse a specific problem."
|
|
|
61 |
ML {*
|
|
|
62 |
map TPTP_Parser.parse_file
|
|
|
63 |
["$TPTP_PROBLEMS_PATH/FLD/FLD051-1.p",
|
|
|
64 |
"$TPTP_PROBLEMS_PATH/FLD/FLD005-3.p",
|
|
|
65 |
"$TPTP_PROBLEMS_PATH/SWV/SWV567-1.015.p",
|
|
|
66 |
"$TPTP_PROBLEMS_PATH/SWV/SWV546-1.010.p"]
|
|
|
67 |
*}
|
|
|
68 |
ML {*
|
|
|
69 |
parser_test @{context} (situate "DAT/DAT001=1.p");
|
|
|
70 |
parser_test @{context} (situate "ALG/ALG001^5.p");
|
|
|
71 |
parser_test @{context} (situate "NUM/NUM021^1.p");
|
|
|
72 |
parser_test @{context} (situate "SYN/SYN000^1.p")
|
|
|
73 |
*}
|
|
|
74 |
|
|
|
75 |
text "Run the parser over all problems."
|
|
|
76 |
ML {*report @{context} "Testing parser"*}
|
|
|
77 |
ML {*
|
|
|
78 |
(* val _ = S timed_test parser_test @{context}*)
|
|
|
79 |
*}
|
|
|
80 |
|
|
|
81 |
|
|
|
82 |
end |