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