src/HOL/TPTP/TPTP_Interpret_Test.thy
author sultana
Wed Apr 18 17:33:11 2012 +0100 (2012-04-18)
changeset 47547 1a5dc8377b5c
parent 47518 b2f209258621
child 47548 60849d8c457d
permissions -rw-r--r--
more tptp testing support functions;
     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   (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
    33   List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
    34 *}
    35 
    36 subsection "Multiple tests"
    37 
    38 ML {*
    39   (*default timeout is 1 min*)
    40   fun interpret timeout file thy =
    41     TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
    42      (TPTP_Interpret.interpret_file
    43        false
    44        (Path.dir tptp_probs_dir)
    45        file
    46        []
    47        []) thy
    48 
    49   fun interpret_timed timeout file thy =
    50     Timing.timing (interpret timeout file) thy
    51 
    52   fun interpretation_test timeout ctxt =
    53     test_fn ctxt
    54      (fn file => interpret timeout file (Proof_Context.theory_of ctxt))
    55      "interpreter"
    56      ()
    57 
    58   fun interpretation_tests timeout ctxt probs =
    59     List.app
    60      (interpretation_test timeout ctxt)
    61      (List.map situate probs)
    62 *}
    63 
    64 ML {*
    65   val some_probs =
    66     ["LCL/LCL825-1.p",
    67      "ALG/ALG001^5.p",
    68      "COM/COM003+2.p",
    69      "COM/COM003-1.p",
    70      "COM/COM024^5.p",
    71      "DAT/DAT017=1.p",
    72      "NUM/NUM021^1.p",
    73      "NUM/NUM858=1.p",
    74      "SYN/SYN000^2.p"]
    75 
    76   val take_too_long =
    77     ["NLP/NLP562+1.p",
    78      "SWV/SWV546-1.010.p",
    79      "SWV/SWV567-1.015.p",
    80      "LCL/LCL680+1.020.p"]
    81 
    82   val timeouts =
    83     ["NUM/NUM923^4.p",
    84     "NUM/NUM926^4.p",
    85     "NUM/NUM925^4.p",
    86     "NUM/NUM924^4.p",
    87     "CSR/CSR153^3.p",
    88     "CSR/CSR151^3.p",
    89     "CSR/CSR148^3.p",
    90     "CSR/CSR120^3.p",
    91     "CSR/CSR150^3.p",
    92     "CSR/CSR119^3.p",
    93     "CSR/CSR149^3.p"]
    94 
    95   val more_probs =
    96     ["GEG/GEG014^1.p",
    97      "GEG/GEG009^1.p",
    98      "GEG/GEG004^1.p",
    99      "GEG/GEG007^1.p",
   100      "GEG/GEG016^1.p",
   101      "GEG/GEG024=1.p",
   102      "GEG/GEG010^1.p",
   103      "GEG/GEG003^1.p",
   104      "GEG/GEG018^1.p",
   105      "SYN/SYN045^4.p",
   106      "SYN/SYN001^4.001.p",
   107      "SYN/SYN000^2.p",
   108      "SYN/SYN387^4.p",
   109      "SYN/SYN393^4.002.p",
   110      "SYN/SYN978^4.p",
   111      "SYN/SYN044^4.p",
   112      "SYN/SYN393^4.003.p",
   113      "SYN/SYN389^4.p"]
   114 *}
   115 
   116 ML {*
   117  interpretation_tests (get_timeout @{context}) @{context}
   118    (some_probs @ take_too_long @ timeouts @ more_probs)
   119 *}
   120 
   121 ML {*
   122   parse_timed (situate "NUM/NUM923^4.p");
   123   interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
   124 *}
   125 
   126 ML {*
   127   fun interp_gain timeout thy file =
   128     let
   129       val t1 = (parse_timed file |> fst)
   130       val t2 = (interpret_timed timeout file thy |> fst)
   131         handle exn => (*FIXME*)
   132           if Exn.is_interrupt exn then reraise exn
   133           else
   134             (warning (" test: file " ^ Path.print file ^
   135              " raised exception: " ^ ML_Compiler.exn_message exn);
   136              {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
   137       val to_real = Time.toReal
   138       val diff_elapsed =
   139         #elapsed t2 - #elapsed t1
   140         |> to_real
   141       val elapsed = to_real (#elapsed t2)
   142     in
   143       (Path.base file, diff_elapsed,
   144        diff_elapsed / elapsed,
   145        elapsed)
   146     end
   147 *}
   148 
   149 
   150 subsection "Test against whole TPTP"
   151 
   152 text "Run interpretation over all problems. This works only for logics
   153  for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
   154 ML {*
   155   if test_all @{context} then
   156     (report @{context} "Interpreting all problems";
   157      S timed_test (interpretation_test (get_timeout @{context})) @{context})
   158   else ()
   159 *}
   160 
   161 end