1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7structure CrunchTheoryData = Theory_Data
8  (struct
9     type T =
10       ((Token.src list -> string -> string
11         -> (string * ((Facts.ref * Token.src list), xstring) sum) list
12         -> string list -> local_theory -> local_theory)
13        * (string list -> string list -> theory -> theory)) Symtab.table
14     val empty = Symtab.empty
15     val extend = I
16     val merge = Symtab.merge (fn _ => true);
17   end);
18
19fun get_crunch_instance name lthy =
20  CrunchTheoryData.get lthy
21  |> (fn tab => Symtab.lookup tab name)
22
23fun add_crunch_instance name instance lthy  =
24  CrunchTheoryData.map (Symtab.update_new (name, instance)) lthy
25
26structure CallCrunch =
27struct
28
29local structure P = Parse and K = Keyword in
30
31(* Read a list of names, up to the next section identifier *)
32fun read_thm_list section sections =
33    let val match_section_name = Scan.first (map (P.reserved o #1) sections)
34in
35    Scan.repeat (Scan.unless match_section_name (#2 section))
36end
37
38fun read_section all_sections section =
39    (P.reserved (#1 section) -- P.$$$ ":") |-- read_thm_list section all_sections
40    >> map (fn n => (#1 section, n))
41
42fun read_sections sections =
43    Scan.repeat (Scan.first (map (read_section sections) sections)) >> List.concat
44
45val crunch_parser =
46    (((Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" -- P.name
47     -- Parse.opt_attribs --| P.$$$ ":") -- P.list1 P.const -- Scan.optional P.term ""
48     -- Scan.optional
49       (P.$$$ "(" |-- read_sections [wp_sect,wp_del_sect,wps_sect,ignore_sect,simp_sect,
50                                     simp_del_sect,rule_sect,rule_del_sect,ignore_del_sect]
51        --| P.$$$ ")")
52       []
53    )
54    >> (fn (((((crunch_instance, prp_name), att_srcs), consts), extra), wpigs) =>
55           (fn lthy =>
56             (case get_crunch_instance crunch_instance (Proof_Context.theory_of lthy) of
57                 NONE => error ("Crunch has not been defined for " ^ crunch_instance)
58               | SOME (crunch_x, _) =>
59                   crunch_x att_srcs extra prp_name wpigs consts lthy))));
60
61val crunches_parser =
62    (((P.list1 P.const --| P.$$$ "for")
63     -- P.and_list1 ((Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" -- P.name
64         -- Parse.opt_attribs) -- Scan.optional (P.$$$ ":" |-- P.term) "")
65     -- Scan.optional
66       (P.$$$ "(" |-- read_sections [wp_sect,wp_del_sect,wps_sect,ignore_sect,simp_sect,
67                                     simp_del_sect,rule_sect,rule_del_sect,ignore_del_sect]
68        --| P.$$$ ")")
69       []
70    )
71    >> (fn ((consts, confs), wpigs) =>
72           fold (fn (((crunch_instance, prp_name), att_srcs), extra) => fn lthy =>
73             (case get_crunch_instance crunch_instance (Proof_Context.theory_of lthy) of
74                 NONE => error ("Crunch has not been defined for " ^ crunch_instance)
75               | SOME (crunch_x, _) =>
76                   crunch_x att_srcs extra prp_name wpigs consts lthy)) confs));
77
78(*
79 example: crunch(kind) inv[wp]: f,g  P  (wp: h_P simp: .. ignore: ..)
80
81 or: crunches f,g for (kind)inv: P and (kind2)inv2: Q (wp: etc)
82
83 where: crunch = command keyword
84        kind   = instance of crunch, e.g. valid, no_fail
85        inv    = lemma name pattern
86        [wp]   = optional list of attributes for all proved thms
87        f,g    = constants under investigation
88        P,Q    = property to be shown (not required for no_fail/empty_fail instance)
89        h_P    = wp lemma to use (h will not be unfolded)
90        simp: ..   = simp lemmas to use
91        ignore: .. = constants to ignore for unfolding
92
93 will prove lemmas for f and for any constituents required.
94 for the default crunch instance "valid", lemmas of the form
95    "{P and X} f {%_. P}" will be proven.
96 the additional preconditions X are propagated upwards from similar
97    preconditions in preexisting lemmas.
98
99 There is a longer description of what each crunch does in crunch-cmd.ML
100*)
101
102val crunchP =
103    Outer_Syntax.local_theory
104        @{command_keyword "crunch"}
105        "crunch through monadic definitions with a given property"
106        crunch_parser
107
108val crunchesP =
109    Outer_Syntax.local_theory
110        @{command_keyword "crunches"}
111        "crunch through monadic definitions with multiple properties"
112        crunches_parser
113
114val add_sect = ("add", Parse.const >> Constant);
115val del_sect = ("del", Parse.const >> Constant);
116
117val crunch_ignoreP =
118    Outer_Syntax.local_theory
119         @{command_keyword "crunch_ignore"}
120        "add to and delete from list of things that crunch should ignore in finding prerequisites"
121        ((Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" -- Scan.optional
122          (P.$$$ "(" |-- read_sections [add_sect, del_sect] --| P.$$$ ")")
123          []
124        )
125        >> (fn (crunch_instance, wpigs) => fn lthy =>
126               let fun const_name const = dest_Const (read_const lthy const) |> #1;
127                   val add = wpigs |> filter (fn (s,_) => s = #1 add_sect) |> map #2 |> constants
128                                   |> map const_name;
129                   val del = wpigs |> filter (fn (s,_) => s = #1 del_sect) |> map #2 |> constants
130                                   |> map const_name;
131                   val crunch_ignore_add_del = (case get_crunch_instance crunch_instance (Proof_Context.theory_of lthy) of
132                     NONE => error ("Crunch has not been defined for " ^ crunch_instance)
133                   | SOME x => snd x);
134               in
135                  Local_Theory.raw_theory (crunch_ignore_add_del add del) lthy
136               end));
137
138end;
139
140fun setup thy = thy
141
142end;
143
144