-
Notifications
You must be signed in to change notification settings - Fork 103
/
Crunch.ML
136 lines (113 loc) · 5.37 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
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
structure CrunchTheoryData = Theory_Data
(struct
type T =
((Token.src list -> string -> string
-> (string * ((Facts.ref * Token.src list), xstring) sum) list
-> string list -> local_theory -> local_theory)
* (string list -> string list -> local_theory -> local_theory)) Symtab.table
val empty = Symtab.empty
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 CallCrunch =
struct
local structure P = Parse and K = Keyword in
(* Read a list of names, up to the next section identifier *)
fun read_thm_list section sections =
let val match_section_name = Scan.first (map (P.reserved o #1) sections)
in
Scan.repeat (Scan.unless match_section_name (#2 section))
end
fun read_section all_sections section =
(P.reserved (#1 section) -- P.$$$ ":") |-- read_thm_list section all_sections
>> map (fn n => (#1 section, n))
fun read_sections sections =
Scan.repeat (Scan.first (map (read_section sections) sections)) >> List.concat
val crunch_parser =
(((Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" -- P.name
-- Parse.opt_attribs --| P.$$$ ":") -- P.list1 P.const -- Scan.optional P.term ""
-- Scan.optional (P.$$$ "(" |-- read_sections crunch_sections --| 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 crunches_parser =
(((P.list1 P.const --| P.$$$ "for")
-- P.and_list1 ((Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" -- P.name
-- Parse.opt_attribs) -- Scan.optional (P.$$$ ":" |-- P.term) "")
-- Scan.optional (P.$$$ "(" |-- read_sections crunch_sections --| P.$$$ ")") []
)
>> (fn ((consts, confs), wpigs) =>
fold (fn (((crunch_instance, prp_name), att_srcs), extra) => 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)) confs));
(*
example: crunch(kind) inv[wp]: f,g P (wp: h_P simp: .. ignore: ..)
or: crunches f,g for (kind)inv: P and (kind2)inv2: Q (wp: etc)
where: crunch = command keyword
kind = instance of crunch, e.g. valid, no_fail
inv = lemma name pattern
[wp] = optional list of attributes for all proved thms
f,g = constants under investigation
P,Q = property to be shown (not required for no_fail/empty_fail instance)
h_P = wp lemma to use (h will not be unfolded)
simp: .. = simp lemmas to use
ignore: .. = constants to ignore for unfolding
will prove lemmas for f and for any constituents required.
for the default crunch instance "valid", lemmas of the form
"{P and X} f {%_. P}" will be proven.
the additional preconditions X are propagated upwards from similar
preconditions in preexisting lemmas.
There is a longer description of what each crunch does in crunch-cmd.ML
*)
val crunchP =
Outer_Syntax.local_theory
@{command_keyword "crunch"}
"crunch through monadic definitions with a given property"
crunch_parser
val crunchesP =
Outer_Syntax.local_theory
@{command_keyword "crunches"}
"crunch through monadic definitions with multiple properties"
crunches_parser
val add_sect = ("add", Parse.const >> Constant);
val del_sect = ("del", Parse.const >> Constant);
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.list1 P.name --| P.$$$ ")") [""] -- Scan.optional
(P.$$$ "(" |-- read_sections [add_sect, del_sect] --| P.$$$ ")")
[])
>> (fn (crunch_instances, wpigs) => fn lthy =>
let fun const_name const = dest_Const (read_const lthy const) |> #1;
val add = wpigs |> filter (fn (s,_) => s = #1 add_sect) |> map #2 |> constants
|> map const_name;
val del = wpigs |> filter (fn (s,_) => s = #1 del_sect) |> map #2 |> constants
|> map const_name;
fun crunch_ignore_add_del inst =
(case get_crunch_instance inst (Proof_Context.theory_of lthy) of
NONE => error ("Crunch has not been defined for " ^ inst)
| SOME x => snd x);
val crunch_ignore_add_dels =
map (fn inst => crunch_ignore_add_del inst add del) crunch_instances
in
fold (curry (op #>)) crunch_ignore_add_dels I lthy
end));
end;
fun setup thy = thy
end;