]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/hbugs/hbugs_broker_registry.ml
incomplete proof completed
[helm.git] / helm / ocaml / hbugs / hbugs_broker_registry.ml
1 (*
2  * Copyright (C) 2003:
3  *    Stefano Zacchiroli <zack@cs.unibo.it>
4  *    for the HELM Team http://helm.cs.unibo.it/
5  *
6  *  This file is part of HELM, an Hypertextual, Electronic
7  *  Library of Mathematics, developed at the Computer Science
8  *  Department, University of Bologna, Italy.
9  *
10  *  HELM is free software; you can redistribute it and/or
11  *  modify it under the terms of the GNU General Public License
12  *  as published by the Free Software Foundation; either version 2
13  *  of the License, or (at your option) any later version.
14  *
15  *  HELM is distributed in the hope that it will be useful,
16  *  but WITHOUT ANY WARRANTY; without even the implied warranty of
17  *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
18  *  GNU General Public License for more details.
19  *
20  *  You should have received a copy of the GNU General Public License
21  *  along with HELM; if not, write to the Free Software
22  *  Foundation, Inc., 59 Temple Place - Suite 330, Boston,
23  *  MA  02111-1307, USA.
24  *
25  *  For details, see the HELM World-Wide-Web page,
26  *  http://helm.cs.unibo.it/
27  *)
28
29 open Hbugs_misc;;
30 open Hbugs_types;;
31 open Printf;;
32
33 exception Client_already_in of client_id;;
34 exception Client_not_found of client_id;;
35 exception Musing_already_in of musing_id;;
36 exception Musing_not_found of musing_id;;
37 exception Tutor_already_in of tutor_id;;
38 exception Tutor_not_found of tutor_id;;
39
40 class type registry =
41   object
42     method dump: string
43     method purge: unit
44   end
45
46 let expire_time = 1800. (* 30 minutes *)
47
48 class clients =
49   object (self)
50
51     inherit ThreadSafe.threadSafe
52 (*
53     (* <DEBUGGING> *)
54     method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
55     method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
56     method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
57     (* </DEBUGGING> *)
58 *)
59
60     val timetable: (client_id, float) Hashtbl.t = Hashtbl.create 17
61     val urls: (client_id, string) Hashtbl.t = Hashtbl.create 17
62     val subscriptions: (client_id, tutor_id list) Hashtbl.t = Hashtbl.create 17
63
64       (** INVARIANT: each client registered has an entry in 'urls' hash table
65       _and_ in 'subscriptions hash table even if it hasn't yet invoked
66       'subscribe' method *)
67
68     method register id url = self#doWriter (lazy (
69       if Hashtbl.mem urls id then
70         raise (Client_already_in id)
71       else begin
72         Hashtbl.add urls id url;
73         Hashtbl.add subscriptions id [];
74         Hashtbl.add timetable id (Unix.time ())
75       end
76     ))
77     method private remove id =
78       Hashtbl.remove urls id;
79       Hashtbl.remove subscriptions id;
80       Hashtbl.remove timetable id
81     method unregister id = self#doWriter (lazy (
82       if Hashtbl.mem urls id then
83         self#remove id
84       else
85         raise (Client_not_found id)
86     ))
87     method isAuthenticated id = self#doReader (lazy (
88       Hashtbl.mem urls id
89     ))
90     method subscribe client_id tutor_ids = self#doWriter (lazy (
91       if Hashtbl.mem urls client_id then
92         Hashtbl.replace subscriptions client_id tutor_ids
93       else
94         raise (Client_not_found client_id)
95     ))
96     method getUrl id = self#doReader (lazy (
97       if Hashtbl.mem urls id then
98         Hashtbl.find urls id
99       else
100         raise (Client_not_found id)
101     ))
102     method getSubscription id = self#doReader (lazy (
103       if Hashtbl.mem urls id then
104         Hashtbl.find subscriptions id
105       else
106         raise (Client_not_found id)
107     ))
108
109     method dump = self#doReader (lazy (
110       "<clients>\n" ^
111       (Hashtbl.fold
112         (fun id url dump ->
113           (dump ^
114           (sprintf "<client id=\"%s\" url=\"%s\">\n" id url) ^
115           "<subscriptions>\n" ^
116           (String.concat "\n" (* id's subscriptions *)
117             (List.map
118               (fun tutor_id -> sprintf "<tutor id=\"%s\" />\n" tutor_id)
119               (Hashtbl.find subscriptions id))) ^
120           "</subscriptions>\n</client>\n"))
121         urls "") ^
122       "</clients>"
123     ))
124     method purge = self#doWriter (lazy (
125       let now = Unix.time () in
126       Hashtbl.iter
127         (fun id birthday ->
128           if now -. birthday > expire_time then
129             self#remove id)
130         timetable
131     ))
132
133   end
134
135 class tutors =
136   object (self)
137
138     inherit ThreadSafe.threadSafe
139 (*
140     (* <DEBUGGING> *)
141     method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
142     method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
143     method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
144     (* </DEBUGGING> *)
145 *)
146
147     val timetable: (tutor_id, float) Hashtbl.t = Hashtbl.create 17
148     val tbl: (tutor_id, string * hint_type * string) Hashtbl.t =
149       Hashtbl.create 17
150
151     method register id url hint_type dsc = self#doWriter (lazy (
152       if Hashtbl.mem tbl id then
153         raise (Tutor_already_in id)
154       else begin
155         Hashtbl.add tbl id (url, hint_type, dsc);
156         Hashtbl.add timetable id (Unix.time ())
157       end
158     ))
159     method private remove id =
160       Hashtbl.remove tbl id;
161       Hashtbl.remove timetable id
162     method unregister id = self#doWriter (lazy (
163       if Hashtbl.mem tbl id then
164         self#remove id
165       else
166         raise (Tutor_not_found id)
167     ))
168     method isAuthenticated id = self#doReader (lazy (
169       Hashtbl.mem tbl id
170     ))
171     method exists id = self#doReader (lazy (
172       Hashtbl.mem tbl id
173     ))
174     method getTutor id = self#doReader (lazy (
175       if Hashtbl.mem tbl id then
176         Hashtbl.find tbl id
177       else
178         raise (Tutor_not_found id)
179     ))
180     method getUrl id =
181       let (url, _, _) = self#getTutor id in
182       url
183     method getHintType id =
184       let (_, hint_type, _) = self#getTutor id in
185       hint_type
186     method getDescription id =
187       let (_, _, dsc) = self#getTutor id in
188       dsc
189     method index = self#doReader (lazy (
190       Hashtbl.fold
191         (fun id (url, hint_type, dsc) idx -> (id, dsc) :: idx) tbl []
192     ))
193
194     method dump = self#doReader (lazy (
195       "<tutors>\n" ^
196       (Hashtbl.fold
197         (fun id (url, hint_type, dsc) dump ->
198           dump ^
199           (sprintf
200 "<tutor id=\"%s\" url=\"%s\">\n<hint_type>%s</hint_type>\n<description>%s</description>\n</tutor>"
201             id url hint_type dsc))
202         tbl "") ^
203       "</tutors>"
204     ))
205     method purge = self#doWriter (lazy (
206       let now = Unix.time () in
207       Hashtbl.iter
208         (fun id birthday ->
209           if now -. birthday > expire_time then
210             self#remove id)
211         timetable
212     ))
213
214   end
215
216 class musings =
217   object (self)
218
219     inherit ThreadSafe.threadSafe
220 (*
221     (* <DEBUGGING> *)
222     method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
223     method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
224     method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
225     (* </DEBUGGING> *)
226 *)
227
228     val timetable: (musing_id, float) Hashtbl.t = Hashtbl.create 17
229     val musings: (musing_id, client_id * tutor_id) Hashtbl.t = Hashtbl.create 17
230     val clients: (client_id, musing_id list) Hashtbl.t = Hashtbl.create 17
231     val tutors: (tutor_id, musing_id list) Hashtbl.t = Hashtbl.create 17
232
233       (** INVARIANT: each registered musing <musing_id, client_id, tutor_id> has
234       an entry in 'musings' table, an entry in 'clients' (i.e. one of the
235       musings for client_id is musing_id) table, an entry in 'tutors' table
236       (i.e. one of the musings for tutor_id is musing_id) and an entry in
237       'timetable' table *)
238
239
240     method register musing_id client_id tutor_id = self#doWriter (lazy (
241       if Hashtbl.mem musings musing_id then
242         raise (Musing_already_in musing_id)
243       else begin
244         Hashtbl.add musings musing_id (client_id, tutor_id);
245           (* now add this musing as the first one of musings list for client and
246           tutor *)
247         Hashtbl.replace clients client_id
248           (musing_id ::
249             (try Hashtbl.find clients client_id with Not_found -> []));
250         Hashtbl.replace tutors tutor_id
251           (musing_id ::
252             (try Hashtbl.find tutors tutor_id with Not_found -> []));
253         Hashtbl.add timetable musing_id (Unix.time ())
254       end
255     ))
256     method private remove id =
257         (* ASSUMPTION: this method is invoked under a 'writer' lock *)
258       let (client_id, tutor_id) = self#getByMusingId' id in
259       Hashtbl.remove musings id;
260         (* now remove this musing from the list of musings for client and tutor
261         *)
262       Hashtbl.replace clients client_id
263         (List.filter ((<>) id)
264           (try Hashtbl.find clients client_id with Not_found -> []));
265       Hashtbl.replace tutors tutor_id
266         (List.filter ((<>) id)
267           (try Hashtbl.find tutors tutor_id with Not_found -> []));
268       Hashtbl.remove timetable id
269     method unregister id = self#doWriter (lazy (
270       if Hashtbl.mem musings id then
271         self#remove id
272     ))
273     method private getByMusingId' id =
274       (* ASSUMPTION: this method is invoked under a 'reader' lock *)
275       try
276         Hashtbl.find musings id
277       with Not_found -> raise (Musing_not_found id)
278     method getByMusingId id = self#doReader (lazy (
279       self#getByMusingId' id
280     ))
281     method getByClientId id = self#doReader (lazy (
282       try
283         Hashtbl.find clients id
284       with Not_found -> []
285     ))
286     method getByTutorId id = self#doReader (lazy (
287       try
288         Hashtbl.find tutors id
289       with Not_found -> []
290     ))
291     method isActive id = self#doReader (lazy (
292       Hashtbl.mem musings id
293     ))
294
295     method dump = self#doReader (lazy (
296       "<musings>\n" ^
297       (Hashtbl.fold
298         (fun mid (cid, tid) dump ->
299           dump ^
300           (sprintf "<musing id=\"%s\" client=\"%s\" tutor=\"%s\" />\n"
301             mid cid tid))
302         musings "") ^
303       "</musings>"
304     ))
305     method purge = self#doWriter (lazy (
306       let now = Unix.time () in
307       Hashtbl.iter
308         (fun id birthday ->
309           if now -. birthday > expire_time then
310             self#remove id)
311         timetable
312     ))
313
314   end
315