author | wenzelm |
Sat, 05 Mar 2016 17:01:45 +0100 | |
changeset 62519 | a564458f94db |
parent 47847 | 7cddb6c8f93c |
permissions | -rw-r--r-- |
47847 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML |
32564 | 2 |
Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
3 |
*) |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
4 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
5 |
structure Mirabelle_Arith : MIRABELLE_ACTION = |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
6 |
struct |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
7 |
|
32521 | 8 |
fun arith_tag id = "#" ^ string_of_int id ^ " arith: " |
9 |
||
10 |
fun init _ = I |
|
11 |
fun done _ _ = () |
|
12 |
||
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
13 |
fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
14 |
if Mirabelle.can_apply timeout Arith_Data.arith_tac pre |
32521 | 15 |
then log (arith_tag id ^ "succeeded") |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
16 |
else () |
62519 | 17 |
handle Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout") |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
18 |
|
32521 | 19 |
fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
20 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
21 |
end |