--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Tue Apr 17 16:14:07 2012 +0100
@@ -0,0 +1,128 @@
+(* Title: HOL/TPTP/TPTP_Interpret_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_PROBLEMS_PATH, which should point to the
+TPTP-vX.Y.Z/Problems directory.
+*)
+
+theory TPTP_Interpret_Test
+imports TPTP_Test TPTP_Interpret
+begin
+
+section "Interpreter tests"
+
+text "Interpret a problem."
+ML {*
+ val (time, ((type_map, const_map, fmlas), thy)) =
+ Timing.timing
+ (TPTP_Interpret.interpret_file
+ false
+ (Path.dir tptp_probs_dir)
+ (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
+ []
+ [])
+ @{theory}
+*}
+
+text "... and display nicely."
+ML {*
+ List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
+*}
+ML {*
+ (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
+ List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
+*}
+
+
+subsection "Multiple tests"
+
+ML {*
+ fun interpretation_test timeout ctxt =
+ test_fn ctxt
+ (fn file =>
+ TimeLimit.timeLimit (Time.fromSeconds timeout)
+ (TPTP_Interpret.interpret_file
+ false
+ (Path.dir tptp_probs_dir)
+ file
+ []
+ [])
+ @{theory})
+ "interpreter"
+ ()
+
+ fun interpretation_tests timeout ctxt probs =
+ List.app
+ (interpretation_test timeout ctxt)
+ (List.map situate probs)
+*}
+
+ML {*
+ val some_probs =
+ ["LCL/LCL825-1.p",
+ "ALG/ALG001^5.p",
+ "COM/COM003+2.p",
+ "COM/COM003-1.p",
+ "COM/COM024^5.p",
+ "DAT/DAT017=1.p",
+ "NUM/NUM021^1.p",
+ "NUM/NUM858=1.p",
+ "SYN/SYN000^2.p"]
+
+ val take_too_long =
+ ["NLP/NLP562+1.p",
+ "SWV/SWV546-1.010.p",
+ "SWV/SWV567-1.015.p",
+ "LCL/LCL680+1.020.p"]
+
+ val more_probs =
+ ["GEG/GEG014^1.p",
+ "GEG/GEG009^1.p",
+ "GEG/GEG004^1.p",
+ "GEG/GEG007^1.p",
+ "GEG/GEG016^1.p",
+ "GEG/GEG024=1.p",
+ "GEG/GEG010^1.p",
+ "GEG/GEG003^1.p",
+ "GEG/GEG018^1.p",
+ "SYN/SYN045^4.p",
+ "SYN/SYN001^4.001.p",
+ "SYN/SYN000^2.p",
+ "SYN/SYN387^4.p",
+ "SYN/SYN393^4.002.p",
+ "SYN/SYN978^4.p",
+ "SYN/SYN044^4.p",
+ "SYN/SYN393^4.003.p",
+ "SYN/SYN389^4.p"]
+*}
+
+ML {*
+ interpretation_tests 5 @{context}
+ (some_probs @ take_too_long @ more_probs)
+*}
+
+
+subsection "Test against whole TPTP"
+
+text "Run interpretation over all problems. This works only for logics
+ for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
+ML {*
+ report @{context} "Interpreting all problems.";
+ fun interpretation_test timeout ctxt =
+ test_fn ctxt
+ (fn file =>
+ TimeLimit.timeLimit (Time.fromSeconds timeout)
+ (TPTP_Interpret.interpret_file
+ false
+ (Path.dir tptp_probs_dir)
+ file
+ []
+ [])
+ @{theory})
+ "interpreter"
+ ()
+ (*val _ = S timed_test (interpretation_test 5) @{context}*)
+*}
+
+end
\ No newline at end of file
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy Tue Apr 17 16:14:07 2012 +0100
@@ -7,21 +7,12 @@
*)
theory TPTP_Parser_Test
-imports TPTP_Parser TPTP_Parser_Example
+imports TPTP_Test (*TPTP_Parser_Example*)
begin
-ML {*
- val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
- fun S x y z = x z (y z)
-*}
-
section "Parser tests"
ML {*
- fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
- val payloads_of = map payload_of
-*}
-ML {*
TPTP_Parser.parse_expression "" "fof(dt_k4_waybel34, axiom, ~ v3).";
TPTP_Parser.parse_expression "" "thf(dt_k4_waybel34, axiom, ~ ($true | $false)).";
TPTP_Parser.parse_expression ""
@@ -66,94 +57,6 @@
*}
-section "Source problems"
-ML {*
- (*problem source*)
- val tptp_probs_dir =
- Path.explode "$TPTP_PROBLEMS_PATH"
- |> Path.expand;
-
- (*list of files to under test*)
- val files = TPTP_Syntax.get_file_list tptp_probs_dir;
-
-(* (*test problem-name parsing and mangling*)
- val problem_names =
- map (Path.base #>
- Path.implode #>
- TPTP_Problem_Name.parse_problem_name #>
- TPTP_Problem_Name.mangle_problem_name)
- files*)
-*}
-
-
-section "Supporting test functions"
-ML {*
- fun report ctxt str =
- let
- val warning_out = Config.get ctxt warning_out
- in
- if warning_out = "" then warning str
- else
- let
- val out_stream = TextIO.openAppend warning_out
- in (TextIO.output (out_stream, str ^ "\n");
- TextIO.flushOut out_stream;
- TextIO.closeOut out_stream)
- end
- end
-
- fun test_fn ctxt f msg default_val file_name =
- let
- val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
- in
- (f file_name; ())
- (*otherwise report exceptions as warnings*)
- handle exn =>
- if Exn.is_interrupt exn then
- reraise exn
- else
- (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
- " raised exception: " ^ ML_Compiler.exn_message exn);
- default_val)
- end
-
- fun timed_test ctxt f =
- let
- fun f' x = (f x; ())
- val time =
- Timing.timing (List.app f') files
- |> fst
- val duration =
- #elapsed time
- |> Time.toSeconds
- |> Real.fromLargeInt
- val average =
- (StringCvt.FIX (SOME 3),
- (duration / Real.fromInt (length files)))
- |-> Real.fmt
- in
- report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
- "s per problem)")
- end
-*}
-
-
-subsection "More parser tests"
-ML {*
- fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
- fun parser_test ctxt = (*FIXME argument order*)
- test_fn ctxt
- (fn file_name =>
- Path.implode file_name
- |> (fn file =>
- ((*report ctxt file; this is if you want the filename in the log*)
- TPTP_Parser.parse_file file)))
- "parser"
- ()
-*}
-
-declare [[warning_out = ""]]
-
text "Parse a specific problem."
ML {*
map TPTP_Parser.parse_file
@@ -176,66 +79,4 @@
*}
-subsection "Interpretation"
-
-text "Interpret a problem."
-ML {*
- val (time, ((type_map, const_map, fmlas), thy)) =
- Timing.timing
- (TPTP_Interpret.interpret_file
- false
- (Path.dir tptp_probs_dir)
- (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
- []
- [])
- @{theory}
-
- (*also tried
- "ALG/ALG001^5.p"
- "COM/COM003+2.p"
- "COM/COM003-1.p"
- "COM/COM024^5.p"
- "DAT/DAT017=1.p"
- "NUM/NUM021^1.p"
- "NUM/NUM858=1.p"
- "SYN/SYN000^2.p"*)
-
- (*These take too long
- "NLP/NLP562+1.p"
- "SWV/SWV546-1.010.p"
- "SWV/SWV567-1.015.p"
- "LCL/LCL680+1.020.p"*)
-*}
-
-text "... and display nicely."
-ML {*
- List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
-*}
-ML {*
- (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
- List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
-*}
-
-
-text "Run interpretation over all problems. This works only for logics
- for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
-ML {*
- report @{context} "Interpreting all problems.";
- fun interpretation_test timeout ctxt =
- test_fn ctxt
- (fn file =>
- (writeln (Path.implode file);
- TimeLimit.timeLimit (Time.fromSeconds timeout)
- (TPTP_Interpret.interpret_file
- false
- (Path.dir tptp_probs_dir)
- file
- []
- [])
- @{theory}))
- "interpreter"
- ()
- val _ = S timed_test (interpretation_test 5) @{context}
-*}
-
end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Test.thy Tue Apr 17 16:14:07 2012 +0100
@@ -0,0 +1,113 @@
+(* Title: HOL/TPTP/TPTP_Test.thy
+5A Author: Nik Sultana, Cambridge University Computer Laboratory
+
+Some tests for the TPTP interface. Some of the tests rely on the Isabelle
+environment variable TPTP_PROBLEMS_PATH, which should point to the
+TPTP-vX.Y.Z/Problems directory.
+*)
+
+theory TPTP_Test
+imports TPTP_Parser
+begin
+
+ML {*
+ val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
+ fun S x y z = x z (y z)
+*}
+
+section "Parser tests"
+
+ML {*
+ fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
+ val payloads_of = map payload_of
+*}
+
+
+section "Source problems"
+ML {*
+ (*problem source*)
+ val tptp_probs_dir =
+ Path.explode "$TPTP_PROBLEMS_PATH"
+ |> Path.expand;
+
+ (*list of files to under test*)
+ val files = TPTP_Syntax.get_file_list tptp_probs_dir;
+
+(* (*test problem-name parsing and mangling*)
+ val problem_names =
+ map (Path.base #>
+ Path.implode #>
+ TPTP_Problem_Name.parse_problem_name #>
+ TPTP_Problem_Name.mangle_problem_name)
+ files*)
+*}
+
+
+section "Supporting test functions"
+ML {*
+ fun report ctxt str =
+ let
+ val warning_out = Config.get ctxt warning_out
+ in
+ if warning_out = "" then warning str
+ else
+ let
+ val out_stream = TextIO.openAppend warning_out
+ in (TextIO.output (out_stream, str ^ "\n");
+ TextIO.flushOut out_stream;
+ TextIO.closeOut out_stream)
+ end
+ end
+
+ fun test_fn ctxt f msg default_val file_name =
+ let
+ val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
+ in
+ (f file_name; ())
+ (*otherwise report exceptions as warnings*)
+ handle exn =>
+ if Exn.is_interrupt exn then
+ reraise exn
+ else
+ (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
+ " raised exception: " ^ ML_Compiler.exn_message exn);
+ default_val)
+ end
+
+ fun timed_test ctxt f =
+ let
+ fun f' x = (f x; ())
+ val time =
+ Timing.timing (List.app f') files
+ |> fst
+ val duration =
+ #elapsed time
+ |> Time.toSeconds
+ |> Real.fromLargeInt
+ val average =
+ (StringCvt.FIX (SOME 3),
+ (duration / Real.fromInt (length files)))
+ |-> Real.fmt
+ in
+ report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
+ "s per problem)")
+ end
+*}
+
+
+ML {*
+ fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
+ fun parser_test ctxt = (*FIXME argument order*)
+ test_fn ctxt
+ (fn file_name =>
+ Path.implode file_name
+ |> (fn file =>
+ ((*report ctxt file; this is if you want the filename in the log*)
+ TPTP_Parser.parse_file file)))
+ "parser"
+ ()
+*}
+
+declare [[warning_out = ""]]
+
+end
\ No newline at end of file