src/HOL/TPTP/TPTP_Interpret_Test.thy
author wenzelm
Thu Mar 27 17:12:40 2014 +0100 (2014-03-27)
changeset 56303 4cc3f4db3447
parent 55595 2e2e9bc7c4c6
child 58412 f65f11f4854c
permissions -rw-r--r--
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
sultana@47512
     1
(*  Title:      HOL/TPTP/TPTP_Interpret_Test.thy
sultana@47512
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
sultana@47512
     3
sultana@47512
     4
Some tests for the TPTP interface. Some of the tests rely on the Isabelle
blanchet@47558
     5
environment variable $TPTP, which should point to the TPTP-vX.Y.Z directory.
sultana@47512
     6
*)
sultana@47512
     7
sultana@47512
     8
theory TPTP_Interpret_Test
sultana@47512
     9
imports TPTP_Test TPTP_Interpret
sultana@47512
    10
begin
sultana@47512
    11
sultana@47512
    12
section "Interpreter tests"
sultana@47518
    13
sultana@47512
    14
text "Interpret a problem."
sultana@47512
    15
ML {*
sultana@47512
    16
  val (time, ((type_map, const_map, fmlas), thy)) =
sultana@47512
    17
    Timing.timing
sultana@47512
    18
      (TPTP_Interpret.interpret_file
sultana@47512
    19
       false
blanchet@48829
    20
       [Path.explode "$TPTP"]
sultana@47693
    21
       (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
sultana@47512
    22
       []
sultana@47512
    23
       [])
sultana@47512
    24
      @{theory}
sultana@47512
    25
*}
sultana@47512
    26
sultana@47693
    27
sultana@47512
    28
text "... and display nicely."
sultana@47512
    29
ML {*
sultana@47548
    30
  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #3) fmlas;
sultana@47512
    31
*}
sultana@47512
    32
sultana@47512
    33
subsection "Multiple tests"
sultana@47512
    34
sultana@47512
    35
ML {*
sultana@47518
    36
  (*default timeout is 1 min*)
sultana@47516
    37
  fun interpret timeout file thy =
sultana@47518
    38
    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
sultana@47516
    39
     (TPTP_Interpret.interpret_file
sultana@47516
    40
       false
blanchet@48829
    41
       [Path.explode "$TPTP"]
sultana@47516
    42
       file
sultana@47516
    43
       []
sultana@47516
    44
       []) thy
sultana@47516
    45
sultana@47516
    46
  fun interpret_timed timeout file thy =
sultana@47516
    47
    Timing.timing (interpret timeout file) thy
sultana@47516
    48
sultana@47512
    49
  fun interpretation_test timeout ctxt =
sultana@47512
    50
    test_fn ctxt
sultana@47518
    51
     (fn file => interpret timeout file (Proof_Context.theory_of ctxt))
sultana@47512
    52
     "interpreter"
sultana@47512
    53
     ()
sultana@47512
    54
sultana@47512
    55
  fun interpretation_tests timeout ctxt probs =
sultana@47512
    56
    List.app
sultana@47512
    57
     (interpretation_test timeout ctxt)
sultana@47512
    58
     (List.map situate probs)
sultana@47512
    59
*}
sultana@47512
    60
sultana@47512
    61
ML {*
sultana@47512
    62
  val some_probs =
sultana@47512
    63
    ["LCL/LCL825-1.p",
sultana@47512
    64
     "ALG/ALG001^5.p",
sultana@47512
    65
     "COM/COM003+2.p",
sultana@47512
    66
     "COM/COM003-1.p",
sultana@47512
    67
     "COM/COM024^5.p",
sultana@47512
    68
     "DAT/DAT017=1.p",
sultana@47512
    69
     "NUM/NUM021^1.p",
sultana@47512
    70
     "NUM/NUM858=1.p",
sultana@47512
    71
     "SYN/SYN000^2.p"]
sultana@47512
    72
sultana@47512
    73
  val take_too_long =
sultana@47512
    74
    ["NLP/NLP562+1.p",
sultana@47512
    75
     "SWV/SWV546-1.010.p",
sultana@47512
    76
     "SWV/SWV567-1.015.p",
sultana@47512
    77
     "LCL/LCL680+1.020.p"]
sultana@47512
    78
sultana@47516
    79
  val timeouts =
sultana@47516
    80
    ["NUM/NUM923^4.p",
sultana@47516
    81
    "NUM/NUM926^4.p",
sultana@47516
    82
    "NUM/NUM925^4.p",
sultana@47516
    83
    "NUM/NUM924^4.p",
sultana@47516
    84
    "CSR/CSR153^3.p",
sultana@47516
    85
    "CSR/CSR151^3.p",
sultana@47516
    86
    "CSR/CSR148^3.p",
sultana@47516
    87
    "CSR/CSR120^3.p",
sultana@47516
    88
    "CSR/CSR150^3.p",
sultana@47516
    89
    "CSR/CSR119^3.p",
sultana@47516
    90
    "CSR/CSR149^3.p"]
sultana@47516
    91
sultana@47512
    92
  val more_probs =
sultana@47512
    93
    ["GEG/GEG014^1.p",
sultana@47512
    94
     "GEG/GEG009^1.p",
sultana@47512
    95
     "GEG/GEG004^1.p",
sultana@47512
    96
     "GEG/GEG007^1.p",
sultana@47512
    97
     "GEG/GEG016^1.p",
sultana@47512
    98
     "GEG/GEG024=1.p",
sultana@47512
    99
     "GEG/GEG010^1.p",
sultana@47512
   100
     "GEG/GEG003^1.p",
sultana@47512
   101
     "GEG/GEG018^1.p",
sultana@47512
   102
     "SYN/SYN045^4.p",
sultana@47512
   103
     "SYN/SYN001^4.001.p",
sultana@47512
   104
     "SYN/SYN387^4.p",
sultana@47512
   105
     "SYN/SYN393^4.002.p",
sultana@47512
   106
     "SYN/SYN978^4.p",
sultana@47512
   107
     "SYN/SYN044^4.p",
sultana@47512
   108
     "SYN/SYN393^4.003.p",
sultana@47693
   109
     "SYN/SYN389^4.p",
sultana@47693
   110
     "ARI/ARI625=1.p",
sultana@47693
   111
     "SYO/SYO561_2.p",
sultana@47693
   112
     "SYO/SYO562_1.p",
sultana@47693
   113
     "SYN/SYN000_2.p"]
sultana@47512
   114
*}
sultana@47512
   115
sultana@47512
   116
ML {*
sultana@47547
   117
 interpretation_tests (get_timeout @{context}) @{context}
sultana@47547
   118
   (some_probs @ take_too_long @ timeouts @ more_probs)
sultana@47547
   119
*}
sultana@47547
   120
sultana@47547
   121
ML {*
sultana@47547
   122
  parse_timed (situate "NUM/NUM923^4.p");
sultana@47516
   123
  interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
sultana@47512
   124
*}
sultana@47512
   125
sultana@47516
   126
ML {*
sultana@47547
   127
  fun interp_gain timeout thy file =
sultana@47547
   128
    let
sultana@47547
   129
      val t1 = (parse_timed file |> fst)
sultana@47547
   130
      val t2 = (interpret_timed timeout file thy |> fst)
sultana@47547
   131
        handle exn => (*FIXME*)
sultana@47547
   132
          if Exn.is_interrupt exn then reraise exn
sultana@47547
   133
          else
sultana@47547
   134
            (warning (" test: file " ^ Path.print file ^
wenzelm@56303
   135
             " raised exception: " ^ Runtime.exn_message exn);
sultana@47547
   136
             {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
sultana@47547
   137
      val to_real = Time.toReal
sultana@47547
   138
      val diff_elapsed =
sultana@47547
   139
        #elapsed t2 - #elapsed t1
sultana@47547
   140
        |> to_real
sultana@47547
   141
      val elapsed = to_real (#elapsed t2)
sultana@47547
   142
    in
sultana@47547
   143
      (Path.base file, diff_elapsed,
sultana@47547
   144
       diff_elapsed / elapsed,
sultana@47547
   145
       elapsed)
sultana@47547
   146
    end
sultana@47516
   147
*}
sultana@47516
   148
sultana@47512
   149
sultana@47512
   150
subsection "Test against whole TPTP"
sultana@47512
   151
sultana@47512
   152
text "Run interpretation over all problems. This works only for logics
sultana@47512
   153
 for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
sultana@47512
   154
ML {*
sultana@47518
   155
  if test_all @{context} then
sultana@47518
   156
    (report @{context} "Interpreting all problems";
sultana@55595
   157
     S timed_test (interpretation_test (get_timeout @{context})) @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
sultana@47518
   158
  else ()
sultana@47512
   159
*}
sultana@47512
   160
sultana@47518
   161
end