src/HOL/TPTP/TPTP_Interpret_Test.thy
changeset 63167 0909deb8059b
parent 62519 a564458f94db
     1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  section "Interpreter tests"
     1.5  
     1.6  text "Interpret a problem."
     1.7 -ML {*
     1.8 +ML \<open>
     1.9    val (time, ((type_map, const_map, fmlas), thy)) =
    1.10      Timing.timing
    1.11        (TPTP_Interpret.interpret_file
    1.12 @@ -22,17 +22,17 @@
    1.13         []
    1.14         [])
    1.15        @{theory}
    1.16 -*}
    1.17 +\<close>
    1.18  
    1.19  
    1.20  text "... and display nicely."
    1.21 -ML {*
    1.22 +ML \<open>
    1.23    List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #3) fmlas;
    1.24 -*}
    1.25 +\<close>
    1.26  
    1.27  subsection "Multiple tests"
    1.28  
    1.29 -ML {*
    1.30 +ML \<open>
    1.31    (*default timeout is 1 min*)
    1.32    fun interpret timeout file thy =
    1.33      Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
    1.34 @@ -56,9 +56,9 @@
    1.35      List.app
    1.36       (interpretation_test timeout ctxt)
    1.37       (map situate probs)
    1.38 -*}
    1.39 +\<close>
    1.40  
    1.41 -ML {*
    1.42 +ML \<open>
    1.43    val some_probs =
    1.44      ["LCL/LCL825-1.p",
    1.45       "ALG/ALG001^5.p",
    1.46 @@ -111,19 +111,19 @@
    1.47       "SYO/SYO561_2.p",
    1.48       "SYO/SYO562_1.p",
    1.49       "SYN/SYN000_2.p"]
    1.50 -*}
    1.51 +\<close>
    1.52  
    1.53 -ML {*
    1.54 +ML \<open>
    1.55   interpretation_tests (get_timeout @{context}) @{context}
    1.56     (some_probs @ take_too_long @ timeouts @ more_probs)
    1.57 -*}
    1.58 +\<close>
    1.59  
    1.60 -ML {*
    1.61 +ML \<open>
    1.62    parse_timed (situate "NUM/NUM923^4.p");
    1.63    interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
    1.64 -*}
    1.65 +\<close>
    1.66  
    1.67 -ML {*
    1.68 +ML \<open>
    1.69    fun interp_gain timeout thy file =
    1.70      let
    1.71        val t1 = (parse_timed file |> fst)
    1.72 @@ -144,18 +144,18 @@
    1.73         diff_elapsed / elapsed,
    1.74         elapsed)
    1.75      end
    1.76 -*}
    1.77 +\<close>
    1.78  
    1.79  
    1.80  subsection "Test against whole TPTP"
    1.81  
    1.82  text "Run interpretation over all problems. This works only for logics
    1.83   for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
    1.84 -ML {*
    1.85 +ML \<open>
    1.86    if test_all @{context} then
    1.87      (report @{context} "Interpreting all problems";
    1.88       S timed_test (interpretation_test (get_timeout @{context})) @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
    1.89    else ()
    1.90 -*}
    1.91 +\<close>
    1.92  
    1.93  end