+++ /dev/null
-(*
- * Copyright (C) 2003:
- * Stefano Zacchiroli <zack@cs.unibo.it>
- * 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
- "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n" ^
- "<!DOCTYPE " ^ root ^ " SYSTEM \""^ dtdname ^ "\">\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
-
projects / helm.git / blobdiff