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