1structure KernelSig :> KernelSig =
2struct
3
4  type kernelname = {Thy : string, Name : string}
5  fun name_compare ({Thy = thy1, Name = n1}, {Thy = thy2, Name = n2}) =
6      case String.compare (n1, n2) of
7        EQUAL => String.compare(thy1,thy2)
8      | x => x
9
10  fun name_toString {Thy,Name} = Thy ^ "$" ^ Name
11  fun name_toMLString {Thy,Name} =
12    "{Thy=\"" ^ String.toString Thy ^ "\",Name=\"" ^ String.toString Name ^ "\"}"
13
14  type kernelid = (kernelname * bool) ref (* bool is uptodate flag *)
15
16  fun name_of_id r = case !r of (n,utd) => n
17  fun uptodate_id r = case !r of (n,utd) => utd
18  fun new_id n = ref (n, true)
19  fun retire_id r = case !r of ({Thy,Name}, _) =>
20      r := ({Thy = Thy, Name = Globals.old Name}, false)
21  fun name_of r = case !r of  ({Name,Thy},_) => Name
22  fun seg_of r = case !r of ({Thy,Name},_) => Thy
23  fun id_toString id = name_toString (name_of_id id)
24  fun id_compare(i1, i2) =
25    case (!i1, !i2) of ((n1,_), (n2,_)) =>
26      if i1 = i2 then EQUAL else name_compare(n1,n2)
27
28
29  type 'a symboltable = (kernelname, kernelid * 'a) Binarymap.dict ref
30  exception NotFound
31
32  fun new_table() = ref (Binarymap.mkDict name_compare)
33  fun find(tab,n) = Binarymap.find(!tab,n)
34      handle Binarymap.NotFound => raise NotFound
35  fun peek(tab,n) = Binarymap.peek(!tab,n)
36  fun remove(r, n) = let
37    val (tab', (id,v)) = Binarymap.remove(!r,n)
38  in
39    r := tab';
40    SOME (id,v)
41  end handle Binarymap.NotFound => NONE
42
43  fun numItems r = Binarymap.numItems (!r)
44
45  fun app f r = Binarymap.app f (!r)
46
47  fun foldl f acc r = Binarymap.foldl f acc (!r)
48
49  fun retire_name (r, n) =
50      case remove(r, n) of
51        NONE => raise NotFound
52      | SOME (kid, v) => retire_id kid
53
54  fun insert(r,n,v) = let
55    val id = new_id n
56  in
57    retire_name(r,n) handle NotFound => ();
58    r := Binarymap.insert(!r,n,(id, v));
59    id
60  end
61
62
63  fun uptodate_name (r, n) = let
64    val (kid, _) = find(r, n)
65  in
66    uptodate_id kid
67  end
68
69  fun listItems r = Binarymap.listItems (!r)
70  fun listThy tab thy = let
71    fun foldthis ({Thy,Name},(kid,v),acc) =
72        if Thy = thy then ({Thy = Thy,Name = Name},(kid,v)) :: acc
73        else acc
74  in
75    foldl foldthis [] tab
76  end
77
78  fun listName tab nm = let
79    fun foldthis ({Thy,Name},(kid,v),acc) =
80        if Name = nm  then ({Thy = Thy,Name = Name},(kid,v)) :: acc
81        else acc
82  in
83    foldl foldthis [] tab
84  end
85
86  fun del_segment (r, thyname) = let
87    fun appthis (knm as {Name,Thy},(id,v)) =
88        if Thy = thyname then retire_name(r,knm)
89        else ()
90  in
91    app appthis r
92  end
93
94
95
96
97end
98