X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Ftutors%2Fhbugs_tutors_common.ml;fp=helm%2Fhbugs%2Ftutors%2Fhbugs_tutors_common.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=ca3de9fed48335036e6b384796e3ea414de817a1;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml deleted file mode 100644 index ca3de9fed..000000000 --- a/helm/hbugs/tutors/hbugs_tutors_common.ml +++ /dev/null @@ -1,241 +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 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 - Configuration.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 - 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 (pid, reason) -> - prerr_endline (sprintf "Unable to kill slave %d: %s" pid 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 main () = - try - Sys.catch_break true; - at_exit (fun () -> unregister_from_broker my_own_id); - broker_id := - Some (register_to_broker - my_own_id my_own_url Dsc.hint_type Dsc.description); - 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 -