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