open Hbugs_types;; open Printf;; exception Empty_must;; 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 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) = Hbugs_tutors_common.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.searchPattern ~choose_must () ~status:(proof, goal) (* ["cic:/pippo.con"; "cic:/pluto.con"] *) 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_common.broker_url answer); prerr_endline (sprintf "Bye, I've completed my duties (success = %b)" (hint <> Sorry)) let hbugs_callback = 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 prerr_endline (sprintf "starting a new musing (id = %s)" new_musing_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) -> if is_authenticated broker_id then begin prerr_endline "Ignoring 'Abort_musing' message ..."; 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 postgresqlconnectionstring = try Sys.getenv "POSTGRESQL_CONNECTION_STRING" with Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" ;; let main () = 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 ; Http_daemon.start' ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback; Mqint.close () with Sys.Break -> () (* exit nicely, invoking at_exit functions *) ;; main ()