src/HOL/TPTP/TPTP_Interpret_Test.thy
changeset 47547 1a5dc8377b5c
parent 47518 b2f209258621
child 47548 60849d8c457d
     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