moved function for testing problem-name parsing;
list of TPTP test files not immediately evaluated;
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Mon Apr 23 12:23:23 2012 +0100
@@ -9,7 +9,7 @@
uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
begin
-import_tptp "$TPTP/Problems/ALG/ALG001^5.p"
+import_tptp "$TPTP/Problems/CSR/CSR077+1.p"
ML {*
val an_fmlas =
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy Mon Apr 23 12:23:23 2012 +0100
@@ -44,6 +44,14 @@
val _ = map (fn (str, res) =>
@{assert}(TPTP_Problem_Name.parse_problem_name str = res)) name_tests
end
+
+(*test against all TPTP problems*)
+fun problem_names () =
+ map (Path.base #>
+ Path.implode #>
+ TPTP_Problem_Name.parse_problem_name #>
+ TPTP_Problem_Name.mangle_problem_name)
+ (test_files ())
*}
--- a/src/HOL/TPTP/TPTP_Test.thy Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Test.thy Mon Apr 23 12:23:23 2012 +0100
@@ -35,15 +35,7 @@
|> 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*)
+ fun test_files () = TPTP_Syntax.get_file_list tptp_probs_dir;
*}
@@ -82,7 +74,7 @@
let
fun f' x = (f x; ())
val time =
- Timing.timing (List.app f') files
+ Timing.timing (List.app f') (test_files ())
|> fst
val duration =
#elapsed time
@@ -90,7 +82,7 @@
|> Real.fromLargeInt
val average =
(StringCvt.FIX (SOME 3),
- (duration / Real.fromInt (length files)))
+ (duration / Real.fromInt (length (test_files ()))))
|-> Real.fmt
in
report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^