more tptp testing support functions;

--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Apr 18 18:24:16 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Apr 18 17:33:11 2012 +0100
@@ -114,12 +114,36 @@
 *}
 
 ML {*
+ interpretation_tests (get_timeout @{context}) @{context}
+   (some_probs @ take_too_long @ timeouts @ more_probs)
+*}
+
+ML {*
+  parse_timed (situate "NUM/NUM923^4.p");
   interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
 *}
 
 ML {*
- interpretation_tests (get_timeout @{context}) @{context}
-   (some_probs @ take_too_long @ timeouts @ more_probs)
+  fun interp_gain timeout thy file =
+    let
+      val t1 = (parse_timed file |> fst)
+      val t2 = (interpret_timed timeout file thy |> fst)
+        handle exn => (*FIXME*)
+          if Exn.is_interrupt exn then reraise exn
+          else
+            (warning (" test: file " ^ Path.print file ^
+             " raised exception: " ^ ML_Compiler.exn_message exn);
+             {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
+      val to_real = Time.toReal
+      val diff_elapsed =
+        #elapsed t2 - #elapsed t1
+        |> to_real
+      val elapsed = to_real (#elapsed t2)
+    in
+      (Path.base file, diff_elapsed,
+       diff_elapsed / elapsed,
+       elapsed)
+    end
 *}
 
 

--- a/src/HOL/TPTP/TPTP_Test.thy	Wed Apr 18 18:24:16 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Test.thy	Wed Apr 18 17:33:11 2012 +0100
@@ -102,6 +102,7 @@
 
 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 =>
@@ -111,6 +112,9 @@
               TPTP_Parser.parse_file file)))
      "parser"
      ()
+
+  fun parse_timed file =
+    Timing.timing TPTP_Parser.parse_file (Path.implode file)
 *}
 
 end
\ No newline at end of file