X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fhbugs%2Fhbugs_tutors.ml;fp=components%2Fhbugs%2Fhbugs_tutors.ml;h=ca6250262ada9961628636b98bb56705af3efcb1;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/hbugs/hbugs_tutors.ml b/components/hbugs/hbugs_tutors.ml new file mode 100644 index 000000000..ca6250262 --- /dev/null +++ b/components/hbugs/hbugs_tutors.ml @@ -0,0 +1,266 @@ +(* + * 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/ + *) + +(* $Id$ *) + +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,attrs) -> (* 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, attrs), goal) + | _ -> assert false) + in + prerr_endline "a6"; + Sys.remove tmp1; Sys.remove tmp2; + (proof, goal) + +(* tutors creation stuff from now on *) + +module type HbugsTutor = + sig + val start: unit -> unit + end + +module type HbugsTutorDescription = + sig + val addr: string + val port: int + val tactic: ProofEngineTypes.tactic + val hint: hint + val hint_type: hint_type + val description: string + val environment_file: string + end + +module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor = + struct + let broker_id = ref None + let my_own_id = init_tutor () + let my_own_addr, my_own_port = Dsc.addr, Dsc.port + let my_own_url = sprintf "%s:%d" my_own_addr my_own_port + + let is_authenticated id = + match !broker_id with + | None -> false + | Some broker_id -> id = broker_id + + (* thread who do the dirty work *) + let slave (state, musing_id) = + prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id); + let (proof, goal) = load_state state in + let success = + try + ignore (Dsc.tactic (proof, goal)); + true + with e -> false + in + let answer = + Musing_completed + (my_own_id, musing_id, (if success then Eureka Dsc.hint else Sorry)) + in + ignore (Hbugs_messages.submit_req ~url:broker_url answer); + prerr_endline + (sprintf "Bye, I've completed my duties (success = %b)" success) + + let hbugs_callback = + (* hashtbl mapping musings ids to PID of threads doing the related (dirty) + work *) + let slaves = Hashtbl.create 17 in + let forbidden () = + prerr_endline "ignoring request from unauthorized broker"; + Exception ("forbidden", "") + in + function (* _the_ callback *) + | Start_musing (broker_id, state) -> + if is_authenticated broker_id then begin + prerr_endline "received Start_musing"; + let new_musing_id = Hbugs_id_generator.new_musing_id () in + prerr_endline + (sprintf "starting a new musing (id = %s)" new_musing_id); +(* let slave_thread = Thread.create slave (state, new_musing_id) in *) + let slave_thread = + ExtThread.create slave (state, new_musing_id) + in + Hashtbl.add slaves new_musing_id slave_thread; + Musing_started (my_own_id, new_musing_id) + end else (* broker unauthorized *) + forbidden (); + | Abort_musing (broker_id, musing_id) -> + if is_authenticated broker_id then begin + (try (* kill thread responsible for "musing_id" *) + let slave_thread = Hashtbl.find slaves musing_id in + ExtThread.kill slave_thread; + Hashtbl.remove slaves musing_id + with + | ExtThread.Can_t_kill (_, reason) -> + prerr_endline (sprintf "Unable to kill slave: %s" reason) + | Not_found -> + prerr_endline (sprintf + "Can't find slave corresponding to musing %s, can't kill it" + musing_id)); + Musing_aborted (my_own_id, musing_id) + end else (* broker unauthorized *) + forbidden (); + | unexpected_msg -> + Exception ("unexpected_msg", + Hbugs_messages.string_of_msg unexpected_msg) + + let callback (req: Http_types.request) outchan = + try + let req_msg = Hbugs_messages.msg_of_string req#body in + let answer = hbugs_callback req_msg in + Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan + with Hbugs_messages.Parse_error (subj, reason) -> + Http_daemon.respond + ~body:(Hbugs_messages.string_of_msg + (Exception ("parse_error", reason))) + outchan + + let restore_environment () = + let ic = open_in Dsc.environment_file in + prerr_endline "Restoring environment ..."; + CicEnvironment.restore_from_channel + ~callback:(fun uri -> prerr_endline uri) ic; + prerr_endline "... done!"; + close_in ic + + let dump_environment () = + let oc = open_out Dsc.environment_file in + prerr_endline "Dumping environment ..."; + CicEnvironment.dump_to_channel + ~callback:(fun uri -> prerr_endline uri) oc; + prerr_endline "... done!"; + close_out oc + + let main () = + try + Sys.catch_break true; + at_exit (fun () -> + if dump_environment_on_exit then + dump_environment (); + unregister_from_broker my_own_id); + broker_id := + Some (register_to_broker + my_own_id my_own_url Dsc.hint_type Dsc.description); + if Sys.file_exists Dsc.environment_file then + restore_environment (); + Http_daemon.start' + ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback + with Sys.Break -> () (* exit nicely, invoking at_exit functions *) + + let start = main + + end +