# HG changeset patch
# User sultana
# Date 1335180203 -3600
# Node ID bfbd2d0bb34856fb47e306ea2e539703505b581d
# Parent  ba064cc165df9608914b4809ff20b9655e9793e8
moved function for testing problem-name parsing;
list of TPTP test files not immediately evaluated;

diff -r ba064cc165df -r bfbd2d0bb348 src/HOL/TPTP/TPTP_Parser_Example.thy
--- 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 =
diff -r ba064cc165df -r bfbd2d0bb348 src/HOL/TPTP/TPTP_Parser_Test.thy
--- 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 ())
 *}
 
 
diff -r ba064cc165df -r bfbd2d0bb348 src/HOL/TPTP/TPTP_Test.thy
--- 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 ^