equal
deleted
inserted
replaced
1 (* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML |
|
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 |
|
13 fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time) |
|
14 |
|
15 fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = |
|
16 if Timeout.apply (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre |
|
17 then log (try0_tag id ^ "succeeded") |
|
18 else () |
|
19 handle Timeout.TIMEOUT _ => log (try0_tag id ^ "timeout") |
|
20 |
|
21 fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done) |
|
22 |
|
23 end |
|