author | desharna |
Fri, 17 Dec 2021 09:51:37 +0100 | |
changeset 74948 | 15ce207f69c8 |
parent 74515 | 64c0d78d2f19 |
child 75003 | f21e7e6172a0 |
permissions | -rw-r--r-- |
47847 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Munich |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
3 |
Author: Sascha Boehme, TU Munich |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
62519
diff
changeset
|
4 |
Author: Makarius |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
5 |
Author: Martin Desharnais, UniBw Munich |
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
62519
diff
changeset
|
6 |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
62519
diff
changeset
|
7 |
Mirabelle action: "arith". |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
8 |
*) |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
9 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
10 |
structure Mirabelle_Arith: MIRABELLE_ACTION = |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
11 |
struct |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
12 |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
13 |
fun make_action ({timeout, ...} : Mirabelle.action_context) = |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
14 |
let |
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
15 |
fun run_action ({pre, ...} : Mirabelle.command) = |
74515 | 16 |
(case Timing.timing (Mirabelle.can_apply timeout Arith_Data.arith_tac) pre of |
17 |
({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)" |
|
18 |
| (_, false) => "failed") |
|
74948
15ce207f69c8
added support for initialization messages to Mirabelle
desharna
parents:
74515
diff
changeset
|
19 |
in ("", {run_action = run_action, finalize = K ""}) end |
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
20 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
21 |
val () = Mirabelle.register_action "arith" make_action |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
22 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
23 |
end |