-
Notifications
You must be signed in to change notification settings - Fork 108
/
Copy pathCrunch.ML
116 lines (96 loc) · 4.51 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
(*
* 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 =
(((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 f,g for (kind) inv: P and (kind2) inv2: Q (wp: h_P simp: .. ignore: ..)
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 g 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 multiple properties"
crunch_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;