1structure ThmAttribute :> ThmAttribute = 2struct 3 4 local open Symtab in end 5 type attrfun = {name:string,attrname:string,thm:Thm.thm} -> unit 6 type attrfuns = {localf: attrfun, storedf : attrfun} 7 structure Map = Symtab 8 9 val funstore = ref (Map.empty : attrfuns Map.table) 10 11 val reserved_attrnames = ["local", "private", "nocompute", "schematic"] 12 13 fun okchar c = Char.isAlphaNum c orelse c = #"_" orelse c = #"'" 14 fun illegal_attrname s = Lib.mem s reserved_attrnames orelse 15 String.isPrefix "induction=" s orelse 16 s = "" orelse 17 not (Char.isAlpha (String.sub(s,0))) orelse 18 not (CharVector.all okchar s) 19 20 fun register_attribute (kv as (s, f)) = 21 let 22 val _ = not (illegal_attrname s) orelse 23 raise Feedback.mk_HOL_ERR "ThmAttribute" "register_attribute" 24 ("Illegal attribute name: \""^s^"\"") 25 val oldm = !funstore 26 val newm = 27 case Map.lookup oldm s of 28 NONE => Map.update kv oldm 29 | SOME _ => ( 30 Feedback.HOL_WARNING "ThmAttribute" 31 "register_attribute" 32 ("Replacing existing attribute functions for "^s); 33 Map.update kv oldm 34 ) 35 in 36 funstore := newm 37 end 38 39 fun at_attribute nm sel (arg as {name,attrname,thm}) = 40 case Map.lookup (!funstore) attrname of 41 NONE => raise Feedback.mk_HOL_ERR "ThmAttribute" 42 nm ("No such attribute: " ^ attrname) 43 | SOME a => sel a arg 44 val store_at_attribute = at_attribute "store_at_attribute" #storedf 45 val local_attribute = at_attribute "local_attribute" #localf 46 47 fun extract_attributes s = let 48 open Substring 49 val (bracketl,rest) = position "[" (full s) 50 in 51 if isEmpty rest then (s,[]) 52 else let 53 val (names,bracketr) = position "]" (slice(rest,1,NONE)) 54 in 55 if size bracketr <> 1 then 56 raise Feedback.mk_HOL_ERR "boolLib" "resolve_storename" 57 ("Malformed theorem-binding specifier: "^s) 58 else 59 (string bracketl, String.fields (fn c => c = #",") (string names)) 60 end 61 end 62 63 64end 65