# HG changeset patch
# User sultana
# Date 1334675647 -3600
# Node ID b2f209258621e762314ddc41bffe4abc61d1cb6a
# Parent  6bc4c66d8c1ba4f867ea3998991d6f83d3a58f25
more cleaning of tptp tests;

diff -r 6bc4c66d8c1b -r b2f209258621 src/HOL/TPTP/TPTP_Interpret_Test.thy
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Tue Apr 17 16:14:07 2012 +0100
@@ -11,7 +11,7 @@
 begin
 
 section "Interpreter tests"
-(*
+
 text "Interpret a problem."
 ML {*
   val (time, ((type_map, const_map, fmlas), thy)) =
@@ -27,19 +27,18 @@
 
 text "... and display nicely."
 ML {*
-  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
-*}
-ML {*
+  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
+
   (*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 {*
+  (*default timeout is 1 min*)
   fun interpret timeout file thy =
-    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout))
+    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
      (TPTP_Interpret.interpret_file
        false
        (Path.dir tptp_probs_dir)
@@ -50,18 +49,9 @@
   fun interpret_timed timeout file thy =
     Timing.timing (interpret timeout file) thy
 
-  (*default timeout is 10 mins*)
   fun interpretation_test timeout ctxt =
     test_fn ctxt
-     (fn file => (*FIXME use "interpret" function above*)
-       TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout))
-        (TPTP_Interpret.interpret_file
-          false
-          (Path.dir tptp_probs_dir)
-          file
-          []
-          [])
-          @{theory}(*FIXME*))
+     (fn file => interpret timeout file (Proof_Context.theory_of ctxt))
      "interpreter"
      ()
 
@@ -128,19 +118,20 @@
 *}
 
 ML {*
- interpretation_tests 5 @{context}
+ interpretation_tests (get_timeout @{context}) @{context}
    (some_probs @ take_too_long @ timeouts @ more_probs)
 *}
 
-declare [[warning_out = ""]]
 
 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.";
-  (*val _ = S timed_test (interpretation_test 5) @{context}*)
+  if test_all @{context} then
+    (report @{context} "Interpreting all problems";
+     S timed_test (interpretation_test (get_timeout @{context})) @{context})
+  else ()
 *}
 
-end
+end
\ No newline at end of file
diff -r 6bc4c66d8c1b -r b2f209258621 src/HOL/TPTP/TPTP_Parser_Example.thy
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Tue Apr 17 16:14:07 2012 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory TPTP_Parser_Example
-imports TPTP_Parser
+imports TPTP_Parser TPTP_Interpret
 uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
 begin
 
diff -r 6bc4c66d8c1b -r b2f209258621 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,7 +7,7 @@
 *)
 
 theory TPTP_Parser_Test
-imports TPTP_Test (*TPTP_Parser_Example*)
+imports TPTP_Test TPTP_Parser_Example
 begin
 
 section "Parser tests"
@@ -73,10 +73,11 @@
 *}
 
 text "Run the parser over all problems."
-ML {*report @{context} "Testing parser"*}
 ML {*
-(*  val _ = S timed_test parser_test @{context}*)
+  if test_all @{context} then
+    (report @{context} "Testing parser";
+     S timed_test parser_test @{context})
+  else ()
 *}
 
-
 end
\ No newline at end of file
diff -r 6bc4c66d8c1b -r b2f209258621 src/HOL/TPTP/TPTP_Test.thy
--- a/src/HOL/TPTP/TPTP_Test.thy	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Test.thy	Tue Apr 17 16:14:07 2012 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOL/TPTP/TPTP_Test.thy
-5A    Author:     Nik Sultana, Cambridge University Computer Laboratory
+    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.
+Some test support 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
@@ -11,7 +11,12 @@
 begin
 
 ML {*
-  val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
+  val tptp_test_out = Attrib.setup_config_string @{binding "tptp_test_out"} (K "")
+  val tptp_test_all = Attrib.setup_config_bool @{binding "tptp_test_all"} (K false)
+  val tptp_test_timeout =
+    Attrib.setup_config_int @{binding "tptp_test_timeout"} (K 5)
+  fun test_all ctxt = Config.get ctxt tptp_test_all
+  fun get_timeout ctxt = Config.get ctxt tptp_test_timeout
   fun S x y z = x z (y z)
 *}
 
@@ -47,12 +52,12 @@
 ML {*
   fun report ctxt str =
     let
-      val warning_out = Config.get ctxt warning_out
+      val tptp_test_out = Config.get ctxt tptp_test_out
     in
-      if warning_out = "" then warning str
+      if tptp_test_out = "" then warning str
       else
         let
-          val out_stream = TextIO.openAppend warning_out
+          val out_stream = TextIO.openAppend tptp_test_out
         in (TextIO.output (out_stream, str ^ "\n");
             TextIO.flushOut out_stream;
             TextIO.closeOut out_stream)
@@ -108,6 +113,4 @@
      ()
 *}
 
-declare [[warning_out = ""]]
-
 end
\ No newline at end of file