+++ /dev/null
-
-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.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.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.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 = ExtThread.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
- ExtThread.kill (Hashtbl.find ids musing_id) ;
- Hashtbl.remove ids musing_id ;
- with
- Not_found
- | ExtThread.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.unregister_from_broker my_own_id);
- broker_id :=
- Some (Hbugs_tutors.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 ()
-
projects / helm.git / blobdiff