From: Stefano Zacchiroli Date: Mon, 19 Apr 2004 12:04:26 +0000 (+0000) Subject: injected hbugs under ocaml/ dir X-Git-Tag: dead_dir_walking~42 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a21777bd2ac02fd346f168ead468405e4c300855;p=helm.git injected hbugs under ocaml/ dir --- diff --git a/helm/ocaml/hbugs/.depend b/helm/ocaml/hbugs/.depend new file mode 100644 index 000000000..f3f5f6261 --- /dev/null +++ b/helm/ocaml/hbugs/.depend @@ -0,0 +1,20 @@ +hbugs_common.cmi: hbugs_types.cmi +hbugs_id_generator.cmi: hbugs_types.cmi +hbugs_messages.cmi: hbugs_types.cmi +hbugs_client.cmi: hbugs_types.cmi +hbugs_misc.cmo: hbugs_misc.cmi +hbugs_misc.cmx: hbugs_misc.cmi +hbugs_common.cmo: hbugs_types.cmi hbugs_common.cmi +hbugs_common.cmx: hbugs_types.cmi hbugs_common.cmi +hbugs_id_generator.cmo: hbugs_id_generator.cmi +hbugs_id_generator.cmx: hbugs_id_generator.cmi +hbugs_messages.cmo: hbugs_misc.cmi hbugs_types.cmi hbugs_messages.cmi +hbugs_messages.cmx: hbugs_misc.cmx hbugs_types.cmi hbugs_messages.cmi +hbugs_client_gui.cmo: hbugs_client_gui.cmi +hbugs_client_gui.cmx: hbugs_client_gui.cmi +hbugs_client.cmo: hbugs_client_gui.cmi hbugs_common.cmi \ + hbugs_id_generator.cmi hbugs_messages.cmi hbugs_misc.cmi hbugs_types.cmi \ + hbugs_client.cmi +hbugs_client.cmx: hbugs_client_gui.cmx hbugs_common.cmx \ + hbugs_id_generator.cmx hbugs_messages.cmx hbugs_misc.cmx hbugs_types.cmi \ + hbugs_client.cmi diff --git a/helm/ocaml/hbugs/Makefile b/helm/ocaml/hbugs/Makefile new file mode 100644 index 000000000..af2d287ae --- /dev/null +++ b/helm/ocaml/hbugs/Makefile @@ -0,0 +1,100 @@ + +# Targets description: +# all (default) -> builds hbugs bytecode library hbugs.cma +# opt -> builds hbugs native library hbugs.cmxa +# daemons -> builds hbugs broker and tutors executables +# +# start -> starts up broker and tutors +# stop -> stop broker and tutors +# +# broker -> builds broker executable +# tutors -> builds tutors executables +# client -> builds hbugs client + +PACKAGE = hbugs +REQUIRES = \ + pcre lablgtk2.glade \ + helm-thread helm-xml helm-pxp helm-tactics + +IMPLEMENTATION_FILES = \ + hbugs_misc.ml \ + hbugs_common.ml \ + hbugs_id_generator.ml \ + hbugs_messages.ml \ + hbugs_client_gui.ml \ + hbugs_client.ml +INTERFACE_FILES = \ + hbugs_types.mli \ + $(patsubst %.ml, %.mli, $(IMPLEMENTATION_FILES)) + +include ../Makefile.common +include .tutors.ml +include .generated_tutors.ml + +.tutors.ml: + echo -n "TUTORS_ML = " > $@ + scripts/ls_tutors.ml | xargs >> $@ +.generated_tutors.ml: + echo -n "GENERATED_TUTORS_ML = " > $@ + scripts/ls_tutors.ml -auto | xargs >> $@ + +TUTORS = $(patsubst %.ml, %, $(TUTORS_ML)) +TUTORS_OPT = $(patsubst %, %.opt, $(TUTORS)) +GENERATED_TUTORS = $(patsubst %.ml, %, $(GENERATED_TUTORS_ML)) + +hbugs_client_gui.ml hbugs_client_gui.mli: hbugs_client_gui.glade + lablgladecc2 $< > hbugs_client_gui.ml + $(OCAMLC) -i hbugs_client_gui.ml > hbugs_client_gui.mli + +clean: clean_mains +.PHONY: clean_mains +clean_mains: + rm -f $(TUTORS) $(TUTORS_OPT) broker{,.opt} client{,.opt} +distclean: clean + rm -f $(GENERATED_TUTORS_ML) hbugs_client_gui.ml{,i} + rm -f .tutors.ml .generated_tutors.ml + +MAINS_DEPS = \ + hbugs_misc.cmo \ + hbugs_messages.cmo \ + hbugs_id_generator.cmo +TUTOR_DEPS = $(MAINS_DEPS) \ + hbugs_tutors.cmo +BROKER_DEPS = $(MAINS_DEPS) \ + hbugs_broker_registry.cmo +CLIENT_DEPS = $(MAINS_DEPS) \ + hbugs_client_gui.cmo \ + hbugs_common.cmo \ + hbugs_client.cmo +TUTOR_DEPS_OPT = $(patsubst %.cmo, %.cmx, $(TUTOR_DEPS)) +BROKER_DEPS_OPT = $(patsubst %.cmo, %.cmx, $(BROKER_DEPS)) +CLIENT_DEPS_OPT = $(patsubst %.cmo, %.cmx, $(CLIENT_DEPS)) +$(GENERATED_TUTORS_ML): scripts/build_tutors.ml data/tutors_index.xml data/hbugs_tutor.TPL.ml + scripts/build_tutors.ml +hbugs_tutors.cmo: hbugs_tutors.cmi +hbugs_broker_registry.cmo: hbugs_broker_registry.cmi +.PHONY: daemons +daemons: tutors broker +.PHONY: tutors +tutors: all $(TUTORS) +%_tutor: $(TUTOR_DEPS) %_tutor.ml + $(OCAMLC) -linkpkg -o $@ $^ +%_tutor.opt: $(TUTOR_DEPS_OPT) %_tutor.ml + $(OCAMLOPT) -linkpkg -o $@ $^ +broker: $(BROKER_DEPS) broker.ml + $(OCAMLC) -linkpkg -o $@ $^ +broker.opt: $(BROKER_DEPS_OPT) broker.ml + $(OCAMLOPT) -linkpkg -o $@ $^ +client: $(CLIENT_DEPS) client.ml + $(OCAMLC) -linkpkg -o $@ $^ +client.opt: $(CLIENT_DEPS_OPT) client.ml + $(OCAMLOPT) -linkpkg -o $@ $^ + +.PHONY: start stop +start: + scripts/brokerctl.sh start + scripts/sabba.sh start +stop: + scripts/brokerctl.sh stop + scripts/sabba.sh stop + diff --git a/helm/ocaml/hbugs/broker.ml b/helm/ocaml/hbugs/broker.ml new file mode 100644 index 000000000..2ff8b9834 --- /dev/null +++ b/helm/ocaml/hbugs/broker.ml @@ -0,0 +1,292 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_types;; +open Printf;; + +let debug = true ;; +let debug_print s = if debug then prerr_endline s ;; +Http_common.debug := false;; + +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 +;; +let usage_string = "HBugs Broker: usage string not yet written :-(";; + +exception Unexpected_msg of message;; + +let return_xml_msg body outchan = + Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan +;; +let parse_musing_id = function + | Musing_started (_, musing_id) -> + prerr_endline ("#### Started musing ID: " ^ musing_id); + musing_id + | Musing_aborted (_, musing_id) -> musing_id + | msg -> + prerr_endline (sprintf "Assertion failed, received msg: %s" + (Hbugs_messages.string_of_msg msg)); + assert false +;; + +let do_critical = + let mutex = Mutex.create () in + fun action -> + try +(* debug_print "Acquiring lock ..."; *) + Mutex.lock mutex; +(* debug_print "Lock Acquired!"; *) + let res = Lazy.force action in +(* debug_print "Releaseing lock ..."; *) + Mutex.unlock mutex; +(* debug_print "Lock released!"; *) + res + with e -> Mutex.unlock mutex; raise e +;; + + (* registries *) +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 registries = + [ (clients :> Hbugs_broker_registry.registry); + (tutors :> Hbugs_broker_registry.registry); + (musings :> Hbugs_broker_registry.registry) ] +in + +let my_own_id = Hbugs_id_generator.new_broker_id () in + + (* debugging: dump broker internal status, used by '/dump' method *) +let dump_registries () = + assert debug; + String.concat "\n" (List.map (fun o -> o#dump) registries) +in + +let handle_msg outchan msg = + (* messages from clients *) + (match msg with + + | Help -> + Hbugs_messages.respond_msg (Usage usage_string) outchan + | Register_client (client_id, client_url) -> do_critical (lazy ( + try + clients#register client_id client_url; + Hbugs_messages.respond_msg (Client_registered my_own_id) outchan + with Hbugs_broker_registry.Client_already_in id -> + Hbugs_messages.respond_exc "already_registered" id outchan + )) + | Unregister_client client_id -> do_critical (lazy ( + if clients#isAuthenticated client_id then begin + clients#unregister client_id; + Hbugs_messages.respond_msg (Client_unregistered my_own_id) outchan + end else + Hbugs_messages.respond_exc "forbidden" client_id outchan + )) + | List_tutors client_id -> do_critical (lazy ( + if clients#isAuthenticated client_id then begin + Hbugs_messages.respond_msg + (Tutor_list (my_own_id, tutors#index)) + outchan + end else + Hbugs_messages.respond_exc "forbidden" client_id outchan + )) + | Subscribe (client_id, tutor_ids) -> do_critical (lazy ( + if clients#isAuthenticated client_id then begin + if List.length tutor_ids <> 0 then begin (* at least one tutor id *) + if List.for_all tutors#exists tutor_ids then begin + clients#subscribe client_id tutor_ids; + Hbugs_messages.respond_msg + (Subscribed (my_own_id, tutor_ids)) outchan + end else (* required subscription to at least one unexistent tutor *) + let missing_tutors = + List.filter (fun id -> not (tutors#exists id)) tutor_ids + in + Hbugs_messages.respond_exc + "tutor_not_found" (String.concat " " missing_tutors) outchan + end else (* no tutor id specified *) + Hbugs_messages.respond_exc "no_tutor_specified" "" outchan + end else + Hbugs_messages.respond_exc "forbidden" client_id outchan + )) + | State_change (client_id, new_state) -> do_critical (lazy ( + if clients#isAuthenticated client_id then begin + let active_musings = musings#getByClientId client_id in + prerr_endline (sprintf "ACTIVE MUSINGS: %s" (String.concat ", " active_musings)); + if List.length active_musings = 0 then + prerr_endline ("No active musings for client " ^ client_id); + prerr_endline "CSC: State change!!!" ; + let stop_answers = + List.map (* collect Abort_musing message's responses *) + (fun id -> (* musing id *) + let tutor = snd (musings#getByMusingId id) in + Hbugs_messages.submit_req + ~url:(tutors#getUrl tutor) (Abort_musing (my_own_id, id))) + active_musings + in + let stopped_musing_ids = List.map parse_musing_id stop_answers in + List.iter musings#unregister active_musings; + (match new_state with + | Some new_state -> (* need to start new musings *) + let subscriptions = clients#getSubscription client_id in + if List.length subscriptions = 0 then + prerr_endline ("No subscriptions for client " ^ client_id); + let started_musing_ids = + List.map (* register new musings and collect their ids *) + (fun tutor_id -> + let res = + Hbugs_messages.submit_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) + subscriptions + in + Hbugs_messages.respond_msg + (State_accepted (my_own_id, stopped_musing_ids, started_musing_ids)) + outchan + | None -> (* no need to start new musings *) + Hbugs_messages.respond_msg + (State_accepted (my_own_id, stopped_musing_ids, [])) + outchan) + end else + Hbugs_messages.respond_exc "forbidden" client_id outchan + )) + + (* messages from tutors *) + + | Register_tutor (tutor_id, tutor_url, hint_type, dsc) -> do_critical (lazy ( + try + tutors#register tutor_id tutor_url hint_type dsc; + Hbugs_messages.respond_msg (Tutor_registered my_own_id) outchan + with Hbugs_broker_registry.Tutor_already_in id -> + Hbugs_messages.respond_exc "already_registered" id outchan + )) + | Unregister_tutor tutor_id -> do_critical (lazy ( + if tutors#isAuthenticated tutor_id then begin + tutors#unregister tutor_id; + Hbugs_messages.respond_msg (Tutor_unregistered my_own_id) outchan + end else + Hbugs_messages.respond_exc "forbidden" tutor_id outchan + )) + + | Musing_completed (tutor_id, musing_id, result) -> do_critical (lazy ( + if not (tutors#isAuthenticated tutor_id) then begin (* unauthorized *) + Hbugs_messages.respond_exc "forbidden" tutor_id outchan; + end else if not (musings#isActive musing_id) then begin (* too late *) + Hbugs_messages.respond_msg (Too_late (my_own_id, musing_id)) outchan; + end else begin (* all is ok: autorhized and on time *) + (match result with + | Sorry -> () + | Eureka hint -> + let client_url = + clients#getUrl (fst (musings#getByMusingId musing_id)) + in + let res = + Hbugs_messages.submit_req ~url:client_url (Hint (my_own_id, hint)) + in + (match res with + | Wow _ -> () (* ok: client is happy with our hint *) + | unexpected_msg -> + prerr_endline + (sprintf + "Warning: unexpected msg from client: %s\nExpected was: Wow" + (Hbugs_messages.string_of_msg msg)))); + Hbugs_messages.respond_msg (Thanks (my_own_id, musing_id)) outchan; + musings#unregister musing_id + end + )) + + | msg -> (* unexpected message *) + debug_print "Unknown message!"; + Hbugs_messages.respond_exc + "unexpected_msg" (Hbugs_messages.string_of_msg msg) outchan) +in +(* (* DEBUGGING wrapper around 'handle_msg' *) +let handle_msg outchan = + if debug then + (fun msg -> (* filter handle_msg through a function which dumps input + messages *) + debug_print (Hbugs_messages.string_of_msg msg); + handle_msg outchan msg) + else + handle_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" -> + let msg = Hbugs_messages.msg_of_string req#body in + handle_msg outchan msg + | "/dump" -> + if debug then + Http_daemon.respond ~body:(dump_registries ()) outchan + else + Http_daemon.respond_error ~code:400 outchan + | _ -> Http_daemon.respond_error ~code:400 outchan); + debug_print "Done!\n" + with + | Http_types.Param_not_found attr_name -> + Hbugs_messages.respond_exc "missing_parameter" attr_name outchan + | exc -> + Hbugs_messages.respond_exc + "uncaught_exception" (Printexc.to_string exc) outchan +in + + (* thread who cleans up ancient client/tutor/musing registrations *) +let ragman () = + let delay = 3600.0 in (* 1 hour delay *) + while true do + Thread.delay delay; + List.iter (fun o -> o#purge) registries + done +in + + (* start daemon *) +printf "Listening on port %d ...\n" port; +flush stdout; +ignore (Thread.create ragman ()); +Http_daemon.start' ~port ~mode:`Thread callback + diff --git a/helm/ocaml/hbugs/client.ml b/helm/ocaml/hbugs/client.ml new file mode 100644 index 000000000..85972ace3 --- /dev/null +++ b/helm/ocaml/hbugs/client.ml @@ -0,0 +1,44 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_common;; +open Printf;; + +let client = + new Hbugs_client.hbugsClient + ~use_hint_callback: + (fun hint -> + prerr_endline (sprintf "Using hint: %s" (string_of_hint hint))) + ~describe_hint_callback: + (fun hint -> + prerr_endline (sprintf "Describing hint: %s" (string_of_hint hint))) + () +in +client#show (); +GtkThread.main () + diff --git a/helm/ocaml/hbugs/data/.cvsignore b/helm/ocaml/hbugs/data/.cvsignore new file mode 100644 index 000000000..1fa56db7a --- /dev/null +++ b/helm/ocaml/hbugs/data/.cvsignore @@ -0,0 +1 @@ +*.environment diff --git a/helm/ocaml/hbugs/data/hbugs_tutor.TPL.ml b/helm/ocaml/hbugs/data/hbugs_tutor.TPL.ml new file mode 100644 index 000000000..947e351c7 --- /dev/null +++ b/helm/ocaml/hbugs/data/hbugs_tutor.TPL.ml @@ -0,0 +1,42 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +module TutorDescription = + struct + let addr = "@ADDR@" + let port = @PORT@ + let tactic = @TACTIC@ + let hint = @HINT@ + let hint_type = "@HINT_TYPE@" + let description = "@DESCRIPTION@" + let environment_file = "@ENVIRONMENT_FILE@" + end +;; +module Tutor = Hbugs_tutors.BuildTutor (TutorDescription) ;; +Tutor.start () ;; + diff --git a/helm/ocaml/hbugs/data/tutors_index.xml b/helm/ocaml/hbugs/data/tutors_index.xml new file mode 100644 index 000000000..bd4baad45 --- /dev/null +++ b/helm/ocaml/hbugs/data/tutors_index.xml @@ -0,0 +1,140 @@ + + + + + + + + + 127.0.0.1 + 50001 + Ring.ring_tac + Hbugs_types.Use_ring_Luke + Use Ring Luke + Ring tutor + ring.environment + + + 127.0.0.1 + 50002 + FourierR.fourier_tac + Hbugs_types.Use_fourier_Luke + Use Fourier Luke + Fourier tutor + fourier.environment + + + 127.0.0.1 + 50003 + EqualityTactics.reflexivity_tac + Hbugs_types.Use_reflexivity_Luke + Use Reflexivity Luke + Reflexivity tutor + reflexivity.environment + + + 127.0.0.1 + 50004 + EqualityTactics.symmetry_tac + Hbugs_types.Use_symmetry_Luke + Use Symmetry Luke + Symmetry tutor + symmetry.environment + + + 127.0.0.1 + 50005 + VariousTactics.assumption_tac + Hbugs_types.Use_assumption_Luke + Use Assumption Luke + Assumption tutor + assumption.environment + + + 127.0.0.1 + 50006 + NegationTactics.contradiction_tac + Hbugs_types.Use_contradiction_Luke + Use Contradiction Luke + Contradiction tutor + contradiction.environment + + + 127.0.0.1 + 50007 + IntroductionTactics.exists_tac + Hbugs_types.Use_exists_Luke + Use Exists Luke + Exists tutor + exists.environment + + + 127.0.0.1 + 50008 + IntroductionTactics.split_tac + Hbugs_types.Use_split_Luke + Use Split Luke + Split tutor + split.environment + + + 127.0.0.1 + 50009 + IntroductionTactics.left_tac + Hbugs_types.Use_left_Luke + Use Left Luke + Left tutor + left.environment + + + 127.0.0.1 + 50010 + IntroductionTactics.right_tac + Hbugs_types.Use_right_Luke + Use Right Luke + Right tutor + right.environment + + + + 127.0.0.1 + 50011 + PrimitiveTactics.apply_tac + Hbugs_types.Use_apply_Luke + Use Apply Luke (with argument) + Search pattern apply tutor + search_pattern_apply.environment + + + diff --git a/helm/ocaml/hbugs/doc/.cvsignore b/helm/ocaml/hbugs/doc/.cvsignore new file mode 100644 index 000000000..743328ec1 --- /dev/null +++ b/helm/ocaml/hbugs/doc/.cvsignore @@ -0,0 +1 @@ +*.dia~ diff --git a/helm/ocaml/hbugs/doc/hbugs.dia b/helm/ocaml/hbugs/doc/hbugs.dia new file mode 100644 index 000000000..b1c4e64e2 Binary files /dev/null and b/helm/ocaml/hbugs/doc/hbugs.dia differ diff --git a/helm/ocaml/hbugs/hbugs_broker_registry.ml b/helm/ocaml/hbugs/hbugs_broker_registry.ml new file mode 100644 index 000000000..879d746ac --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_broker_registry.ml @@ -0,0 +1,315 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_misc;; +open Hbugs_types;; +open Printf;; + +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 type registry = + object + method dump: string + method purge: unit + end + +let expire_time = 1800. (* 30 minutes *) + +class clients = + object (self) + + inherit ThreadSafe.threadSafe +(* + (* *) + method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act + method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act + method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act + (* *) +*) + + val timetable: (client_id, float) Hashtbl.t = Hashtbl.create 17 + val urls: (client_id, string) Hashtbl.t = Hashtbl.create 17 + val subscriptions: (client_id, tutor_id list) Hashtbl.t = Hashtbl.create 17 + + (** INVARIANT: each client registered has an entry in 'urls' hash table + _and_ in 'subscriptions hash table even if it hasn't yet invoked + 'subscribe' method *) + + 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 []; + Hashtbl.add timetable id (Unix.time ()) + end + )) + method private remove id = + Hashtbl.remove urls id; + Hashtbl.remove subscriptions id; + Hashtbl.remove timetable id + method unregister id = self#doWriter (lazy ( + if Hashtbl.mem urls id then + self#remove id + 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) + )) + + method dump = self#doReader (lazy ( + "\n" ^ + (Hashtbl.fold + (fun id url dump -> + (dump ^ + (sprintf "\n" id url) ^ + "\n" ^ + (String.concat "\n" (* id's subscriptions *) + (List.map + (fun tutor_id -> sprintf "\n" tutor_id) + (Hashtbl.find subscriptions id))) ^ + "\n\n")) + urls "") ^ + "" + )) + method purge = self#doWriter (lazy ( + let now = Unix.time () in + Hashtbl.iter + (fun id birthday -> + if now -. birthday > expire_time then + self#remove id) + timetable + )) + + end + +class tutors = + object (self) + + inherit ThreadSafe.threadSafe +(* + (* *) + method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act + method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act + method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act + (* *) +*) + + val timetable: (tutor_id, float) Hashtbl.t = Hashtbl.create 17 + 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 begin + Hashtbl.add tbl id (url, hint_type, dsc); + Hashtbl.add timetable id (Unix.time ()) + end + )) + method private remove id = + Hashtbl.remove tbl id; + Hashtbl.remove timetable id + method unregister id = self#doWriter (lazy ( + if Hashtbl.mem tbl id then + self#remove 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 [] + )) + + method dump = self#doReader (lazy ( + "\n" ^ + (Hashtbl.fold + (fun id (url, hint_type, dsc) dump -> + dump ^ + (sprintf +"\n%s\n%s\n" + id url hint_type dsc)) + tbl "") ^ + "" + )) + method purge = self#doWriter (lazy ( + let now = Unix.time () in + Hashtbl.iter + (fun id birthday -> + if now -. birthday > expire_time then + self#remove id) + timetable + )) + + end + +class musings = + object (self) + + inherit ThreadSafe.threadSafe +(* + (* *) + method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act + method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act + method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act + (* *) +*) + + val timetable: (musing_id, float) Hashtbl.t = Hashtbl.create 17 + val musings: (musing_id, client_id * tutor_id) Hashtbl.t = Hashtbl.create 17 + val clients: (client_id, musing_id list) Hashtbl.t = Hashtbl.create 17 + val tutors: (tutor_id, musing_id list) Hashtbl.t = Hashtbl.create 17 + + (** INVARIANT: each registered musing has + an entry in 'musings' table, an entry in 'clients' (i.e. one of the + musings for client_id is musing_id) table, an entry in 'tutors' table + (i.e. one of the musings for tutor_id is musing_id) and an entry in + 'timetable' table *) + + + 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); + (* now add this musing as the first one of musings list for client and + tutor *) + Hashtbl.replace clients client_id + (musing_id :: + (try Hashtbl.find clients client_id with Not_found -> [])); + Hashtbl.replace tutors tutor_id + (musing_id :: + (try Hashtbl.find tutors tutor_id with Not_found -> [])); + Hashtbl.add timetable musing_id (Unix.time ()) + end + )) + method private remove id = + (* ASSUMPTION: this method is invoked under a 'writer' lock *) + let (client_id, tutor_id) = self#getByMusingId' id in + Hashtbl.remove musings id; + (* now remove this musing from the list of musings for client and tutor + *) + Hashtbl.replace clients client_id + (List.filter ((<>) id) + (try Hashtbl.find clients client_id with Not_found -> [])); + Hashtbl.replace tutors tutor_id + (List.filter ((<>) id) + (try Hashtbl.find tutors tutor_id with Not_found -> [])); + Hashtbl.remove timetable id + method unregister id = self#doWriter (lazy ( + if Hashtbl.mem musings id then + self#remove id + )) + method private getByMusingId' id = + (* ASSUMPTION: this method is invoked under a 'reader' lock *) + try + Hashtbl.find musings id + with Not_found -> raise (Musing_not_found id) + method getByMusingId id = self#doReader (lazy ( + self#getByMusingId' id + )) + method getByClientId id = self#doReader (lazy ( + try + Hashtbl.find clients id + with Not_found -> [] + )) + method getByTutorId id = self#doReader (lazy ( + try + Hashtbl.find tutors id + with Not_found -> [] + )) + method isActive id = self#doReader (lazy ( + Hashtbl.mem musings id + )) + + method dump = self#doReader (lazy ( + "\n" ^ + (Hashtbl.fold + (fun mid (cid, tid) dump -> + dump ^ + (sprintf "\n" + mid cid tid)) + musings "") ^ + "" + )) + method purge = self#doWriter (lazy ( + let now = Unix.time () in + Hashtbl.iter + (fun id birthday -> + if now -. birthday > expire_time then + self#remove id) + timetable + )) + + end + diff --git a/helm/ocaml/hbugs/hbugs_broker_registry.mli b/helm/ocaml/hbugs/hbugs_broker_registry.mli new file mode 100644 index 000000000..ece9e07cf --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_broker_registry.mli @@ -0,0 +1,87 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +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 type registry = + object + method dump: string + method purge: unit + end + +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 + + method dump: string + method purge: unit + 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 + + method dump: string + method purge: unit + 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 + method isActive: musing_id -> bool + + method dump: string + method purge: unit + end + diff --git a/helm/ocaml/hbugs/hbugs_client.ml b/helm/ocaml/hbugs/hbugs_client.ml new file mode 100644 index 000000000..4613dbf0d --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_client.ml @@ -0,0 +1,524 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_common;; +open Hbugs_types;; +open Printf;; + +exception Invalid_URL of string;; + +let do_nothing _ = ();; + +module SmartHbugs_client_gui = + struct + class ['a] oneColumnCList gtree_view ~column_type ~column_title + = + let obj = + ((Gobject.unsafe_cast gtree_view#as_widget) : Gtk.tree_view Gtk.obj) in + let columns = new GTree.column_list in + let col = columns#add column_type in + let vcol = GTree.view_column ~title:column_title () + ~renderer:(GTree.cell_renderer_text[], ["text",col]) in + let store = GTree.list_store columns in + object(self) + inherit GTree.view obj + method clear = store#clear + method append (v : 'a) = + let row = store#append () in + store#set ~row ~column:col v; + method column = col + initializer + self#set_model (Some (store :> GTree.model)) ; + ignore (self#append_column vcol) + end + + class ['a,'b] twoColumnsCList gtree_view ~column1_type ~column2_type + ~column1_title ~column2_title + = + let obj = + ((Gobject.unsafe_cast gtree_view#as_widget) : Gtk.tree_view Gtk.obj) in + let columns = new GTree.column_list in + let col1 = columns#add column1_type in + let vcol1 = GTree.view_column ~title:column1_title () + ~renderer:(GTree.cell_renderer_text[], ["text",col1]) in + let col2 = columns#add column2_type in + let vcol2 = GTree.view_column ~title:column2_title () + ~renderer:(GTree.cell_renderer_text[], ["text",col2]) in + let store = GTree.list_store columns in + object(self) + inherit GTree.view obj + method clear = store#clear + method append (v1 : 'a) (v2 : 'b) = + let row = store#append () in + store#set ~row ~column:col1 v1; + store#set ~row ~column:col2 v2 + method column1 = col1 + method column2 = col2 + initializer + self#set_model (Some (store :> GTree.model)) ; + ignore (self#append_column vcol1) ; + ignore (self#append_column vcol2) ; + end + + class subscribeWindow () = + object(self) + inherit Hbugs_client_gui.subscribeWindow () + val mutable tutorsSmartCList = None + method tutorsSmartCList = + match tutorsSmartCList with + None -> assert false + | Some w -> w + initializer + tutorsSmartCList <- + Some + (new twoColumnsCList self#tutorsCList + ~column1_type:Gobject.Data.string ~column2_type:Gobject.Data.string + ~column1_title:"Id" ~column2_title:"Description") + end + + class hbugsMainWindow () = + object(self) + inherit Hbugs_client_gui.hbugsMainWindow () + val mutable subscriptionSmartCList = None + val mutable hintsSmartCList = None + method subscriptionSmartCList = + match subscriptionSmartCList with + None -> assert false + | Some w -> w + method hintsSmartCList = + match hintsSmartCList with + None -> assert false + | Some w -> w + initializer + subscriptionSmartCList <- + Some + (new oneColumnCList self#subscriptionCList + ~column_type:Gobject.Data.string ~column_title:"Description") + initializer + hintsSmartCList <- + Some + (new oneColumnCList self#hintsCList + ~column_type:Gobject.Data.string ~column_title:"Description") + end + + end +;; + +class hbugsClient + ?(use_hint_callback: hint -> unit = do_nothing) + ?(describe_hint_callback: hint -> unit = do_nothing) + ?(destroy_callback: unit -> unit = do_nothing) + () + = + + let http_url_RE = Pcre.regexp "^(http://)?(.*):(\\d+)" in + let port_of_http_url url = + try + let subs = Pcre.extract ~rex:http_url_RE url in + int_of_string subs.(3) + with e -> raise (Invalid_URL url) + in + + object (self) + + val mainWindow = new SmartHbugs_client_gui.hbugsMainWindow () + val subscribeWindow = new SmartHbugs_client_gui.subscribeWindow () + val messageDialog = new Hbugs_client_gui.messageDialog () + val myOwnId = Hbugs_id_generator.new_client_id () + val mutable use_hint_callback = use_hint_callback + val mutable myOwnUrl = "localhost:49082" + val mutable brokerUrl = "localhost:49081" + val mutable brokerId: broker_id option = None + (* all available tutors, saved last time a List_tutors message was sent to + broker *) + val mutable availableTutors: tutor_dsc list = [] + val mutable statusContext = None + val mutable subscribeWindowStatusContext = None + val mutable debug = false (* enable/disable debugging buttons *) + val mutable hints = [] (* actually available hints *) + + initializer + self#initGui; + self#startLocalHttpDaemon (); + self#testLocalHttpDaemon (); + self#testBroker (); + self#registerToBroker (); + self#reconfigDebuggingButtons + + method show = mainWindow#hbugsMainWindow#show + method hide = mainWindow#hbugsMainWindow#misc#hide + + method setUseHintCallback callback = + use_hint_callback <- callback + + method private debugButtons = + List.map + (fun (b: GButton.button) -> new GObj.misc_ops b#as_widget) + [ mainWindow#startLocalHttpDaemonButton; + mainWindow#testLocalHttpDaemonButton; mainWindow#testBrokerButton ] + + method private initGui = + + (* GUI: main window *) + + (* ignore delete events so that hbugs window is closable only using + menu; on destroy (e.g. while quitting gTopLevel) self#quit is invoked + *) + + ignore (mainWindow#hbugsMainWindow#event#connect#delete (fun _ -> true)); + ignore (mainWindow#hbugsMainWindow#event#connect#destroy + (fun _ -> self#quit (); false)); + + (* GUI main window's menu *) + mainWindow#toggleDebuggingMenuItem#set_active debug; + ignore (mainWindow#toggleDebuggingMenuItem#connect#toggled + self#toggleDebug); + + (* GUI: local HTTP daemon settings *) + ignore (mainWindow#clientUrlEntry#connect#changed + (fun _ -> myOwnUrl <- mainWindow#clientUrlEntry#text)); + mainWindow#clientUrlEntry#set_text myOwnUrl; + ignore (mainWindow#startLocalHttpDaemonButton#connect#clicked + self#startLocalHttpDaemon); + ignore (mainWindow#testLocalHttpDaemonButton#connect#clicked + self#testLocalHttpDaemon); + + (* GUI: broker choice *) + ignore (mainWindow#brokerUrlEntry#connect#changed + (fun _ -> brokerUrl <- mainWindow#brokerUrlEntry#text)); + mainWindow#brokerUrlEntry#set_text brokerUrl; + ignore (mainWindow#testBrokerButton#connect#clicked self#testBroker); + mainWindow#clientIdLabel#set_text myOwnId; + + (* GUI: client registration *) + ignore (mainWindow#registerClientButton#connect#clicked + self#registerToBroker); + + (* GUI: subscriptions *) + ignore (mainWindow#showSubscriptionWindowButton#connect#clicked + (fun () -> + self#listTutors (); + subscribeWindow#subscribeWindow#show ())); + + let get_selected_row_index () = + match mainWindow#hintsCList#selection#get_selected_rows with + [path] -> + (match GTree.Path.get_indices path with + [|n|] -> n + | _ -> assert false) + | _ -> assert false + in + (* GUI: hints list *) + ignore ( + let event_ops = new GObj.event_ops mainWindow#hintsCList#as_widget in + event_ops#connect#button_press + (fun event -> + if GdkEvent.get_type event = `TWO_BUTTON_PRESS then + use_hint_callback (self#hint (get_selected_row_index ())) ; + false)); + + ignore (mainWindow#hintsCList#selection#connect#changed + (fun () -> + describe_hint_callback (self#hint (get_selected_row_index ())))) ; + + (* GUI: main status bar *) + let ctxt = mainWindow#mainWindowStatusBar#new_context "0" in + statusContext <- Some ctxt; + ignore (ctxt#push "Ready"); + + (* GUI: subscription window *) + subscribeWindow#tutorsCList#selection#set_mode `MULTIPLE; + ignore (subscribeWindow#subscribeWindow#event#connect#delete + (fun _ -> subscribeWindow#subscribeWindow#misc#hide (); true)); + ignore (subscribeWindow#listTutorsButton#connect#clicked self#listTutors); + ignore (subscribeWindow#subscribeButton#connect#clicked + self#subscribeSelected); + ignore (subscribeWindow#subscribeAllButton#connect#clicked + self#subscribeAll); + (subscribeWindow#tutorsCList#get_column 0)#set_visible false; + let ctxt = subscribeWindow#subscribeWindowStatusBar#new_context "0" in + subscribeWindowStatusContext <- Some ctxt; + ignore (ctxt#push "Ready"); + + (* GUI: message dialog *) + ignore (messageDialog#messageDialog#event#connect#delete + (fun _ -> messageDialog#messageDialog#misc#hide (); true)); + ignore (messageDialog#okDialogButton#connect#clicked + (fun _ -> messageDialog#messageDialog#misc#hide ())) + + (* accessory methods *) + + (** pop up a (modal) dialog window showing msg to the user *) + method private showDialog msg = + messageDialog#dialogLabel#set_text msg; + messageDialog#messageDialog#show () + (** use showDialog to display an hbugs message to the user *) + method private showMsgInDialog msg = + self#showDialog (Hbugs_messages.string_of_msg msg) + + (** create a new thread which sends msg to broker, wait for an answer and + invoke callback passing response message as argument *) + method private sendReq ?(wait = false) ~msg callback = + let thread () = + try + callback (Hbugs_messages.submit_req ~url:(brokerUrl ^ "/act") msg) + with + | (Hbugs_messages.Parse_error (subj, reason)) as e -> + self#showDialog + (sprintf +"Parse_error, unable to fullfill request. Details follow. +Request: %s +Error: %s" + (Hbugs_messages.string_of_msg msg) (Printexc.to_string e)); + | (Unix.Unix_error _) as e -> + self#showDialog + (sprintf +"Can't connect to HBugs Broker +Url: %s +Error: %s" + brokerUrl (Printexc.to_string e)) + | e -> + self#showDialog + (sprintf "hbugsClient#sendReq: Uncaught exception: %s" + (Printexc.to_string e)) + in + let th = Thread.create thread () in + if wait then + Thread.join th + else () + + (** check if a broker is authenticated using its broker_id + [ Background: during client registration, client save broker_id of its + broker, further messages from broker are accepted only if they carry the + same broker id ] *) + method private isAuthenticated id = + match brokerId with + | None -> false + | Some broker_id -> (id = broker_id) + + (* actions *) + + method private startLocalHttpDaemon = + (* flatten an hint tree to an hint list *) + let rec flatten_hint = function + | Hints hints -> List.concat (List.map flatten_hint hints) + | hint -> [hint] + in + fun () -> + let callback req outchan = + try + (match Hbugs_messages.msg_of_string req#body with + | Help -> + Hbugs_messages.respond_msg + (Usage "Local Http Daemon up and running!") outchan + | Hint (broker_id, hint) -> + if self#isAuthenticated broker_id then begin + let received_hints = flatten_hint hint in + List.iter + (fun h -> + (match h with Hints _ -> assert false | _ -> ()); + ignore(mainWindow#hintsSmartCList#append(string_of_hint h))) + received_hints; + hints <- hints @ received_hints; + Hbugs_messages.respond_msg (Wow myOwnId) outchan + end else (* msg from unauthorized broker *) + Hbugs_messages.respond_exc "forbidden" broker_id outchan + | msg -> + Hbugs_messages.respond_exc + "unexpected_msg" (Hbugs_messages.string_of_msg msg) outchan) + with (Hbugs_messages.Parse_error _) as e -> + Hbugs_messages.respond_exc + "parse_error" (Printexc.to_string e) outchan + in + let addr = "0.0.0.0" in (* TODO actually user specified "My URL" is used + only as a value to be sent to broker, local HTTP + daemon will listen on "0.0.0.0", port is parsed + from My URL though *) + let httpDaemonThread () = + try + Http_daemon.start' + ~addr ~port:(port_of_http_url myOwnUrl) ~mode:`Single callback + with + | Invalid_URL url -> self#showDialog (sprintf "Invalid URL: \"%s\"" url) + | e -> + self#showDialog (sprintf "Can't start local HTTP daemon: %s" + (Printexc.to_string e)) + in + ignore (Thread.create httpDaemonThread ()) + + method private testLocalHttpDaemon () = + try + let msg = + Hbugs_misc.http_post ~body:(Hbugs_messages.string_of_msg Help) + myOwnUrl + in + ignore msg +(* self#showDialog msg *) + with + | Hbugs_misc.Malformed_URL url -> + self#showDialog + (sprintf + "Handshake with local HTTP daemon failed, Invalid URL: \"%s\"" + url) + | Hbugs_misc.Malformed_HTTP_response res -> + self#showDialog + (sprintf + "Handshake with local HTTP daemon failed, can't parse HTTP response: \"%s\"" + res) + | (Unix.Unix_error _) as e -> + self#showDialog + (sprintf + "Handshake with local HTTP daemon failed, can't connect: \"%s\"" + (Printexc.to_string e)) + + method private testBroker () = + self#sendReq ~msg:Help + (function + | Usage _ -> () + | unexpected_msg -> + self#showDialog + (sprintf + "Handshake with HBugs Broker failed, unexpected message:\n%s" + (Hbugs_messages.string_of_msg unexpected_msg))) + + method registerToBroker () = + (match brokerId with (* undo previous registration, if any *) + | Some id -> self#unregisterFromBroker () + | _ -> ()); + self#sendReq ~msg:(Register_client (myOwnId, myOwnUrl)) + (function + | Client_registered broker_id -> (brokerId <- Some broker_id) + | unexpected_msg -> + self#showDialog + (sprintf "Client NOT registered, unexpected message:\n%s" + (Hbugs_messages.string_of_msg unexpected_msg))) + + method unregisterFromBroker () = + self#sendReq ~wait:true ~msg:(Unregister_client myOwnId) + (function + | Client_unregistered _ -> (brokerId <- None) + | unexpected_msg -> ()) +(* + self#showDialog + (sprintf "Client NOT unregistered, unexpected message:\n%s" + (Hbugs_messages.string_of_msg unexpected_msg))) +*) + + method stateChange new_state = + mainWindow#hintsSmartCList#clear (); + hints <- []; + self#sendReq + ~msg:(State_change (myOwnId, new_state)) + (function + | State_accepted _ -> () + | unexpected_msg -> + self#showDialog + (sprintf "State NOT accepted by Hbugs, unexpected message:\n%s" + (Hbugs_messages.string_of_msg unexpected_msg))) + + method hint = List.nth hints + + method private listTutors () = + (* wait is set to true just to make sure that after invoking listTutors + "availableTutors" is correctly filled *) + self#sendReq ~wait:true ~msg:(List_tutors myOwnId) + (function + | Tutor_list (_, descriptions) -> + availableTutors <- (* sort accordingly to tutor description *) + List.sort (fun (a,b) (c,d) -> compare (b,a) (d,c)) descriptions; + subscribeWindow#tutorsSmartCList#clear (); + List.iter + (fun (id, dsc) -> + ignore (subscribeWindow#tutorsSmartCList#append id dsc)) + availableTutors + | unexpected_msg -> + self#showDialog + (sprintf "Can't list tutors, unexpected message:\n%s" + (Hbugs_messages.string_of_msg unexpected_msg))) + + (* low level used by subscribeSelected and subscribeAll *) + method private subscribe' tutors_id = + self#sendReq ~msg:(Subscribe (myOwnId, tutors_id)) + (function + | (Subscribed (_, subscribedTutors)) as msg -> + let sort = List.sort compare in + mainWindow#subscriptionSmartCList#clear (); + List.iter + (fun tutor_id -> + ignore + (mainWindow#subscriptionSmartCList#append + ( try + List.assoc tutor_id availableTutors + with Not_found -> assert false ))) + tutors_id; + subscribeWindow#subscribeWindow#misc#hide (); + if sort subscribedTutors <> sort tutors_id then + self#showDialog + (sprintf "Subscription mismatch\n: %s" + (Hbugs_messages.string_of_msg msg)) + | unexpected_msg -> + mainWindow#subscriptionSmartCList#clear (); + self#showDialog + (sprintf "Subscription FAILED, unexpected message:\n%s" + (Hbugs_messages.string_of_msg unexpected_msg))) + + method private subscribeSelected () = + let tutorsSmartCList = subscribeWindow#tutorsSmartCList in + let selectedTutors = + List.map + (fun p -> + tutorsSmartCList#model#get + ~row:(tutorsSmartCList#model#get_iter p) + ~column:tutorsSmartCList#column1) + tutorsSmartCList#selection#get_selected_rows + in + self#subscribe' selectedTutors + + method subscribeAll () = + self#listTutors (); (* this fills 'availableTutors' field *) + self#subscribe' (List.map fst availableTutors) + + method private quit () = + self#unregisterFromBroker (); + destroy_callback () + + (** enable/disable debugging *) + method private setDebug value = debug <- value + + method private reconfigDebuggingButtons = + List.iter (* debug value changed, reconfigure buttons *) + (fun (b: GObj.misc_ops) -> if debug then b#show () else b#hide ()) + self#debugButtons; + + method private toggleDebug () = + self#setDebug (not debug); + self#reconfigDebuggingButtons + + end +;; + diff --git a/helm/ocaml/hbugs/hbugs_client.mli b/helm/ocaml/hbugs/hbugs_client.mli new file mode 100644 index 000000000..0c2e93d80 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_client.mli @@ -0,0 +1,33 @@ + +open Hbugs_types + +exception Invalid_URL of string + + (* + @param use_hint_callback is called when the user double click on a hint + (default: do nothing) + @param describe_hint_callback is called when the user click on a hint + (default: do nothing) + *) +class hbugsClient : + ?use_hint_callback: (hint -> unit) -> + ?describe_hint_callback: (hint -> unit) -> + ?destroy_callback: (unit -> unit) -> + unit -> + object + + method show : unit -> unit + method hide : unit -> unit + + method setUseHintCallback : (hint -> unit) -> unit + method registerToBroker : unit -> unit + method unregisterFromBroker : unit -> unit + method subscribeAll : unit -> unit + + method stateChange : state option -> unit + + (** @return an hint by index *) + method hint : int -> hint + + end + diff --git a/helm/ocaml/hbugs/hbugs_client_gui.glade b/helm/ocaml/hbugs/hbugs_client_gui.glade new file mode 100644 index 000000000..f88a8c388 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_client_gui.glade @@ -0,0 +1,672 @@ + + + + + + + + Hbugs: your personal proof trainer! + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + + + + True + False + 0 + + + + + + + True + Tools + True + + + + True + + + + True + Debugging + True + False + + + + + + + + + 0 + False + False + + + + + + True + False + 2 + + + + True + My URL: + False + False + GTK_JUSTIFY_CENTER + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + Local HTTP daemon URL + True + False + True + 0 + + True + * + False + + + 0 + True + True + + + + + + True + Start the local HTTP daemon listening on the specified URL + True + Start! + True + GTK_RELIEF_NORMAL + + + 0 + False + False + + + + + + True + True + Test! + True + GTK_RELIEF_NORMAL + + + 0 + False + False + + + + + 0 + False + False + + + + + + True + False + 0 + + + + True + False + 2 + + + + True + Broker: + False + False + GTK_JUSTIFY_CENTER + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + HBugs broker URL + True + False + True + 0 + + True + * + False + + + 0 + True + True + + + + + + True + True + Test! + True + GTK_RELIEF_NORMAL + + + 0 + False + False + + + + + 0 + False + False + + + + + + True + False + 2 + + + + Client ID: + False + False + GTK_JUSTIFY_CENTER + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + True + True + + + + + + True + True + (Re)Register + True + GTK_RELIEF_NORMAL + + + 0 + False + False + + + + + 0 + False + False + + + + + 0 + False + True + + + + + + True + 0 + + + + 4 + True + 0 + 0.5 + GTK_SHADOW_ETCHED_IN + + + + True + False + 2 + + + + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + False + True + + + + + 0 + True + True + + + + + + True + + + + 0 + 0 + True + True + Subscribe ... + True + GTK_RELIEF_NORMAL + + + 0 + 0 + + + + + 0 + False + False + + + + + + + + True + Subscriptions + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + label_item + + + + + False + False + + + + + + 4 + True + 0 + 0.5 + GTK_SHADOW_ETCHED_IN + + + + True + False + 0 + + + + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + False + True + + + + + 0 + True + True + + + + + + + + True + Hints + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + label_item + + + + + True + True + + + + + 0 + True + True + + + + + + True + + + 0 + False + False + + + + + + + + Hbugs: subscribe ... + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + + + + True + False + 0 + + + + True + True + Refresh + True + GTK_RELIEF_NORMAL + + + 0 + False + False + + + + + + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + False + True + + + + + 0 + True + True + + + + + + True + False + 0 + + + + True + True + Subscribe to Selected + True + GTK_RELIEF_NORMAL + + + 0 + True + True + + + + + + True + True + Subscribe to All + True + GTK_RELIEF_NORMAL + + + 0 + True + True + + + + + 0 + False + False + + + + + + True + True + + + 0 + False + False + + + + + + + + Message + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + True + 220 + 150 + True + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + OK + True + GTK_RELIEF_NORMAL + 0 + + + + + 0 + False + True + GTK_PACK_END + + + + + + 5 + True + 1 + 1 + False + 0 + 0 + + + + True + + False + False + GTK_JUSTIFY_CENTER + True + False + 0.5 + 0.5 + 0 + 0 + + + 0 + 1 + 0 + 1 + + + + + 0 + True + True + + + + + + + diff --git a/helm/ocaml/hbugs/hbugs_common.ml b/helm/ocaml/hbugs/hbugs_common.ml new file mode 100644 index 000000000..3b19ceec0 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_common.ml @@ -0,0 +1,46 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_types;; +open Printf;; + +let rec string_of_hint = function + | Use_ring_Luke -> "Use Ring, Luke!" + | Use_fourier_Luke -> "Use Fourier, Luke!" + | Use_reflexivity_Luke -> "Use reflexivity, Luke!" + | Use_symmetry_Luke -> "Use symmetry, Luke!" + | Use_assumption_Luke -> "Use assumption, Luke!" + | Use_contradiction_Luke -> "Use contradiction, Luke!" + | Use_exists_Luke -> "Use exists, Luke!" + | Use_split_Luke -> "Use split, Luke!" + | Use_left_Luke -> "Use left, Luke!" + | Use_right_Luke -> "Use right, Luke!" + | Use_apply_Luke term -> sprintf "Apply %s, Luke!" term + | Hints hints -> String.concat "; " (List.map string_of_hint hints) +;; + diff --git a/helm/ocaml/hbugs/hbugs_common.mli b/helm/ocaml/hbugs/hbugs_common.mli new file mode 100644 index 000000000..2d51075f3 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_common.mli @@ -0,0 +1,32 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_types;; + +val string_of_hint: hint -> string + diff --git a/helm/ocaml/hbugs/hbugs_id_generator.ml b/helm/ocaml/hbugs/hbugs_id_generator.ml new file mode 100644 index 000000000..f535f4739 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_id_generator.ml @@ -0,0 +1,65 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +let _ = Random.self_init () + +let id_length = 32 +let min_ascii = 33 +let max_ascii = 126 + (* characters forbidden inside an XML attribute value. Well, '>' and ''' + aren't really forbidden, but are listed here ... just to be sure *) +let forbidden_chars = (* i.e. [ '"'; '&'; '\''; '<'; '>' ] *) + [ 34; 38; 39; 60; 62 ] (* assumption: is sorted! *) +let chars_range = max_ascii - min_ascii + 1 - (List.length forbidden_chars) + + (* return a random id char c such that + (min_ascii <= Char.code c) && + (Char.code c <= max_ascii) && + (not (List.mem (Char.code c) forbidden_chars)) + *) +let random_id_char () = + let rec nth_char ascii shifts = function + | [] -> Char.chr (ascii + shifts) + | hd::tl when ascii + shifts < hd -> Char.chr (ascii + shifts) + | hd::tl (* when ascii + shifts >= hd *) -> nth_char ascii (shifts + 1) tl + in + nth_char (Random.int chars_range + min_ascii) 0 forbidden_chars + + (* return a random id string which have length id_length *) +let new_id () = + let str = String.create id_length in + for i = 0 to id_length - 1 do + String.set str i (random_id_char ()) + done; + str + +let new_broker_id = new_id +let new_client_id = new_id +let new_musing_id = new_id +let new_tutor_id = new_id + diff --git a/helm/ocaml/hbugs/hbugs_id_generator.mli b/helm/ocaml/hbugs/hbugs_id_generator.mli new file mode 100644 index 000000000..dad0c9391 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_id_generator.mli @@ -0,0 +1,35 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_types;; + +val new_broker_id: unit -> broker_id +val new_client_id: unit -> client_id +val new_musing_id: unit -> musing_id +val new_tutor_id: unit -> tutor_id + diff --git a/helm/ocaml/hbugs/hbugs_messages.ml b/helm/ocaml/hbugs/hbugs_messages.ml new file mode 100644 index 000000000..d792c3250 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_messages.ml @@ -0,0 +1,366 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_types;; +open Printf;; +open Pxp_document;; +open Pxp_dtd;; +open Pxp_types;; +open Pxp_yacc;; + +let debug = 2;; (* 0 -> no debug + 1 -> waiting for an answer / answer received + 2 -> XML messages dumping + *) + +exception Attribute_not_found of string;; +exception Empty_node;; (** found a node with no _element_ children *) +exception No_element_found of string;; +exception Parse_error of string * string;; (* parsing subject, reason *) +exception Unexpected_message of message;; + +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 assert_element n name = + match n#node_type with + | T_element n when n = name -> + () + | _ -> raise (Parse_error ("", "Expected node: " ^ name)) + + (** given a string representation of a proof asistant state (e.g. the first + child of the XML root of a State_change or Start_musing message), build from + it an HBugs view of a proof assistant state *) +let parse_state (root: ('a node extension as 'a) node) = + if (List.filter is_xml_element root#sub_nodes) = [] then + raise Empty_node; + let buf = Buffer.create 10240 in + let node_to_string (node: ('a node extension as 'a) node) = + Buffer.clear buf; + node#write (`Out_buffer buf) `Enc_utf8; + let res = Buffer.contents buf in + Buffer.clear buf; + res + in + let (goal_node, type_node, body_node) = + try + (find_element "CurrentGoal" root, + find_element "ConstantType" root, + find_element "CurrentProof" root) + with Not_found -> + raise (Parse_error ("", "Malformed HBugs status XML document")) + in + assert_element root "gTopLevelStatus"; + assert_element goal_node "CurrentGoal"; + assert_element type_node "ConstantType"; + assert_element body_node "CurrentProof"; + goal_node#write (`Out_buffer buf) `Enc_utf8; + let (type_string, body_string) = + (node_to_string type_node, node_to_string body_node) + in + let goal = + try + int_of_string (goal_node#data) + with Failure "int_of_string" -> + raise (Parse_error (goal_node#data, "can't parse goal")) + in + (type_string, body_string, goal) + + (** parse an hint from an XML node, XML node should have type 'T_element _' + (the name is ignored), attributes on it are ignored *) +let parse_hint node = + let rec parse_hint_node node = + match node#node_type with + | T_element "ring" -> Use_ring_Luke + | T_element "fourier" -> Use_fourier_Luke + | T_element "reflexivity" -> Use_reflexivity_Luke + | T_element "symmetry" -> Use_symmetry_Luke + | T_element "assumption" -> Use_assumption_Luke + | T_element "contradiction" -> Use_contradiction_Luke + | T_element "exists" -> Use_exists_Luke + | T_element "split" -> Use_split_Luke + | T_element "left" -> Use_left_Luke + | T_element "right" -> Use_right_Luke + | T_element "apply" -> Use_apply_Luke node#data + | T_element "hints" -> + Hints + (List.map parse_hint_node (List.filter is_xml_element node#sub_nodes)) + | _ -> assert false (* CSC: should this assert false be a raise something? *) + in + match List.filter is_xml_element node#sub_nodes with + [node] -> parse_hint_node node + | _ -> assert false (* CSC: should this assert false be a raise something? *) + +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 pxp_config = PxpHelmConf.pxp_config +let msg_of_string' s = + let root = (* xml tree's root *) + parse_wfcontent_entity pxp_config (from_string s) PxpHelmConf.pxp_spec + in + match root#node_type with + + (* general purpose *) + | T_element "help" -> Help + | T_element "usage" -> Usage root#data + | 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" -> + let state_node = + try + Some (find_element ~deeply:false "gTopLevelStatus" root) + with Not_found -> None + in + State_change + (get_attr root "id", + match state_node with + | Some n -> (try Some (parse_state n) with Empty_node -> None) + | None -> None) + | T_element "wow" -> Wow (get_attr root "id") + + (* 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 (parse_hint main_node) + | 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) + + (* 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" -> + let state_node = + try + find_element ~deeply:false "gTopLevelStatus" root + with Not_found -> raise (No_element_found "gTopLevelStatus") + in + Start_musing (get_attr root "id", parse_state state_node) + | 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") + | T_element "too_late" -> + Too_late (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 = function + | Some (type_string, body_string, goal) -> + (* ASSUMPTION: type_string and body_string are well formed XML document + contents (i.e. they don't contain heading declaration nor + DOCTYPE one *) + "\n" ^ + (sprintf "%d\n" goal) ^ + type_string ^ "\n" ^ + body_string ^ "\n" ^ + "\n" + | None -> "\n" + +let rec pp_hint = function + | Use_ring_Luke -> sprintf "" + | Use_fourier_Luke -> sprintf "" + | Use_reflexivity_Luke -> sprintf "" + | Use_symmetry_Luke -> sprintf "" + | Use_assumption_Luke -> sprintf "" + | Use_contradiction_Luke -> sprintf "" + | Use_exists_Luke -> sprintf "" + | Use_split_Luke -> sprintf "" + | Use_left_Luke -> sprintf "" + | Use_right_Luke -> sprintf "" + | Use_apply_Luke term -> sprintf "%s" term + | Hints hints -> + sprintf "\n%s\n" + (String.concat "\n" (List.map pp_hint hints)) + +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 + | Help -> "" + | Usage usage_string -> sprintf "%s" usage_string + | 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) + | Wow id -> sprintf "" id + | 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 hint -> sprintf "%s" (pp_hint hint)) + | 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 (Some state)) + | Abort_musing (id, musing_id) -> + sprintf "" id musing_id + | Thanks (id, musing_id) -> + sprintf "" id musing_id + | Too_late (id, musing_id) -> + sprintf "" id musing_id +;; + + (* debugging function that dump on stderr the sent messages *) +let dump_msg msg = + if debug >= 2 then + prerr_endline + (sprintf "\n%s\n" + (match msg with + | State_change _ -> "omissis ..." + | msg -> string_of_msg msg)) +;; + +let submit_req ~url msg = + dump_msg msg; + if debug >= 1 then (prerr_string "Waiting for an answer ... "; flush stderr); + let res = + msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url) + in + if debug >= 1 then (prerr_string "answer received!\n"; flush stderr); + res +;; +let return_xml_msg body outchan = + Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan +;; +let respond_msg msg outchan = + dump_msg msg; + return_xml_msg (string_of_msg msg) outchan +(* close_out outchan *) +;; +let respond_exc name value = respond_msg (Exception (name, value));; + diff --git a/helm/ocaml/hbugs/hbugs_messages.mli b/helm/ocaml/hbugs/hbugs_messages.mli new file mode 100644 index 000000000..642c0b0e2 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_messages.mli @@ -0,0 +1,49 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_types;; + +exception Parse_error of string * string (* parsing subject, reason *) +exception Unexpected_message of message;; + +val msg_of_string: string -> message +val string_of_msg: message -> string + +val submit_req: url:string -> message -> message + (** close outchan afterwards *) +val respond_msg: message -> out_channel -> unit + (** close outchan afterwards *) + (* exception_name, exception_value, output_channel *) +val respond_exc: string -> string -> out_channel -> unit + +(* TODO the below functions are for debugging only and shouldn't be exposed *) +val parse_state: + ('a Pxp_document.node Pxp_document.extension as 'a) Pxp_document.node -> + (string * string * int) +val pp_state: (string * string * int) option -> string + diff --git a/helm/ocaml/hbugs/hbugs_misc.ml b/helm/ocaml/hbugs/hbugs_misc.ml new file mode 100644 index 000000000..b826318e0 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_misc.ml @@ -0,0 +1,120 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Printf;; + +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 + () + + (** follows cut and paste from zack's Http_client_smart module *) + +exception Malformed_URL of string;; +exception Malformed_HTTP_response of string;; + +let bufsiz = 16384;; +let tcp_bufsiz = 4096;; + +let body_sep_RE = Pcre.regexp "\r\n\r\n";; +let http_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:http_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 -> raise (Malformed_URL url) +;; +let get_body answer = + match Pcre.split ~rex:body_sep_RE answer with + | [_; body] -> body + | _ -> raise (Malformed_HTTP_response answer) +;; + +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_iter_buf ~callback url = + let (address, port, path) = parse_url url in + let buf = String.create tcp_bufsiz in + let (inchan, outchan) = init_socket address port in + output_string outchan (sprintf "GET %s\r\n" path); + flush outchan; + (try + while true do + match input inchan buf 0 tcp_bufsiz with + | 0 -> raise End_of_file + | bytes when bytes = tcp_bufsiz -> (* buffer full, no need to slice it *) + callback buf + | bytes when bytes < tcp_bufsiz -> (* buffer not full, slice it *) + callback (String.sub buf 0 bytes) + | _ -> (* ( bytes < 0 ) || ( bytes > tcp_bufsiz ) *) + assert false + done + with End_of_file -> ()); + close_in inchan (* close also outchan, same fd *) +;; + +let http_get url = + let buf = Buffer.create (tcp_bufsiz * 10) in + http_get_iter_buf (fun data -> Buffer.add_string buf data) url; + 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 bufsiz in + (try + retrieve inchan buf + with End_of_file -> close_in inchan); (* close also outchan, same fd *) + get_body (Buffer.contents buf) +;; + diff --git a/helm/ocaml/hbugs/hbugs_misc.mli b/helm/ocaml/hbugs/hbugs_misc.mli new file mode 100644 index 000000000..b0ef59719 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_misc.mli @@ -0,0 +1,50 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + + (** helpers *) + + (** remove all bindings of a given key from an hash table *) +val hashtbl_remove_all: ('a, 'b) Hashtbl.t -> 'a -> unit + + (** follows cut and paste from zack's Http_client_smart module *) + + (** can't parse an HTTP url *) +exception Malformed_URL of string + (** can't parse an HTTP response *) +exception Malformed_HTTP_response of string + + (** 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 + + (** perform an HTTP GET request and apply a given function on each + 'slice' of HTTP response read from server *) +val http_get_iter_buf: callback:(string -> unit) -> string -> unit + diff --git a/helm/ocaml/hbugs/hbugs_tutors.ml b/helm/ocaml/hbugs/hbugs_tutors.ml new file mode 100644 index 000000000..7bb732624 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_tutors.ml @@ -0,0 +1,264 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_types;; +open Printf;; + +let broker_url = "localhost:49081/act";; +let dump_environment_on_exit = false;; + +let init_tutor = Hbugs_id_generator.new_tutor_id;; + + (** register a tutor to broker *) +let register_to_broker id url hint_type dsc = + try + let res = + Hbugs_messages.submit_req + ~url:broker_url (Register_tutor (id, url, hint_type, dsc)) + in + (match res with + | Tutor_registered id -> + prerr_endline (sprintf "Tutor registered, broker id: %s" id); + id + | unexpected_msg -> + raise (Hbugs_messages.Unexpected_message unexpected_msg)) + with e -> + failwith (sprintf "Can't register tutor to broker: uncaught exception: %s" + (Printexc.to_string e)) +;; + (** unregister a tutor from the broker *) +let unregister_from_broker id = + let res = Hbugs_messages.submit_req ~url:broker_url (Unregister_tutor id) in + match res with + | Tutor_unregistered _ -> prerr_endline "Tutor unregistered!" + | unexpected_msg -> + failwith + (sprintf "Can't unregister from broker, received unexpected msg: %s" + (Hbugs_messages.string_of_msg unexpected_msg)) +;; + + (* typecheck a loaded proof *) + (* TODO this is a cut and paste from gTopLevel.ml *) +let typecheck_loaded_proof metasenv bo ty = + let module T = CicTypeChecker in + ignore ( + List.fold_left + (fun metasenv ((_,context,ty) as conj) -> + ignore (T.type_of_aux' metasenv context ty) ; + metasenv @ [conj] + ) [] metasenv) ; + ignore (T.type_of_aux' metasenv [] ty) ; + ignore (T.type_of_aux' metasenv [] bo) +;; + +type xml_kind = Body | Type;; +let mk_dtdname ~ask_dtd_to_the_getter dtd = + if ask_dtd_to_the_getter then + Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd + else + "http://mowgli.cs.unibo.it/dtd/" ^ dtd +;; + (** this function must be the inverse function of GTopLevel.strip_xml_headings + *) +let add_xml_headings ~kind s = + let dtdname = mk_dtdname ~ask_dtd_to_the_getter:true "cic.dtd" in + let root = + match kind with + | Body -> "CurrentProof" + | Type -> "ConstantType" + in + "\n\n" ^ + "\n\n" ^ + s +;; + +let load_state (type_string, body_string, goal) = + prerr_endline "a0"; + let ((tmp1, oc1), (tmp2, oc2)) = + (Filename.open_temp_file "" "", Filename.open_temp_file "" "") + in + prerr_endline "a1"; + output_string oc1 (add_xml_headings ~kind:Type type_string); + output_string oc2 (add_xml_headings ~kind:Body body_string); + close_out oc1; close_out oc2; + prerr_endline (sprintf "Proof Type available in %s" tmp1); + prerr_endline (sprintf "Proof Body available in %s" tmp2); + let (proof, goal) = + prerr_endline "a2"; + (match CicParser.obj_of_xml tmp1 (Some tmp2) with + | Cic.CurrentProof (_,metasenv,bo,ty,_) -> (* TODO il primo argomento e' una URI valida o e' casuale? *) + prerr_endline "a3"; + let uri = UriManager.uri_of_string "cic:/foo.con" in + prerr_endline "a4"; + typecheck_loaded_proof metasenv bo ty; + prerr_endline "a5"; + ((uri, metasenv, bo, ty), goal) + | _ -> assert false) + in + prerr_endline "a6"; + Sys.remove tmp1; Sys.remove tmp2; + (proof, goal) + +(* tutors creation stuff from now on *) + +module type HbugsTutor = + sig + val start: unit -> unit + end + +module type HbugsTutorDescription = + sig + val addr: string + val port: int + val tactic: ProofEngineTypes.tactic + val hint: hint + val hint_type: hint_type + val description: string + val environment_file: string + end + +module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor = + struct + let broker_id = ref None + let my_own_id = init_tutor () + let my_own_addr, my_own_port = Dsc.addr, Dsc.port + let my_own_url = sprintf "%s:%d" my_own_addr my_own_port + + let is_authenticated id = + match !broker_id with + | None -> false + | Some broker_id -> id = broker_id + + (* thread who do the dirty work *) + let slave (state, musing_id) = + prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id); + let (proof, goal) = load_state state in + let success = + try + ignore (Dsc.tactic (proof, goal)); + true + with e -> false + in + let answer = + Musing_completed + (my_own_id, musing_id, (if success then Eureka Dsc.hint else Sorry)) + in + ignore (Hbugs_messages.submit_req ~url:broker_url answer); + prerr_endline + (sprintf "Bye, I've completed my duties (success = %b)" success) + + let hbugs_callback = + (* hashtbl mapping musings ids to PID of threads doing the related (dirty) + work *) + let slaves = Hashtbl.create 17 in + let forbidden () = + prerr_endline "ignoring request from unauthorized broker"; + Exception ("forbidden", "") + in + function (* _the_ callback *) + | Start_musing (broker_id, state) -> + if is_authenticated broker_id then begin + prerr_endline "received Start_musing"; + let new_musing_id = Hbugs_id_generator.new_musing_id () in + prerr_endline + (sprintf "starting a new musing (id = %s)" new_musing_id); +(* let slave_thread = Thread.create slave (state, new_musing_id) in *) + let slave_thread = + ExtThread.create slave (state, new_musing_id) + in + Hashtbl.add slaves new_musing_id slave_thread; + Musing_started (my_own_id, new_musing_id) + end else (* broker unauthorized *) + forbidden (); + | Abort_musing (broker_id, musing_id) -> + if is_authenticated broker_id then begin + (try (* kill thread responsible for "musing_id" *) + let slave_thread = Hashtbl.find slaves musing_id in + ExtThread.kill slave_thread; + Hashtbl.remove slaves musing_id + with + | ExtThread.Can_t_kill (_, reason) -> + prerr_endline (sprintf "Unable to kill slave: %s" reason) + | Not_found -> + prerr_endline (sprintf + "Can't find slave corresponding to musing %s, can't kill it" + musing_id)); + Musing_aborted (my_own_id, musing_id) + end else (* broker unauthorized *) + forbidden (); + | unexpected_msg -> + Exception ("unexpected_msg", + Hbugs_messages.string_of_msg unexpected_msg) + + let callback (req: Http_types.request) outchan = + try + let req_msg = Hbugs_messages.msg_of_string req#body in + let answer = hbugs_callback req_msg in + Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan + with Hbugs_messages.Parse_error (subj, reason) -> + Http_daemon.respond + ~body:(Hbugs_messages.string_of_msg + (Exception ("parse_error", reason))) + outchan + + let restore_environment () = + let ic = open_in Dsc.environment_file in + prerr_endline "Restoring environment ..."; + CicEnvironment.restore_from_channel + ~callback:(fun uri -> prerr_endline uri) ic; + prerr_endline "... done!"; + close_in ic + + let dump_environment () = + let oc = open_out Dsc.environment_file in + prerr_endline "Dumping environment ..."; + CicEnvironment.dump_to_channel + ~callback:(fun uri -> prerr_endline uri) oc; + prerr_endline "... done!"; + close_out oc + + let main () = + try + Sys.catch_break true; + at_exit (fun () -> + if dump_environment_on_exit then + dump_environment (); + unregister_from_broker my_own_id); + broker_id := + Some (register_to_broker + my_own_id my_own_url Dsc.hint_type Dsc.description); + if Sys.file_exists Dsc.environment_file then + restore_environment (); + Http_daemon.start' + ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback + with Sys.Break -> () (* exit nicely, invoking at_exit functions *) + + let start = main + + end + diff --git a/helm/ocaml/hbugs/hbugs_tutors.mli b/helm/ocaml/hbugs/hbugs_tutors.mli new file mode 100644 index 000000000..43cd99cce --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_tutors.mli @@ -0,0 +1,60 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Hbugs_types;; + +val broker_url: string + +val register_to_broker: + tutor_id -> string -> hint_type -> string -> + broker_id +val unregister_from_broker: tutor_id -> unit + +val init_tutor: unit -> tutor_id +val load_state: + Hbugs_types.state -> + ProofEngineTypes.proof * ProofEngineTypes.goal + +module type HbugsTutor = + sig + val start: unit -> unit + end + +module type HbugsTutorDescription = + sig + val addr: string + val port: int + val tactic: ProofEngineTypes.tactic + val hint: hint + val hint_type: hint_type + val description: string + val environment_file: string + end + +module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor + diff --git a/helm/ocaml/hbugs/hbugs_types.mli b/helm/ocaml/hbugs/hbugs_types.mli new file mode 100644 index 000000000..ebfa17994 --- /dev/null +++ b/helm/ocaml/hbugs/hbugs_types.mli @@ -0,0 +1,104 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +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 = (* proof assitant's state: proof type, proof body, goal *) + string * string * int + +type hint = + (* tactics usage related hints *) + | Use_ring_Luke + | Use_fourier_Luke + | Use_reflexivity_Luke + | Use_symmetry_Luke + | Use_assumption_Luke + | Use_contradiction_Luke + | Use_exists_Luke + | Use_split_Luke + | Use_left_Luke + | Use_right_Luke + | Use_apply_Luke of string (* use apply tactic on embedded term *) + (* hints list *) + | Hints of hint list + +type hint_type = string (* TODO tipo di consiglio per l'utente *) + +type musing_result = + | Eureka of hint (* 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 *) + | Help (* help request *) + | Usage of string (* help response *) (* usage string *) + | 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 option (* client_id, new state *) + | Wow of client_id (* client_id *) + + (* 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 *) + | Too_late of broker_id * musing_id (* broker id, musing id *) + diff --git a/helm/ocaml/hbugs/run/.cvsignore b/helm/ocaml/hbugs/run/.cvsignore new file mode 100644 index 000000000..397b4a762 --- /dev/null +++ b/helm/ocaml/hbugs/run/.cvsignore @@ -0,0 +1 @@ +*.log diff --git a/helm/ocaml/hbugs/scripts/brokerctl.sh b/helm/ocaml/hbugs/scripts/brokerctl.sh new file mode 100755 index 000000000..3da998d6c --- /dev/null +++ b/helm/ocaml/hbugs/scripts/brokerctl.sh @@ -0,0 +1,15 @@ +#!/bin/sh +daemon="broker" +if [ "$1" = "--help" -o "$1" = "" ]; then + echo "ctl.sh { start | stop | --help }" + exit 0 +fi +if [ "$1" = "start" ]; then + echo -n "Starting HBugs broker ... " + ./$daemon &> run/$daemon.log & + echo "done!" +elif [ "$1" = "stop" ]; then + echo -n "Stopping HBugs broker ... " + killall -9 $daemon + echo "done!" +fi diff --git a/helm/ocaml/hbugs/scripts/build_tutors.ml b/helm/ocaml/hbugs/scripts/build_tutors.ml new file mode 100755 index 000000000..9b742d84d --- /dev/null +++ b/helm/ocaml/hbugs/scripts/build_tutors.ml @@ -0,0 +1,112 @@ +#!/usr/bin/ocamlrun /usr/bin/ocaml +(* + * Copyright (C) 2003-2004: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) +#use "topfind" +#require "pcre" +#require "pxp" +open Printf +open Pxp_document +open Pxp_dtd +open Pxp_types +open Pxp_yacc + +let index = "data/tutors_index.xml" +let template = "data/hbugs_tutor.TPL.ml" + + (* apply a set of regexp substitutions specified as a list of pairs + to a string *) +let rec apply_subst ~fill s = + match fill with + | [] -> s + | (pat, templ)::rest -> + apply_subst ~fill:rest (Pcre.replace ~pat ~templ s) + (* fill a ~template file with substitutions specified in ~fill (see + apply_subst) and save output to ~output *) +let fill_template ~template ~fill ~output = + printf "Creating %s ... " output; flush stdout; + let (ic, oc) = (open_in template, open_out output) in + let rec fill_template' () = + output_string oc ((apply_subst ~fill (input_line ic)) ^ "\n"); + fill_template' () + in + try + output_string oc (sprintf +"(* + THIS CODE IS GENERATED - DO NOT MODIFY! + + the source of this code is template \"%s\" + the template was filled with data read from \"%s\" +*)\n" + template index); + fill_template' () + with End_of_file -> + close_in ic; + close_out oc; + printf "done!\n"; flush stdout +let parse_xml fname = + parse_wfdocument_entity default_config (from_file fname) default_spec +let is_tutor node = + match node#node_type with T_element "tutor" -> true | _ -> false +let is_element node = + match node#node_type with T_element _ -> true | _ -> false +let main () = + (parse_xml index)#root#iter_nodes + (fun node -> + try + (match node with + | node when is_tutor node -> + (try (* skip hand-written tutors *) + ignore (find_element "no_auto" node); + raise Exit + with Not_found -> ()); + let output = + try + (match node#attribute "source" with + | Value s -> s + | _ -> assert false) + with Not_found -> assert false + in + let fill = + List.map (* create substitution list from index data *) + (fun node -> + let name = (* node name *) + (match node#node_type with + | T_element s -> s + | _ -> assert false) + in + let value = node#data in (* node value *) + (sprintf "@%s@" (String.uppercase name), (* pattern *) + value)) (* substitution *) + (List.filter is_element node#sub_nodes) + in + fill_template ~fill ~template ~output + | _ -> ()) + with Exit -> ()) + +let _ = main () + diff --git a/helm/ocaml/hbugs/scripts/ls_tutors.ml b/helm/ocaml/hbugs/scripts/ls_tutors.ml new file mode 100755 index 000000000..5fe796ca1 --- /dev/null +++ b/helm/ocaml/hbugs/scripts/ls_tutors.ml @@ -0,0 +1,68 @@ +#!/usr/bin/ocamlrun /usr/bin/ocaml +(* + * Copyright (C) 2003-2004: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +(* Usage: ls_tutors.ml # lists all tutors + * ls_tutors.ml -auto # lists only generated tutors + *) + +#use "topfind" +#require "pxp" +open Printf +open Pxp_document +open Pxp_dtd +open Pxp_types +open Pxp_yacc + +let index = "data/tutors_index.xml" +let auto_only = + try + (match Sys.argv.(1) with "-auto" -> true | _ -> false) + with Invalid_argument _ -> false +let parse_xml fname = + parse_wfdocument_entity default_config (from_file fname) default_spec +let is_tutor node = + match node#node_type with T_element "tutor" -> true | _ -> false +let main () = + List.iter + (fun tutor -> + try + (match tutor#attribute "source" with + | Value s -> + if not auto_only then + print_endline s + else (* we should print only generated tutors *) + (try + ignore (find_element "no_auto" tutor); + with Not_found -> + print_endline s) + | _ -> assert false) + with Not_found -> assert false) + (List.filter is_tutor (parse_xml index)#root#sub_nodes) +let _ = main () + diff --git a/helm/ocaml/hbugs/scripts/sabba.sh b/helm/ocaml/hbugs/scripts/sabba.sh new file mode 100755 index 000000000..2031e295f --- /dev/null +++ b/helm/ocaml/hbugs/scripts/sabba.sh @@ -0,0 +1,47 @@ +#!/bin/sh +# Copyright (C) 2003: +# Stefano Zacchiroli +# for the HELM Team http://helm.cs.unibo.it/ +# +# 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://helm.cs.unibo.it/ +if [ "$1" = "--help" -o "$1" = "" ]; then + echo "sabba.sh { start | stop | --help }" + exit 0 +fi + +./scripts/ls_tutors.ml | +while read line; do + tutor=`echo $line | sed 's/\.ml//'` + if [ "$1" = "stop" ]; then + echo -n "Stopping HBugs tutor $tutor ... " + killall -9 $tutor + echo "done!" + elif [ "$1" = "start" ]; then + echo -n "Starting HBugs tutor $tutor ... " + nice -n 19 ./$tutor &> run/$tutor.log & + echo "done!" + else + echo "Uh? Try --help" + exit 1 + fi +done diff --git a/helm/ocaml/hbugs/search_pattern_apply_tutor.ml b/helm/ocaml/hbugs/search_pattern_apply_tutor.ml new file mode 100644 index 000000000..0c1e7d0ae --- /dev/null +++ b/helm/ocaml/hbugs/search_pattern_apply_tutor.ml @@ -0,0 +1,146 @@ + +open Hbugs_types;; +open Printf;; + +exception Empty_must;; + +module MQI = MQueryInterpreter +module MQIC = MQIConn + +let broker_id = ref None +let my_own_id = Hbugs_tutors.init_tutor () +let my_own_addr, my_own_port = "127.0.0.1", 50011 +let my_own_url = sprintf "%s:%d" my_own_addr my_own_port +let environment_file = "search_pattern_apply.environment" +let dump_environment_on_exit = false + +let is_authenticated id = + match !broker_id with + | None -> false + | Some broker_id -> id = broker_id + + (* thread who do the dirty work *) +let slave mqi_handle (state, musing_id) = + try + prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id); + let (proof, goal) = Hbugs_tutors.load_state state in + let hint = + try + let choose_must must only = (* euristic: use 2nd precision level + 1st is more precise but is more slow *) + match must with + | [] -> raise Empty_must + | _::hd::tl -> hd + | hd::tl -> hd + in + let uris = + TacticChaser.matchConclusion mqi_handle + ~output_html:prerr_endline ~choose_must () ~status:(proof, goal) + in + if uris = [] then + Sorry + else + Eureka (Hints (List.map (fun uri -> Use_apply_Luke uri) uris)) + with Empty_must -> Sorry + in + let answer = Musing_completed (my_own_id, musing_id, hint) in + ignore (Hbugs_messages.submit_req ~url:Hbugs_tutors.broker_url answer); + prerr_endline + (sprintf "Bye, I've completed my duties (success = %b)" (hint <> Sorry)) + with + (Pxp_types.At _) as e -> + let rec unbox_exception = + function + Pxp_types.At (_,e) -> unbox_exception e + | e -> e + in + prerr_endline ("Uncaught PXP exception: " ^ Pxp_types.string_of_exn e) ; + (* e could be the Thread.exit exception; otherwise we will release an *) + (* uncaught exception and the Pxp_types.At was already an uncaught *) + (* exception ==> no additional arm *) + raise (unbox_exception e) + +let hbugs_callback mqi_handle = + let ids = Hashtbl.create 17 in + let forbidden () = + prerr_endline "ignoring request from unauthorized broker"; + Exception ("forbidden", "") + in + function + | Start_musing (broker_id, state) -> + if is_authenticated broker_id then begin + prerr_endline "received Start_musing"; + let new_musing_id = Hbugs_id_generator.new_musing_id () in + let id = ExtThread.create (slave mqi_handle) (state, new_musing_id) in + prerr_endline (sprintf "starting a new musing (id = %s)" new_musing_id); + Hashtbl.add ids new_musing_id id; + (*ignore (Thread.create slave (state, new_musing_id));*) + Musing_started (my_own_id, new_musing_id) + end else (* broker unauthorized *) + forbidden (); + | Abort_musing (broker_id, musing_id) -> + prerr_endline "CSC: Abort_musing received" ; + if is_authenticated broker_id then begin + (* prerr_endline "Ignoring 'Abort_musing' message ..."; *) + (try + ExtThread.kill (Hashtbl.find ids musing_id) ; + Hashtbl.remove ids musing_id ; + with + Not_found + | ExtThread.Can_t_kill _ -> + prerr_endline ("Can not kill slave " ^ musing_id)) ; + Musing_aborted (my_own_id, musing_id) + end else (* broker unauthorized *) + forbidden (); + | unexpected_msg -> + Exception ("unexpected_msg", + Hbugs_messages.string_of_msg unexpected_msg) + +let callback mqi_handle (req: Http_types.request) outchan = + try + let req_msg = Hbugs_messages.msg_of_string req#body in + let answer = hbugs_callback mqi_handle req_msg in + Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan + with Hbugs_messages.Parse_error (subj, reason) -> + Http_daemon.respond + ~body:(Hbugs_messages.string_of_msg + (Exception ("parse_error", reason))) + outchan + +let restore_environment () = + let ic = open_in environment_file in + prerr_endline "Restoring environment ..."; + CicEnvironment.restore_from_channel + ~callback:(fun uri -> prerr_endline uri) ic; + prerr_endline "... done!"; + close_in ic + +let dump_environment () = + let oc = open_out environment_file in + prerr_endline "Dumping environment ..."; + CicEnvironment.dump_to_channel + ~callback:(fun uri -> prerr_endline uri) oc; + prerr_endline "... done!"; + close_out oc + +let main () = + try + Sys.catch_break true; + at_exit (fun () -> + if dump_environment_on_exit then + dump_environment (); + Hbugs_tutors.unregister_from_broker my_own_id); + broker_id := + Some (Hbugs_tutors.register_to_broker + my_own_id my_own_url "FOO" "Search_pattern_apply tutor"); + let mqi_handle = MQIC.init ~log:prerr_string () in + if Sys.file_exists environment_file then + restore_environment (); + Http_daemon.start' + ~addr:my_own_addr ~port:my_own_port ~mode:`Thread (callback mqi_handle); + MQIC.close mqi_handle + with Sys.Break -> () (* exit nicely, invoking at_exit functions *) +;; + +main () + diff --git a/helm/ocaml/hbugs/test/.cvsignore b/helm/ocaml/hbugs/test/.cvsignore new file mode 100644 index 000000000..d9ed0701b --- /dev/null +++ b/helm/ocaml/hbugs/test/.cvsignore @@ -0,0 +1,7 @@ +*.cmi +*.cmo +*.cma +*.cmx +*.o +*.a +test_serialization diff --git a/helm/ocaml/hbugs/test/HBUGS_MESSAGES.xml b/helm/ocaml/hbugs/test/HBUGS_MESSAGES.xml new file mode 100644 index 000000000..cf15dde3d --- /dev/null +++ b/helm/ocaml/hbugs/test/HBUGS_MESSAGES.xml @@ -0,0 +1,144 @@ + + + + + + + usage string + + corpo dell'exc + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + + + + + + + + + + + descrizione del tutor + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + description 1 + description 2 + + description N + + + + description 1 + description 2 + + description N + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + + + + diff --git a/helm/ocaml/hbugs/test/Makefile b/helm/ocaml/hbugs/test/Makefile new file mode 100644 index 000000000..0b3debf74 --- /dev/null +++ b/helm/ocaml/hbugs/test/Makefile @@ -0,0 +1,5 @@ +all: test_serialization +test_serialization: test_serialization.ml + OCAMLPATH="../meta" ocamlfind ocamlc -linkpkg -package hbugs-common -o test_serialization test_serialization.ml +clean: + rm -f *.cm[io] test_serialization diff --git a/helm/ocaml/hbugs/test/test_serialization.ml b/helm/ocaml/hbugs/test/test_serialization.ml new file mode 100644 index 000000000..1afd74379 --- /dev/null +++ b/helm/ocaml/hbugs/test/test_serialization.ml @@ -0,0 +1,70 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * 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://helm.cs.unibo.it/ + *) + +open Pxp_document;; +open Pxp_dtd;; +open Pxp_types;; +open Pxp_yacc;; + +open Printf;; + +let test_data = "HBUGS_MESSAGES.xml" ;; + +let test_message (n:('a Pxp_document.extension as 'b) Pxp_document.node as 'a) = + try + let msg_string = + let buf = Buffer.create 1000 in + n#write (`Out_buffer buf) `Enc_utf8; + Buffer.contents buf + in + let msg = Hbugs_messages.msg_of_string msg_string in + let pp = Hbugs_messages.string_of_msg msg in + let msg' = Hbugs_messages.msg_of_string pp in + if (msg <> msg') then + prerr_endline + (sprintf "Failure with msg %s" + (match n#node_type with T_element name -> name | _ -> assert false)) + with e -> + prerr_endline + (sprintf "Failure with msg %s: uncaught exception %s" + (match n#node_type with T_element name -> name | _ -> assert false) + (Printexc.to_string e)) +;; + +let is_xml_element n = + match n#node_type with T_element _ -> true | _ -> false +;; + +let root = + parse_wfcontent_entity default_config (from_file test_data) default_spec +in +printf "Testing all messages from %s ...\n" test_data; flush stdout; +List.iter test_message (List.filter is_xml_element root#sub_nodes); +printf "Done!\n" +;; +