src/HOL/TPTP/TPTP_Interpret_Test.thy
author sultana
Tue Apr 17 16:14:07 2012 +0100 (2012-04-17)
changeset 47516 9c29589c9b31
parent 47512 b381d428a725
child 47518 b2f209258621
permissions -rw-r--r--
improved tptp interpretation test thy
     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 interpret timeout file thy =
    42     TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout))
    43      (TPTP_Interpret.interpret_file
    44        false
    45        (Path.dir tptp_probs_dir)
    46        file
    47        []
    48        []) thy
    49 
    50   fun interpret_timed timeout file thy =
    51     Timing.timing (interpret timeout file) thy
    52 
    53   (*default timeout is 10 mins*)
    54   fun interpretation_test timeout ctxt =
    55     test_fn ctxt
    56      (fn file => (*FIXME use "interpret" function above*)
    57        TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout))
    58         (TPTP_Interpret.interpret_file
    59           false
    60           (Path.dir tptp_probs_dir)
    61           file
    62           []
    63           [])
    64           @{theory}(*FIXME*))
    65      "interpreter"
    66      ()
    67 
    68   fun interpretation_tests timeout ctxt probs =
    69     List.app
    70      (interpretation_test timeout ctxt)
    71      (List.map situate probs)
    72 *}
    73 
    74 ML {*
    75   val some_probs =
    76     ["LCL/LCL825-1.p",
    77      "ALG/ALG001^5.p",
    78      "COM/COM003+2.p",
    79      "COM/COM003-1.p",
    80      "COM/COM024^5.p",
    81      "DAT/DAT017=1.p",
    82      "NUM/NUM021^1.p",
    83      "NUM/NUM858=1.p",
    84      "SYN/SYN000^2.p"]
    85 
    86   val take_too_long =
    87     ["NLP/NLP562+1.p",
    88      "SWV/SWV546-1.010.p",
    89      "SWV/SWV567-1.015.p",
    90      "LCL/LCL680+1.020.p"]
    91 
    92   val timeouts =
    93     ["NUM/NUM923^4.p",
    94     "NUM/NUM926^4.p",
    95     "NUM/NUM925^4.p",
    96     "NUM/NUM924^4.p",
    97     "CSR/CSR153^3.p",
    98     "CSR/CSR151^3.p",
    99     "CSR/CSR148^3.p",
   100     "CSR/CSR120^3.p",
   101     "CSR/CSR150^3.p",
   102     "CSR/CSR119^3.p",
   103     "CSR/CSR149^3.p"]
   104 
   105   val more_probs =
   106     ["GEG/GEG014^1.p",
   107      "GEG/GEG009^1.p",
   108      "GEG/GEG004^1.p",
   109      "GEG/GEG007^1.p",
   110      "GEG/GEG016^1.p",
   111      "GEG/GEG024=1.p",
   112      "GEG/GEG010^1.p",
   113      "GEG/GEG003^1.p",
   114      "GEG/GEG018^1.p",
   115      "SYN/SYN045^4.p",
   116      "SYN/SYN001^4.001.p",
   117      "SYN/SYN000^2.p",
   118      "SYN/SYN387^4.p",
   119      "SYN/SYN393^4.002.p",
   120      "SYN/SYN978^4.p",
   121      "SYN/SYN044^4.p",
   122      "SYN/SYN393^4.003.p",
   123      "SYN/SYN389^4.p"]
   124 *}
   125 
   126 ML {*
   127   interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
   128 *}
   129 
   130 ML {*
   131  interpretation_tests 5 @{context}
   132    (some_probs @ take_too_long @ timeouts @ more_probs)
   133 *}
   134 
   135 declare [[warning_out = ""]]
   136 
   137 subsection "Test against whole TPTP"
   138 
   139 text "Run interpretation over all problems. This works only for logics
   140  for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
   141 ML {*
   142   report @{context} "Interpreting all problems.";
   143   (*val _ = S timed_test (interpretation_test 5) @{context}*)
   144 *}
   145 
   146 end