1(* ------------------------------------------------------------------------- *) 2(* *) 3(* A database of lemmas. This is currently accessible in the *) 4(* following ways: *) 5(* *) 6(* - strings used to denote (part of) the name of the binding, *) 7(* or the full name of the theory of interest. Case is not *) 8(* significant. *) 9(* *) 10(* - a general matcher on the term structure of theorems. *) 11(* *) 12(* - matching (higher order) on the term structure of theorems. *) 13(* *) 14(* - looking up a specific theorem in a specific segment. *) 15(* *) 16(* ------------------------------------------------------------------------- *) 17 18structure DB :> DB = 19struct 20 21open HolKernel DB_dtype; 22 23val ERR = mk_HOL_ERR "DB"; 24 25fun indef_class2string Thm = "a theorem" 26 | indef_class2string Axm = "an axiom" 27 | indef_class2string Def = "a definition" 28 29 30(*--------------------------------------------------------------------------- 31 The pair of strings is theory * bindname 32 ---------------------------------------------------------------------------*) 33 34type data = (string * string) * (thm * class) 35 36fun dataName (((_, nm), _) : data) = nm 37fun dataThy (((thy, _), _) : data) = thy 38fun dataNameEq s d = dataName d = s 39 40 41(*--------------------------------------------------------------------------- 42 Map keys to canonical case 43 ---------------------------------------------------------------------------*) 44 45fun toLower s = 46 let open Char CharVector in tabulate(size s, fn i => toLower(sub(s,i))) end 47 48(*--------------------------------------------------------------------------- 49 Persistence: bindl is used to populate the database when a theory 50 is loaded. 51 ---------------------------------------------------------------------------*) 52 53structure Map = Redblackmap 54(* the keys are lower-cased, but the data also stores the keys, and there 55 the key infomration is kept in its original case *) 56 57fun updexisting key f m = 58 case Map.peek(m,key) of 59 NONE => m 60 | SOME v => Map.insert(m,key,f v) 61 62(* the submap is a map from lowercased item-name to those items with the 63 same name. There is a list of them because item-names are really 64 case-sensitive *) 65type submap = (string, data list) Map.dict 66val empty_sdata_map = Map.mkDict String.compare 67 68(* the dbmap contains: 69 - a map from theory-name to a submap (as above) 70*) 71datatype dbmap = DB of { namemap : (string, submap) Map.dict, 72 revmap : location list Termtab.table, 73 localmap : thm Symtab.table 74 } 75 76fun namemap (DB{namemap,...}) = namemap 77fun revmap (DB{revmap,...}) = revmap 78fun localmap (DB{localmap,...}) = localmap 79fun updnamemap f (DB{namemap,revmap,localmap}) = 80 DB {namemap = f namemap, revmap = revmap, localmap = localmap} 81fun updrevmap f (DB{namemap,revmap,localmap}) = 82 DB {namemap = namemap, revmap = f revmap, localmap=localmap} 83fun updlocalmap f (DB{namemap,revmap,localmap}) = 84 DB {namemap = namemap, revmap = revmap, localmap = f localmap} 85 86val empty_dbmap = DB {namemap = Map.mkDict String.compare, 87 localmap = Symtab.empty, revmap = Termtab.empty} 88 89local val DBref = ref empty_dbmap 90 fun lemmas() = !DBref 91 fun add_to_submap m (newdata as ((s1, s2), x)) = 92 let val s2key = toLower s2 93 val oldvalue = case Map.peek(m, s2key) of 94 NONE => [] 95 | SOME items => items 96 in 97 Map.insert(m, s2key, 98 newdata :: List.filter (not o dataNameEq s2) oldvalue) 99 end 100 fun functional_bindl_names thy blist namemap = 101 (* used when a theory is loaded from disk *) 102 let val submap = 103 case Map.peek(namemap, thy) of 104 NONE => empty_sdata_map 105 | SOME m => m 106 fun foldthis ((n,th,cl), m) = add_to_submap m ((thy,n), (th,cl)) 107 val submap' = List.foldl foldthis submap blist 108 in 109 Map.insert(namemap, thy, submap') 110 end 111 fun functional_bindl_revmap thy blist revmap = 112 List.foldl 113 (fn ((n,th,cl), A) => 114 Termtab.cons_list(concl th,Stored {Thy = thy,Name = n}) A) 115 revmap 116 blist 117 fun functional_bindl db thy blist = 118 db |> updnamemap (functional_bindl_names thy blist) 119 |> updrevmap (functional_bindl_revmap thy blist) 120 121 fun purge_stale_bindings() = 122 let 123 open Map 124 fun foldthis (n, datas : data list, m) = 125 let 126 val data' = List.filter (fn (_, (th, _)) => uptodate_thm th) 127 datas 128 in 129 insert(m,n,data') 130 end 131 fun purge_stale ttab = 132 let open Termtab 133 in 134 fold (fn (t,d) => fn A => 135 if uptodate_term t then update (t,d) A else A) 136 ttab 137 empty 138 end 139 val ct = current_theory() 140 in 141 DBref := ((!DBref) 142 |> updnamemap 143 (updexisting ct (foldl foldthis empty_sdata_map)) 144 |> updrevmap purge_stale) 145 end 146 147 fun delete_binding bnm = 148 let 149 open Map 150 val ct = current_theory() 151 fun smdelbinding bnm sm = 152 case peek (sm, toLower bnm) of 153 NONE => sm 154 | SOME datas => 155 insert(sm,toLower bnm, 156 List.filter(not o dataNameEq bnm) datas) 157 in 158 DBref := updnamemap (updexisting ct (smdelbinding bnm)) (!DBref) 159 end 160 161 162 fun hook thydelta = 163 let 164 open TheoryDelta 165 fun toThmClass (s, ThmKind_dtype.Thm th) = (s, th, Thm) 166 | toThmClass (s, ThmKind_dtype.Axiom(sn,th)) = (s, th, Axm) 167 | toThmClass (s, ThmKind_dtype.Defn th) = (s, th, Def) 168 in 169 case thydelta of 170 DelConstant _ => purge_stale_bindings() 171 | DelTypeOp _ => purge_stale_bindings() 172 | NewBinding nb => 173 ( 174 if Theory.is_temp_binding (#1 nb) then () 175 else 176 DBref := functional_bindl (!DBref) (current_theory()) 177 [toThmClass nb] 178 ) 179 | DelBinding s => delete_binding s 180 | _ => () 181 end 182 val _ = Theory.register_hook("DB", hook) 183in 184fun bindl thy blist = DBref := functional_bindl (lemmas()) thy blist 185fun revlookup th = Termtab.lookup_list (revmap (!DBref)) (concl th) 186(*--------------------------------------------------------------------------- 187 To the database representing all ancestor theories, add the 188 entries in the current theory segment. 189 ---------------------------------------------------------------------------*) 190fun CT() = !DBref 191 192fun store_local s th = 193 DBref := (!DBref |> updlocalmap (Symtab.update(s,th)) 194 |> updrevmap (Termtab.cons_list(concl th, Local s))) 195fun local_thm s = Symtab.lookup (localmap (!DBref)) s 196 197end (* local *) 198 199 200 201(*--------------------------------------------------------------------------- 202 Misc. support 203 ---------------------------------------------------------------------------*) 204 205val occurs = String.isSubstring 206 207fun norm_thyname "-" = current_theory() 208 | norm_thyname s = s; 209 210 211(*--------------------------------------------------------------------------- 212 thy : All entries in a specified theory 213 find : Look up something by name fragment 214 ---------------------------------------------------------------------------*) 215 216fun thy s = 217 let 218 val DB{namemap,...} = CT() 219 in 220 case Map.peek(namemap, norm_thyname s) of 221 NONE => [] 222 | SOME m => Map.foldl (fn (lcnm, datas, A) => datas @ A) [] m 223 end 224 225fun findpred pat s = 226 let 227 val pat = toLower pat and s = toLower s 228 val orparts = String.tokens (equal #"|") pat 229 val subparts = map (String.tokens (equal #"~")) orparts 230 val subpred = List.all (C occurs s) 231 in 232 List.exists subpred subparts 233 end 234 235fun find s = 236 let 237 val DB{namemap,...} = CT() 238 fun subfold (k, v, acc) = if findpred s k then v @ acc else acc 239 fun fold (thy, m, acc) = Map.foldr subfold acc m 240 in 241 Map.foldr fold [] namemap 242 end 243 244 245(*--------------------------------------------------------------------------- 246 Look up something by matching. Parameterized by the matcher. 247 ---------------------------------------------------------------------------*) 248 249fun matchp P thylist = 250 let fun data_P (_, (th, _)) = P th 251 fun subfold (k, v, acc) = List.filter data_P v @ acc 252 in 253 case thylist of 254 [] => let fun fold (k, m, acc) = Map.foldr subfold acc m 255 in 256 Map.foldr fold [] (namemap (CT())) 257 end 258 | _ => let val db = namemap (CT()) 259 fun fold (thyn, acc) = 260 case Map.peek(db, norm_thyname thyn) of 261 NONE => acc 262 | SOME m => Map.foldr subfold acc m 263 in 264 List.foldr fold [] thylist 265 end 266 end 267 268 269fun matcher f thyl pat = 270 matchp (fn th => can (find_term (can (f pat))) (concl th)) thyl; 271 272val match = matcher (ho_match_term [] empty_tmset); 273val apropos = match []; 274 275(* matches : term -> thm -> bool 276 tests whether theorem matches pattern *) 277fun matches pat th = 278 can (find_term (can (ho_match_term [] empty_tmset pat))) (concl th) ; 279 280fun apropos_in pat dbdata = 281 List.filter (fn (_, (th, _)) => matches pat th) dbdata ; 282 283fun find_in s = List.filter (findpred s o dataName) 284 285fun listDB () = 286 let fun subfold (k,v,acc) = v @ acc 287 fun fold (_, m, acc) = Map.foldr subfold acc m 288 in 289 Map.foldr fold [] (namemap (CT())) 290 end 291 292fun selectDB sels = 293 let 294 fun selfn (SelTM pat) = apropos_in pat 295 | selfn (SelNM s) = find_in s 296 | selfn (SelTHY s) = List.filter (equal (norm_thyname s) o dataThy) 297 fun recurse sels d = 298 case sels of 299 [] => d 300 | s::rest => recurse rest (selfn s d) 301 in 302 recurse sels (listDB()) 303 end 304 305 306(*--------------------------------------------------------------------------- 307 Some other lookup functions 308 ---------------------------------------------------------------------------*) 309 310fun thm_class origf thy name = let 311 val db = namemap (CT()) 312 val thy = norm_thyname thy 313 val nosuchthm = ("theorem "^thy^"$"^name^" not found") 314 val thymap = Map.find(db, thy) 315 handle Map.NotFound => raise ERR origf ("no such theory: "^thy) 316 val result = Map.find(thymap, toLower name) 317 handle Map.NotFound => raise ERR origf nosuchthm 318in 319 case filter (equal (norm_thyname thy,name) o fst) result of 320 [(_,p)] => p 321 | [] => raise ERR origf nosuchthm 322 | other => raise ERR origf 323 ("multiple things in theory "^thy^" with name "^name) 324end 325 326fun fetch s1 s2 = fst (thm_class "fetch" s1 s2); 327 328fun thm_of ((_,n),(th,_)) = (n,th); 329fun is x (_,(_,cl)) = (cl=x) 330 331val thms = List.map thm_of o thy 332val theorems = List.map thm_of o Lib.filter (is Thm) o thy 333val definitions = List.map thm_of o Lib.filter (is Def) o thy 334val axioms = List.map thm_of o Lib.filter (is Axm) o thy 335 336fun theorem s = let 337 val (thm,c) = thm_class "theorem" "-" s 338in 339 if c = Thm then thm 340 else raise ERR "theorem" ("No theorem in current theory of name "^s^ 341 " (but there is "^indef_class2string c^")") 342end 343 344fun definition s = let 345 val (thm,c) = thm_class "definition" "-" s 346in 347 if c = Def then thm 348 else raise ERR "theorem" ("No definition in current theory of name "^s^ 349 " (but there is "^indef_class2string c^")") 350end 351 352fun axiom s = let 353 val (thm,c) = thm_class "axiom" "-" s 354in 355 if c = Axm then thm 356 else raise ERR "axiom" ("No axiom in current theory of name "^s^ 357 " (but there is "^indef_class2string c^")") 358end 359 360fun dest_theory s = 361 let val thyname = if s = "-" then Theory.current_theory () else s 362 in 363 THEORY (thyname, 364 {types = rev (Theory.types thyname), 365 consts = rev (map dest_const (Theory.constants thyname)), 366 parents = Theory.parents thyname, 367 axioms = axioms thyname, 368 definitions = definitions thyname, 369 theorems = theorems thyname}) 370 end 371 handle e => raise ERR "dest_theory" (Lib.quote s^" is not a known theory"); 372 373end 374