author | boehmes |
Thu, 03 Sep 2009 14:05:13 +0200 | |
changeset 32503 | 14efbc20b708 |
parent 32498 | 1132c7c13f36 |
child 32510 | 1b56f8b1e5cc |
permissions | -rw-r--r-- |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
1 |
(* Title: mirabelle_sledgehammer.ML |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette and Sascha Boehme |
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_Sledgehammer : 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 |
|
32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
8 |
fun thms_of_name ctxt name = |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
9 |
let |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
10 |
val lex = OuterKeyword.get_lexicons |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
11 |
val get = maps (ProofContext.get_fact ctxt o fst) |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
12 |
in |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
13 |
Source.of_string name |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
14 |
|> Symbol.source {do_recover=false} |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
15 |
|> OuterLex.source {do_recover=SOME false} lex Position.start |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
16 |
|> OuterLex.source_proper |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
17 |
|> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
18 |
|> Source.exhaust |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
19 |
end |
32452
d84edd022efe
apply metis with found theorems in case sledgehammer was successful
boehmes
parents:
32434
diff
changeset
|
20 |
|
32455
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
21 |
fun safe init done f x = |
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
22 |
let |
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
23 |
val y = init x |
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
24 |
val z = Exn.capture f y |
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
25 |
val _ = done y |
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
26 |
in Exn.release z end |
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
27 |
|
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
28 |
fun with_time true t = "succeeded (" ^ string_of_int t ^ ")" |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
29 |
| with_time false t = "failed (" ^ string_of_int t ^ ")" |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
30 |
|
32455
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
31 |
val proverK = "prover" |
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
32 |
val keepK = "keep" |
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
33 |
val metisK = "metis" |
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
34 |
|
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
35 |
|
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
36 |
local |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
37 |
|
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
38 |
fun init NONE = !AtpWrapper.destdir |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
39 |
| init (SOME path) = |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
40 |
let |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
41 |
(* Warning: we implicitly assume single-threaded execution here! *) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
42 |
val old = !AtpWrapper.destdir |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
43 |
val _ = AtpWrapper.destdir := path |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
44 |
in old end |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
45 |
|
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
46 |
fun done path = AtpWrapper.destdir := path |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
47 |
|
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
48 |
fun run prover_name timeout st _ = |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
49 |
let |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
50 |
val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st)) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
51 |
val atp_timeout = AtpManager.get_timeout () |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
52 |
val atp = prover atp_timeout NONE NONE prover_name 1 |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
53 |
val (success, (message, thm_names), _, _, _) = |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
54 |
TimeLimit.timeLimit timeout atp (Proof.get_goal st) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
55 |
in (success, message, SOME thm_names) end |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
56 |
handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME []) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
57 |
| TimeLimit.TimeOut => (false, "time out", NONE) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
58 |
| ERROR msg => (false, "error: " ^ msg, NONE) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
59 |
|
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
60 |
in |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
61 |
|
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
62 |
fun run_sledgehammer (args, st, timeout, log) = |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
63 |
let |
32434
6b93b73a712b
selectable prover for sledgehammer, proper environment lookup
boehmes
parents:
32385
diff
changeset
|
64 |
val prover_name = |
32455
c71414177792
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes
parents:
32454
diff
changeset
|
65 |
AList.lookup (op =) args proverK |
32434
6b93b73a712b
selectable prover for sledgehammer, proper environment lookup
boehmes
parents:
32385
diff
changeset
|
66 |
|> the_default (hd (space_explode " " (AtpManager.get_atps ()))) |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
67 |
val dir = AList.lookup (op =) args keepK |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
68 |
val ((success, msg, thm_names), time) = |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
69 |
safe init done (Mirabelle.cpu_time (run prover_name timeout st)) dir |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
70 |
fun sh_log s = log ("sledgehammer: " ^ with_time success time ^ " [" ^ |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
71 |
prover_name ^ "]" ^ s) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
72 |
val _ = if success then sh_log (":\n" ^ msg) else sh_log "" |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
73 |
in if success then thm_names else NONE end |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
74 |
|
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
75 |
end |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
76 |
|
32452
d84edd022efe
apply metis with found theorems in case sledgehammer was successful
boehmes
parents:
32434
diff
changeset
|
77 |
|
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
78 |
fun run_metis (args, st, timeout, log) thm_names = |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
79 |
let |
32454
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
80 |
fun get_thms ctxt = maps (thms_of_name ctxt) |
a1a5589207ad
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents:
32452
diff
changeset
|
81 |
fun metis thms ctxt = MetisTools.metis_tac ctxt thms |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
82 |
fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
83 |
fun timed_metis thms = |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
84 |
uncurry with_time (Mirabelle.cpu_time apply_metis thms) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
85 |
handle TimeLimit.TimeOut => "time out" |
32503
14efbc20b708
Mirabelle: logging of exceptions (works only for PolyML)
boehmes
parents:
32498
diff
changeset
|
86 |
| ERROR msg => "error: " ^ msg |
14efbc20b708
Mirabelle: logging of exceptions (works only for PolyML)
boehmes
parents:
32498
diff
changeset
|
87 |
fun log_metis s = log ("metis (sledgehammer): " ^ s) |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
88 |
in |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
89 |
if not (AList.defined (op =) args metisK) then () |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
90 |
else if is_none thm_names then () |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
91 |
else |
32503
14efbc20b708
Mirabelle: logging of exceptions (works only for PolyML)
boehmes
parents:
32498
diff
changeset
|
92 |
log "-----" |
14efbc20b708
Mirabelle: logging of exceptions (works only for PolyML)
boehmes
parents:
32498
diff
changeset
|
93 |
|> K (these thm_names) |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
94 |
|> get_thms (Proof.context_of st) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
95 |
|> timed_metis |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
96 |
|> log_metis |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
97 |
end |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
98 |
|
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
99 |
|
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
100 |
fun sledgehammer_action args {pre, timeout, log, ...} = |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
101 |
run_sledgehammer (args, pre, timeout, log) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
102 |
|> run_metis (args, pre, timeout, log) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
103 |
|
32434
6b93b73a712b
selectable prover for sledgehammer, proper environment lookup
boehmes
parents:
32385
diff
changeset
|
104 |
fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
105 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
106 |
end |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
107 |