-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCrunch.ML
221 lines (195 loc) · 8.73 KB
/
Crunch.ML
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
(*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*)
structure CrunchTheoryData = Theory_Data
(struct
type T = ((Token.src list -> string -> string -> (string * xstring) list
-> string list -> local_theory -> local_theory) * (string list -> string list -> theory -> theory)) Symtab.table
val empty = Symtab.empty
val extend = I
val merge = Symtab.merge (fn _ => true);
end);
fun get_crunch_instance name lthy =
CrunchTheoryData.get lthy
|> (fn tab => Symtab.lookup tab name)
fun add_crunch_instance name instance lthy =
CrunchTheoryData.map (Symtab.update_new (name, instance)) lthy
structure CrunchValidInstance : CrunchInstance =
struct
type extra = term;
val eq_extra = ae_conv;
val name = "valid";
val has_preconds = true;
fun mk_term pre body post =
(Syntax.parse_term @{context} "valid") $ pre $ body $ Abs ("_", dummyT, post);
fun get_precond (Const (@{const_name "valid"}, _) $ pre $ _ $ _) = pre
| get_precond _ = error "get_precond: not a hoare triple";
fun put_precond pre ((v as Const (@{const_name "valid"}, _)) $ _ $ body $ post)
= v $ pre $ body $ post
| put_precond _ _ = error "put_precond: not a hoare triple";
fun dest_term ((Const (@{const_name "valid"}, _)) $ pre $ body $ post)
= SOME (pre, body, betapply (post, Bound 0))
| dest_term _ = NONE
val pre_thms = @{thms "hoare_pre"};
val wpc_tactic = wp_cases_tactic_weak;
fun parse_extra ctxt extra
= case extra of
"" => error "A post condition is required"
| extra => let val post = Syntax.parse_term ctxt extra in (post, post) end;
val magic = Syntax.parse_term @{context}
"\<lambda>mapp_lambda_ignore. valid P_free_ignore mapp_lambda_ignore Q_free_ignore"
end;
structure CrunchValid : CRUNCH = Crunch(CrunchValidInstance);
structure CrunchNoFailInstance : CrunchInstance =
struct
type extra = unit;
val eq_extra = op =;
val name = "no_fail";
val has_preconds = true;
fun mk_term pre body _ =
(Syntax.parse_term @{context} "no_fail") $ pre $ body;
fun get_precond (Const (@{const_name "no_fail"}, _) $ pre $ _ ) = pre
| get_precond _ = error "get_precond: not a no_fail term";
fun put_precond pre ((v as Const (@{const_name "no_fail"}, _)) $ _ $ body)
= v $ pre $ body
| put_precond _ _ = error "put_precond: not a no_fail term";
fun dest_term ((Const (@{const_name "no_fail"}, _)) $ pre $ body)
= SOME (pre, body, ())
| dest_term _ = NONE
val pre_thms = @{thms "no_fail_pre"};
val wpc_tactic = wp_cases_tactic_weak;
fun parse_extra ctxt extra
= case extra of
"" => (Syntax.parse_term ctxt "%_. True", ())
| _ => (Syntax.parse_term ctxt extra, ());
val magic = Syntax.parse_term @{context}
"\<lambda>mapp_lambda_ignore. no_fail P_free_ignore mapp_lambda_ignore"
end;
structure CrunchNoFail : CRUNCH = Crunch(CrunchNoFailInstance);
structure CrunchEmptyFailInstance : CrunchInstance =
struct
type extra = unit;
val eq_extra = op =;
val name = "empty_fail";
val has_preconds = false;
fun mk_term _ body _ =
(Syntax.parse_term @{context} "empty_fail") $ body;
fun get_precond _ = error "crunch empty_fail should not be calling get_precond";
fun put_precond _ _ = error "crunch empty_fail should not be calling put_precond";
fun dest_term (Const (@{const_name empty_fail}, _) $ b)
= SOME (Term.dummy, b, ())
| dest_term _ = NONE
val pre_thms = [];
val wpc_tactic = wp_cases_tactic_weak;
fun parse_extra ctxt extra
= case extra of
"" => (Syntax.parse_term ctxt "%_. True", ())
| _ => error "empty_fail does not need a precondition";
val magic = Syntax.parse_term @{context}
"\<lambda>mapp_lambda_ignore. empty_fail mapp_lambda_ignore"
end;
structure CrunchEmptyFail : CRUNCH = Crunch(CrunchEmptyFailInstance);
structure CrunchValidEInstance : CrunchInstance =
struct
type extra = term * term;
fun eq_extra ((a, b), (c, d)) = (ae_conv (a, c) andalso ae_conv (b, d));
val name = "valid_E";
val has_preconds = true;
fun mk_term pre body extra =
(Syntax.parse_term @{context} "validE") $ pre $ body $
Abs ("_", dummyT, fst extra) $ Abs ("_", dummyT, snd extra);
fun get_precond (Const (@{const_name "validE"}, _) $ pre $ _ $ _ $ _) = pre
| get_precond _ = error "get_precond: not a validE term";
fun put_precond pre ((v as Const (@{const_name "validE"}, _)) $ _ $ body $ post $ post')
= v $ pre $ body $ post $ post'
| put_precond _ _ = error "put_precond: not a validE term";
fun dest_term (Const (@{const_name "validE"}, _) $ pre $ body $ p1 $ p2)
= SOME (pre, body, (betapply (p1, Bound 0), betapply (p2, Bound 0)))
| dest_term _ = NONE
val pre_thms = @{thms "hoare_pre"};
val wpc_tactic = wp_cases_tactic_weak;
fun parse_extra ctxt extra
= case extra of
"" => error "A post condition is required"
| extra => let val post = Syntax.parse_term ctxt extra in (post, (post, post)) end;
val magic = Syntax.parse_term @{context}
"\<lambda>mapp_lambda_ignore. validE P_free_ignore mapp_lambda_ignore Q_free_ignore Q_free_ignore"
end;
structure CrunchValidE : CRUNCH = Crunch(CrunchValidEInstance);
structure CallCrunch =
struct
local structure P = Parse and K = Keyword in
(* FIXME: Slightly outdated: *)
(*
example: crunch inv[wp]: f P (wp: h_P simp: .. ignore: ..)
where: crunch = command keyword
inv = lemma name pattern
[wp] = optional list of attributes for all proved thms
f = constant under investigation
P = property to be shown
h_P = wp lemma to use (h will not be unfolded)
simp: .. = simp lemmas to use
ignore: .. = constants to ignore for unfolding
will prove:
"{P and X} f {%_. P}" and any lemmas of this form for constituents of f,
for additional preconditions X propagated upwards from additional
preconditions in preexisting lemmas for constituents of f.
*)
(* Read a list of names, up to the next section identifier *)
fun read_thm_list sections =
let val match_section_name = Scan.first (map P.reserved sections)
in
Scan.repeat (Scan.unless match_section_name (P.name || P.long_ident))
end
fun read_section all_sections section =
(P.reserved section -- P.$$$ ":") |-- read_thm_list all_sections >> map (fn n => (section, n))
fun read_sections sections =
Scan.repeat (Scan.first (map (read_section sections) sections)) >> List.concat
val crunchP =
Outer_Syntax.local_theory
@{command_keyword "crunch"}
"crunch through monadic definitions with a given property"
(((Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" -- P.name
-- Parse.opt_attribs --| P.$$$ ":") -- P.list1 P.name -- Scan.optional P.term ""
-- Scan.optional
(P.$$$ "(" |-- read_sections [wp_sect,wp_del_sect,ignore_sect,simp_sect,simp_del_sect,rule_sect,rule_del_sect,ignore_del_sect] --| P.$$$ ")")
[]
)
>> (fn (((((crunch_instance, prp_name), att_srcs), consts), extra), wpigs) =>
(fn lthy =>
(case get_crunch_instance crunch_instance (Proof_Context.theory_of lthy) of
NONE => error ("Crunch has not been defined for " ^ crunch_instance)
| SOME (crunch_x, _) =>
crunch_x att_srcs extra prp_name wpigs consts lthy))));
val add_sect = "add";
val del_sect = "del";
val crunch_ignoreP =
Outer_Syntax.local_theory
@{command_keyword "crunch_ignore"}
"add to and delete from list of things that crunch should ignore in finding prerequisites"
((Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" -- Scan.optional
(P.$$$ "(" |-- read_sections [add_sect, del_sect] --| P.$$$ ")")
[]
)
>> (fn (crunch_instance, wpigs) => fn lthy =>
let fun const_name const = dest_Const (read_const lthy const) |> #1;
val add = wpigs |> filter (fn (s,_) => s = add_sect)
|> map (const_name o #2);
val del = wpigs |> filter (fn (s,_) => s = del_sect)
|> map (const_name o #2);
val crunch_ignore_add_del = (case get_crunch_instance crunch_instance (Proof_Context.theory_of lthy) of
NONE => error ("Crunch has not been defined for " ^ crunch_instance)
| SOME x => snd x);
in
Local_Theory.raw_theory (crunch_ignore_add_del add del) lthy
(* |> (fn lthy => Named_Target.reinit lthy lthy) *)
end));
end;
fun setup thy = thy
end;