1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Apr 18 18:24:16 2012 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Apr 18 17:33:11 2012 +0100
     1.3 @@ -114,12 +114,36 @@
     1.4  *}
     1.5  
     1.6  ML {*
     1.7 + interpretation_tests (get_timeout @{context}) @{context}
     1.8 +   (some_probs @ take_too_long @ timeouts @ more_probs)
     1.9 +*}
    1.10 +
    1.11 +ML {*
    1.12 +  parse_timed (situate "NUM/NUM923^4.p");
    1.13    interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
    1.14  *}
    1.15  
    1.16  ML {*
    1.17 - interpretation_tests (get_timeout @{context}) @{context}
    1.18 -   (some_probs @ take_too_long @ timeouts @ more_probs)
    1.19 +  fun interp_gain timeout thy file =
    1.20 +    let
    1.21 +      val t1 = (parse_timed file |> fst)
    1.22 +      val t2 = (interpret_timed timeout file thy |> fst)
    1.23 +        handle exn => (*FIXME*)
    1.24 +          if Exn.is_interrupt exn then reraise exn
    1.25 +          else
    1.26 +            (warning (" test: file " ^ Path.print file ^
    1.27 +             " raised exception: " ^ ML_Compiler.exn_message exn);
    1.28 +             {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
    1.29 +      val to_real = Time.toReal
    1.30 +      val diff_elapsed =
    1.31 +        #elapsed t2 - #elapsed t1
    1.32 +        |> to_real
    1.33 +      val elapsed = to_real (#elapsed t2)
    1.34 +    in
    1.35 +      (Path.base file, diff_elapsed,
    1.36 +       diff_elapsed / elapsed,
    1.37 +       elapsed)
    1.38 +    end
    1.39  *}
    1.40  
    1.41  

     2.1 --- a/src/HOL/TPTP/TPTP_Test.thy	Wed Apr 18 18:24:16 2012 +0200
     2.2 +++ b/src/HOL/TPTP/TPTP_Test.thy	Wed Apr 18 17:33:11 2012 +0100
     2.3 @@ -102,6 +102,7 @@
     2.4  
     2.5  ML {*
     2.6    fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
     2.7 +
     2.8    fun parser_test ctxt = (*FIXME argument order*)
     2.9      test_fn ctxt
    2.10       (fn file_name =>
    2.11 @@ -111,6 +112,9 @@
    2.12                TPTP_Parser.parse_file file)))
    2.13       "parser"
    2.14       ()
    2.15 +
    2.16 +  fun parse_timed file =
    2.17 +    Timing.timing TPTP_Parser.parse_file (Path.implode file)
    2.18  *}
    2.19  
    2.20  end
    2.21 \ No newline at end of file