src/HOL/TPTP/TPTP_Test.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63167 0909deb8059b
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
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
wenzelm@63167
    12
ML \<open>
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)
wenzelm@63167
    20
\<close>
sultana@47512
    21
sultana@47512
    22
section "Parser tests"
sultana@47512
    23
wenzelm@63167
    24
ML \<open>
sultana@47512
    25
  fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
sultana@47512
    26
  val payloads_of = map payload_of
wenzelm@63167
    27
\<close>
sultana@47512
    28
sultana@47512
    29
sultana@47512
    30
section "Source problems"
wenzelm@63167
    31
ML \<open>
sultana@47512
    32
  (*problem source*)
sultana@47512
    33
  val tptp_probs_dir =
blanchet@47558
    34
    Path.explode "$TPTP/Problems"
sultana@47512
    35
    |> Path.expand;
wenzelm@63167
    36
\<close>
sultana@47512
    37
sultana@47512
    38
sultana@47512
    39
section "Supporting test functions"
wenzelm@63167
    40
ML \<open>
sultana@47512
    41
  fun report ctxt str =
sultana@47512
    42
    let
sultana@47518
    43
      val tptp_test_out = Config.get ctxt tptp_test_out
sultana@47512
    44
    in
sultana@47518
    45
      if tptp_test_out = "" then warning str
sultana@47512
    46
      else
sultana@47512
    47
        let
sultana@47518
    48
          val out_stream = TextIO.openAppend tptp_test_out
sultana@47512
    49
        in (TextIO.output (out_stream, str ^ "\n");
sultana@47512
    50
            TextIO.flushOut out_stream;
sultana@47512
    51
            TextIO.closeOut out_stream)
sultana@47512
    52
        end
sultana@47512
    53
    end
sultana@47512
    54
sultana@47512
    55
  fun test_fn ctxt f msg default_val file_name =
sultana@47512
    56
    let
sultana@47512
    57
      val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
sultana@47512
    58
    in
sultana@47512
    59
     (f file_name; ())
sultana@47512
    60
     (*otherwise report exceptions as warnings*)
sultana@47512
    61
     handle exn =>
sultana@47512
    62
       if Exn.is_interrupt exn then
wenzelm@62505
    63
         Exn.reraise exn
sultana@47512
    64
       else
sultana@47512
    65
         (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
wenzelm@56303
    66
          " raised exception: " ^ Runtime.exn_message exn);
sultana@47512
    67
          default_val)
sultana@47512
    68
    end
sultana@47512
    69
sultana@55595
    70
  fun timed_test ctxt f test_files =
sultana@47512
    71
    let
sultana@47512
    72
      fun f' x = (f x; ())
sultana@47512
    73
      val time =
sultana@55595
    74
        Timing.timing (List.app f') test_files
sultana@47512
    75
        |> fst
sultana@47512
    76
      val duration =
sultana@47512
    77
        #elapsed time
sultana@47512
    78
        |> Time.toSeconds
sultana@47512
    79
        |> Real.fromLargeInt
sultana@47512
    80
      val average =
sultana@47512
    81
        (StringCvt.FIX (SOME 3),
sultana@55595
    82
         (duration / Real.fromInt (length test_files)))
sultana@47512
    83
        |-> Real.fmt
sultana@47512
    84
    in
sultana@47512
    85
      report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
sultana@47512
    86
       "s per problem)")
sultana@47512
    87
    end
wenzelm@63167
    88
\<close>
sultana@47512
    89
sultana@47512
    90
wenzelm@63167
    91
ML \<open>
sultana@47512
    92
  fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
sultana@47547
    93
sultana@47512
    94
  fun parser_test ctxt = (*FIXME argument order*)
sultana@47512
    95
    test_fn ctxt
sultana@47512
    96
     (fn file_name =>
sultana@47512
    97
        Path.implode file_name
sultana@47512
    98
        |> (fn file =>
sultana@47512
    99
             ((*report ctxt file; this is if you want the filename in the log*)
sultana@47512
   100
              TPTP_Parser.parse_file file)))
sultana@47512
   101
     "parser"
sultana@47512
   102
     ()
sultana@47547
   103
sultana@47547
   104
  fun parse_timed file =
sultana@47547
   105
    Timing.timing TPTP_Parser.parse_file (Path.implode file)
wenzelm@63167
   106
\<close>
sultana@47512
   107
nipkow@62390
   108
end