src/HOL/TPTP/TPTP_Test.thy
changeset 47512 b381d428a725
child 47518 b2f209258621
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/TPTP/TPTP_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     1.3 @@ -0,0 +1,113 @@
     1.4 +(*  Title:      HOL/TPTP/TPTP_Test.thy
     1.5 +5A    Author:     Nik Sultana, Cambridge University Computer Laboratory
     1.6 +
     1.7 +Some tests for the TPTP interface. Some of the tests rely on the Isabelle
     1.8 +environment variable TPTP_PROBLEMS_PATH, which should point to the
     1.9 +TPTP-vX.Y.Z/Problems directory.
    1.10 +*)
    1.11 +
    1.12 +theory TPTP_Test
    1.13 +imports TPTP_Parser
    1.14 +begin
    1.15 +
    1.16 +ML {*
    1.17 +  val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
    1.18 +  fun S x y z = x z (y z)
    1.19 +*}
    1.20 +
    1.21 +section "Parser tests"
    1.22 +
    1.23 +ML {*
    1.24 +  fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
    1.25 +  val payloads_of = map payload_of
    1.26 +*}
    1.27 +
    1.28 +
    1.29 +section "Source problems"
    1.30 +ML {*
    1.31 +  (*problem source*)
    1.32 +  val tptp_probs_dir =
    1.33 +    Path.explode "$TPTP_PROBLEMS_PATH"
    1.34 +    |> Path.expand;
    1.35 +
    1.36 +  (*list of files to under test*)
    1.37 +  val files = TPTP_Syntax.get_file_list tptp_probs_dir;
    1.38 +
    1.39 +(*  (*test problem-name parsing and mangling*)
    1.40 +  val problem_names =
    1.41 +    map (Path.base #>
    1.42 +         Path.implode #>
    1.43 +         TPTP_Problem_Name.parse_problem_name #>
    1.44 +         TPTP_Problem_Name.mangle_problem_name)
    1.45 +        files*)
    1.46 +*}
    1.47 +
    1.48 +
    1.49 +section "Supporting test functions"
    1.50 +ML {*
    1.51 +  fun report ctxt str =
    1.52 +    let
    1.53 +      val warning_out = Config.get ctxt warning_out
    1.54 +    in
    1.55 +      if warning_out = "" then warning str
    1.56 +      else
    1.57 +        let
    1.58 +          val out_stream = TextIO.openAppend warning_out
    1.59 +        in (TextIO.output (out_stream, str ^ "\n");
    1.60 +            TextIO.flushOut out_stream;
    1.61 +            TextIO.closeOut out_stream)
    1.62 +        end
    1.63 +    end
    1.64 +
    1.65 +  fun test_fn ctxt f msg default_val file_name =
    1.66 +    let
    1.67 +      val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
    1.68 +    in
    1.69 +     (f file_name; ())
    1.70 +     (*otherwise report exceptions as warnings*)
    1.71 +     handle exn =>
    1.72 +       if Exn.is_interrupt exn then
    1.73 +         reraise exn
    1.74 +       else
    1.75 +         (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
    1.76 +          " raised exception: " ^ ML_Compiler.exn_message exn);
    1.77 +          default_val)
    1.78 +    end
    1.79 +
    1.80 +  fun timed_test ctxt f =
    1.81 +    let
    1.82 +      fun f' x = (f x; ())
    1.83 +      val time =
    1.84 +        Timing.timing (List.app f') files
    1.85 +        |> fst
    1.86 +      val duration =
    1.87 +        #elapsed time
    1.88 +        |> Time.toSeconds
    1.89 +        |> Real.fromLargeInt
    1.90 +      val average =
    1.91 +        (StringCvt.FIX (SOME 3),
    1.92 +         (duration / Real.fromInt (length files)))
    1.93 +        |-> Real.fmt
    1.94 +    in
    1.95 +      report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
    1.96 +       "s per problem)")
    1.97 +    end
    1.98 +*}
    1.99 +
   1.100 +
   1.101 +ML {*
   1.102 +  fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
   1.103 +  fun parser_test ctxt = (*FIXME argument order*)
   1.104 +    test_fn ctxt
   1.105 +     (fn file_name =>
   1.106 +        Path.implode file_name
   1.107 +        |> (fn file =>
   1.108 +             ((*report ctxt file; this is if you want the filename in the log*)
   1.109 +              TPTP_Parser.parse_file file)))
   1.110 +     "parser"
   1.111 +     ()
   1.112 +*}
   1.113 +
   1.114 +declare [[warning_out = ""]]
   1.115 +
   1.116 +end
   1.117 \ No newline at end of file