helm/hbugs/tutors/search_pattern_apply_tutor.ml

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