helm/hbugs/tutors/search_pattern_apply_tutor.ml

   1
   2 open Hbugs_types;;
   3 open Printf;;
   4
   5 exception Empty_must;;
   6
   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
  11
  12 let is_authenticated id =
  13   match !broker_id with
  14   | None -> false
  15   | Some broker_id -> id = broker_id
  16
  17   (* thread who do the dirty work *)
  18 let slave (state, musing_id) =
  19  try
  20   prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
  21   let (proof, goal) = Hbugs_tutors_common.load_state state in
  22   let hint =
  23     try
  24       let choose_must must only = (* euristic: use 2nd precision level
  25                                   1st is more precise but is more slow *)
  26         match must with
  27         | [] -> raise Empty_must
  28         | _::hd::tl -> hd
  29         | hd::tl -> hd
  30       in
  31       let uris =
  32         TacticChaser.searchPattern
  33          ~output_html:prerr_endline ~choose_must () ~status:(proof, goal)
  34       in
  35       if uris = [] then
  36         Sorry
  37       else
  38         Eureka (Hints (List.map (fun uri -> Use_apply_Luke uri) uris))
  39     with Empty_must -> Sorry
  40   in
  41   let answer = Musing_completed (my_own_id, musing_id, hint) in
  42   ignore (Hbugs_messages.submit_req ~url:Hbugs_tutors_common.broker_url answer);
  43   prerr_endline
  44     (sprintf "Bye, I've completed my duties (success = %b)" (hint <> Sorry))
  45  with
  46   (Pxp_types.At _) as e ->
  47     let rec unbox_exception =
  48      function
  49          Pxp_types.At (_,e) -> unbox_exception e
  50       | e -> e
  51     in
  52      prerr_endline ("Uncaught PXP exception: " ^ Pxp_types.string_of_exn e) ;
  53      (* e could be the Thread.exit exception; otherwise we will release an  *)
  54      (* uncaught exception and the Pxp_types.At was already an uncaught     *)
  55      (* exception ==> no additional arm                                     *)
  56      raise (unbox_exception e)
  57
  58 let hbugs_callback =
  59   let ids = Hashtbl.create 17 in
  60   let forbidden () =
  61     prerr_endline "ignoring request from unauthorized broker";
  62     Exception ("forbidden", "")
  63   in
  64   function
  65   | Start_musing (broker_id, state) ->
  66       if is_authenticated broker_id then begin
  67         prerr_endline "received Start_musing";
  68         let new_musing_id = Hbugs_id_generator.new_musing_id () in
  69         let id = Hbugs_deity.create slave (state, new_musing_id) in
  70         prerr_endline
  71          (sprintf "starting a new musing (tid = %d, id = %s)" id new_musing_id);
  72         Hashtbl.add ids new_musing_id id ;
  73         (*ignore (Thread.create slave (state, new_musing_id));*)
  74         Musing_started (my_own_id, new_musing_id)
  75       end else  (* broker unauthorized *)
  76         forbidden ();
  77   | Abort_musing (broker_id, musing_id) ->
  78       prerr_endline "CSC: Abort_musing received" ;
  79       if is_authenticated broker_id then begin
  80         (* prerr_endline "Ignoring 'Abort_musing' message ..."; *)
  81         (try
  82           Hbugs_deity.kill (Hashtbl.find ids musing_id) ;
  83           Hashtbl.remove ids musing_id ;
  84          with
  85             Not_found
  86           | Hbugs_deity.Can_t_kill _ ->
  87              prerr_endline ("Can not kill slave " ^ musing_id)) ;
  88         Musing_aborted (my_own_id, musing_id)
  89       end else (* broker unauthorized *)
  90         forbidden ();
  91   | unexpected_msg ->
  92       Exception ("unexpected_msg",
  93         Hbugs_messages.string_of_msg unexpected_msg)
  94
  95 let callback (req: Http_types.request) outchan =
  96   try
  97     let req_msg = Hbugs_messages.msg_of_string req#body in
  98     let answer = hbugs_callback req_msg in
  99     Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan
 100   with Hbugs_messages.Parse_error (subj, reason) ->
 101     Http_daemon.respond
 102       ~body:(Hbugs_messages.string_of_msg
 103         (Exception ("parse_error", reason)))
 104       outchan
 105
 106 let postgresqlconnectionstring =
 107  try
 108   Sys.getenv "POSTGRESQL_CONNECTION_STRING"
 109  with
 110   Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
 111 ;;
 112
 113 let main () =
 114   try
 115     Sys.catch_break true;
 116     at_exit (fun () -> Hbugs_tutors_common.unregister_from_broker my_own_id);
 117     broker_id :=
 118       Some (Hbugs_tutors_common.register_to_broker
 119         my_own_id my_own_url "FOO" "Search_pattern_apply tutor");
 120     Mqint.set_database Mqint.postgres_db ;
 121     Mqint.init postgresqlconnectionstring ;
 122     Http_daemon.start'
 123       ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback;
 124     Mqint.close ()
 125   with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
 126 ;;
 127
 128 main ()
 129