| author | wenzelm |
| Wed, 25 Jun 2025 16:35:25 +0200 | |
| changeset 82768 | 8f866fd6fae1 |
| parent 80306 | c2537860ccf8 |
| permissions | -rw-r--r-- |
| 76183 | 1 |
(* Title: HOL/Tools/Mirabelle/mirabelle_metis.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 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
4 |
Author: Martin Desharnais, UniBw Munich |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
63337
diff
changeset
|
5 |
|
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
63337
diff
changeset
|
6 |
Mirabelle action: "metis". |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
7 |
*) |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
8 |
|
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
9 |
structure Mirabelle_Metis: MIRABELLE_ACTION = |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
10 |
struct |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
11 |
|
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
12 |
fun make_action ({timeout, ...} : Mirabelle.action_context) =
|
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
13 |
let |
|
75003
f21e7e6172a0
renamed run_action to run in Mirabelle.action record
desharna
parents:
74948
diff
changeset
|
14 |
fun run ({pre, post, ...} : Mirabelle.command) =
|
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
63337
diff
changeset
|
15 |
let |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
63337
diff
changeset
|
16 |
val thms = Mirabelle.theorems_of_sucessful_proof post; |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
63337
diff
changeset
|
17 |
val names = map Thm.get_name_hint thms; |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
63337
diff
changeset
|
18 |
val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre))); |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
63337
diff
changeset
|
19 |
fun metis ctxt = Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt (thms @ facts); |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
63337
diff
changeset
|
20 |
in |
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
63337
diff
changeset
|
21 |
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |
| 80306 | 22 |
|> not (null names) ? suffix (":\n" ^ commas (map Thm_Name.short names))
|
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
23 |
end |
|
75003
f21e7e6172a0
renamed run_action to run in Mirabelle.action record
desharna
parents:
74948
diff
changeset
|
24 |
in ("", {run = run, finalize = K ""}) end
|
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
25 |
|
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
26 |
val () = Mirabelle.register_action "metis" make_action |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
27 |
|
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
28 |
end |