1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Tue Apr 17 16:14:07 2012 +0100
1.3 @@ -0,0 +1,128 @@
1.4 +(* Title: HOL/TPTP/TPTP_Interpret_Test.thy
1.5 + Author: Nik Sultana, Cambridge University Computer Laboratory
1.6 +
1.7 +Some tests for the TPTP interface. Some of the tests rely on the Isabelle
1.8 +environment variable TPTP_PROBLEMS_PATH, which should point to the
1.9 +TPTP-vX.Y.Z/Problems directory.
1.10 +*)
1.11 +
1.12 +theory TPTP_Interpret_Test
1.13 +imports TPTP_Test TPTP_Interpret
1.14 +begin
1.15 +
1.16 +section "Interpreter tests"
1.17 +
1.18 +text "Interpret a problem."
1.19 +ML {*
1.20 + val (time, ((type_map, const_map, fmlas), thy)) =
1.21 + Timing.timing
1.22 + (TPTP_Interpret.interpret_file
1.23 + false
1.24 + (Path.dir tptp_probs_dir)
1.25 + (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
1.26 + []
1.27 + [])
1.28 + @{theory}
1.29 +*}
1.30 +
1.31 +text "... and display nicely."
1.32 +ML {*
1.33 + List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
1.34 +*}
1.35 +ML {*
1.36 + (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
1.37 + List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
1.38 +*}
1.39 +
1.40 +
1.41 +subsection "Multiple tests"
1.42 +
1.43 +ML {*
1.44 + fun interpretation_test timeout ctxt =
1.45 + test_fn ctxt
1.46 + (fn file =>
1.47 + TimeLimit.timeLimit (Time.fromSeconds timeout)
1.48 + (TPTP_Interpret.interpret_file
1.49 + false
1.50 + (Path.dir tptp_probs_dir)
1.51 + file
1.52 + []
1.53 + [])
1.54 + @{theory})
1.55 + "interpreter"
1.56 + ()
1.57 +
1.58 + fun interpretation_tests timeout ctxt probs =
1.59 + List.app
1.60 + (interpretation_test timeout ctxt)
1.61 + (List.map situate probs)
1.62 +*}
1.63 +
1.64 +ML {*
1.65 + val some_probs =
1.66 + ["LCL/LCL825-1.p",
1.67 + "ALG/ALG001^5.p",
1.68 + "COM/COM003+2.p",
1.69 + "COM/COM003-1.p",
1.70 + "COM/COM024^5.p",
1.71 + "DAT/DAT017=1.p",
1.72 + "NUM/NUM021^1.p",
1.73 + "NUM/NUM858=1.p",
1.74 + "SYN/SYN000^2.p"]
1.75 +
1.76 + val take_too_long =
1.77 + ["NLP/NLP562+1.p",
1.78 + "SWV/SWV546-1.010.p",
1.79 + "SWV/SWV567-1.015.p",
1.80 + "LCL/LCL680+1.020.p"]
1.81 +
1.82 + val more_probs =
1.83 + ["GEG/GEG014^1.p",
1.84 + "GEG/GEG009^1.p",
1.85 + "GEG/GEG004^1.p",
1.86 + "GEG/GEG007^1.p",
1.87 + "GEG/GEG016^1.p",
1.88 + "GEG/GEG024=1.p",
1.89 + "GEG/GEG010^1.p",
1.90 + "GEG/GEG003^1.p",
1.91 + "GEG/GEG018^1.p",
1.92 + "SYN/SYN045^4.p",
1.93 + "SYN/SYN001^4.001.p",
1.94 + "SYN/SYN000^2.p",
1.95 + "SYN/SYN387^4.p",
1.96 + "SYN/SYN393^4.002.p",
1.97 + "SYN/SYN978^4.p",
1.98 + "SYN/SYN044^4.p",
1.99 + "SYN/SYN393^4.003.p",
1.100 + "SYN/SYN389^4.p"]
1.101 +*}
1.102 +
1.103 +ML {*
1.104 + interpretation_tests 5 @{context}
1.105 + (some_probs @ take_too_long @ more_probs)
1.106 +*}
1.107 +
1.108 +
1.109 +subsection "Test against whole TPTP"
1.110 +
1.111 +text "Run interpretation over all problems. This works only for logics
1.112 + for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
1.113 +ML {*
1.114 + report @{context} "Interpreting all problems.";
1.115 + fun interpretation_test timeout ctxt =
1.116 + test_fn ctxt
1.117 + (fn file =>
1.118 + TimeLimit.timeLimit (Time.fromSeconds timeout)
1.119 + (TPTP_Interpret.interpret_file
1.120 + false
1.121 + (Path.dir tptp_probs_dir)
1.122 + file
1.123 + []
1.124 + [])
1.125 + @{theory})
1.126 + "interpreter"
1.127 + ()
1.128 + (*val _ = S timed_test (interpretation_test 5) @{context}*)
1.129 +*}
1.130 +
1.131 +end
1.132 \ No newline at end of file
2.1 --- a/src/HOL/TPTP/TPTP_Parser_Test.thy Tue Apr 17 16:14:07 2012 +0100
2.2 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy Tue Apr 17 16:14:07 2012 +0100
2.3 @@ -7,21 +7,12 @@
2.4 *)
2.5
2.6 theory TPTP_Parser_Test
2.7 -imports TPTP_Parser TPTP_Parser_Example
2.8 +imports TPTP_Test (*TPTP_Parser_Example*)
2.9 begin
2.10
2.11 -ML {*
2.12 - val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
2.13 - fun S x y z = x z (y z)
2.14 -*}
2.15 -
2.16 section "Parser tests"
2.17
2.18 ML {*
2.19 - fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
2.20 - val payloads_of = map payload_of
2.21 -*}
2.22 -ML {*
2.23 TPTP_Parser.parse_expression "" "fof(dt_k4_waybel34, axiom, ~ v3).";
2.24 TPTP_Parser.parse_expression "" "thf(dt_k4_waybel34, axiom, ~ ($true | $false)).";
2.25 TPTP_Parser.parse_expression ""
2.26 @@ -66,94 +57,6 @@
2.27 *}
2.28
2.29
2.30 -section "Source problems"
2.31 -ML {*
2.32 - (*problem source*)
2.33 - val tptp_probs_dir =
2.34 - Path.explode "$TPTP_PROBLEMS_PATH"
2.35 - |> Path.expand;
2.36 -
2.37 - (*list of files to under test*)
2.38 - val files = TPTP_Syntax.get_file_list tptp_probs_dir;
2.39 -
2.40 -(* (*test problem-name parsing and mangling*)
2.41 - val problem_names =
2.42 - map (Path.base #>
2.43 - Path.implode #>
2.44 - TPTP_Problem_Name.parse_problem_name #>
2.45 - TPTP_Problem_Name.mangle_problem_name)
2.46 - files*)
2.47 -*}
2.48 -
2.49 -
2.50 -section "Supporting test functions"
2.51 -ML {*
2.52 - fun report ctxt str =
2.53 - let
2.54 - val warning_out = Config.get ctxt warning_out
2.55 - in
2.56 - if warning_out = "" then warning str
2.57 - else
2.58 - let
2.59 - val out_stream = TextIO.openAppend warning_out
2.60 - in (TextIO.output (out_stream, str ^ "\n");
2.61 - TextIO.flushOut out_stream;
2.62 - TextIO.closeOut out_stream)
2.63 - end
2.64 - end
2.65 -
2.66 - fun test_fn ctxt f msg default_val file_name =
2.67 - let
2.68 - val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
2.69 - in
2.70 - (f file_name; ())
2.71 - (*otherwise report exceptions as warnings*)
2.72 - handle exn =>
2.73 - if Exn.is_interrupt exn then
2.74 - reraise exn
2.75 - else
2.76 - (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
2.77 - " raised exception: " ^ ML_Compiler.exn_message exn);
2.78 - default_val)
2.79 - end
2.80 -
2.81 - fun timed_test ctxt f =
2.82 - let
2.83 - fun f' x = (f x; ())
2.84 - val time =
2.85 - Timing.timing (List.app f') files
2.86 - |> fst
2.87 - val duration =
2.88 - #elapsed time
2.89 - |> Time.toSeconds
2.90 - |> Real.fromLargeInt
2.91 - val average =
2.92 - (StringCvt.FIX (SOME 3),
2.93 - (duration / Real.fromInt (length files)))
2.94 - |-> Real.fmt
2.95 - in
2.96 - report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
2.97 - "s per problem)")
2.98 - end
2.99 -*}
2.100 -
2.101 -
2.102 -subsection "More parser tests"
2.103 -ML {*
2.104 - fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
2.105 - fun parser_test ctxt = (*FIXME argument order*)
2.106 - test_fn ctxt
2.107 - (fn file_name =>
2.108 - Path.implode file_name
2.109 - |> (fn file =>
2.110 - ((*report ctxt file; this is if you want the filename in the log*)
2.111 - TPTP_Parser.parse_file file)))
2.112 - "parser"
2.113 - ()
2.114 -*}
2.115 -
2.116 -declare [[warning_out = ""]]
2.117 -
2.118 text "Parse a specific problem."
2.119 ML {*
2.120 map TPTP_Parser.parse_file
2.121 @@ -176,66 +79,4 @@
2.122 *}
2.123
2.124
2.125 -subsection "Interpretation"
2.126 -
2.127 -text "Interpret a problem."
2.128 -ML {*
2.129 - val (time, ((type_map, const_map, fmlas), thy)) =
2.130 - Timing.timing
2.131 - (TPTP_Interpret.interpret_file
2.132 - false
2.133 - (Path.dir tptp_probs_dir)
2.134 - (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
2.135 - []
2.136 - [])
2.137 - @{theory}
2.138 -
2.139 - (*also tried
2.140 - "ALG/ALG001^5.p"
2.141 - "COM/COM003+2.p"
2.142 - "COM/COM003-1.p"
2.143 - "COM/COM024^5.p"
2.144 - "DAT/DAT017=1.p"
2.145 - "NUM/NUM021^1.p"
2.146 - "NUM/NUM858=1.p"
2.147 - "SYN/SYN000^2.p"*)
2.148 -
2.149 - (*These take too long
2.150 - "NLP/NLP562+1.p"
2.151 - "SWV/SWV546-1.010.p"
2.152 - "SWV/SWV567-1.015.p"
2.153 - "LCL/LCL680+1.020.p"*)
2.154 -*}
2.155 -
2.156 -text "... and display nicely."
2.157 -ML {*
2.158 - List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
2.159 -*}
2.160 -ML {*
2.161 - (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
2.162 - List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
2.163 -*}
2.164 -
2.165 -
2.166 -text "Run interpretation over all problems. This works only for logics
2.167 - for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
2.168 -ML {*
2.169 - report @{context} "Interpreting all problems.";
2.170 - fun interpretation_test timeout ctxt =
2.171 - test_fn ctxt
2.172 - (fn file =>
2.173 - (writeln (Path.implode file);
2.174 - TimeLimit.timeLimit (Time.fromSeconds timeout)
2.175 - (TPTP_Interpret.interpret_file
2.176 - false
2.177 - (Path.dir tptp_probs_dir)
2.178 - file
2.179 - []
2.180 - [])
2.181 - @{theory}))
2.182 - "interpreter"
2.183 - ()
2.184 - val _ = S timed_test (interpretation_test 5) @{context}
2.185 -*}
2.186 -
2.187 end
2.188 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/TPTP/TPTP_Test.thy Tue Apr 17 16:14:07 2012 +0100
3.3 @@ -0,0 +1,113 @@
3.4 +(* Title: HOL/TPTP/TPTP_Test.thy
3.5 +5A Author: Nik Sultana, Cambridge University Computer Laboratory
3.6 +
3.7 +Some tests for the TPTP interface. Some of the tests rely on the Isabelle
3.8 +environment variable TPTP_PROBLEMS_PATH, which should point to the
3.9 +TPTP-vX.Y.Z/Problems directory.
3.10 +*)
3.11 +
3.12 +theory TPTP_Test
3.13 +imports TPTP_Parser
3.14 +begin
3.15 +
3.16 +ML {*
3.17 + val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
3.18 + fun S x y z = x z (y z)
3.19 +*}
3.20 +
3.21 +section "Parser tests"
3.22 +
3.23 +ML {*
3.24 + fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
3.25 + val payloads_of = map payload_of
3.26 +*}
3.27 +
3.28 +
3.29 +section "Source problems"
3.30 +ML {*
3.31 + (*problem source*)
3.32 + val tptp_probs_dir =
3.33 + Path.explode "$TPTP_PROBLEMS_PATH"
3.34 + |> Path.expand;
3.35 +
3.36 + (*list of files to under test*)
3.37 + val files = TPTP_Syntax.get_file_list tptp_probs_dir;
3.38 +
3.39 +(* (*test problem-name parsing and mangling*)
3.40 + val problem_names =
3.41 + map (Path.base #>
3.42 + Path.implode #>
3.43 + TPTP_Problem_Name.parse_problem_name #>
3.44 + TPTP_Problem_Name.mangle_problem_name)
3.45 + files*)
3.46 +*}
3.47 +
3.48 +
3.49 +section "Supporting test functions"
3.50 +ML {*
3.51 + fun report ctxt str =
3.52 + let
3.53 + val warning_out = Config.get ctxt warning_out
3.54 + in
3.55 + if warning_out = "" then warning str
3.56 + else
3.57 + let
3.58 + val out_stream = TextIO.openAppend warning_out
3.59 + in (TextIO.output (out_stream, str ^ "\n");
3.60 + TextIO.flushOut out_stream;
3.61 + TextIO.closeOut out_stream)
3.62 + end
3.63 + end
3.64 +
3.65 + fun test_fn ctxt f msg default_val file_name =
3.66 + let
3.67 + val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
3.68 + in
3.69 + (f file_name; ())
3.70 + (*otherwise report exceptions as warnings*)
3.71 + handle exn =>
3.72 + if Exn.is_interrupt exn then
3.73 + reraise exn
3.74 + else
3.75 + (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
3.76 + " raised exception: " ^ ML_Compiler.exn_message exn);
3.77 + default_val)
3.78 + end
3.79 +
3.80 + fun timed_test ctxt f =
3.81 + let
3.82 + fun f' x = (f x; ())
3.83 + val time =
3.84 + Timing.timing (List.app f') files
3.85 + |> fst
3.86 + val duration =
3.87 + #elapsed time
3.88 + |> Time.toSeconds
3.89 + |> Real.fromLargeInt
3.90 + val average =
3.91 + (StringCvt.FIX (SOME 3),
3.92 + (duration / Real.fromInt (length files)))
3.93 + |-> Real.fmt
3.94 + in
3.95 + report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
3.96 + "s per problem)")
3.97 + end
3.98 +*}
3.99 +
3.100 +
3.101 +ML {*
3.102 + fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
3.103 + fun parser_test ctxt = (*FIXME argument order*)
3.104 + test_fn ctxt
3.105 + (fn file_name =>
3.106 + Path.implode file_name
3.107 + |> (fn file =>
3.108 + ((*report ctxt file; this is if you want the filename in the log*)
3.109 + TPTP_Parser.parse_file file)))
3.110 + "parser"
3.111 + ()
3.112 +*}
3.113 +
3.114 +declare [[warning_out = ""]]
3.115 +
3.116 +end
3.117 \ No newline at end of file