src/HOL/TPTP/TPTP_Parser_Test.thy

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

(*  Title:      HOL/TPTP/TPTP_Parser_Test.thy
    Author:     Nik Sultana, Cambridge University Computer Laboratory

Some tests for the TPTP interface. Some of the tests rely on the Isabelle
environment variable TPTP_PROBLEMS_PATH, which should point to the
TPTP-vX.Y.Z/Problems directory.
*)

theory TPTP_Parser_Test
imports TPTP_Parser TPTP_Parser_Example
begin

ML {*
  val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
  fun S x y z = x z (y z)
*}

section "Parser tests"

ML {*
  fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
  val payloads_of = map payload_of
*}
ML {*
  TPTP_Parser.parse_expression "" "fof(dt_k4_waybel34, axiom, ~ v3).";
  TPTP_Parser.parse_expression "" "thf(dt_k4_waybel34, axiom, ~ ($true | $false)).";
  TPTP_Parser.parse_expression ""
   "thf(dt_k4_waybel34, axiom, ~ (! [X : $o, Y : ($o > $o)] : ( (X | (Y = Y))))).";
  TPTP_Parser.parse_expression "" "tff(dt_k4_waybel34, axiom, ~ ($true)).";
  payloads_of it;
*}
ML {*
  TPTP_Parser.parse_expression "" "thf(bla, type, x : $o).";
  TPTP_Parser.parse_expression ""
   "fof(dt_k4_waybel34, axiom, ~ v3_struct_0(k4_waybel34(A))).";
  TPTP_Parser.parse_expression ""
   "fof(dt_k4_waybel34, axiom, (! [A] : (v1_xboole_0(A) => ( ~ v3_struct_0(k4_waybel34(A)))))).";
*}
ML {*
  TPTP_Parser.parse_expression ""
  ("fof(dt_k4_waybel34,axiom,(" ^
    "! [A] :" ^
      "( ~ v1_xboole_0(A)" ^
     "=> ( ~ v3_struct_0(k4_waybel34(A))" ^
        "& v2_altcat_1(k4_waybel34(A))" ^
        "& v6_altcat_1(k4_waybel34(A))" ^
        "& v11_altcat_1(k4_waybel34(A))" ^
        "& v12_altcat_1(k4_waybel34(A))" ^
        "& v2_yellow21(k4_waybel34(A))" ^
        "& l2_altcat_1(k4_waybel34(A)) ) ) )).")
*}

ML {*
open TPTP_Syntax;
@{assert}
  ((TPTP_Parser.parse_expression ""
   "thf(x,axiom,^ [X] : ^ [Y] : f @ g)."
   |> payloads_of |> hd)
  =
  Fmla (Interpreted_ExtraLogic Apply,
   [Quant (Lambda, [("X", NONE)],
      Quant (Lambda, [("Y", NONE)],
       Atom (THF_Atom_term (Term_Func (Uninterpreted "f", []))))),
    Atom (THF_Atom_term (Term_Func (Uninterpreted "g", [])))])
)
*}


section "Source problems"
ML {*
  (*problem source*)
  val tptp_probs_dir =
    Path.explode "$TPTP_PROBLEMS_PATH"
    |> Path.expand;

  (*list of files to under test*)
  val files = TPTP_Syntax.get_file_list tptp_probs_dir;

(*  (*test problem-name parsing and mangling*)
  val problem_names =
    map (Path.base #>
         Path.implode #>
         TPTP_Problem_Name.parse_problem_name #>
         TPTP_Problem_Name.mangle_problem_name)
        files*)
*}


section "Supporting test functions"
ML {*
  fun report ctxt str =
    let
      val warning_out = Config.get ctxt warning_out
    in
      if warning_out = "" then warning str
      else
        let
          val out_stream = TextIO.openAppend warning_out
        in (TextIO.output (out_stream, str ^ "\n");
            TextIO.flushOut out_stream;
            TextIO.closeOut out_stream)
        end
    end

  fun test_fn ctxt f msg default_val file_name =
    let
      val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
    in
     (f file_name; ())
     (*otherwise report exceptions as warnings*)
     handle exn =>
       if Exn.is_interrupt exn then
         reraise exn
       else
         (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
          " raised exception: " ^ ML_Compiler.exn_message exn);
          default_val)
    end

  fun timed_test ctxt f =
    let
      fun f' x = (f x; ())
      val time =
        Timing.timing (List.app f') files
        |> fst
      val duration =
        #elapsed time
        |> Time.toSeconds
        |> Real.fromLargeInt
      val average =
        (StringCvt.FIX (SOME 3),
         (duration / Real.fromInt (length files)))
        |-> Real.fmt
    in
      report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
       "s per problem)")
    end
*}


subsection "More parser tests"
ML {*
  fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
  fun parser_test ctxt = (*FIXME argument order*)
    test_fn ctxt
     (fn file_name =>
        Path.implode file_name
        |> (fn file =>
             ((*report ctxt file; this is if you want the filename in the log*)
              TPTP_Parser.parse_file file)))
     "parser"
     ()
*}

declare [[warning_out = ""]]

text "Parse a specific problem."
ML {*
  map TPTP_Parser.parse_file
   ["$TPTP_PROBLEMS_PATH/FLD/FLD051-1.p",
    "$TPTP_PROBLEMS_PATH/FLD/FLD005-3.p",
    "$TPTP_PROBLEMS_PATH/SWV/SWV567-1.015.p",
    "$TPTP_PROBLEMS_PATH/SWV/SWV546-1.010.p"]
*}
ML {*
  parser_test @{context} (situate "DAT/DAT001=1.p");
  parser_test @{context} (situate "ALG/ALG001^5.p");
  parser_test @{context} (situate "NUM/NUM021^1.p");
  parser_test @{context} (situate "SYN/SYN000^1.p")
*}

text "Run the parser over all problems."
ML {*report @{context} "Testing parser"*}
ML {*
(*  val _ = S timed_test parser_test @{context}*)
*}


subsection "Interpretation"

text "Interpret a problem."
ML {*
  val (time, ((type_map, const_map, fmlas), thy)) =
    Timing.timing
    (TPTP_Interpret.interpret_file
     false
     (Path.dir tptp_probs_dir)
    (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
     []
     [])
    @{theory}

  (*also tried
     "ALG/ALG001^5.p"
     "COM/COM003+2.p"
     "COM/COM003-1.p"
     "COM/COM024^5.p"
     "DAT/DAT017=1.p"
     "NUM/NUM021^1.p"
     "NUM/NUM858=1.p"
     "SYN/SYN000^2.p"*)

 (*These take too long
    "NLP/NLP562+1.p"
    "SWV/SWV546-1.010.p"
    "SWV/SWV567-1.015.p"
    "LCL/LCL680+1.020.p"*)
*}

text "... and display nicely."
ML {*
  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
*}
ML {*
  (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
  List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
*}


text "Run interpretation over all problems. This works only for logics
 for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
ML {*
  report @{context} "Interpreting all problems.";
  fun interpretation_test timeout ctxt =
    test_fn ctxt
     (fn file =>
      (writeln (Path.implode file);
       TimeLimit.timeLimit (Time.fromSeconds timeout)
       (TPTP_Interpret.interpret_file
         false
         (Path.dir tptp_probs_dir)
         file
         []
         [])
         @{theory}))
     "interpreter"
     ()
  val _ = S timed_test (interpretation_test 5) @{context}
*}

end