src/HOL/TPTP/TPTP_Interpret_Test.thy
author sultana
Tue Apr 17 16:14:07 2012 +0100 (2012-04-17)
changeset 47512 b381d428a725
child 47516 9c29589c9b31
permissions -rw-r--r--
reorganised tptp testing thys
     1 (*  Title:      HOL/TPTP/TPTP_Interpret_Test.thy
     2     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_Interpret_Test
    10 imports TPTP_Test TPTP_Interpret
    11 begin
    12 
    13 section "Interpreter tests"
    14 
    15 text "Interpret a problem."
    16 ML {*
    17   val (time, ((type_map, const_map, fmlas), thy)) =
    18     Timing.timing
    19       (TPTP_Interpret.interpret_file
    20        false
    21        (Path.dir tptp_probs_dir)
    22       (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
    23        []
    24        [])
    25       @{theory}
    26 *}
    27 
    28 text "... and display nicely."
    29 ML {*
    30   List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
    31 *}
    32 ML {*
    33   (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
    34   List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
    35 *}
    36 
    37 
    38 subsection "Multiple tests"
    39 
    40 ML {*
    41   fun interpretation_test timeout ctxt =
    42     test_fn ctxt
    43      (fn file =>
    44        TimeLimit.timeLimit (Time.fromSeconds timeout)
    45         (TPTP_Interpret.interpret_file
    46           false
    47           (Path.dir tptp_probs_dir)
    48           file
    49           []
    50           [])
    51           @{theory})
    52      "interpreter"
    53      ()
    54 
    55   fun interpretation_tests timeout ctxt probs =
    56     List.app
    57      (interpretation_test timeout ctxt)
    58      (List.map situate probs)
    59 *}
    60 
    61 ML {*
    62   val some_probs =
    63     ["LCL/LCL825-1.p",
    64      "ALG/ALG001^5.p",
    65      "COM/COM003+2.p",
    66      "COM/COM003-1.p",
    67      "COM/COM024^5.p",
    68      "DAT/DAT017=1.p",
    69      "NUM/NUM021^1.p",
    70      "NUM/NUM858=1.p",
    71      "SYN/SYN000^2.p"]
    72 
    73   val take_too_long =
    74     ["NLP/NLP562+1.p",
    75      "SWV/SWV546-1.010.p",
    76      "SWV/SWV567-1.015.p",
    77      "LCL/LCL680+1.020.p"]
    78 
    79   val more_probs =
    80     ["GEG/GEG014^1.p",
    81      "GEG/GEG009^1.p",
    82      "GEG/GEG004^1.p",
    83      "GEG/GEG007^1.p",
    84      "GEG/GEG016^1.p",
    85      "GEG/GEG024=1.p",
    86      "GEG/GEG010^1.p",
    87      "GEG/GEG003^1.p",
    88      "GEG/GEG018^1.p",
    89      "SYN/SYN045^4.p",
    90      "SYN/SYN001^4.001.p",
    91      "SYN/SYN000^2.p",
    92      "SYN/SYN387^4.p",
    93      "SYN/SYN393^4.002.p",
    94      "SYN/SYN978^4.p",
    95      "SYN/SYN044^4.p",
    96      "SYN/SYN393^4.003.p",
    97      "SYN/SYN389^4.p"]
    98 *}
    99 
   100 ML {*
   101  interpretation_tests 5 @{context}
   102    (some_probs @ take_too_long @ more_probs)
   103 *}
   104 
   105 
   106 subsection "Test against whole TPTP"
   107 
   108 text "Run interpretation over all problems. This works only for logics
   109  for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
   110 ML {*
   111   report @{context} "Interpreting all problems.";
   112   fun interpretation_test timeout ctxt =
   113     test_fn ctxt
   114      (fn file =>
   115        TimeLimit.timeLimit (Time.fromSeconds timeout)
   116         (TPTP_Interpret.interpret_file
   117           false
   118           (Path.dir tptp_probs_dir)
   119           file
   120           []
   121           [])
   122           @{theory})
   123      "interpreter"
   124      ()
   125   (*val _ = S timed_test (interpretation_test 5) @{context}*)
   126 *}
   127 
   128 end