1(* Database.sml *)
2structure Database :> Database = struct
3
4
5(* For unknown reasons, BinIO.inputN is raising Subscript exceptions *)
6local
7fun myInputN' (is, 0) = []
8  | myInputN' (is, n) =
9  case BinIO.input1 is of
10    NONE => []
11  | SOME v => v :: myInputN' (is, n-1);
12in
13fun myInputN (is, n) = Word8Vector.fromList (myInputN' (is, n))
14end;
15
16fun writeInt32 os i =
17  let
18    val w = Word32.fromInt i
19    fun w32tow8 w = Word8.fromInt (Word32.toInt w)
20  in
21    (BinIO.output1 (os, w32tow8 w);
22     BinIO.output1 (os, w32tow8 (Word32.>> (w, 0w8)));
23     BinIO.output1 (os, w32tow8 (Word32.>> (w, 0w16)));
24     BinIO.output1 (os, w32tow8 (Word32.>> (w, 0w24))))
25  end;
26
27fun readInt32 is =
28  let
29    val v = myInputN (is, 4)
30    fun w8tow32 i s =
31      Word32.<< (Word32.fromInt (Word8.toInt (Word8Vector.sub (v, i))), s)
32  in
33    Word32.toInt (Word32.orb (w8tow32 0 0w0,
34                  Word32.orb (w8tow32 1 0w8,
35                  Word32.orb (w8tow32 2 0w16,
36                              w8tow32 3 0w24))))
37  end;
38
39fun writeString os s =
40  (writeInt32 os (String.size s);
41   BinIO.output (os, Byte.stringToBytes s));
42
43fun readString is =
44  let val len = readInt32 is in
45    Byte.bytesToString (myInputN (is, len))
46  end;
47
48fun writeList write os l =
49  let
50    fun f [] =
51        BinIO.output1 (os, 0w0)
52      | f (e::t) =
53        (BinIO.output1 (os, 0w1);
54         write os e;
55         writeList write os t)
56  in
57    f (List.rev l)
58  end;
59
60fun readList read is acc =
61  let val tag = BinIO.input1 is in
62    case tag of
63         SOME 0w0 => acc
64       | _ => readList read is (read is :: acc)
65  end;
66
67datatype component =
68    Str					(* structure                       *)
69  | Exc of string			(* exception constructor with name *)
70  | Typ of string			(* type constructor with name      *)
71  | Val of string			(* value with name                 *)
72  | Con of string			(* value constructor with name	   *)
73  | Term of string * string option	(* term and optional kind          *)
74
75fun writeComponent os Str =
76    BinIO.output1 (os, 0w0)
77  | writeComponent os (Exc s) =
78    (BinIO.output1 (os, 0w1);
79     writeString os s)
80  | writeComponent os (Typ s) =
81    (BinIO.output1 (os, 0w2);
82     writeString os s)
83  | writeComponent os (Val s) =
84    (BinIO.output1 (os, 0w3);
85     writeString os s)
86  | writeComponent os (Con s) =
87    (BinIO.output1 (os, 0w4);
88     writeString os s)
89  | writeComponent os (Term (s, NONE)) =
90    (BinIO.output1 (os, 0w5);
91     writeString os s)
92  | writeComponent os (Term (s1, SOME s2)) =
93    (BinIO.output1 (os, 0w6);
94     writeString os s1;
95     writeString os s2);
96
97fun readComponent is =
98  let val tag = BinIO.input1 is in
99    case tag of
100         SOME 0w0 => Str
101       | SOME 0w1 => Exc (readString is)
102       | SOME 0w2 => Typ (readString is)
103       | SOME 0w3 => Val (readString is)
104       | SOME 0w4 => Con (readString is)
105       | SOME 0w5 => Term (readString is, NONE)
106       | _ =>
107           let
108             val s1 = readString is
109             val s2 = readString is
110           in
111             Term (s1, SOME s2)
112           end
113  end;
114
115(* An entry consist of a component and the name of its structure: *)
116
117type entry = { comp : component, file : string, line : int }
118
119fun writeEntry os (e:entry) =
120  (writeComponent os (#comp e);
121   writeString os (#file e);
122   writeInt32 os (#line e));
123
124fun readEntry is =
125  let
126    val c = readComponent is
127    val f = readString is
128    val l = readInt32 is
129  in
130    {comp = c, file = f, line = l}
131  end;
132
133(* Table represented by ordered binary tree, where key is lowercase: *)
134
135datatype 'contents table =
136    Empty
137  | Node of string * 'contents * 'contents table * 'contents table
138
139fun writeTable os Empty =
140    BinIO.output1 (os, 0w0)
141  | writeTable os (Node (s, el, t1, t2)) =
142    (BinIO.output1 (os, 0w1);
143     writeString os s;
144     writeList writeEntry os el;
145     writeTable os t1;
146     writeTable os t2);
147
148fun readTable is =
149  let val tag = BinIO.input1 is in
150    case tag of
151         SOME 0w0 => Empty
152       | _ =>
153           let
154             val s = readString is
155             val c = readList readEntry is []
156             val t1 = readTable is
157             val t2 = readTable is
158           in
159             Node (s, c, t1, t2)
160           end
161  end;
162
163(* The database is a table of sorted lists of entries: *)
164
165type database = entry list table
166
167fun writebase(filename, db) =
168  let val os = BinIO.openOut filename in
169    writeTable os db;
170    BinIO.closeOut os
171  end;
172
173fun readbase filename =
174  let
175    val is = BinIO.openIn filename
176    val t = readTable is
177  in
178    BinIO.closeIn is;
179    t
180  end;
181
182(* Make sure tilde and | and \ are collated as symbols, before "A": *)
183
184fun caseless(#"~", #"~")  = EQUAL
185  | caseless(#"|", #"|")  = EQUAL
186  | caseless(#"\\", #"\\") = EQUAL
187  | caseless(#"\\", #"~") = LESS
188  | caseless(#"\\", #"|") = LESS
189  | caseless(#"|", #"~")  = LESS
190  | caseless(#"~", #"|")  = GREATER
191  | caseless(#"~", #"\\")  = GREATER
192  | caseless(#"|", #"\\")  = GREATER
193  | caseless(#"~", c2) = if Char.toLower c2 < #"a" then GREATER else LESS
194  | caseless(c1, #"~") = if Char.toLower c1 < #"a" then LESS else GREATER
195  | caseless(#"|", c2) = if Char.toLower c2 < #"a" then GREATER else LESS
196  | caseless(c1, #"|") = if Char.toLower c1 < #"a" then LESS else GREATER
197  | caseless(#"\\", c2) = if Char.toLower c2 < #"a" then GREATER else LESS
198  | caseless(c1, #"\\") = if Char.toLower c1 < #"a" then LESS else GREATER
199  | caseless(c1, c2) = Char.compare(Char.toLower c1, Char.toLower c2);
200
201val keycompare = String.collate caseless
202
203fun lookup(db : database, sought : string) =
204    let fun look Empty                      = []
205	  | look (Node(key, value, t1, t2)) =
206	    case keycompare(sought, key) of
207		LESS    => look t1
208	      | GREATER => look t2
209	      | EQUAL   => value
210    in look db end
211
212(* Extract the name from an entry: *)
213
214fun getname ({comp, file, ...} : entry) =
215    case comp of
216	Str    => file
217      | Exc id => id
218      | Typ id => id
219      | Val id => id
220      | Con id => id
221      | Term (id, _) => case String.tokens (fn c => c = #".") id
222                         of [strName,vName] => vName
223                          | other => id;
224
225end
226