50923
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
|
|
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)
|
|
95 |
cases)
|
|
96 |
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
|
|
97 |
|> obtain ? Config.put Metis_Tactic.new_skolem true
|
|
98 |
val goal =
|
|
99 |
Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
|
|
100 |
fun tac {context = ctxt, prems = _} =
|
|
101 |
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
|
|
102 |
in
|
50924
|
103 |
take_time timeout
|
|
104 |
(fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg))
|
50923
|
105 |
end
|
50924
|
106 |
handle ZEROTIME => K zero_preplay_time
|
50923
|
107 |
|
50924
|
108 |
(* this version treats exceptions like timeouts *)
|
|
109 |
fun try_metis_quietly debug type_enc lam_trans ctxt timeout =
|
|
110 |
the_default (true, timeout) oo try o try_metis debug type_enc lam_trans ctxt timeout
|
50923
|
111 |
|
|
112 |
end
|