7 let broker_id = ref None
8 let my_own_id = Hbugs_tutors_common.init_tutor ()
9 let my_own_addr, my_own_port = "127.0.0.1", 50011
10 let my_own_url = sprintf "%s:%d" my_own_addr my_own_port
12 let is_authenticated id =
15 | Some broker_id -> id = broker_id
17 (* thread who do the dirty work *)
18 let slave (state, musing_id) =
19 prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
20 let (proof, goal) = Hbugs_tutors_common.load_state state in
23 let choose_must must only = (* euristic: use 2nd precision level
24 1st is more precise but is more slow *)
26 | [] -> raise Empty_must
31 TacticChaser.searchPattern ~choose_must () ~status:(proof, goal)
32 (* ["cic:/pippo.con"; "cic:/pluto.con"] *)
37 Eureka (Hints (List.map (fun uri -> Use_apply_Luke uri) uris))
38 with Empty_must -> Sorry
40 let answer = Musing_completed (my_own_id, musing_id, hint) in
41 ignore (Hbugs_messages.submit_req ~url:Hbugs_tutors_common.broker_url answer);
43 (sprintf "Bye, I've completed my duties (success = %b)" (hint <> Sorry))
47 prerr_endline "ignoring request from unauthorized broker";
48 Exception ("forbidden", "")
51 | Start_musing (broker_id, state) ->
52 if is_authenticated broker_id then begin
53 prerr_endline "received Start_musing";
54 let new_musing_id = Hbugs_id_generator.new_musing_id () in
56 (sprintf "starting a new musing (id = %s)" new_musing_id);
57 ignore (Thread.create slave (state, new_musing_id));
58 Musing_started (my_own_id, new_musing_id)
59 end else (* broker unauthorized *)
61 | Abort_musing (broker_id, musing_id) ->
62 if is_authenticated broker_id then begin
63 prerr_endline "Ignoring 'Abort_musing' message ...";
64 Musing_aborted (my_own_id, musing_id)
65 end else (* broker unauthorized *)
68 Exception ("unexpected_msg",
69 Hbugs_messages.string_of_msg unexpected_msg)
71 let callback (req: Http_types.request) outchan =
73 let req_msg = Hbugs_messages.msg_of_string req#body in
74 let answer = hbugs_callback req_msg in
75 Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan
76 with Hbugs_messages.Parse_error (subj, reason) ->
78 ~body:(Hbugs_messages.string_of_msg
79 (Exception ("parse_error", reason)))
82 let postgresqlconnectionstring =
84 Sys.getenv "POSTGRESQL_CONNECTION_STRING"
86 Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
92 at_exit (fun () -> Hbugs_tutors_common.unregister_from_broker my_own_id);
94 Some (Hbugs_tutors_common.register_to_broker
95 my_own_id my_own_url "FOO" "Search_pattern_apply tutor");
96 Mqint.set_database Mqint.postgres_db ;
97 Mqint.init postgresqlconnectionstring ;
99 ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback;
101 with Sys.Break -> () (* exit nicely, invoking at_exit functions *)