author | smolkas |
Mon, 18 Feb 2013 12:16:02 +0100 | |
changeset 51178 | 06689dbfe072 |
parent 51155 | f18862753271 |
child 51179 | 0d5f8812856f |
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 -> |
51178 | 17 |
Time.time -> isar_step -> unit -> preplay_time |
50923 | 18 |
val try_metis_quietly : bool -> string -> string -> Proof.context -> |
51178 | 19 |
Time.time -> 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 |
51131 | 29 |
(true): |
30 |
(t, false) = "t ms" |
|
31 |
(t, true) = "> t ms" *) |
|
50924 | 32 |
type preplay_time = bool * Time.time |
33 |
||
51131 | 34 |
val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *) |
35 |
val some_preplay_time = (true, Time.zeroTime) (* > 0 ms *) |
|
50924 | 36 |
|
37 |
fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) |
|
38 |
||
39 |
val string_of_preplay_time = ATP_Util.string_from_ext_time |
|
40 |
||
50923 | 41 |
(* timing *) |
42 |
fun take_time timeout tac arg = |
|
43 |
let |
|
44 |
val timing = Timing.start () |
|
45 |
in |
|
50924 | 46 |
(TimeLimit.timeLimit timeout tac arg; |
47 |
Timing.result timing |> #cpu |> pair false) |
|
48 |
handle TimeLimit.TimeOut => (true, timeout) |
|
50923 | 49 |
end |
50 |
||
51 |
(* lookup facts in context *) |
|
52 |
fun resolve_fact_names ctxt names = |
|
53 |
names |
|
54 |
|>> map string_for_label |
|
55 |
|> op @ |
|
56 |
|> maps (thms_of_name ctxt) |
|
57 |
||
51178 | 58 |
(* *) |
59 |
fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
|
60 |
fun fact_of_subproof ctxt proof = |
|
50923 | 61 |
let |
51178 | 62 |
val (fixed_frees, assms, concl) = split_proof proof |
63 |
val var_idx = maxidx_of_term concl + 1 |
|
64 |
fun var_of_free (x, T) = Var((x, var_idx), T) |
|
65 |
val substitutions = |
|
66 |
map (`var_of_free #> swap #> apfst Free) fixed_frees |
|
67 |
val assms = assms |> map snd |
|
68 |
in |
|
69 |
Logic.list_implies(assms, concl) |
|
70 |
|> subst_free substitutions |
|
71 |
|> thm_of_term ctxt |
|
72 |
end |
|
73 |
||
74 |
exception ZEROTIME |
|
75 |
fun try_metis debug type_enc lam_trans ctxt timeout step = |
|
76 |
let |
|
77 |
val (t, subproofs, fact_names, obtain) = |
|
50923 | 78 |
(case step of |
51178 | 79 |
Prove (_, _, t, By_Metis (subproofs, fact_names)) => |
80 |
(t, subproofs, fact_names, false) |
|
81 |
| Obtain (_, xs, _, t, By_Metis (subproofs, fact_names)) => |
|
50923 | 82 |
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
83 |
(see ~~/src/Pure/Isar/obtain.ML) *) |
|
84 |
let |
|
85 |
val thesis = Term.Free ("thesis", HOLogic.boolT) |
|
86 |
val thesis_prop = thesis |> HOLogic.mk_Trueprop |
|
87 |
val frees = map Term.Free xs |
|
88 |
||
89 |
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
|
90 |
val inner_prop = |
|
91 |
fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) |
|
92 |
||
93 |
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
|
94 |
val prop = |
|
95 |
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
|
96 |
in |
|
51178 | 97 |
(prop, subproofs, fact_names, true) |
50923 | 98 |
end |
99 |
| _ => raise ZEROTIME) |
|
100 |
val facts = |
|
51178 | 101 |
map (fact_of_subproof ctxt) subproofs @ |
102 |
resolve_fact_names ctxt fact_names |
|
50923 | 103 |
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |
104 |
|> obtain ? Config.put Metis_Tactic.new_skolem true |
|
105 |
val goal = |
|
106 |
Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t |
|
107 |
fun tac {context = ctxt, prems = _} = |
|
108 |
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 |
|
109 |
in |
|
50924 | 110 |
take_time timeout |
111 |
(fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg)) |
|
50923 | 112 |
end |
50924 | 113 |
handle ZEROTIME => K zero_preplay_time |
50923 | 114 |
|
50924 | 115 |
(* this version treats exceptions like timeouts *) |
116 |
fun try_metis_quietly debug type_enc lam_trans ctxt timeout = |
|
117 |
the_default (true, timeout) oo try o try_metis debug type_enc lam_trans ctxt timeout |
|
50923 | 118 |
|
119 |
end |