|
48740
|
1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML
|
|
47891
|
2 |
Author: Jasmin Blanchette, TU Munich
|
|
|
3 |
*)
|
|
|
4 |
|
|
|
5 |
structure Mirabelle_Try0 : MIRABELLE_ACTION =
|
|
|
6 |
struct
|
|
|
7 |
|
|
|
8 |
fun try0_tag id = "#" ^ string_of_int id ^ " try0: "
|
|
|
9 |
|
|
|
10 |
fun init _ = I
|
|
|
11 |
fun done _ _ = ()
|
|
|
12 |
|
|
47942
|
13 |
fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time)
|
|
|
14 |
|
|
|
15 |
fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
|
|
|
16 |
if TimeLimit.timeLimit (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
|
|
47891
|
17 |
then log (try0_tag id ^ "succeeded")
|
|
|
18 |
else ()
|
|
|
19 |
handle TimeLimit.TimeOut => log (try0_tag id ^ "timeout")
|
|
|
20 |
|
|
|
21 |
fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done)
|
|
|
22 |
|
|
|
23 |
end
|