author | smolkas |
Thu, 14 Feb 2013 22:49:22 +0100 | |
changeset 51131 | 7de262be1e95 |
parent 51130 | 76d68444cd59 |
child 51147 | 020a6812a204 |
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 |
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 |
||
58 |
exception ZEROTIME |
|
59 |
fun try_metis debug type_enc lam_trans ctxt timeout (succedent, step) = |
|
60 |
let |
|
61 |
val (t, byline, obtain) = |
|
62 |
(case step of |
|
63 |
Prove (_, _, t, byline) => (t, byline, false) |
|
64 |
| Obtain (_, xs, _, t, byline) => |
|
65 |
(* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis |
|
66 |
(see ~~/src/Pure/Isar/obtain.ML) *) |
|
67 |
let |
|
68 |
val thesis = Term.Free ("thesis", HOLogic.boolT) |
|
69 |
val thesis_prop = thesis |> HOLogic.mk_Trueprop |
|
70 |
val frees = map Term.Free xs |
|
71 |
||
72 |
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) |
|
73 |
val inner_prop = |
|
74 |
fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) |
|
75 |
||
76 |
(* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *) |
|
77 |
val prop = |
|
78 |
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) |
|
79 |
in |
|
80 |
(prop, byline, true) |
|
81 |
end |
|
82 |
| _ => raise ZEROTIME) |
|
83 |
val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
|
84 |
val facts = |
|
85 |
(case byline of |
|
86 |
By_Metis fact_names => resolve_fact_names ctxt fact_names |
|
87 |
| Case_Split (cases, fact_names) => |
|
88 |
resolve_fact_names ctxt fact_names |
|
89 |
@ (case the succedent of |
|
90 |
Assume (_, t) => make_thm t |
|
91 |
| Obtain (_, _, _, t, _) => make_thm t |
|
92 |
| Prove (_, _, t, _) => make_thm t |
|
50924 | 93 |
| _ => error "preplay error: unexpected succedent of case split") |
50923 | 94 |
:: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) |
50924 | 95 |
| _ => error "preplay error: malformed case split") |
50923 | 96 |
#> make_thm) |
51128
0021ea861129
introduced subblock in isar_step datatype for conjecture herbrandization
smolkas
parents:
50924
diff
changeset
|
97 |
cases |
51131 | 98 |
| Subblock proof => |
99 |
let |
|
100 |
val (steps, last_step) = split_last proof |
|
101 |
(* TODO: assuming Fix may only occur at the beginning of a subblock, |
|
102 |
this can be optimized *) |
|
103 |
val fixed_frees = |
|
104 |
fold (fn Fix xs => append (map Free xs) | _ => I) steps [] |
|
105 |
(* TODO: make sure the var indexnames are actually fresh *) |
|
106 |
fun var_of_free (Free (x, T)) = Var((x, 1), T) |
|
107 |
| var_of_free _ = error "preplay error: not a free variable" |
|
108 |
val substitutions = map (`var_of_free #> swap) fixed_frees |
|
109 |
val concl = |
|
110 |
(case last_step of |
|
111 |
Prove (_, _, t, _) => t |
|
112 |
| _ => error "preplay error: unexpected conclusion of subblock") |
|
113 |
in |
|
114 |
concl |> subst_free substitutions |> make_thm |> single |
|
115 |
end) |
|
50923 | 116 |
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |
117 |
|> obtain ? Config.put Metis_Tactic.new_skolem true |
|
118 |
val goal = |
|
119 |
Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t |
|
120 |
fun tac {context = ctxt, prems = _} = |
|
121 |
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 |
|
122 |
in |
|
50924 | 123 |
take_time timeout |
124 |
(fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg)) |
|
50923 | 125 |
end |
50924 | 126 |
handle ZEROTIME => K zero_preplay_time |
50923 | 127 |
|
50924 | 128 |
(* this version treats exceptions like timeouts *) |
129 |
fun try_metis_quietly debug type_enc lam_trans ctxt timeout = |
|
130 |
the_default (true, timeout) oo try o try_metis debug type_enc lam_trans ctxt timeout |
|
50923 | 131 |
|
132 |
end |