From 3c1a6c534877f7b7266809e4d92de02c7f1ee9d4 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sun, 5 Jan 2003 15:03:03 +0000 Subject: [PATCH] - hbugs first draft release, not yet tested --- helm/hbugs/META.hbugs-common | 2 + helm/hbugs/Makefile | 17 ++ helm/hbugs/broker/.cvsignore | 8 + helm/hbugs/broker/.depend | 4 + helm/hbugs/broker/Makefile | 43 ++++ helm/hbugs/broker/Makefile.overrides | 0 helm/hbugs/broker/hbugs_broker.ml | 220 ++++++++++++++++++++ helm/hbugs/broker/hbugs_broker_registry.ml | 170 +++++++++++++++ helm/hbugs/broker/hbugs_broker_registry.mli | 69 ++++++ helm/hbugs/common/.cvsignore | 6 + helm/hbugs/common/.depend | 8 + helm/hbugs/common/Makefile | 34 +++ helm/hbugs/common/Makefile.overrides | 6 + helm/hbugs/common/hbugs_id_generator.ml | 29 +++ helm/hbugs/common/hbugs_id_generator.mli | 30 +++ helm/hbugs/common/hbugs_messages.ml | 207 ++++++++++++++++++ helm/hbugs/common/hbugs_messages.mli | 31 +++ helm/hbugs/common/hbugs_misc.ml | 95 +++++++++ helm/hbugs/common/hbugs_misc.mli | 34 +++ helm/hbugs/common/hbugs_types.ml | 82 ++++++++ helm/hbugs/common/threadSafe.ml | 94 +++++++++ 21 files changed, 1189 insertions(+) create mode 100644 helm/hbugs/META.hbugs-common create mode 100644 helm/hbugs/Makefile create mode 100644 helm/hbugs/broker/.cvsignore create mode 100644 helm/hbugs/broker/.depend create mode 100644 helm/hbugs/broker/Makefile create mode 100644 helm/hbugs/broker/Makefile.overrides create mode 100644 helm/hbugs/broker/hbugs_broker.ml create mode 100644 helm/hbugs/broker/hbugs_broker_registry.ml create mode 100644 helm/hbugs/broker/hbugs_broker_registry.mli create mode 100644 helm/hbugs/common/.cvsignore create mode 100644 helm/hbugs/common/.depend create mode 100644 helm/hbugs/common/Makefile create mode 100644 helm/hbugs/common/Makefile.overrides create mode 100644 helm/hbugs/common/hbugs_id_generator.ml create mode 100644 helm/hbugs/common/hbugs_id_generator.mli create mode 100644 helm/hbugs/common/hbugs_messages.ml create mode 100644 helm/hbugs/common/hbugs_messages.mli create mode 100644 helm/hbugs/common/hbugs_misc.ml create mode 100644 helm/hbugs/common/hbugs_misc.mli create mode 100644 helm/hbugs/common/hbugs_types.ml create mode 100644 helm/hbugs/common/threadSafe.ml diff --git a/helm/hbugs/META.hbugs-common b/helm/hbugs/META.hbugs-common new file mode 100644 index 000000000..b39f54045 --- /dev/null +++ b/helm/hbugs/META.hbugs-common @@ -0,0 +1,2 @@ +requires="pcre pxp" +directory="." # hack, just to shut up findlib's warnings diff --git a/helm/hbugs/Makefile b/helm/hbugs/Makefile new file mode 100644 index 000000000..da34da0ac --- /dev/null +++ b/helm/hbugs/Makefile @@ -0,0 +1,17 @@ +DIRS = common broker + +DIRS_BYTE = $(patsubst %,%.byte,$(DIRS)) +DIRS_OPT = $(patsubst %,%.opt,$(DIRS)) +DIRS_CLEAN = $(patsubst %,%.clean,$(DIRS)) +all: byte +byte: $(DIRS_BYTE) +opt: $(DIRS_OPT) +world: byte opt +clean: $(DIRS_CLEAN) +%.byte: + $(MAKE) -C $*/ all +%.opt: + $(MAKE) -C $*/ opt +%.clean: + $(MAKE) -C $*/ clean +.PHONY: all byte opt world clean diff --git a/helm/hbugs/broker/.cvsignore b/helm/hbugs/broker/.cvsignore new file mode 100644 index 000000000..2527ca9d9 --- /dev/null +++ b/helm/hbugs/broker/.cvsignore @@ -0,0 +1,8 @@ +*.cmi +*.cmo +*.cma +*.cmx +*.o +*.a +hbugs_broker +hbugs_broker.opt diff --git a/helm/hbugs/broker/.depend b/helm/hbugs/broker/.depend new file mode 100644 index 000000000..46f3ac82e --- /dev/null +++ b/helm/hbugs/broker/.depend @@ -0,0 +1,4 @@ +hbugs_broker.cmo: hbugs_broker_registry.cmi +hbugs_broker.cmx: hbugs_broker_registry.cmx +hbugs_broker_registry.cmo: hbugs_broker_registry.cmi +hbugs_broker_registry.cmx: hbugs_broker_registry.cmi diff --git a/helm/hbugs/broker/Makefile b/helm/hbugs/broker/Makefile new file mode 100644 index 000000000..07d255780 --- /dev/null +++ b/helm/hbugs/broker/Makefile @@ -0,0 +1,43 @@ +NAME = hbugs_broker +REQUIRES = http threads hbugs-common +COMMONDIR = ../common +COMMONOPTS = -package "$(REQUIRES)" -pp camlp4o +OCAMLC = ocamlfind ocamlc -I $(COMMONDIR) $(COMMONOPTS) +OCAMLOPT = ocamlfind ocamlopt -I $(COMMONDIR) $(COMMONOPTS) +OCAMLDEP = ocamlfind ocamldep $(COMMONOPTS) +MODULES = hbugs_broker_registry +COMMON_MODULES = \ + hbugs_types threadSafe hbugs_misc hbugs_id_generator hbugs_messages + +OBJS = $(patsubst %,%.cmo,$(MODULES)) +OBJSOPT = $(patsubst %,%.cmx,$(MODULES)) +COMMON_OBJS = $(patsubst %,$(COMMONDIR)/%.cmo,$(COMMON_MODULES)) +COMMON_OBJSOPT = $(patsubst %,$(COMMONDIR)/%.cmx,$(COMMON_MODULES)) + +all: byte +byte: $(NAME) +opt: $(NAME).opt +world: byte opt + +include .depend +depend: + $(OCAMLDEP) *.ml *.mli > .depend + +%.cmi: %.mli + OCAMLPATH=".." $(OCAMLC) -c $< +%.cmo: %.ml %.cmi + OCAMLPATH=".." $(OCAMLC) -c $< +%.cmx: %.ml %.cmi + OCAMLPATH=".." $(OCAMLOPT) -c $< +include Makefile.overrides +$(NAME): $(OBJS) $(NAME).ml + OCAMLPATH=".." $(OCAMLC) -linkpkg -thread -o $@ $(COMMON_OBJS) $^ +$(NAME).opt: $(OBJSOPT) $(NAME).ml + OCAMLPATH=".." $(OCAMLOPT) -linkpkg -thread -o $@ $(COMMON_OBJSOPT) $^ + +distclean: clean +clean: + rm -f *.cm[aiox] *.o $(NAME){,.opt} + +.PHONY: all byte opt world depend clean + diff --git a/helm/hbugs/broker/Makefile.overrides b/helm/hbugs/broker/Makefile.overrides new file mode 100644 index 000000000..e69de29bb diff --git a/helm/hbugs/broker/hbugs_broker.ml b/helm/hbugs/broker/hbugs_broker.ml new file mode 100644 index 000000000..3a9fb9383 --- /dev/null +++ b/helm/hbugs/broker/hbugs_broker.ml @@ -0,0 +1,220 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open Hbugs_types;; +open Printf;; + +let debug = true ;; +let debug_print s = if debug then prerr_endline s ;; + +let daemon_name = "H-Bugs Broker" ;; +let default_port = 49081 ;; +let port_env_var = "HELM_HBUGS_BROKER_PORT" ;; +let port = + try + int_of_string (Sys.getenv port_env_var) + with + | Not_found -> default_port + | Failure "int_of_string" -> + prerr_endline "Warning: invalid port, reverting to default"; + default_port +;; + +exception Unexpected_msg of message;; + +let xml_contype = ("Content-Type", "text/xml") ;; +let return_xml_msg body outchan = + Http_daemon.respond ~headers:[xml_contype] ~body outchan +;; +let return_hbugs_msg msg = return_xml_msg (Hbugs_messages.string_of_msg msg);; +let return_hbugs_exc name value = return_hbugs_msg (Exception (name, value));; +let send_hbugs_req ~url msg = + Hbugs_messages.msg_of_string + (Hbugs_misc.http_post ~body:(Hbugs_messages.string_of_msg msg) url) +;; +let parse_musing_id = function + | Musing_started (_, musing_id) -> musing_id + | Musing_aborted (_, musing_id) -> musing_id + | _ -> assert false +;; + +let do_critical = + let mutex = Mutex.create () in + fun action -> + try + Mutex.lock mutex; let res = Lazy.force action in Mutex.unlock mutex; res + with e -> Mutex.unlock mutex; raise e +;; + +let clients = new Hbugs_broker_registry.clients in +let tutors = new Hbugs_broker_registry.tutors in +let musings = new Hbugs_broker_registry.musings in +let my_own_id = Hbugs_id_generator.new_broker_id () in + +let handle_msg outchan = function + + (* messages from clients *) + | Register_client (client_id, client_url) -> do_critical (lazy ( + debug_print "Register_client"; + try + clients#register client_id client_url; + return_hbugs_msg (Client_registered my_own_id) outchan + with Hbugs_broker_registry.Client_already_in id -> + return_hbugs_exc "already_registered" id outchan + )) + | Unregister_client client_id -> do_critical (lazy ( + debug_print "Unregister_client"; + if clients#isAuthenticated client_id then begin + clients#unregister client_id; + return_hbugs_msg (Client_unregistered my_own_id) outchan + end else + return_hbugs_exc "forbidden" client_id outchan + )) + | List_tutors client_id -> do_critical (lazy ( + debug_print "List_tutors"; + if clients#isAuthenticated client_id then begin + return_hbugs_msg (Tutor_list (my_own_id, tutors#index)) outchan + end else + return_hbugs_exc "forbidden" client_id outchan + )) + | Subscribe (client_id, tutor_ids) -> do_critical (lazy ( + debug_print "Subscribe"; + if clients#isAuthenticated client_id then begin + if List.for_all tutors#exists tutor_ids then begin + clients#subscribe client_id tutor_ids; + return_hbugs_msg (Subscribed (my_own_id, tutor_ids)) outchan + end else (* required subscription to an unexistent tutor *) + let tutor_id = + List.find (fun id -> not (tutors#exists id)) tutor_ids + in + return_hbugs_exc "tutor_not_found" tutor_id outchan + end else + return_hbugs_exc "forbidden" client_id outchan + )) + | State_change (client_id, new_state) -> do_critical (lazy ( + debug_print "State_change"; + if clients#isAuthenticated client_id then begin + let active_musings = musings#getByClientId client_id in + let stop_answers = + List.map (* collect Abort_musing message's responses *) + (fun id -> (* musing id *) + let tutor = snd (musings#getByMusingId id) in + send_hbugs_req + ~url:(tutors#getUrl tutor) (Abort_musing (my_own_id, id))) + active_musings + in + List.iter musings#unregister active_musings; + let started_musing_ids = + List.map (* register new musings and collect their ids *) + (fun tutor_id -> + let res = + send_hbugs_req + ~url:(tutors#getUrl tutor_id) + (Start_musing (my_own_id, new_state)) + in + let musing_id = parse_musing_id res in + musings#register musing_id client_id tutor_id; + musing_id) + (clients#getSubscription client_id) + in + let stopped_musing_ids = List.map parse_musing_id stop_answers in + return_hbugs_msg + (State_accepted (my_own_id, stopped_musing_ids, started_musing_ids)) + outchan + end else + return_hbugs_exc "forbidden" client_id outchan + )) + + (* messages from tutors *) + | Register_tutor (tutor_id, tutor_url, hint_type, dsc) -> do_critical (lazy ( + debug_print "Register_tutor"; + try + tutors#register tutor_id tutor_url hint_type dsc; + return_hbugs_msg (Tutor_registered my_own_id) outchan + with Hbugs_broker_registry.Tutor_already_in id -> + return_hbugs_exc "already_registered" id outchan + )) + | Unregister_tutor tutor_id -> do_critical (lazy ( + debug_print "Unregister_tutor"; + if tutors#isAuthenticated tutor_id then begin + tutors#unregister tutor_id; + return_hbugs_msg (Tutor_unregistered my_own_id) outchan + end else + return_hbugs_exc "forbidden" tutor_id outchan + )) + | Musing_completed (tutor_id, musing_id, result) -> do_critical (lazy ( + debug_print "Musing_completed"; + if tutors#isAuthenticated tutor_id then begin + (match result with + | Sorry -> () + | Eureka extras -> + let res = + let hint = (* TODO decidere la hint *) "hint!!!!" in + let url = + clients#getUrl (fst (musings#getByMusingId musing_id)) + in + send_hbugs_req ~url (Hint (my_own_id, hint)) + in + ignore res (* TODO mi interessa la risposta? *) + ); + return_hbugs_msg (Thanks (my_own_id, musing_id)) outchan; + musings#unregister musing_id + end else + return_hbugs_exc "forbidden" tutor_id outchan + )) + + | msg -> (* unexpected message *) + debug_print "Unknown message!"; + return_hbugs_msg + (Exception ("Unexpected_msg", Hbugs_messages.string_of_msg msg)) + outchan +in + + (* thread action *) +let callback (req: Http_types.request) outchan = + try + debug_print ("Connection from " ^ req#clientAddr); + debug_print ("Received request: " ^ req#path); + (match req#path with + (* TODO write help message *) + | "/help" -> return_xml_msg " not yet written " outchan + | "/act" -> handle_msg outchan (Hbugs_messages.msg_of_string req#body) + | _ -> Http_daemon.respond_error ~code:400 outchan); + debug_print "Done!\n" + with + | Http_types.Param_not_found attr_name -> + return_hbugs_exc "missing_parameter" attr_name outchan + | exc -> + return_hbugs_exc "uncaught_exception" (Printexc.to_string exc) outchan +in + +(* TODO aggiungere lo spazzino che elimina i client/tutor/computation che non si +fanno sentire da troppo tempo ... *) + (* start daemon *) +printf "Listening on port %d ...\n" port; +flush stdout; +Http_daemon.start' ~port ~mode:`Thread callback + diff --git a/helm/hbugs/broker/hbugs_broker_registry.ml b/helm/hbugs/broker/hbugs_broker_registry.ml new file mode 100644 index 000000000..adf8bc379 --- /dev/null +++ b/helm/hbugs/broker/hbugs_broker_registry.ml @@ -0,0 +1,170 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open Hbugs_misc;; +open Hbugs_types;; + +exception Client_already_in of client_id;; +exception Client_not_found of client_id;; +exception Musing_already_in of musing_id;; +exception Musing_not_found of musing_id;; +exception Tutor_already_in of tutor_id;; +exception Tutor_not_found of tutor_id;; + +class clients = + object (self) + + inherit ThreadSafe.threadSafe + + val urls: (client_id, string) Hashtbl.t = Hashtbl.create 17 + val subscriptions: (client_id, tutor_id list) Hashtbl.t = Hashtbl.create 17 + + method register id url = self#doWriter (lazy ( + if Hashtbl.mem urls id then + raise (Client_already_in id) + else begin + Hashtbl.add urls id url; + Hashtbl.add subscriptions id [] + end + )) + method unregister id = self#doWriter (lazy ( + if Hashtbl.mem urls id then begin + Hashtbl.remove urls id; + Hashtbl.remove subscriptions id + end else + raise (Client_not_found id) + )) + method isAuthenticated id = self#doReader (lazy ( + Hashtbl.mem urls id + )) + method subscribe client_id tutor_ids = self#doWriter (lazy ( + if Hashtbl.mem urls client_id then + Hashtbl.replace subscriptions client_id tutor_ids + else + raise (Client_not_found client_id) + )) + method getUrl id = self#doReader (lazy ( + if Hashtbl.mem urls id then + Hashtbl.find urls id + else + raise (Client_not_found id) + )) + method getSubscription id = self#doReader (lazy ( + if Hashtbl.mem urls id then + Hashtbl.find subscriptions id + else + raise (Client_not_found id) + )) + + end + +class tutors = + object (self) + + inherit ThreadSafe.threadSafe + + val tbl: (tutor_id, string * hint_type * string) Hashtbl.t = + Hashtbl.create 17 + + method register id url hint_type dsc = self#doWriter (lazy ( + if Hashtbl.mem tbl id then + raise (Tutor_already_in id) + else + Hashtbl.add tbl id (url, hint_type, dsc) + )) + method unregister id = self#doWriter (lazy ( + if Hashtbl.mem tbl id then + Hashtbl.remove tbl id + else + raise (Tutor_not_found id) + )) + method isAuthenticated id = self#doReader (lazy ( + Hashtbl.mem tbl id + )) + method exists id = self#doReader (lazy ( + Hashtbl.mem tbl id + )) + method getTutor id = self#doReader (lazy ( + if Hashtbl.mem tbl id then + Hashtbl.find tbl id + else + raise (Tutor_not_found id) + )) + method getUrl id = + let (url, _, _) = self#getTutor id in + url + method getHintType id = + let (_, hint_type, _) = self#getTutor id in + hint_type + method getDescription id = + let (_, _, dsc) = self#getTutor id in + dsc + method index = self#doReader (lazy ( + Hashtbl.fold + (fun id (url, hint_type, dsc) idx -> (id, dsc) :: idx) tbl [] + )) + + end + +class musings = + object (self) + + inherit ThreadSafe.threadSafe + + val musings: (musing_id, client_id * tutor_id) Hashtbl.t = Hashtbl.create 17 + val clients: (client_id, musing_id) Hashtbl.t = Hashtbl.create 17 + val tutors: (tutor_id, musing_id) Hashtbl.t = Hashtbl.create 17 + + method register musing_id client_id tutor_id = self#doWriter (lazy ( + if Hashtbl.mem musings musing_id then + raise (Musing_already_in musing_id) + else begin + Hashtbl.add musings musing_id (client_id, tutor_id); + Hashtbl.add clients client_id musing_id; + Hashtbl.add tutors tutor_id musing_id + end + )) + method unregister id = self#doWriter (lazy ( + if Hashtbl.mem musings id then begin + Hashtbl.remove musings id; + hashtbl_remove_all clients id; + hashtbl_remove_all tutors id + end + )) + method getByMusingId id = self#doReader (lazy ( + try + Hashtbl.find musings id + with Not_found -> raise (Musing_not_found id) + )) + method getByClientId id = self#doReader (lazy ( + Hashtbl.find_all clients id + )) + method getByTutorId id = self#doReader (lazy ( + Hashtbl.find_all tutors id + )) + + end + diff --git a/helm/hbugs/broker/hbugs_broker_registry.mli b/helm/hbugs/broker/hbugs_broker_registry.mli new file mode 100644 index 000000000..5b42cf3b9 --- /dev/null +++ b/helm/hbugs/broker/hbugs_broker_registry.mli @@ -0,0 +1,69 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open Hbugs_types;; + +exception Client_already_in of client_id +exception Client_not_found of client_id +exception Musing_already_in of musing_id +exception Musing_not_found of musing_id +exception Tutor_already_in of tutor_id +exception Tutor_not_found of tutor_id + +class clients: + object + (** 'register client_id client_url' *) + method register: client_id -> string -> unit + method unregister: client_id -> unit + method isAuthenticated: client_id -> bool + (** subcribe a client to a set of tutor removing previous subcriptions *) + method subscribe: client_id -> tutor_id list -> unit + method getUrl: client_id -> string + method getSubscription: client_id -> tutor_id list + end + +class tutors: + object + method register: tutor_id -> string -> hint_type -> string -> unit + method unregister: tutor_id -> unit + method isAuthenticated: tutor_id -> bool + method exists: tutor_id -> bool + method getTutor: tutor_id -> string * hint_type * string + method getUrl: tutor_id -> string + method getHintType: tutor_id -> hint_type + method getDescription: tutor_id -> string + method index: tutor_dsc list + end + +class musings: + object + method register: musing_id -> client_id -> tutor_id -> unit + method unregister: musing_id -> unit + method getByMusingId: musing_id -> client_id * tutor_id + method getByClientId: client_id -> musing_id list + method getByTutorId: tutor_id -> musing_id list + end + diff --git a/helm/hbugs/common/.cvsignore b/helm/hbugs/common/.cvsignore new file mode 100644 index 000000000..a3cccbc0c --- /dev/null +++ b/helm/hbugs/common/.cvsignore @@ -0,0 +1,6 @@ +*.cmi +*.cmo +*.cma +*.cmx +*.o +*.a diff --git a/helm/hbugs/common/.depend b/helm/hbugs/common/.depend new file mode 100644 index 000000000..93f7c7534 --- /dev/null +++ b/helm/hbugs/common/.depend @@ -0,0 +1,8 @@ +hbugs_id_generator.cmo: hbugs_id_generator.cmi +hbugs_id_generator.cmx: hbugs_id_generator.cmi +hbugs_messages.cmo: hbugs_types.cmo hbugs_messages.cmi +hbugs_messages.cmx: hbugs_types.cmx hbugs_messages.cmi +hbugs_misc.cmo: hbugs_misc.cmi +hbugs_misc.cmx: hbugs_misc.cmi +hbugs_id_generator.cmi: hbugs_types.cmo +hbugs_messages.cmi: hbugs_types.cmo diff --git a/helm/hbugs/common/Makefile b/helm/hbugs/common/Makefile new file mode 100644 index 000000000..4055f88c9 --- /dev/null +++ b/helm/hbugs/common/Makefile @@ -0,0 +1,34 @@ +REQUIRES = pcre pxp +COMMONOPTS = -package "$(REQUIRES)" -pp camlp4o +OCAMLC = ocamlfind ocamlc $(COMMONOPTS) +OCAMLOPT = ocamlfind ocamlopt $(COMMONOPTS) +OCAMLDEP = ocamlfind ocamldep $(COMMONOPTS) +MODULES = \ + hbugs_types threadSafe hbugs_misc hbugs_id_generator hbugs_messages + +OBJS = $(patsubst %,%.cmo,$(MODULES)) +OBJSOPT = $(patsubst %,%.cmx,$(MODULES)) + +all: byte +byte: $(OBJS) +opt: $(OBJSOPT) +world: byte opt + +include .depend +depend: + $(OCAMLDEP) *.ml *.mli > .depend + +%.cmi: %.mli + $(OCAMLC) -c $< +%.cmo: %.ml %.cmi + $(OCAMLC) -c $< +%.cmx: %.ml %.cmi + $(OCAMLOPT) -c $< +include Makefile.overrides + +distclean: clean +clean: + rm -f *.cm[aiox] *.o $(NAME){,.opt} + +.PHONY: all byte opt world depend clean + diff --git a/helm/hbugs/common/Makefile.overrides b/helm/hbugs/common/Makefile.overrides new file mode 100644 index 000000000..f1ce52121 --- /dev/null +++ b/helm/hbugs/common/Makefile.overrides @@ -0,0 +1,6 @@ +hbugs_types.cmi hbugs_types.cmo: hbugs_types.ml + $(OCAMLC) -c $< +threadSafe.cmi threadSafe.cmo: threadSafe.ml + $(OCAMLC) -package threads -c $< +threadSafe.cmx: threadSafe.ml threadSafe.cmi + $(OCAMLOPT) -package threads -c $< diff --git a/helm/hbugs/common/hbugs_id_generator.ml b/helm/hbugs/common/hbugs_id_generator.ml new file mode 100644 index 000000000..59f67347c --- /dev/null +++ b/helm/hbugs/common/hbugs_id_generator.ml @@ -0,0 +1,29 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let new_broker_id () = (* TODO write a real id generator! *) + "FOO BROKER ID!" + diff --git a/helm/hbugs/common/hbugs_id_generator.mli b/helm/hbugs/common/hbugs_id_generator.mli new file mode 100644 index 000000000..7992fa365 --- /dev/null +++ b/helm/hbugs/common/hbugs_id_generator.mli @@ -0,0 +1,30 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open Hbugs_types;; + +val new_broker_id: unit -> broker_id + diff --git a/helm/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml new file mode 100644 index 000000000..67e739c60 --- /dev/null +++ b/helm/hbugs/common/hbugs_messages.ml @@ -0,0 +1,207 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open Hbugs_types;; +open Printf;; +open Pxp_document;; +open Pxp_types;; +open Pxp_yacc;; + +exception Attribute_not_found of string;; +exception No_element_found of string;; +exception Parse_error of string * string;; (* parsing subject, reason *) + +let is_xml_element n = match n#node_type with T_element _ -> true | _ -> false +let get_attr node name = + try + (match node#attribute name with + | Value s -> s + | _ -> raise Not_found) + with Not_found -> raise (Attribute_not_found name) + +let parse_state s = s (* TODO parsare lo stato del proof assistant! *) +let parse_hint s = s (* TODO parsare il possibile suggerimento *) +let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *) +let parse_tutor_dscs n = + List.map + (fun n -> (get_attr n "id", n#data)) + (List.filter is_xml_element n#sub_nodes) +let parse_tutor_ids node = + List.map + (fun n -> get_attr n "id") (List.filter is_xml_element node#sub_nodes) + +let tutors_sep = Pcre.regexp ",\\s*" + +let msg_of_string' s = + let root = (* xml tree's root *) + parse_wfcontent_entity default_config (from_string s) default_spec + in + match root#node_type with + + (* general purpose *) + | T_element "exception" -> Exception (get_attr root "name", root#data) + + (* client -> broker *) + | T_element "register_client" -> + Register_client (get_attr root "id", get_attr root "url") + | T_element "unregister_client" -> Unregister_client (get_attr root "id") + | T_element "list_tutors" -> List_tutors (get_attr root "id") + | T_element "subscribe" -> + Subscribe (get_attr root "id", parse_tutor_ids root) + | T_element "state_change" -> + State_change (get_attr root "id", parse_state root#data) + + (* tutor -> broker *) + | T_element "register_tutor" -> + let hint_node = find_element "hint_type" root in + let dsc_node = find_element "description" root in + Register_tutor + (get_attr root "id", get_attr root "url", + parse_hint_type hint_node, dsc_node#data) + | T_element "unregister_tutor" -> Unregister_tutor (get_attr root "id") + | T_element "musing_started" -> + Musing_started (get_attr root "id", get_attr root "musing_id") + | T_element "musing_aborted" -> + Musing_started (get_attr root "id", get_attr root "musing_id") + | T_element "musing_completed" -> + let main_node = + try + find_element "eureka" root + with Not_found -> find_element "sorry" root + in + Musing_completed + (get_attr root "id", get_attr root "musing_id", + (match main_node#node_type with + | T_element "eureka" -> Eureka main_node#data (* TODO come parsare sta roba? *) + | T_element "sorry" -> Sorry + | _ -> assert false)) (* can't be there, see 'find_element' above *) + + (* broker -> client *) + | T_element "client_registered" -> Client_registered (get_attr root "id") + | T_element "client_unregistered" -> Client_unregistered (get_attr root "id") + | T_element "tutor_list" -> + Tutor_list (get_attr root "id", parse_tutor_dscs root) + | T_element "subscribed" -> + Subscribed (get_attr root "id", parse_tutor_ids root) + | T_element "state_accepted" -> + State_accepted + (get_attr root "id", + List.map + (fun n -> get_attr n "id") + (List.filter is_xml_element (find_element "stopped" root)#sub_nodes), + List.map + (fun n -> get_attr n "id") + (List.filter is_xml_element (find_element "started" root)#sub_nodes)) + | T_element "hint" -> Hint (get_attr root "id", parse_hint root#data) + + (* broker -> tutor *) + | T_element "tutor_registered" -> Tutor_registered (get_attr root "id") + | T_element "tutor_unregistered" -> Tutor_unregistered (get_attr root "id") + | T_element "start_musing" -> + Start_musing (get_attr root "id", parse_state root#data) + | T_element "abort_musing" -> + Abort_musing (get_attr root "id", get_attr root "musing_id") + | T_element "thanks" -> Thanks (get_attr root "id", get_attr root "musing_id") + + | _ -> raise (No_element_found s) + +let msg_of_string s = + try + msg_of_string' s + with e -> raise (Parse_error (s, Printexc.to_string e)) + +let pp_state s = s (* TODO pretty print state *) +let pp_hint s = s (* TODO pretty print hint *) +let pp_hint_type s = s (* TODO pretty print hint_type *) +let pp_tutor_dscs = + List.fold_left + (fun s (id, dsc) -> + sprintf "%s%s" s id dsc) + "" +let pp_tutor_ids = + List.fold_left (fun s id -> sprintf "%s" s id) "" + +let string_of_msg = function + | Exception (name, value) -> + sprintf "%s" name value + | Register_client (id, url) -> + sprintf "" id url + | Unregister_client id -> sprintf "" id + | List_tutors id -> sprintf "" id + | Subscribe (id, tutor_ids) -> + sprintf "%s" + id (pp_tutor_ids tutor_ids) + | State_change (id, state) -> + sprintf "%s" + id (pp_state state) + | Register_tutor (id, url, hint_type, dsc) -> + sprintf +" +%s +%s +" + id url (pp_hint_type hint_type) dsc + | Unregister_tutor id -> sprintf "" id + | Musing_started (id, musing_id) -> + sprintf "" id musing_id + | Musing_aborted (id, musing_id) -> + sprintf "" id musing_id + | Musing_completed (id, musing_id, result) -> + sprintf + "%s" + id musing_id + (match result with + | Sorry -> "" + | Eureka s -> sprintf "%s" s) + | Client_registered id -> sprintf "" id + | Client_unregistered id -> sprintf "" id + | Tutor_list (id, tutor_dscs) -> + sprintf "%s" + id (pp_tutor_dscs tutor_dscs) + | Subscribed (id, tutor_ids) -> + sprintf "%s" + id (pp_tutor_ids tutor_ids) + | State_accepted (id, stop_ids, start_ids) -> + sprintf +" +%s +%s +" + id + (String.concat "" + (List.map (fun id -> sprintf "" id) stop_ids)) + (String.concat "" + (List.map (fun id -> sprintf "" id) start_ids)) + | Hint (id, hint) -> sprintf "%s" id (pp_hint hint) + | Tutor_registered id -> sprintf "" id + | Tutor_unregistered id -> sprintf "" id + | Start_musing (id, state) -> + sprintf "%s" id (pp_state state) + | Abort_musing (id, musing_id) -> + sprintf "" id musing_id + | Thanks (id, musing_id) -> + sprintf "" id musing_id + diff --git a/helm/hbugs/common/hbugs_messages.mli b/helm/hbugs/common/hbugs_messages.mli new file mode 100644 index 000000000..a11ff654b --- /dev/null +++ b/helm/hbugs/common/hbugs_messages.mli @@ -0,0 +1,31 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open Hbugs_types;; + +val msg_of_string: string -> message +val string_of_msg: message -> string + diff --git a/helm/hbugs/common/hbugs_misc.ml b/helm/hbugs/common/hbugs_misc.ml new file mode 100644 index 000000000..30f460815 --- /dev/null +++ b/helm/hbugs/common/hbugs_misc.ml @@ -0,0 +1,95 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open Printf;; + +let body_sep_RE = Pcre.regexp "\r\n\r\n";; +let url_scheme_RE = Pcre.regexp ~flags:[`CASELESS] "http://";; +let url_RE = Pcre.regexp "^([\\w.]+)(:(\\d+))?(/.*)?$";; +let parse_url url = + try + let subs = Pcre.extract ~rex:url_RE (Pcre.replace ~rex:url_scheme_RE url) in + (subs.(1), + (if subs.(2) = "" then 80 else int_of_string subs.(3)), + (if subs.(4) = "" then "/" else subs.(4))) + with exc -> + failwith + (sprintf "Can't parse url: %s (exception: %s)" + url (Printexc.to_string exc)) +;; +let get_body answer = + match Pcre.split ~rex:body_sep_RE answer with + | [_; body] -> body + | _ -> failwith "Invalid response received: can't parse response's body" +;; + +let init_socket addr port = + let inet_addr = (Unix.gethostbyname addr).Unix.h_addr_list.(0) in + let sockaddr = Unix.ADDR_INET (inet_addr, port) in + let suck = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in + Unix.connect suck sockaddr; + let outchan = Unix.out_channel_of_descr suck in + let inchan = Unix.in_channel_of_descr suck in + (inchan, outchan) +;; +let rec retrieve inchan buf = + Buffer.add_string buf (input_line inchan ^ "\n"); + retrieve inchan buf +;; + +let http_get url = + let (address, port, path) = parse_url url in + let (inchan, outchan) = init_socket address port in + output_string outchan (sprintf "GET %s HTTP/1.0\r\n\r\n" path); + flush outchan; + let buf = Buffer.create 1023 in + try + retrieve inchan buf + with End_of_file -> get_body (Buffer.contents buf) +;; + +let http_post ?(body = "") url = + let (address, port, path) = parse_url url in + let (inchan, outchan) = init_socket address port in + output_string outchan (sprintf "POST %s HTTP/1.0\r\n" path); + output_string outchan (sprintf "Content-Length: %d\r\n" (String.length body)); + output_string outchan "\r\n"; + output_string outchan body; + flush outchan; + let buf = Buffer.create 1023 in + try + retrieve inchan buf + with End_of_file -> get_body (Buffer.contents buf) +;; + +let rec hashtbl_remove_all tbl key = + if Hashtbl.mem tbl key then begin + Hashtbl.remove tbl key; + hashtbl_remove_all tbl key + end else + () +;; + diff --git a/helm/hbugs/common/hbugs_misc.mli b/helm/hbugs/common/hbugs_misc.mli new file mode 100644 index 000000000..991c9fa26 --- /dev/null +++ b/helm/hbugs/common/hbugs_misc.mli @@ -0,0 +1,34 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + (* HTTP GET request for a given url, return http response's body *) +val http_get: string -> string + (* HTTP POST request for a given url, return http response's body, body + argument, if specified, is sent as body along with request *) +val http_post: ?body:string -> string -> string + +val hashtbl_remove_all: ('a, 'b) Hashtbl.t -> 'a -> unit + diff --git a/helm/hbugs/common/hbugs_types.ml b/helm/hbugs/common/hbugs_types.ml new file mode 100644 index 000000000..0e580886b --- /dev/null +++ b/helm/hbugs/common/hbugs_types.ml @@ -0,0 +1,82 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type broker_id = string +type client_id = string +type musing_id = string +type tutor_id = string +type tutor_dsc = tutor_id * string (* tutor id, tutor description *) + +type state = string (* TODO stato del proof assistant *) + +type hint = string (* TODO consiglio per l'utente *) +type hint_type = string (* TODO consiglio per l'utente *) + +type musing_result = + | Eureka of string (* extra information, if any, parsed depending + on tutor's hint_type *) + | Sorry + + (* for each message, first component is an ID that identify the sender *) +type message = + + (* general purpose *) + | Exception of string * string (* name, value *) + + (* client -> broker *) + | Register_client of client_id * string (* client id, client url *) + | Unregister_client of client_id (* client id *) + | List_tutors of client_id (* client_id *) + | Subscribe of client_id * tutor_id list (* client id, tutor id list *) + | State_change of client_id * state (* client_id, new state *) + + (* tutor -> broker *) + | Register_tutor of tutor_id * string * hint_type * string + (* tutor id, tutor url, hint type, + tutor description *) + | Unregister_tutor of tutor_id (* tutor id *) + | Musing_started of tutor_id * musing_id (* tutor id, musing id *) + | Musing_aborted of tutor_id * musing_id (* tutor id, musing id *) + | Musing_completed of tutor_id * musing_id * musing_result + (* tutor id, musing id, result *) + + (* broker -> client *) + | Client_registered of broker_id (* broker id *) + | Client_unregistered of broker_id (* broker id *) + | Tutor_list of broker_id * tutor_dsc list (* broker id, tutor list *) + | Subscribed of broker_id * tutor_id list (* broker id, tutor list *) + | State_accepted of broker_id * musing_id list * musing_id list + (* broker id, stopped musing ids, + started musing ids *) + | Hint of broker_id * hint (* broker id, hint *) + + (* broker -> tutor *) + | Tutor_registered of broker_id (* broker id *) + | Tutor_unregistered of broker_id (* broker id *) + | Start_musing of broker_id * state (* broker id, state *) + | Abort_musing of broker_id * musing_id (* broker id, musing id *) + | Thanks of broker_id * musing_id (* broker id, musing id *) + diff --git a/helm/hbugs/common/threadSafe.ml b/helm/hbugs/common/threadSafe.ml new file mode 100644 index 000000000..9fa10d8d0 --- /dev/null +++ b/helm/hbugs/common/threadSafe.ml @@ -0,0 +1,94 @@ +(* + * Copyright (C) 2003, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let debug_print = let debug = false in fun s -> if debug then prerr_endline s;; + +class threadSafe = + object (self) + + val mutex = Mutex.create () + + (** condition variable: 'no readers is currently reading' *) + val noReaders = Condition.create () + + (** readers count *) + val mutable readersCount = 0 + + method private incrReadersCount = (* internal, not exported *) + self#doCritical (lazy ( + readersCount <- readersCount + 1 + )) + + method private decrReadersCount = (* internal, not exported *) + self#doCritical (lazy ( + if readersCount > 0 then readersCount <- readersCount - 1; + )) + + method private signalNoReaders = (* internal, not exported *) + self#doCritical (lazy ( + if readersCount = 0 then Condition.signal noReaders + )) + + method private doCritical: 'a. 'a lazy_t -> 'a = + fun action -> + debug_print ""; + (try + Mutex.lock mutex; + let res = Lazy.force action in + Mutex.unlock mutex; + debug_print ""; + res + with e -> + Mutex.unlock mutex; + raise e); + + method private doReader: 'a. 'a lazy_t -> 'a = + fun action -> + debug_print ""; + let cleanup () = + self#decrReadersCount; + self#signalNoReaders + in + self#incrReadersCount; + let res = (try Lazy.force action with e -> (cleanup (); raise e)) in + cleanup (); + debug_print ""; + res + + (* TODO may starve!!!! is what we want or not? *) + method private doWriter: 'a. 'a lazy_t -> 'a = + fun action -> + debug_print ""; + self#doCritical (lazy ( + while readersCount > 0 do + Condition.wait noReaders mutex + done; + let res = Lazy.force action in + debug_print ""; + res + )) + + end -- 2.39.2