|
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 |
|
10 imports TPTP_Parser |
|
11 begin |
|
12 |
|
13 ML {* |
|
14 val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "") |
|
15 fun S x y z = x z (y z) |
|
16 *} |
|
17 |
|
18 section "Parser tests" |
|
19 |
|
20 ML {* |
|
21 fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla |
|
22 val payloads_of = map payload_of |
|
23 *} |
|
24 ML {* |
|
25 TPTP_Parser.parse_expression "" "fof(dt_k4_waybel34, axiom, ~ v3)."; |
|
26 TPTP_Parser.parse_expression "" "thf(dt_k4_waybel34, axiom, ~ ($true | $false))."; |
|
27 TPTP_Parser.parse_expression "" |
|
28 "thf(dt_k4_waybel34, axiom, ~ (! [X : $o, Y : ($o > $o)] : ( (X | (Y = Y)))))."; |
|
29 TPTP_Parser.parse_expression "" "tff(dt_k4_waybel34, axiom, ~ ($true))."; |
|
30 payloads_of it; |
|
31 *} |
|
32 ML {* |
|
33 TPTP_Parser.parse_expression "" "thf(bla, type, x : $o)."; |
|
34 TPTP_Parser.parse_expression "" |
|
35 "fof(dt_k4_waybel34, axiom, ~ v3_struct_0(k4_waybel34(A)))."; |
|
36 TPTP_Parser.parse_expression "" |
|
37 "fof(dt_k4_waybel34, axiom, (! [A] : (v1_xboole_0(A) => ( ~ v3_struct_0(k4_waybel34(A))))))."; |
|
38 *} |
|
39 ML {* |
|
40 TPTP_Parser.parse_expression "" |
|
41 ("fof(dt_k4_waybel34,axiom,(" ^ |
|
42 "! [A] :" ^ |
|
43 "( ~ v1_xboole_0(A)" ^ |
|
44 "=> ( ~ v3_struct_0(k4_waybel34(A))" ^ |
|
45 "& v2_altcat_1(k4_waybel34(A))" ^ |
|
46 "& v6_altcat_1(k4_waybel34(A))" ^ |
|
47 "& v11_altcat_1(k4_waybel34(A))" ^ |
|
48 "& v12_altcat_1(k4_waybel34(A))" ^ |
|
49 "& v2_yellow21(k4_waybel34(A))" ^ |
|
50 "& l2_altcat_1(k4_waybel34(A)) ) ) )).") |
|
51 *} |
|
52 |
|
53 ML {* |
|
54 open TPTP_Syntax; |
|
55 @{assert} |
|
56 ((TPTP_Parser.parse_expression "" |
|
57 "thf(x,axiom,^ [X] : ^ [Y] : f @ g)." |
|
58 |> payloads_of |> hd) |
|
59 = |
|
60 Fmla (Interpreted_ExtraLogic Apply, |
|
61 [Quant (Lambda, [("X", NONE)], |
|
62 Quant (Lambda, [("Y", NONE)], |
|
63 Atom (THF_Atom_term (Term_Func (Uninterpreted "f", []))))), |
|
64 Atom (THF_Atom_term (Term_Func (Uninterpreted "g", [])))]) |
|
65 ) |
|
66 *} |
|
67 |
|
68 |
|
69 section "Source problems" |
|
70 ML {* |
|
71 (*problem source*) |
|
72 val thf_probs_dir = |
|
73 Path.explode "$TPTP_PROBLEMS_PATH" |
|
74 |> Path.expand; |
|
75 |
|
76 (*list of files to under test*) |
|
77 val files = TPTP_Syntax.get_file_list thf_probs_dir; |
|
78 |
|
79 (* (*test problem-name parsing and mangling*) |
|
80 val problem_names = |
|
81 map (Path.base #> |
|
82 Path.implode #> |
|
83 TPTP_Problem_Name.parse_problem_name #> |
|
84 TPTP_Problem_Name.mangle_problem_name) |
|
85 files*) |
|
86 *} |
|
87 |
|
88 |
|
89 section "Supporting test functions" |
|
90 ML {* |
|
91 fun report ctxt str = |
|
92 let |
|
93 val warning_out = Config.get ctxt warning_out |
|
94 in |
|
95 if warning_out = "" then warning str |
|
96 else |
|
97 let |
|
98 val out_stream = TextIO.openAppend warning_out |
|
99 in (TextIO.output (out_stream, str ^ "\n"); |
|
100 TextIO.flushOut out_stream; |
|
101 TextIO.closeOut out_stream) |
|
102 end |
|
103 end |
|
104 |
|
105 fun test_fn ctxt f msg default_val file_name = |
|
106 let |
|
107 val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name) |
|
108 in |
|
109 (f file_name; ()) |
|
110 (*otherwise report exceptions as warnings*) |
|
111 handle exn => |
|
112 if Exn.is_interrupt exn then |
|
113 reraise exn |
|
114 else |
|
115 (report ctxt (msg ^ " test: file " ^ Path.print file_name ^ |
|
116 " raised exception: " ^ ML_Compiler.exn_message exn); |
|
117 default_val) |
|
118 end |
|
119 |
|
120 fun timed_test ctxt f = |
|
121 let |
|
122 fun f' x = (f x; ()) |
|
123 val time = |
|
124 Timing.timing (List.app f') files |
|
125 |> fst |
|
126 val duration = |
|
127 #elapsed time |
|
128 |> Time.toSeconds |
|
129 |> Real.fromLargeInt |
|
130 val average = |
|
131 (StringCvt.FIX (SOME 3), |
|
132 (duration / Real.fromInt (length files))) |
|
133 |-> Real.fmt |
|
134 in |
|
135 report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^ |
|
136 "s per problem)") |
|
137 end |
|
138 *} |
|
139 |
|
140 |
|
141 subsection "More parser tests" |
|
142 ML {* |
|
143 fun situate file_name = Path.append thf_probs_dir (Path.explode file_name); |
|
144 fun parser_test ctxt = (*FIXME argument order*) |
|
145 test_fn ctxt |
|
146 (fn file_name => |
|
147 Path.implode file_name |
|
148 |> (fn file => |
|
149 ((*report ctxt file; this is if you want the filename in the log*) |
|
150 TPTP_Parser.parse_file file))) |
|
151 "parser" |
|
152 () |
|
153 *} |
|
154 |
|
155 declare [[warning_out = ""]] |
|
156 |
|
157 text "Parse a specific problem." |
|
158 ML {* |
|
159 map TPTP_Parser.parse_file |
|
160 ["$TPTP_PROBLEMS_PATH/FLD/FLD051-1.p", |
|
161 "$TPTP_PROBLEMS_PATH/FLD/FLD005-3.p", |
|
162 "$TPTP_PROBLEMS_PATH/SWV/SWV567-1.015.p", |
|
163 "$TPTP_PROBLEMS_PATH/SWV/SWV546-1.010.p"] |
|
164 *} |
|
165 ML {* |
|
166 parser_test @{context} (situate "DAT/DAT001=1.p"); |
|
167 parser_test @{context} (situate "ALG/ALG001^5.p"); |
|
168 parser_test @{context} (situate "NUM/NUM021^1.p"); |
|
169 parser_test @{context} (situate "SYN/SYN000^1.p") |
|
170 *} |
|
171 |
|
172 text "Run the parser over all problems." |
|
173 ML {*report @{context} "Testing parser"*} |
|
174 ML {* |
|
175 (* val _ = S timed_test parser_test @{context}*) |
|
176 *} |
|
177 |
|
178 |
|
179 subsection "Interpretation" |
|
180 |
|
181 text "Interpret a problem." |
|
182 ML {* |
|
183 val (time, ((type_map, const_map, fmlas), thy)) = |
|
184 Timing.timing |
|
185 (TPTP_Interpret.interpret_file |
|
186 false |
|
187 (Path.dir thf_probs_dir) |
|
188 (Path.append thf_probs_dir (Path.explode "LCL/LCL825-1.p")) |
|
189 [] |
|
190 []) |
|
191 @{theory} |
|
192 |
|
193 (*also tried |
|
194 "ALG/ALG001^5.p" |
|
195 "COM/COM003+2.p" |
|
196 "COM/COM003-1.p" |
|
197 "COM/COM024^5.p" |
|
198 "DAT/DAT017=1.p" |
|
199 "NUM/NUM021^1.p" |
|
200 "NUM/NUM858=1.p" |
|
201 "SYN/SYN000^2.p"*) |
|
202 |
|
203 (*These take too long |
|
204 "NLP/NLP562+1.p" |
|
205 "SWV/SWV546-1.010.p" |
|
206 "SWV/SWV567-1.015.p" |
|
207 "LCL/LCL680+1.020.p"*) |
|
208 *} |
|
209 |
|
210 text "... and display nicely." |
|
211 ML {* |
|
212 List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas |
|
213 *} |
|
214 ML {* |
|
215 (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*) |
|
216 List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas |
|
217 *} |
|
218 |
|
219 |
|
220 text "Run interpretation over all problems. This works only for logics |
|
221 for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)." |
|
222 ML {* |
|
223 report @{context} "Interpreting all problems."; |
|
224 fun interpretation_test timeout ctxt = |
|
225 test_fn ctxt |
|
226 (fn file => |
|
227 (writeln (Path.implode file); |
|
228 TimeLimit.timeLimit (Time.fromSeconds timeout) |
|
229 (TPTP_Interpret.interpret_file |
|
230 false |
|
231 (Path.dir thf_probs_dir) |
|
232 file |
|
233 [] |
|
234 []) |
|
235 @{theory})) |
|
236 "interpreter" |
|
237 () |
|
238 val _ = S timed_test (interpretation_test 5) @{context} |
|
239 *} |
|
240 |
|
241 end |