# HG changeset patch # User sultana # Date 1334675647 -3600 # Node ID b381d428a7259dfd88bc19ef2ebc66b8d6b67fcf # Parent 016ce79deb01b22e24aba208cd7debd925c70301 reorganised tptp testing thys diff -r 016ce79deb01 -r b381d428a725 src/HOL/TPTP/TPTP_Interpret_Test.thy --- /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 diff -r 016ce79deb01 -r b381d428a725 src/HOL/TPTP/TPTP_Parser_Test.thy --- 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 diff -r 016ce79deb01 -r b381d428a725 src/HOL/TPTP/TPTP_Test.thy --- /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