author | smolkas |
Thu, 14 Feb 2013 22:49:22 +0100 | |
changeset 51130 | 76d68444cd59 |
parent 51128 | 0021ea861129 |
child 51131 | 7de262be1e95 |
permissions | -rw-r--r-- |
51130
76d68444cd59
renamed sledgehammer_shrink to sledgehammer_compress
smolkas
parents:
51128
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_preplay.ML |
50923 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
50924 | 5 |
Preplaying of isar proofs. |
50923 | 6 |
*) |
7 |
||
8 |
signature SLEDGEHAMMER_PREPLAY = |
|
9 |
sig |
|
10 |
type isar_step = Sledgehammer_Proof.isar_step |
|
50924 | 11 |
eqtype preplay_time |
12 |
val zero_preplay_time : preplay_time |
|
13 |
val some_preplay_time : preplay_time |
|
14 |
val add_preplay_time : preplay_time -> preplay_time -> preplay_time |
|
15 |
val string_of_preplay_time : preplay_time -> string |
|
50923 | 16 |
val try_metis : bool -> string -> string -> Proof.context -> |
50924 | 17 |
Time.time -> (isar_step option * isar_step) -> unit -> preplay_time |
50923 | 18 |
val try_metis_quietly : bool -> string -> string -> Proof.context -> |
50924 | 19 |
Time.time -> (isar_step option * isar_step) -> unit -> preplay_time |
50923 | 20 |
end |
21 |
||
22 |
structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY = |
|
23 |
struct |
|
24 |
||
25 |
open Sledgehammer_Util |
|
26 |
open Sledgehammer_Proof |
|
27 |
||
50924 | 28 |
(* The boolean flag encodes whether the time is exact (false) or an lower bound |
29 |
(true) *) |
|
30 |
type preplay_time = bool * Time.time |
|
31 |
||
32 |
val zero_preplay_time = (false, Time.zeroTime) |
|
33 |
val some_preplay_time = (true, Time.zeroTime) |
|
34 |
||
35 |
fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) |
|
36 |
||
37 |
val string_of_preplay_time = ATP_Util.string_from_ext_time |
|
38 |
||
50923 | 39 |
(* timing *) |
40 |
fun take_time timeout tac arg = |
|
41 |
let |
|
42 |
val timing = Timing.start () |
|
43 |
in |
|
50924 | 44 |
(TimeLimit.timeLimit timeout tac arg; |
45 |
Timing.result timing |> #cpu |> pair false) |
|
46 |
handle TimeLimit.TimeOut => (true, timeout) |
|
50923 | 47 |
end |
48 |
||
49 |
(* lookup facts in context *) |
|
50 |
fun resolve_fact_names ctxt names = |
|
51 |
names |
|
52 |
|>> map string_for_label |
|
53 |
|> op @ |
|
54 |
|> maps (thms_of_name ctxt) |
|
55 |
||
56 |
exception ZEROTIME |
|
57 |
fun try_metis debug type_enc lam_trans ctxt timeout (succedent, step) = |
|
58 |
let |
|
59 |
val (t, byline, obtain) = |
|
60 |
(case step of |
|
61 |
Prove (_, _, t, byline) => (t, byline, false) |
|
62 |
| Obtain (_, xs, _, t, byline) => |
|
63 |
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
|
64 |
(see ~~/src/Pure/Isar/obtain.ML) *) |
|
65 |
let |
|
66 |
val thesis = Term.Free ("thesis", HOLogic.boolT) |
|
67 |
val thesis_prop = thesis |> HOLogic.mk_Trueprop |
|
68 |
val frees = map Term.Free xs |
|
69 |
||
70 |
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
|
71 |
val inner_prop = |
|
72 |
fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) |
|
73 |
||
74 |
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
|
75 |
val prop = |
|
76 |
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
|
77 |
in |
|
78 |
(prop, byline, true) |
|
79 |
end |
|
80 |
| _ => raise ZEROTIME) |
|
81 |
val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
|
82 |
val facts = |
|
83 |
(case byline of |
|
84 |
By_Metis fact_names => resolve_fact_names ctxt fact_names |
|
85 |
| Case_Split (cases, fact_names) => |
|
86 |
resolve_fact_names ctxt fact_names |
|
87 |
@ (case the succedent of |
|
88 |
Assume (_, t) => make_thm t |
|
89 |
| Obtain (_, _, _, t, _) => make_thm t |
|
90 |
| Prove (_, _, t, _) => make_thm t |
|
50924 | 91 |
| _ => error "preplay error: unexpected succedent of case split") |
50923 | 92 |
:: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) |
50924 | 93 |
| _ => error "preplay error: malformed case split") |
50923 | 94 |
#> make_thm) |
51128
0021ea861129
introduced subblock in isar_step datatype for conjecture herbrandization
smolkas
parents:
50924
diff
changeset
|
95 |
cases |
0021ea861129
introduced subblock in isar_step datatype for conjecture herbrandization
smolkas
parents:
50924
diff
changeset
|
96 |
(* TODO: implement *) |
0021ea861129
introduced subblock in isar_step datatype for conjecture herbrandization
smolkas
parents:
50924
diff
changeset
|
97 |
| Subblock _ => []) |
50923 | 98 |
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |
99 |
|> obtain ? Config.put Metis_Tactic.new_skolem true |
|
100 |
val goal = |
|
101 |
Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t |
|
102 |
fun tac {context = ctxt, prems = _} = |
|
103 |
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 |
|
104 |
in |
|
50924 | 105 |
take_time timeout |
106 |
(fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg)) |
|
50923 | 107 |
end |
50924 | 108 |
handle ZEROTIME => K zero_preplay_time |
50923 | 109 |
|
50924 | 110 |
(* this version treats exceptions like timeouts *) |
111 |
fun try_metis_quietly debug type_enc lam_trans ctxt timeout = |
|
112 |
the_default (true, timeout) oo try o try_metis debug type_enc lam_trans ctxt timeout |
|
50923 | 113 |
|
114 |
end |