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