From: Stefano Zacchiroli Date: Mon, 19 Apr 2004 12:01:03 +0000 (+0000) Subject: moved hbugs under ocaml/ X-Git-Tag: dead_dir_walking~43 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3d4c7ffba4f58ba6e0184e1493d1bd3087096f47;p=helm.git moved hbugs under ocaml/ --- diff --git a/helm/hbugs/Makefile b/helm/hbugs/Makefile deleted file mode 100644 index 133d009f3..000000000 --- a/helm/hbugs/Makefile +++ /dev/null @@ -1,30 +0,0 @@ -DIRS = meta common broker client tutors - -DIRS_BYTE = $(patsubst %,%.byte,$(DIRS)) -DIRS_OPT = $(patsubst %,%.opt,$(DIRS)) -DIRS_CLEAN = $(patsubst %,%.clean,$(DIRS)) -DIRS_DISTCLEAN = $(patsubst %,%.distclean,$(DIRS)) -all: byte -meta: - $(MAKE) -C meta/ -byte: meta $(DIRS_BYTE) -opt: meta $(DIRS_OPT) -world: byte opt -clean: $(DIRS_CLEAN) -distclean: $(DIRS_DISTCLEAN) -%.byte: - $(MAKE) -C $*/ all -%.opt: - $(MAKE) -C $*/ opt -%.clean: - $(MAKE) -C $*/ clean -%.distclean: - $(MAKE) -C $*/ distclean -start: - $(MAKE) -C broker/ start - $(MAKE) -C tutors/ start -stop: - $(MAKE) -C tutors/ stop - $(MAKE) -C broker/ stop -restart: stop start -.PHONY: all byte opt world clean meta restart start stop diff --git a/helm/hbugs/broker/.cvsignore b/helm/hbugs/broker/.cvsignore deleted file mode 100644 index 2527ca9d9..000000000 --- a/helm/hbugs/broker/.cvsignore +++ /dev/null @@ -1,8 +0,0 @@ -*.cmi -*.cmo -*.cma -*.cmx -*.o -*.a -hbugs_broker -hbugs_broker.opt diff --git a/helm/hbugs/broker/.depend b/helm/hbugs/broker/.depend deleted file mode 100644 index 46f3ac82e..000000000 --- a/helm/hbugs/broker/.depend +++ /dev/null @@ -1,4 +0,0 @@ -hbugs_broker.cmo: hbugs_broker_registry.cmi -hbugs_broker.cmx: hbugs_broker_registry.cmx -hbugs_broker_registry.cmo: hbugs_broker_registry.cmi -hbugs_broker_registry.cmx: hbugs_broker_registry.cmi diff --git a/helm/hbugs/broker/Makefile b/helm/hbugs/broker/Makefile deleted file mode 100644 index e4cb57236..000000000 --- a/helm/hbugs/broker/Makefile +++ /dev/null @@ -1,61 +0,0 @@ -NAME = hbugs_broker -METADIR = ../meta -REQUIRES = http threads hbugs-common hbugs-thread-safe threads -COMMONOPTS = -package "$(REQUIRES)" -pp camlp4o -OCAMLFIND = ocamlfind -OCAMLC = $(OCAMLFIND) ocamlc -thread $(COMMONOPTS) -OCAMLOPT = $(OCAMLFIND) ocamlopt -thread $(COMMONOPTS) -OCAMLDEP = $(OCAMLFIND) ocamldep $(COMMONOPTS) -MODULES = hbugs_broker_registry -OCAMLDOC = \ - ocamldoc \ - $(shell $(OCAMLFIND) query -i-format http) \ - $(shell $(OCAMLFIND) query -i-format threads) \ - $(shell $(OCAMLFIND) query -i-format hbugs-common) \ - $(shell $(OCAMLFIND) query -i-format hbugs-thread-safe) \ - $(shell $(OCAMLFIND) query -i-format hbugs-thread-safe) \ - $(shell $(OCAMLFIND) query -i-format pxp-engine) \ - $(shell $(OCAMLFIND) query -i-format pcre) -CTL = ./hbugs_broker_ctl.sh - -OBJS = $(patsubst %,%.cmo,$(MODULES)) -OBJSOPT = $(patsubst %,%.cmx,$(MODULES)) -DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES)) -DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES)) - -all: byte -byte: $(NAME) -opt: $(NAME).opt -world: byte opt -start: - $(CTL) start -stop: - $(CTL) stop - -include .depend -depend: - $(OCAMLDEP) *.ml *.mli > .depend - -%.cmi: %.mli - $(OCAMLC) -c $< -%.cmo: %.ml %.cmi - $(OCAMLC) -c $< -%.cmx: %.ml %.cmi - $(OCAMLOPT) -c $< -include Makefile.overrides -$(OBJS): $(DEPS) -$(OBJSOPT): $(DEPSOPT) -$(NAME): $(OBJS) $(NAME).ml - $(OCAMLC) -linkpkg -thread -o $@ $^ -$(NAME).opt: $(OBJSOPT) $(NAME).ml - $(OCAMLOPT) -linkpkg -thread -o $@ $^ -$(NAME).dot: *.ml *.mli ../common/*.ml ../common/*.mli - $(OCAMLDOC) -dot -o $@ $^ - -distclean: clean - rm -f run/* -clean: - rm -f *.cm[aiox] *.o $(NAME){,.opt} - -.PHONY: all byte opt world depend clean start stop - diff --git a/helm/hbugs/broker/Makefile.overrides b/helm/hbugs/broker/Makefile.overrides deleted file mode 100644 index e69de29bb..000000000 diff --git a/helm/hbugs/broker/hbugs_broker.ml b/helm/hbugs/broker/hbugs_broker.ml deleted file mode 100644 index 2ff8b9834..000000000 --- a/helm/hbugs/broker/hbugs_broker.ml +++ /dev/null @@ -1,292 +0,0 @@ -(* - * 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/hbugs/broker/hbugs_broker_ctl.sh b/helm/hbugs/broker/hbugs_broker_ctl.sh deleted file mode 100755 index 57ee007d5..000000000 --- a/helm/hbugs/broker/hbugs_broker_ctl.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/sh -daemon="hbugs_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/hbugs/broker/hbugs_broker_registry.ml b/helm/hbugs/broker/hbugs_broker_registry.ml deleted file mode 100644 index 879d746ac..000000000 --- a/helm/hbugs/broker/hbugs_broker_registry.ml +++ /dev/null @@ -1,315 +0,0 @@ -(* - * 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/hbugs/broker/hbugs_broker_registry.mli b/helm/hbugs/broker/hbugs_broker_registry.mli deleted file mode 100644 index ece9e07cf..000000000 --- a/helm/hbugs/broker/hbugs_broker_registry.mli +++ /dev/null @@ -1,87 +0,0 @@ -(* - * 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/hbugs/broker/run/.cvsignore b/helm/hbugs/broker/run/.cvsignore deleted file mode 100644 index 7789b92c6..000000000 --- a/helm/hbugs/broker/run/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.LOG diff --git a/helm/hbugs/client/.cvsignore b/helm/hbugs/client/.cvsignore deleted file mode 100644 index 405d7b0f4..000000000 --- a/helm/hbugs/client/.cvsignore +++ /dev/null @@ -1,9 +0,0 @@ -*.cmi -*.cmo -*.cma -*.cmx -*.o -*.a -hbugs_client_gui.ml -hbugs_client -hbugs_client.opt diff --git a/helm/hbugs/client/Makefile b/helm/hbugs/client/Makefile deleted file mode 100644 index 220a3b198..000000000 --- a/helm/hbugs/client/Makefile +++ /dev/null @@ -1,38 +0,0 @@ -NAME = hbugs_client -METADIR = ../meta -REQUIRES = lablgtk2 threads hbugs-common lablgtk2.glade -PREDICATES = glade init -COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -OCAMLC = OCAMLPATH="$(METADIR)" ocamlfind ocamlc -thread $(COMMONOPTS) -OCAMLOPT = OCAMLPATH="$(METADIR)" ocamlfind ocamlopt -thread $(COMMONOPTS) -OCAMLFIND = ocamlfind - -DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES)) -DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES)) - -all: byte -world: byte opt -byte: $(NAME) -opt: $(NAME).opt - -hbugs_client_gui.ml: hbugs_gui.glade - lablgladecc2 $< > $@.tmp - mv $@.tmp $@ -hbugs_client_gui.cmo: hbugs_client_gui.ml - $(OCAMLC) -c $< -hbugs_client_gui.cmx: hbugs_client_gui.ml - $(OCAMLOPT) -c $< -hbugs_client.cmi: hbugs_client.mli - $(OCAMLC) -c $< -hbugs_client.cmo: hbugs_client.ml hbugs_client.cmi - $(OCAMLC) -thread -c $< -hbugs_client.cmx: hbugs_client.ml hbugs_client.cmi - $(OCAMLOPT) -thread -c $< -$(NAME): $(DEPS) hbugs_client_gui.cmo $(NAME).cmo main.ml - $(OCAMLC) -thread -package threads -linkpkg -o $@ hbugs_client_gui.cmo $(NAME).cmo main.ml -$(NAME).opt: $(DEPSOPT) hbugs_client_gui.cmx $(NAME).cmx main.ml - $(OCAMLOPT) -thread -package threads -linkpkg -o $@ hbugs_client_gui.cmx $(NAME).cmx main.ml -clean: - rm -f *.cm[aixo] *.cmxa *.[oa] $(NAME){,.opt} hbugs_client_gui.ml -distclean: clean -.PHONY: all world byte opt clean diff --git a/helm/hbugs/client/hbugs_client.ml b/helm/hbugs/client/hbugs_client.ml deleted file mode 100644 index 4613dbf0d..000000000 --- a/helm/hbugs/client/hbugs_client.ml +++ /dev/null @@ -1,524 +0,0 @@ -(* - * 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/hbugs/client/hbugs_client.mli b/helm/hbugs/client/hbugs_client.mli deleted file mode 100644 index 0c2e93d80..000000000 --- a/helm/hbugs/client/hbugs_client.mli +++ /dev/null @@ -1,33 +0,0 @@ - -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/hbugs/client/hbugs_gui.glade b/helm/hbugs/client/hbugs_gui.glade deleted file mode 100644 index f88a8c388..000000000 --- a/helm/hbugs/client/hbugs_gui.glade +++ /dev/null @@ -1,672 +0,0 @@ - - - - - - - - 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/hbugs/client/main.ml b/helm/hbugs/client/main.ml deleted file mode 100644 index 85972ace3..000000000 --- a/helm/hbugs/client/main.ml +++ /dev/null @@ -1,44 +0,0 @@ -(* - * 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/hbugs/common/.cvsignore b/helm/hbugs/common/.cvsignore deleted file mode 100644 index a3cccbc0c..000000000 --- a/helm/hbugs/common/.cvsignore +++ /dev/null @@ -1,6 +0,0 @@ -*.cmi -*.cmo -*.cma -*.cmx -*.o -*.a diff --git a/helm/hbugs/common/.depend b/helm/hbugs/common/.depend deleted file mode 100644 index 366905460..000000000 --- a/helm/hbugs/common/.depend +++ /dev/null @@ -1,11 +0,0 @@ -hbugs_common.cmo: hbugs_types.cmo hbugs_common.cmi -hbugs_common.cmx: hbugs_types.cmx 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.cmo hbugs_messages.cmi -hbugs_messages.cmx: hbugs_misc.cmx hbugs_types.cmx hbugs_messages.cmi -hbugs_misc.cmo: hbugs_misc.cmi -hbugs_misc.cmx: hbugs_misc.cmi -hbugs_common.cmi: hbugs_types.cmo -hbugs_id_generator.cmi: hbugs_types.cmo -hbugs_messages.cmi: hbugs_types.cmo diff --git a/helm/hbugs/common/Makefile b/helm/hbugs/common/Makefile deleted file mode 100644 index ca95aae24..000000000 --- a/helm/hbugs/common/Makefile +++ /dev/null @@ -1,51 +0,0 @@ -REQUIRES = helm-xml helm-pxp pcre pxp http -COMMONOPTS = -package "$(REQUIRES)" -pp camlp4o -OCAMLFIND = ocamlfind -OCAMLC = $(OCAMLFIND) ocamlc -thread $(COMMONOPTS) -OCAMLOPT = $(OCAMLFIND) ocamlopt -thread $(COMMONOPTS) -OCAMLDEP = $(OCAMLFIND) ocamldep $(COMMONOPTS) -OCAMLDOC = \ - ocamldoc \ - $(shell $(OCAMLFIND) query -i-format helm-xml) \ - $(shell $(OCAMLFIND) query -i-format helm-pxp) \ - $(shell $(OCAMLFIND) query -i-format pcre) \ - $(shell $(OCAMLFIND) query -i-format pxp-engine) \ - $(shell $(OCAMLFIND) query -i-format threads) \ - $(shell $(OCAMLFIND) query -i-format http) -MODULES = \ - hbugs_types threadSafe hbugs_misc \ - hbugs_common hbugs_id_generator hbugs_messages - -OBJS = $(patsubst %,%.cmo,$(MODULES)) -OBJSOPT = $(patsubst %,%.cmx,$(MODULES)) -DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES)) -DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES)) - -all: byte -byte: $(OBJS) -opt: $(OBJSOPT) -world: byte opt - -hbugs_common.dot: *.ml *.mli - $(OCAMLDOC) -dot -o $@ $^ - -include .depend -depend: - $(OCAMLDEP) *.ml *.mli > .depend - -%.cmi: %.mli - $(OCAMLC) -c $< -%.cmo: %.ml %.cmi - $(OCAMLC) -c $< -%.cmx: %.ml %.cmi - $(OCAMLOPT) -c $< -include Makefile.overrides -$(OBJS): $(DEPS) -$(OBJSOPT): $(DEPSOPT) - -distclean: clean -clean: - rm -f *.cm[aiox] *.o $(NAME){,.opt} - -.PHONY: all byte opt world depend clean - diff --git a/helm/hbugs/common/Makefile.overrides b/helm/hbugs/common/Makefile.overrides deleted file mode 100644 index 62506b505..000000000 --- a/helm/hbugs/common/Makefile.overrides +++ /dev/null @@ -1,6 +0,0 @@ -hbugs_types.cmi hbugs_types.cmo: hbugs_types.ml - $(OCAMLC) -c $< -threadSafe.cmi threadSafe.cmo: threadSafe.ml - $(OCAMLC) -thread -package threads -c $< -threadSafe.cmx: threadSafe.ml threadSafe.cmi - $(OCAMLOPT) -thread -package threads -c $< diff --git a/helm/hbugs/common/hbugs_common.ml b/helm/hbugs/common/hbugs_common.ml deleted file mode 100644 index 3b19ceec0..000000000 --- a/helm/hbugs/common/hbugs_common.ml +++ /dev/null @@ -1,46 +0,0 @@ -(* - * 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/hbugs/common/hbugs_common.mli b/helm/hbugs/common/hbugs_common.mli deleted file mode 100644 index 2d51075f3..000000000 --- a/helm/hbugs/common/hbugs_common.mli +++ /dev/null @@ -1,32 +0,0 @@ -(* - * 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/hbugs/common/hbugs_id_generator.ml b/helm/hbugs/common/hbugs_id_generator.ml deleted file mode 100644 index f535f4739..000000000 --- a/helm/hbugs/common/hbugs_id_generator.ml +++ /dev/null @@ -1,65 +0,0 @@ -(* - * 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/hbugs/common/hbugs_id_generator.mli b/helm/hbugs/common/hbugs_id_generator.mli deleted file mode 100644 index dad0c9391..000000000 --- a/helm/hbugs/common/hbugs_id_generator.mli +++ /dev/null @@ -1,35 +0,0 @@ -(* - * 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/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml deleted file mode 100644 index b320501ba..000000000 --- a/helm/hbugs/common/hbugs_messages.ml +++ /dev/null @@ -1,365 +0,0 @@ -(* - * 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 msg_of_string' s = - let root = (* xml tree's root *) - parse_wfcontent_entity default_config (from_string s) default_spec - in - match root#node_type with - - (* general purpose *) - | T_element "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/hbugs/common/hbugs_messages.mli b/helm/hbugs/common/hbugs_messages.mli deleted file mode 100644 index 642c0b0e2..000000000 --- a/helm/hbugs/common/hbugs_messages.mli +++ /dev/null @@ -1,49 +0,0 @@ -(* - * 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/hbugs/common/hbugs_misc.ml b/helm/hbugs/common/hbugs_misc.ml deleted file mode 100644 index b826318e0..000000000 --- a/helm/hbugs/common/hbugs_misc.ml +++ /dev/null @@ -1,120 +0,0 @@ -(* - * 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/hbugs/common/hbugs_misc.mli b/helm/hbugs/common/hbugs_misc.mli deleted file mode 100644 index b0ef59719..000000000 --- a/helm/hbugs/common/hbugs_misc.mli +++ /dev/null @@ -1,50 +0,0 @@ -(* - * 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/hbugs/common/hbugs_types.ml b/helm/hbugs/common/hbugs_types.ml deleted file mode 100644 index ebfa17994..000000000 --- a/helm/hbugs/common/hbugs_types.ml +++ /dev/null @@ -1,104 +0,0 @@ -(* - * 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/hbugs/common/threadSafe.ml b/helm/hbugs/common/threadSafe.ml deleted file mode 100644 index c09301d2f..000000000 --- a/helm/hbugs/common/threadSafe.ml +++ /dev/null @@ -1,96 +0,0 @@ -(* - * 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 debug_print = let debug = false in fun s -> if debug then prerr_endline s;; - -class threadSafe = - object (self) - - val mutex = Mutex.create () - - (** condition variable: 'no readers is currently reading' *) - val noReaders = Condition.create () - - (** readers count *) - val mutable readersCount = 0 - - method private incrReadersCount = (* internal, not exported *) - self#doCritical (lazy ( - readersCount <- readersCount + 1 - )) - - method private decrReadersCount = (* internal, not exported *) - self#doCritical (lazy ( - if readersCount > 0 then readersCount <- readersCount - 1; - )) - - method private signalNoReaders = (* internal, not exported *) - self#doCritical (lazy ( - if readersCount = 0 then Condition.signal noReaders - )) - - method private doCritical: 'a. 'a lazy_t -> 'a = - fun action -> - debug_print ""; - (try - Mutex.lock mutex; - let res = Lazy.force action in - Mutex.unlock mutex; - debug_print ""; - res - with e -> - Mutex.unlock mutex; - raise e); - - method private doReader: 'a. 'a lazy_t -> 'a = - fun action -> - debug_print ""; - let cleanup () = - self#decrReadersCount; - self#signalNoReaders - in - self#incrReadersCount; - let res = (try Lazy.force action with e -> (cleanup (); raise e)) in - cleanup (); - debug_print ""; - res - - (* TODO may starve!!!! is what we want or not? *) - method private doWriter: 'a. 'a lazy_t -> 'a = - fun action -> - debug_print ""; - self#doCritical (lazy ( - while readersCount > 0 do - Condition.wait noReaders mutex - done; - let res = Lazy.force action in - debug_print ""; - res - )) - - end diff --git a/helm/hbugs/doc/.cvsignore b/helm/hbugs/doc/.cvsignore deleted file mode 100644 index 743328ec1..000000000 --- a/helm/hbugs/doc/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.dia~ diff --git a/helm/hbugs/doc/hbugs.dia b/helm/hbugs/doc/hbugs.dia deleted file mode 100644 index b1c4e64e2..000000000 Binary files a/helm/hbugs/doc/hbugs.dia and /dev/null differ diff --git a/helm/hbugs/meta/.cvsignore b/helm/hbugs/meta/.cvsignore deleted file mode 100644 index fcfb940ea..000000000 --- a/helm/hbugs/meta/.cvsignore +++ /dev/null @@ -1,3 +0,0 @@ -META.hbugs-common -META.hbugs-client -META.hbugs-thread-safe diff --git a/helm/hbugs/meta/META.hbugs-client.in b/helm/hbugs/meta/META.hbugs-client.in deleted file mode 100644 index 5b82251cd..000000000 --- a/helm/hbugs/meta/META.hbugs-client.in +++ /dev/null @@ -1,4 +0,0 @@ -requires="pcre pxp http hbugs-common lablgtk2.glade" -directory="@HBUGS_CLIENT_DIR@" -archive(byte) = "hbugs_client_gui.cmo hbugs_client.cmo" -archive(native) = "hbugs_client_gui.cmx hbugs_client.cmx" diff --git a/helm/hbugs/meta/META.hbugs-common.in b/helm/hbugs/meta/META.hbugs-common.in deleted file mode 100644 index e250303cc..000000000 --- a/helm/hbugs/meta/META.hbugs-common.in +++ /dev/null @@ -1,4 +0,0 @@ -requires="pcre pxp http" -directory="@HBUGS_COMMON_DIR@" -archive(byte) = "hbugs_types.cmo hbugs_misc.cmo hbugs_common.cmo hbugs_id_generator.cmo hbugs_messages.cmo" -archive(native) = "hbugs_types.cmx hbugs_misc.cmx hbugs_common.cmx hbugs_id_generator.cmx hbugs_messages.cmx" diff --git a/helm/hbugs/meta/META.hbugs-thread-safe.in b/helm/hbugs/meta/META.hbugs-thread-safe.in deleted file mode 100644 index 157c03570..000000000 --- a/helm/hbugs/meta/META.hbugs-thread-safe.in +++ /dev/null @@ -1,4 +0,0 @@ -requires="threads" -directory="@HBUGS_COMMON_DIR@" -archive(byte) = "threadSafe.cmo" -archive(native) = "threadSafe.cmx" diff --git a/helm/hbugs/meta/Makefile b/helm/hbugs/meta/Makefile deleted file mode 100644 index af3f3f74b..000000000 --- a/helm/hbugs/meta/Makefile +++ /dev/null @@ -1,12 +0,0 @@ -META = META.hbugs-common META.hbugs-thread-safe META.hbugs-client -all: $(META) -opt: -META.hbugs-common: META.hbugs-common.in - sed 's%@HBUGS_COMMON_DIR@%$(CURDIR)/../common%' < $< > $@ -META.hbugs-thread-safe: META.hbugs-thread-safe.in - sed 's%@HBUGS_COMMON_DIR@%$(CURDIR)/../common%' < $< > $@ -META.hbugs-client: META.hbugs-client.in - sed 's%@HBUGS_CLIENT_DIR@%$(CURDIR)/../client%' < $< > $@ -clean: -distclean: clean - rm -f $(META) diff --git a/helm/hbugs/test/.cvsignore b/helm/hbugs/test/.cvsignore deleted file mode 100644 index d9ed0701b..000000000 --- a/helm/hbugs/test/.cvsignore +++ /dev/null @@ -1,7 +0,0 @@ -*.cmi -*.cmo -*.cma -*.cmx -*.o -*.a -test_serialization diff --git a/helm/hbugs/test/HBUGS_MESSAGES.xml b/helm/hbugs/test/HBUGS_MESSAGES.xml deleted file mode 100644 index cf15dde3d..000000000 --- a/helm/hbugs/test/HBUGS_MESSAGES.xml +++ /dev/null @@ -1,144 +0,0 @@ - - - - - - - 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/hbugs/test/Makefile b/helm/hbugs/test/Makefile deleted file mode 100644 index 0b3debf74..000000000 --- a/helm/hbugs/test/Makefile +++ /dev/null @@ -1,5 +0,0 @@ -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/hbugs/test/test_serialization.ml b/helm/hbugs/test/test_serialization.ml deleted file mode 100644 index 1afd74379..000000000 --- a/helm/hbugs/test/test_serialization.ml +++ /dev/null @@ -1,70 +0,0 @@ -(* - * 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" -;; - diff --git a/helm/hbugs/tutors/.cvsignore b/helm/hbugs/tutors/.cvsignore deleted file mode 100644 index 601448cb6..000000000 --- a/helm/hbugs/tutors/.cvsignore +++ /dev/null @@ -1,29 +0,0 @@ -*.environment -*.cmi -*.cmo -*.cma -*.cmx -*.o -*.a -*.opt -ring_tutor.ml -fourier_tutor.ml -reflexivity_tutor.ml -symmetry_tutor.ml -assumption_tutor.ml -contradiction_tutor.ml -exists_tutor.ml -split_tutor.ml -left_tutor.ml -right_tutor.ml -ring_tutor -fourier_tutor -reflexivity_tutor -symmetry_tutor -assumption_tutor -contradiction_tutor -exists_tutor -split_tutor -left_tutor -right_tutor -search_pattern_apply_tutor diff --git a/helm/hbugs/tutors/INDEX.xml b/helm/hbugs/tutors/INDEX.xml deleted file mode 100644 index bd4baad45..000000000 --- a/helm/hbugs/tutors/INDEX.xml +++ /dev/null @@ -1,140 +0,0 @@ - - - - - - - - - 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/hbugs/tutors/Makefile b/helm/hbugs/tutors/Makefile deleted file mode 100644 index 9e84bf4e6..000000000 --- a/helm/hbugs/tutors/Makefile +++ /dev/null @@ -1,57 +0,0 @@ -METADIR = ../meta -REQUIRES = threads hbugs-common helm-cic_proof_checking helm-getter \ - helm-cic_textual_parser \ - helm-mathql helm-mathql_interpreter helm-tactics -COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -OCAMLFIND = ocamlfind -OCAMLC = $(OCAMLFIND) ocamlc -thread $(COMMONOPTS) -OCAMLOPT = $(OCAMLFIND) opt -thread $(COMMONOPTS) -OCAMLDEP = $(OCAMLFIND) ocamldep -package "$(REQUIRES)" -LINK_OPTIONS = -thread -package threads -linkpkg -TUTORS_TEMPLATE = hbugs_tutor.TPL.ml -TUTORS_INDEX = INDEX.xml -GENERATED_TUTORS = \ - ring_tutor fourier_tutor reflexivity_tutor symmetry_tutor \ - assumption_tutor contradiction_tutor exists_tutor split_tutor \ - left_tutor right_tutor -TUTORS = $(GENERATED_TUTORS) search_pattern_apply_tutor -BUILD_TUTORS = ./build_tutors.ml -CTL = ./sabba.sh -TUTORS_OPT = $(patsubst %,%.opt,$(TUTORS)) -GENERATED_TUTORS_SRC = $(patsubst %,%.ml,$(GENERATED_TUTORS)) -COMMON = hbugs_deity.cmo hbugs_tutors_common.cmo -COMMON_OPT = $(patsubst %.cmo,%.cmx,$(COMMON)) - -DEPS = $(shell $(OCAMLFIND) query -recursive -predicates byte -format "%d/%a" $(REQUIRES)) -DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%a" $(REQUIRES)) - -all: byte -world: byte opt -byte: $(COMMON) $(TUTORS) -opt: $(COMMON_OPT) $(TUTORS_OPT) -start: - $(CTL) start -stop: - $(CTL) stop - -$(GENERATED_TUTORS_SRC): $(TUTORS_TEMPLATE) $(TUTORS_INDEX) - $(BUILD_TUTORS) -%_tutor: $(DEPS) $(COMMON) %_tutor.ml - $(OCAMLC) $(LINK_OPTIONS) -o $@ $(COMMON) $*_tutor.ml -%_tutor.opt: $(DEPSOPT) $(COMMON_OPT) %_tutor.ml - $(OCAMLOPT) $(LINK_OPTIONS) -o $@ $(COMMON_OPT) $*_tutor.ml - -%.cmi: %.mli - $(OCAMLC) -c $< -%.cmo: %.ml %.cmi - $(OCAMLC) -c $< -%.cmx: %.ml %.cmi - $(OCAMLOPT) -c $< - -clean: - rm -f *.cm[aixo] *.cmxa *.[oa] $(TUTORS) $(TUTORS_OPT) $(GENERATED_TUTORS_SRC) -distclean: clean - rm -f run/* -.PHONY: all world byte opt clean start stop -.PRECIOUS: %.cmi - diff --git a/helm/hbugs/tutors/build_tutors.ml b/helm/hbugs/tutors/build_tutors.ml deleted file mode 100755 index 73ac9826e..000000000 --- a/helm/hbugs/tutors/build_tutors.ml +++ /dev/null @@ -1,118 +0,0 @@ -#!/usr/bin/ocamlrun /usr/bin/ocaml -(* - * 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/ - *) -#use "topfind";; -#require "pcre";; -#require "pxp";; -open Printf;; -open Pxp_document;; -open Pxp_dtd;; -open Pxp_types;; -open Pxp_yacc;; - -let index = "INDEX.xml" ;; -let template = "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 -;; -exception Skip;; -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 Skip - 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 Skip -> ()) -;; -main ();; - diff --git a/helm/hbugs/tutors/hbugs_deity.ml b/helm/hbugs/tutors/hbugs_deity.ml deleted file mode 100644 index 1b34e09c7..000000000 --- a/helm/hbugs/tutors/hbugs_deity.ml +++ /dev/null @@ -1,108 +0,0 @@ -(* - * 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/ - *) - -let debug = true -let debug_print s = if debug then prerr_endline s - -exception Can_t_kill of Thread.t * string (* thread, reason *) -exception Thread_not_found of Thread.t - -module OrderedPid = - struct - type t = int - let compare = Pervasives.compare - end -module PidSet = Set.Make (OrderedPid) - - (* perform an action inside a critical section controlled by given mutex *) -let do_critical mutex = - fun action -> - try - Mutex.lock mutex; - let res = Lazy.force action in - Mutex.unlock mutex; - res - with e -> Mutex.unlock mutex; raise e - -let kill_signal = Sys.sigusr2 (* signal used to kill children *) -let chan = Event.new_channel () (* communication channel between threads *) -let creation_mutex = Mutex.create () -let dead_threads_walking = ref PidSet.empty -let pids: (Thread.t, int) Hashtbl.t = Hashtbl.create 17 - - (* given a thread body (i.e. first argument of a Thread.create invocation) - return a new thread body which unblock the kill signal and send its pid to - parent over "chan" *) -let wrap_thread body = - fun arg -> - ignore (Unix.sigprocmask Unix.SIG_UNBLOCK [ kill_signal ]); - Event.sync (Event.send chan (Unix.getpid ())); - body arg - -(* -(* FAKE IMPLEMENTATION *) -let create = Thread.create -let kill _ = () -*) - -let create body arg = - do_critical creation_mutex (lazy ( - let thread_t = Thread.create (wrap_thread body) arg in - let pid = Event.sync (Event.receive chan) in - Hashtbl.add pids thread_t pid; - thread_t - )) - -let kill thread_t = - try - let pid = - try - Hashtbl.find pids thread_t - with Not_found -> raise (Thread_not_found thread_t) - in - dead_threads_walking := PidSet.add pid !dead_threads_walking; - Unix.kill pid kill_signal - with e -> raise (Can_t_kill (thread_t, Printexc.to_string e)) - - (* "kill_signal" handler, check if current process must die, if this is the - case exits with Thread.exit *) -let _ = - ignore (Sys.signal kill_signal (Sys.Signal_handle - (fun signal -> - let myself = Unix.getpid () in - match signal with - | sg when (sg = kill_signal) && - (PidSet.mem myself !dead_threads_walking) -> - dead_threads_walking := PidSet.remove myself !dead_threads_walking; - debug_print "AYEEEEH!"; - Thread.exit () - | _ -> ()))) - - (* block kill signal in main process *) -let _ = ignore (Unix.sigprocmask Unix.SIG_BLOCK [ kill_signal ]) - diff --git a/helm/hbugs/tutors/hbugs_deity.mli b/helm/hbugs/tutors/hbugs_deity.mli deleted file mode 100644 index 8ec15c0fe..000000000 --- a/helm/hbugs/tutors/hbugs_deity.mli +++ /dev/null @@ -1,33 +0,0 @@ -(* - * 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/ - *) - -exception Can_t_kill of Thread.t * string - -val create: ('a -> 'b) -> 'a -> Thread.t -val kill: Thread.t -> unit - diff --git a/helm/hbugs/tutors/hbugs_tutor.TPL.ml b/helm/hbugs/tutors/hbugs_tutor.TPL.ml deleted file mode 100644 index 1c635cece..000000000 --- a/helm/hbugs/tutors/hbugs_tutor.TPL.ml +++ /dev/null @@ -1,42 +0,0 @@ -(* - * 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_common.BuildTutor (TutorDescription) ;; -Tutor.start () ;; - diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml deleted file mode 100644 index dca58766a..000000000 --- a/helm/hbugs/tutors/hbugs_tutors_common.ml +++ /dev/null @@ -1,264 +0,0 @@ -(* - * 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 = - Hbugs_deity.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 - Hbugs_deity.kill slave_thread; - Hashtbl.remove slaves musing_id - with - | Hbugs_deity.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/hbugs/tutors/hbugs_tutors_common.mli b/helm/hbugs/tutors/hbugs_tutors_common.mli deleted file mode 100644 index 43cd99cce..000000000 --- a/helm/hbugs/tutors/hbugs_tutors_common.mli +++ /dev/null @@ -1,60 +0,0 @@ -(* - * 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/hbugs/tutors/ls_tutors.ml b/helm/hbugs/tutors/ls_tutors.ml deleted file mode 100755 index 5ddb77d45..000000000 --- a/helm/hbugs/tutors/ls_tutors.ml +++ /dev/null @@ -1,55 +0,0 @@ -#!/usr/bin/ocamlrun /usr/bin/ocaml -(* - * 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/ - *) -#use "topfind";; -#require "pxp";; -open Printf;; -open Pxp_document;; -open Pxp_dtd;; -open Pxp_types;; -open Pxp_yacc;; - -let index = "INDEX.xml" ;; -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 -> print_endline s - | _ -> assert false) - with Not_found -> assert false) - (List.filter is_tutor (parse_xml index)#root#sub_nodes) -;; -main ();; - diff --git a/helm/hbugs/tutors/run/.cvsignore b/helm/hbugs/tutors/run/.cvsignore deleted file mode 100644 index 7789b92c6..000000000 --- a/helm/hbugs/tutors/run/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.LOG diff --git a/helm/hbugs/tutors/sabba.sh b/helm/hbugs/tutors/sabba.sh deleted file mode 100755 index 55188b8c4..000000000 --- a/helm/hbugs/tutors/sabba.sh +++ /dev/null @@ -1,47 +0,0 @@ -#!/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 - -./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/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml deleted file mode 100644 index be2c68d70..000000000 --- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml +++ /dev/null @@ -1,146 +0,0 @@ - -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_common.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_common.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_common.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 = Hbugs_deity.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 - Hbugs_deity.kill (Hashtbl.find ids musing_id) ; - Hashtbl.remove ids musing_id ; - with - Not_found - | Hbugs_deity.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_common.unregister_from_broker my_own_id); - broker_id := - Some (Hbugs_tutors_common.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 () -