src/HOL/TPTP/TPTP_Test.thy
author sultana
Mon Apr 23 12:23:23 2012 +0100 (2012-04-23)
changeset 47687 bfbd2d0bb348
parent 47558 55b42f9af99d
child 55595 2e2e9bc7c4c6
permissions -rw-r--r--
moved function for testing problem-name parsing;
list of TPTP test files not immediately evaluated;
sultana@47512
     1
(*  Title:      HOL/TPTP/TPTP_Test.thy
sultana@47518
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
sultana@47512
     3
blanchet@47558
     4
Some test support for the TPTP interface. Some of the tests rely on the Isabelle
blanchet@47558
     5
environment variable $TPTP, which should point to the TPTP-vX.Y.Z directory.
sultana@47512
     6
*)
sultana@47512
     7
sultana@47512
     8
theory TPTP_Test
sultana@47512
     9
imports TPTP_Parser
sultana@47512
    10
begin
sultana@47512
    11
sultana@47512
    12
ML {*
sultana@47518
    13
  val tptp_test_out = Attrib.setup_config_string @{binding "tptp_test_out"} (K "")
sultana@47518
    14
  val tptp_test_all = Attrib.setup_config_bool @{binding "tptp_test_all"} (K false)
sultana@47518
    15
  val tptp_test_timeout =
sultana@47518
    16
    Attrib.setup_config_int @{binding "tptp_test_timeout"} (K 5)
sultana@47518
    17
  fun test_all ctxt = Config.get ctxt tptp_test_all
sultana@47518
    18
  fun get_timeout ctxt = Config.get ctxt tptp_test_timeout
sultana@47512
    19
  fun S x y z = x z (y z)
sultana@47512
    20
*}
sultana@47512
    21
sultana@47512
    22
section "Parser tests"
sultana@47512
    23
sultana@47512
    24
ML {*
sultana@47512
    25
  fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
sultana@47512
    26
  val payloads_of = map payload_of
sultana@47512
    27
*}
sultana@47512
    28
sultana@47512
    29
sultana@47512
    30
section "Source problems"
sultana@47512
    31
ML {*
sultana@47512
    32
  (*problem source*)
sultana@47512
    33
  val tptp_probs_dir =
blanchet@47558
    34
    Path.explode "$TPTP/Problems"
sultana@47512
    35
    |> Path.expand;
sultana@47512
    36
sultana@47512
    37
  (*list of files to under test*)
sultana@47687
    38
  fun test_files () = TPTP_Syntax.get_file_list tptp_probs_dir;
sultana@47512
    39
*}
sultana@47512
    40
sultana@47512
    41
sultana@47512
    42
section "Supporting test functions"
sultana@47512
    43
ML {*
sultana@47512
    44
  fun report ctxt str =
sultana@47512
    45
    let
sultana@47518
    46
      val tptp_test_out = Config.get ctxt tptp_test_out
sultana@47512
    47
    in
sultana@47518
    48
      if tptp_test_out = "" then warning str
sultana@47512
    49
      else
sultana@47512
    50
        let
sultana@47518
    51
          val out_stream = TextIO.openAppend tptp_test_out
sultana@47512
    52
        in (TextIO.output (out_stream, str ^ "\n");
sultana@47512
    53
            TextIO.flushOut out_stream;
sultana@47512
    54
            TextIO.closeOut out_stream)
sultana@47512
    55
        end
sultana@47512
    56
    end
sultana@47512
    57
sultana@47512
    58
  fun test_fn ctxt f msg default_val file_name =
sultana@47512
    59
    let
sultana@47512
    60
      val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
sultana@47512
    61
    in
sultana@47512
    62
     (f file_name; ())
sultana@47512
    63
     (*otherwise report exceptions as warnings*)
sultana@47512
    64
     handle exn =>
sultana@47512
    65
       if Exn.is_interrupt exn then
sultana@47512
    66
         reraise exn
sultana@47512
    67
       else
sultana@47512
    68
         (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
sultana@47512
    69
          " raised exception: " ^ ML_Compiler.exn_message exn);
sultana@47512
    70
          default_val)
sultana@47512
    71
    end
sultana@47512
    72
sultana@47512
    73
  fun timed_test ctxt f =
sultana@47512
    74
    let
sultana@47512
    75
      fun f' x = (f x; ())
sultana@47512
    76
      val time =
sultana@47687
    77
        Timing.timing (List.app f') (test_files ())
sultana@47512
    78
        |> fst
sultana@47512
    79
      val duration =
sultana@47512
    80
        #elapsed time
sultana@47512
    81
        |> Time.toSeconds
sultana@47512
    82
        |> Real.fromLargeInt
sultana@47512
    83
      val average =
sultana@47512
    84
        (StringCvt.FIX (SOME 3),
sultana@47687
    85
         (duration / Real.fromInt (length (test_files ()))))
sultana@47512
    86
        |-> Real.fmt
sultana@47512
    87
    in
sultana@47512
    88
      report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
sultana@47512
    89
       "s per problem)")
sultana@47512
    90
    end
sultana@47512
    91
*}
sultana@47512
    92
sultana@47512
    93
sultana@47512
    94
ML {*
sultana@47512
    95
  fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
sultana@47547
    96
sultana@47512
    97
  fun parser_test ctxt = (*FIXME argument order*)
sultana@47512
    98
    test_fn ctxt
sultana@47512
    99
     (fn file_name =>
sultana@47512
   100
        Path.implode file_name
sultana@47512
   101
        |> (fn file =>
sultana@47512
   102
             ((*report ctxt file; this is if you want the filename in the log*)
sultana@47512
   103
              TPTP_Parser.parse_file file)))
sultana@47512
   104
     "parser"
sultana@47512
   105
     ()
sultana@47547
   106
sultana@47547
   107
  fun parse_timed file =
sultana@47547
   108
    Timing.timing TPTP_Parser.parse_file (Path.implode file)
sultana@47512
   109
*}
sultana@47512
   110
sultana@47512
   111
end