1structure ThmSetData :> ThmSetData = 2struct 3 4open DB Lib HolKernel 5 6type data = LoadableThyData.t 7 8fun splitnm nm = let 9 val comps = String.fields (equal #".") nm 10in 11 case comps of 12 (thy::nm::_) => (thy, nm) 13 | [name] => (current_theory(), name) 14 | [] => raise Fail "String.fields returns empty list??" 15end 16 17fun lookup ty s nm = 18 SOME (uncurry DB.fetch (splitnm nm)) 19 handle HOL_ERR _ => 20 (Feedback.HOL_WARNING "ThmSetData" "lookup" 21 ("Bad theorem name: \"" ^ nm ^ "\" from string \"" ^ 22 s ^ "\" and set-type \"" ^ ty ^ "\""); 23 NONE) 24 25fun read ty s = 26 SOME (List.mapPartial 27 (fn n => if n = "" then NONE 28 else 29 Option.map (fn r => (n,r)) (lookup ty s n)) 30 (String.fields Char.isSpace s)) 31 handle HOL_ERR _ => NONE 32 33fun writeset set = let 34 fun foldthis ((nm,_), acc) = let 35 val (thy,nm) = splitnm nm 36 in 37 (thy^"."^nm)::acc 38 end 39 val list = List.foldr foldthis [] set 40in 41 String.concatWith " " list 42end 43 44(* ---------------------------------------------------------------------- 45 destfn: takes polymorphic theory data and turns it into the 46 structured theorem data we want to use 47 storefn: takes a theorem name and stores the associated theorem into 48 the theory data. Doesn't perform any associated update in 49 the run-time memory 50 exportfn: takes a string and a list of names and theorems and does 51 something with them at runtime (adds them to a simpset, 52 say). The string is expected to be the name of the 53 theory with which these theorems are associated. 54 ---------------------------------------------------------------------- *) 55type destfn = data -> (string * thm) list option 56type storefn = string -> unit 57type exportfn = (string -> (string * thm) list -> unit) option 58val data_map = let 59 open Binarymap 60in 61 ref (mkDict String.compare : (string,destfn * storefn * exportfn) dict) 62end 63 64fun data_storefn s = Option.map #2 (Binarymap.peek(!data_map,s)) 65fun data_exportfn s = Option.join (Option.map #3 (Binarymap.peek(!data_map,s))) 66 67fun all_set_types () = Binarymap.foldr (fn (k,_,acc) => k::acc) [] (!data_map) 68 69fun foldli f a l = let 70 fun recurse a i l = 71 case l of 72 [] => a 73 | h::t => recurse (f (i,h,a)) (i + 1) t 74in 75 recurse a 0 l 76end 77 78fun set_alist_merge(a1, a2) = let 79 open Binarymap 80 val emptyd = mkDict String.compare 81 val offset = length a2 82 val d1 = foldli (fn (i,(s,th),d) => insert(d,s,(i,th))) emptyd a1 83 val d2 = foldli (fn (i,(s,th),d) => insert(d,s,(i+offset,th))) d1 a2 84 val items0 = listItems d2 85 val items = Listsort.sort (inv_img_cmp (#1 o #2) Int.compare) items0 86in 87 List.map (fn (s,(i,th)) => (s,th)) items 88end 89 90fun new ty = let 91 val (mk,dest) = LoadableThyData.new {merge = set_alist_merge, 92 read = Lib.K (read ty), terms = Lib.K [], 93 write = Lib.K writeset, thydataty = ty} 94 fun foldthis (nm,set) = 95 case lookup ty ("<internal>: "^nm) nm of 96 SOME r => (nm, r) :: set 97 | NONE => raise mk_HOL_ERR "ThmSetData" "new" ("Bad theorem name: "^nm) 98 fun mk' slist = 99 let val unencoded = foldl foldthis [] slist 100 in 101 (mk unencoded, unencoded) 102 end 103 fun store s = let 104 val (data, _) = mk' [s] 105 in 106 LoadableThyData.write_data_update {thydataty = ty, data = data} 107 end 108 109 val _ = data_map := Binarymap.insert(!data_map,ty,(dest,store,NONE)) 110in 111 (mk',dest) 112end 113 114fun theory_data {settype = key, thy} = 115 case Binarymap.peek(!data_map, key) of 116 NONE => raise mk_HOL_ERR "ThmSetData" "theory_data" 117 ("No ThmSetData with name "^Lib.quote key) 118 | SOME (df,_,_) => let 119 open LoadableThyData 120 in 121 case segment_data {thy = thy, thydataty = key} of 122 NONE => [] 123 | SOME d => valOf (df d) 124 handle Option => 125 raise mk_HOL_ERR "ThmSetData" "theory_data" 126 ("ThmSetData for name " ^ Lib.quote key ^ 127 " doesn't decode") 128 end 129 130fun current_data s = theory_data { settype = s, thy = current_theory() } 131 132fun all_data s = map (fn thy => (thy, theory_data {settype = s, thy = thy})) 133 (current_theory() :: ancestry "-") 134 135fun new_exporter name addfn = let 136 val (mk,dest) = new name 137 open LoadableThyData TheoryDelta 138 fun onload thyname = 139 case segment_data {thy = thyname, thydataty = name} of 140 NONE => () 141 | SOME d => let 142 val thms = valOf (dest d) 143 in 144 addfn thyname thms 145 end 146 fun revise_data P td = 147 case segment_data {thy = current_theory(), thydataty = name} of 148 NONE => () 149 | SOME d => let 150 val alist = valOf (dest d) 151 val (ok,notok) = Lib.partition P alist 152 in 153 case notok of 154 [] => () 155 | _ => (HOL_WARNING 156 "ThmSetData" "revise_data" 157 ("\n Theorems in set " ^ Lib.quote name ^ 158 ":\n " ^ String.concatWith ", " (map #1 notok) ^ 159 "\n invalidated by " ^ TheoryDelta.toString td); 160 set_theory_data {thydataty = name, 161 data = #1 (mk (map #1 ok))}) 162 end 163 164 fun hook (TheoryLoaded s) = onload s 165 | hook (td as DelConstant _) = revise_data (uptodate_thm o #2) td 166 | hook (td as DelTypeOp _) = revise_data (uptodate_thm o #2) td 167 | hook (td as NewConstant _) = revise_data (uptodate_thm o #2) td 168 | hook (td as NewTypeOp _) = revise_data (uptodate_thm o #2) td 169 | hook (td as DelBinding s) = revise_data (not o equal s o #1) td 170 | hook _ = () 171 fun export s = let 172 val (data, namedthms) = mk [s] 173 in 174 addfn (current_theory()) namedthms; 175 write_data_update {thydataty = name, data = data} 176 end 177 val store = #2 (Binarymap.find(!data_map,name)) 178in 179 data_map := Binarymap.insert(!data_map,name,(dest,store,SOME addfn)); 180 register_hook ("ThmSetData.onload." ^ name, hook); 181 List.app onload (ancestry "-"); 182 {export = export, mk = mk, dest = dest} 183end 184 185fun new_storage_attribute s = let 186in 187 new_exporter s (fn _ => fn _ => ()); 188 Theory.adjoin_to_theory { 189 sig_ps = NONE, 190 struct_ps = SOME 191 (fn _ => 192 PP.add_string 193 ("val _ = ThmSetData.new_exporter "^Lib.mlquote s^ 194 " (fn _ => fn _ => ())\n")) 195 } 196end 197 198fun store_attribute {attribute, thm_name} = 199 case data_storefn attribute of 200 NONE => raise mk_HOL_ERR "ThmSetData" "store_attribute" 201 ("Unknown attribute: "^attribute) 202 | SOME f => f thm_name 203 204end (* struct *) 205