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