more cleaning of tptp tests;
authorsultana
Tue Apr 17 16:14:07 2012 +0100 (2012-04-17)
changeset 47518b2f209258621
parent 47517 6bc4c66d8c1b
child 47519 9c3acd90063a
more cleaning of tptp tests;
src/HOL/TPTP/TPTP_Interpret_Test.thy
src/HOL/TPTP/TPTP_Parser_Example.thy
src/HOL/TPTP/TPTP_Parser_Test.thy
src/HOL/TPTP/TPTP_Test.thy
     1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  begin
     1.5  
     1.6  section "Interpreter tests"
     1.7 -(*
     1.8 +
     1.9  text "Interpret a problem."
    1.10  ML {*
    1.11    val (time, ((type_map, const_map, fmlas), thy)) =
    1.12 @@ -27,19 +27,18 @@
    1.13  
    1.14  text "... and display nicely."
    1.15  ML {*
    1.16 -  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
    1.17 -*}
    1.18 -ML {*
    1.19 +  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
    1.20 +
    1.21    (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
    1.22    List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
    1.23  *}
    1.24 -*)
    1.25  
    1.26  subsection "Multiple tests"
    1.27  
    1.28  ML {*
    1.29 +  (*default timeout is 1 min*)
    1.30    fun interpret timeout file thy =
    1.31 -    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout))
    1.32 +    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
    1.33       (TPTP_Interpret.interpret_file
    1.34         false
    1.35         (Path.dir tptp_probs_dir)
    1.36 @@ -50,18 +49,9 @@
    1.37    fun interpret_timed timeout file thy =
    1.38      Timing.timing (interpret timeout file) thy
    1.39  
    1.40 -  (*default timeout is 10 mins*)
    1.41    fun interpretation_test timeout ctxt =
    1.42      test_fn ctxt
    1.43 -     (fn file => (*FIXME use "interpret" function above*)
    1.44 -       TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout))
    1.45 -        (TPTP_Interpret.interpret_file
    1.46 -          false
    1.47 -          (Path.dir tptp_probs_dir)
    1.48 -          file
    1.49 -          []
    1.50 -          [])
    1.51 -          @{theory}(*FIXME*))
    1.52 +     (fn file => interpret timeout file (Proof_Context.theory_of ctxt))
    1.53       "interpreter"
    1.54       ()
    1.55  
    1.56 @@ -128,19 +118,20 @@
    1.57  *}
    1.58  
    1.59  ML {*
    1.60 - interpretation_tests 5 @{context}
    1.61 + interpretation_tests (get_timeout @{context}) @{context}
    1.62     (some_probs @ take_too_long @ timeouts @ more_probs)
    1.63  *}
    1.64  
    1.65 -declare [[warning_out = ""]]
    1.66  
    1.67  subsection "Test against whole TPTP"
    1.68  
    1.69  text "Run interpretation over all problems. This works only for logics
    1.70   for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
    1.71  ML {*
    1.72 -  report @{context} "Interpreting all problems.";
    1.73 -  (*val _ = S timed_test (interpretation_test 5) @{context}*)
    1.74 +  if test_all @{context} then
    1.75 +    (report @{context} "Interpreting all problems";
    1.76 +     S timed_test (interpretation_test (get_timeout @{context})) @{context})
    1.77 +  else ()
    1.78  *}
    1.79  
    1.80 -end
    1.81 +end
    1.82 \ No newline at end of file
     2.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Tue Apr 17 16:14:07 2012 +0100
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Tue Apr 17 16:14:07 2012 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  *)
     2.5  
     2.6  theory TPTP_Parser_Example
     2.7 -imports TPTP_Parser
     2.8 +imports TPTP_Parser TPTP_Interpret
     2.9  uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     3.2 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  *)
     3.5  
     3.6  theory TPTP_Parser_Test
     3.7 -imports TPTP_Test (*TPTP_Parser_Example*)
     3.8 +imports TPTP_Test TPTP_Parser_Example
     3.9  begin
    3.10  
    3.11  section "Parser tests"
    3.12 @@ -73,10 +73,11 @@
    3.13  *}
    3.14  
    3.15  text "Run the parser over all problems."
    3.16 -ML {*report @{context} "Testing parser"*}
    3.17  ML {*
    3.18 -(*  val _ = S timed_test parser_test @{context}*)
    3.19 +  if test_all @{context} then
    3.20 +    (report @{context} "Testing parser";
    3.21 +     S timed_test parser_test @{context})
    3.22 +  else ()
    3.23  *}
    3.24  
    3.25 -
    3.26  end
    3.27 \ No newline at end of file
     4.1 --- a/src/HOL/TPTP/TPTP_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     4.2 +++ b/src/HOL/TPTP/TPTP_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     4.3 @@ -1,9 +1,9 @@
     4.4  (*  Title:      HOL/TPTP/TPTP_Test.thy
     4.5 -5A    Author:     Nik Sultana, Cambridge University Computer Laboratory
     4.6 +    Author:     Nik Sultana, Cambridge University Computer Laboratory
     4.7  
     4.8 -Some tests for the TPTP interface. Some of the tests rely on the Isabelle
     4.9 -environment variable TPTP_PROBLEMS_PATH, which should point to the
    4.10 -TPTP-vX.Y.Z/Problems directory.
    4.11 +Some test support for the TPTP interface. Some of the tests rely on
    4.12 +the Isabelle environment variable TPTP_PROBLEMS_PATH, which should
    4.13 +point to the TPTP-vX.Y.Z/Problems directory.
    4.14  *)
    4.15  
    4.16  theory TPTP_Test
    4.17 @@ -11,7 +11,12 @@
    4.18  begin
    4.19  
    4.20  ML {*
    4.21 -  val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
    4.22 +  val tptp_test_out = Attrib.setup_config_string @{binding "tptp_test_out"} (K "")
    4.23 +  val tptp_test_all = Attrib.setup_config_bool @{binding "tptp_test_all"} (K false)
    4.24 +  val tptp_test_timeout =
    4.25 +    Attrib.setup_config_int @{binding "tptp_test_timeout"} (K 5)
    4.26 +  fun test_all ctxt = Config.get ctxt tptp_test_all
    4.27 +  fun get_timeout ctxt = Config.get ctxt tptp_test_timeout
    4.28    fun S x y z = x z (y z)
    4.29  *}
    4.30  
    4.31 @@ -47,12 +52,12 @@
    4.32  ML {*
    4.33    fun report ctxt str =
    4.34      let
    4.35 -      val warning_out = Config.get ctxt warning_out
    4.36 +      val tptp_test_out = Config.get ctxt tptp_test_out
    4.37      in
    4.38 -      if warning_out = "" then warning str
    4.39 +      if tptp_test_out = "" then warning str
    4.40        else
    4.41          let
    4.42 -          val out_stream = TextIO.openAppend warning_out
    4.43 +          val out_stream = TextIO.openAppend tptp_test_out
    4.44          in (TextIO.output (out_stream, str ^ "\n");
    4.45              TextIO.flushOut out_stream;
    4.46              TextIO.closeOut out_stream)
    4.47 @@ -108,6 +113,4 @@
    4.48       ()
    4.49  *}
    4.50  
    4.51 -declare [[warning_out = ""]]
    4.52 -
    4.53  end
    4.54 \ No newline at end of file