equal
deleted
inserted
replaced
1 (* Title: HOL/TPTP/TPTP_Test.thy |
1 (* Title: HOL/TPTP/TPTP_Test.thy |
2 5A Author: Nik Sultana, Cambridge University Computer Laboratory |
2 Author: Nik Sultana, Cambridge University Computer Laboratory |
3 |
3 |
4 Some tests for the TPTP interface. Some of the tests rely on the Isabelle |
4 Some test support for the TPTP interface. Some of the tests rely on |
5 environment variable TPTP_PROBLEMS_PATH, which should point to the |
5 the Isabelle environment variable TPTP_PROBLEMS_PATH, which should |
6 TPTP-vX.Y.Z/Problems directory. |
6 point to the TPTP-vX.Y.Z/Problems directory. |
7 *) |
7 *) |
8 |
8 |
9 theory TPTP_Test |
9 theory TPTP_Test |
10 imports TPTP_Parser |
10 imports TPTP_Parser |
11 begin |
11 begin |
12 |
12 |
13 ML {* |
13 ML {* |
14 val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "") |
14 val tptp_test_out = Attrib.setup_config_string @{binding "tptp_test_out"} (K "") |
|
15 val tptp_test_all = Attrib.setup_config_bool @{binding "tptp_test_all"} (K false) |
|
16 val tptp_test_timeout = |
|
17 Attrib.setup_config_int @{binding "tptp_test_timeout"} (K 5) |
|
18 fun test_all ctxt = Config.get ctxt tptp_test_all |
|
19 fun get_timeout ctxt = Config.get ctxt tptp_test_timeout |
15 fun S x y z = x z (y z) |
20 fun S x y z = x z (y z) |
16 *} |
21 *} |
17 |
22 |
18 section "Parser tests" |
23 section "Parser tests" |
19 |
24 |
45 |
50 |
46 section "Supporting test functions" |
51 section "Supporting test functions" |
47 ML {* |
52 ML {* |
48 fun report ctxt str = |
53 fun report ctxt str = |
49 let |
54 let |
50 val warning_out = Config.get ctxt warning_out |
55 val tptp_test_out = Config.get ctxt tptp_test_out |
51 in |
56 in |
52 if warning_out = "" then warning str |
57 if tptp_test_out = "" then warning str |
53 else |
58 else |
54 let |
59 let |
55 val out_stream = TextIO.openAppend warning_out |
60 val out_stream = TextIO.openAppend tptp_test_out |
56 in (TextIO.output (out_stream, str ^ "\n"); |
61 in (TextIO.output (out_stream, str ^ "\n"); |
57 TextIO.flushOut out_stream; |
62 TextIO.flushOut out_stream; |
58 TextIO.closeOut out_stream) |
63 TextIO.closeOut out_stream) |
59 end |
64 end |
60 end |
65 end |
106 TPTP_Parser.parse_file file))) |
111 TPTP_Parser.parse_file file))) |
107 "parser" |
112 "parser" |
108 () |
113 () |
109 *} |
114 *} |
110 |
115 |
111 declare [[warning_out = ""]] |
|
112 |
|
113 end |
116 end |