equal
deleted
inserted
replaced
1 (* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML |
|
2 Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
|
3 *) |
|
4 |
|
5 structure Mirabelle_Arith : MIRABELLE_ACTION = |
|
6 struct |
|
7 |
|
8 fun arith_tag id = "#" ^ string_of_int id ^ " arith: " |
|
9 |
|
10 fun init _ = I |
|
11 fun done _ _ = () |
|
12 |
|
13 fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = |
|
14 if Mirabelle.can_apply timeout Arith_Data.arith_tac pre |
|
15 then log (arith_tag id ^ "succeeded") |
|
16 else () |
|
17 handle Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout") |
|
18 |
|
19 fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done) |
|
20 |
|
21 end |
|