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