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