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 *)