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