1structure Database :> Database = 2struct 3 4(* Database.sml *) 5 6datatype component = 7 Str (* structure *) 8 | Exc of string (* exception constructor with name *) 9 | Typ of string (* type constructor with name *) 10 | Val of string (* value with name *) 11 | Con of string (* value constructor with name *) 12 | Term of string * string option (* term and optional kind *) 13 14(* An entry consist of a component and the name of its structure: *) 15 16type entry = { comp : component, file : string, line : int } 17 18(* Table represented by ordered binary tree, where key is lowercase: *) 19 20datatype 'contents table = 21 Empty 22 | Node of string * 'contents * 'contents table * 'contents table 23 24(* The database is a table of sorted lists of entries: *) 25 26type database = entry list table 27 28fun writebase(filename, db) = 29 let val os = BasicIO.open_out_bin filename 30 in Nonstdio.output_value os db; BasicIO.close_out os end 31 32fun readbase filename = 33 let open BasicIO 34 prim_type in_channel 35 type instream_ = { closed: bool, ic: in_channel } ref 36 prim_val input_value_ : in_channel -> 'a = 1 "intern_val" 37 prim_val fromI : instream -> instream_ = 1 "identity" 38 fun input_value is = 39 let val ref {closed, ic} = fromI is in 40 if closed then 41 raise SysErr("Input stream is closed", NONE) 42 else 43 input_value_ ic 44 end 45 val is = open_in_bin filename 46 val db = input_value is : database 47 in close_in is; db end 48 49(* Make sure tilde and | and \ are collated as symbols, before "A": *) 50 51fun caseless(#"~", #"~") = EQUAL 52 | caseless(#"|", #"|") = EQUAL 53 | caseless(#"\\", #"\\") = EQUAL 54 | caseless(#"\\", #"~") = LESS 55 | caseless(#"\\", #"|") = LESS 56 | caseless(#"|", #"~") = LESS 57 | caseless(#"~", #"|") = GREATER 58 | caseless(#"~", #"\\") = GREATER 59 | caseless(#"|", #"\\") = GREATER 60 | caseless(#"~", c2) = if Char.toLower c2 < #"a" then GREATER else LESS 61 | caseless(c1, #"~") = if Char.toLower c1 < #"a" then LESS else GREATER 62 | caseless(#"|", c2) = if Char.toLower c2 < #"a" then GREATER else LESS 63 | caseless(c1, #"|") = if Char.toLower c1 < #"a" then LESS else GREATER 64 | caseless(#"\\", c2) = if Char.toLower c2 < #"a" then GREATER else LESS 65 | caseless(c1, #"\\") = if Char.toLower c1 < #"a" then LESS else GREATER 66 | caseless(c1, c2) = Char.compare(Char.toLower c1, Char.toLower c2); 67 68val keycompare = String.collate caseless 69 70fun lookup(db : database, sought : string) = 71 let fun look Empty = [] 72 | look (Node(key, value, t1, t2)) = 73 case keycompare(sought, key) of 74 LESS => look t1 75 | GREATER => look t2 76 | EQUAL => value 77 in look db end 78 79(* Extract the name from an entry: *) 80 81fun getname ({comp, file, ...} : entry) = 82 case comp of 83 Str => file 84 | Exc id => id 85 | Typ id => id 86 | Val id => id 87 | Con id => id 88 | Term (id, _) => case String.tokens (fn c => c = #".") id 89 of [strName,vName] => vName 90 | other => id; 91 92 93end (* struct *)