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
| Some broker_id -> id = broker_id
(* thread who do the dirty work *)
-let slave (state, musing_id) =
+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 =
| hd::tl -> hd
in
let uris =
- TacticChaser.searchPattern ~choose_must () ~status:(proof, goal)
-(* ["cic:/pippo.con"; "cic:/pluto.con"] *)
+ TacticChaser.matchConclusion mqi_handle
+ ~output_html:prerr_endline ~choose_must () ~status:(proof, goal)
in
if uris = [] then
Sorry
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 =
+let hbugs_callback mqi_handle =
+ let ids = Hashtbl.create 17 in
let forbidden () =
prerr_endline "ignoring request from unauthorized broker";
Exception ("forbidden", "")
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);
- ignore (Thread.create slave (state, new_musing_id));
+ (sprintf "starting a new musing (tid = %d, id = %s)" id 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 ...";
+ (* 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 ();
Exception ("unexpected_msg",
Hbugs_messages.string_of_msg unexpected_msg)
-let callback (req: Http_types.request) outchan =
+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 req_msg 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
(Exception ("parse_error", reason)))
outchan
-let postgresqlconnectionstring =
- try
- Sys.getenv "POSTGRESQL_CONNECTION_STRING"
- with
- Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
-;;
-
let main () =
+ let mqi_flags = [] in (* default MathQL interpreter options *)
try
Sys.catch_break true;
at_exit (fun () -> 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");
- Mqint.set_database Mqint.postgres_db ;
- Mqint.init postgresqlconnectionstring ;
+ let mqi_handle = MQIC.init mqi_flags prerr_string in
Http_daemon.start'
- ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback;
- Mqint.close ()
+ ~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 *)
;;