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   prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
  20   let (proof, goal) = Hbugs_tutors_common.load_state state in
  21   let hint =
  22     try
  23       let choose_must must only = (* euristic: use 2nd precision level
  24                                   1st is more precise but is more slow *)
  25         match must with
  26         | [] -> raise Empty_must
  27         | _::hd::tl -> hd
  28         | hd::tl -> hd
  29       in
  30       let uris =
  31         TacticChaser.searchPattern ~choose_must () ~status:(proof, goal)
  32 (*         ["cic:/pippo.con"; "cic:/pluto.con"] *)
  33       in
  34       if uris = [] then
  35         Sorry
  36       else
  37         Eureka (Hints (List.map (fun uri -> Use_apply_Luke uri) uris))
  38     with Empty_must -> Sorry
  39   in
  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);
  42   prerr_endline
  43     (sprintf "Bye, I've completed my duties (success = %b)" (hint <> Sorry))
  44
  45 let hbugs_callback =
  46   let forbidden () =
  47     prerr_endline "ignoring request from unauthorized broker";
  48     Exception ("forbidden", "")
  49   in
  50   function
  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
  55         prerr_endline
  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 *)
  60         forbidden ();
  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 *)
  66         forbidden ();
  67   | unexpected_msg ->
  68       Exception ("unexpected_msg",
  69         Hbugs_messages.string_of_msg unexpected_msg)
  70
  71 let callback (req: Http_types.request) outchan =
  72   try
  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) ->
  77     Http_daemon.respond
  78       ~body:(Hbugs_messages.string_of_msg
  79         (Exception ("parse_error", reason)))
  80       outchan
  81
  82 let postgresqlconnectionstring =
  83  try
  84   Sys.getenv "POSTGRESQL_CONNECTION_STRING"
  85  with
  86   Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
  87 ;;
  88
  89 let main () =
  90   try
  91     Sys.catch_break true;
  92     at_exit (fun () -> Hbugs_tutors_common.unregister_from_broker my_own_id);
  93     broker_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 ;
  98     Http_daemon.start'
  99       ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback;
 100     Mqint.close ()
 101   with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
 102 ;;
 103
 104 main ()
 105