]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/hbugs/search_pattern_apply_tutor.ml
handles bad Appl
[helm.git] / helm / software / components / hbugs / search_pattern_apply_tutor.ml
1 (* $Id$ *)
2
3 open Hbugs_types;;
4 open Printf;;
5
6 exception Empty_must;;
7
8 module MQI  = MQueryInterpreter
9 module MQIC = MQIConn
10
11 let broker_id = ref None
12 let my_own_id = Hbugs_tutors.init_tutor ()
13 let my_own_addr, my_own_port = "127.0.0.1", 50011
14 let my_own_url = sprintf "%s:%d" my_own_addr my_own_port
15 let environment_file = "search_pattern_apply.environment"
16 let dump_environment_on_exit = false
17
18 let is_authenticated id =
19   match !broker_id with
20   | None -> false
21   | Some broker_id -> id = broker_id
22
23   (* thread who do the dirty work *)
24 let slave mqi_handle (state, musing_id) =
25  try
26   prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
27   let (proof, goal) = Hbugs_tutors.load_state state in
28   let hint =
29     try
30       let choose_must must only = (* euristic: use 2nd precision level
31                                   1st is more precise but is more slow *)
32         match must with
33         | [] -> raise Empty_must
34         | _::hd::tl -> hd
35         | hd::tl -> hd
36       in
37       let uris =
38         TacticChaser.matchConclusion mqi_handle
39          ~output_html:prerr_endline ~choose_must () ~status:(proof, goal)
40       in
41       if uris = [] then
42         Sorry
43       else
44         Eureka (Hints (List.map (fun uri -> Use_apply uri) uris))
45     with Empty_must -> Sorry
46   in
47   let answer = Musing_completed (my_own_id, musing_id, hint) in
48   ignore (Hbugs_messages.submit_req ~url:Hbugs_tutors.broker_url answer);
49   prerr_endline
50     (sprintf "Bye, I've completed my duties (success = %b)" (hint <> Sorry))
51  with
52   (Pxp_types.At _) as e ->
53     let rec unbox_exception =
54      function
55          Pxp_types.At (_,e) -> unbox_exception e
56       | e -> e
57     in
58      prerr_endline ("Uncaught PXP exception: " ^ Pxp_types.string_of_exn e) ;
59      (* e could be the Thread.exit exception; otherwise we will release an  *)
60      (* uncaught exception and the Pxp_types.At was already an uncaught     *)
61      (* exception ==> no additional arm                                     *)
62      raise (unbox_exception e)
63
64 let hbugs_callback mqi_handle =
65   let ids = Hashtbl.create 17 in
66   let forbidden () =
67     prerr_endline "ignoring request from unauthorized broker";
68     Exception ("forbidden", "")
69   in
70   function
71   | Start_musing (broker_id, state) ->
72       if is_authenticated broker_id then begin
73         prerr_endline "received Start_musing";
74         let new_musing_id = Hbugs_id_generator.new_musing_id () in
75         let id = ExtThread.create (slave mqi_handle) (state, new_musing_id) in
76         prerr_endline (sprintf "starting a new musing (id = %s)" 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           ExtThread.kill (Hashtbl.find ids musing_id) ;
88           Hashtbl.remove ids musing_id ;
89          with
90             Not_found
91           | ExtThread.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   try
129     Sys.catch_break true;
130     at_exit (fun () ->
131       if dump_environment_on_exit then
132         dump_environment ();
133       Hbugs_tutors.unregister_from_broker my_own_id);
134     broker_id :=
135       Some (Hbugs_tutors.register_to_broker
136         my_own_id my_own_url "FOO" "Search_pattern_apply tutor");
137     let mqi_handle = MQIC.init ~log:prerr_string () in 
138     if Sys.file_exists environment_file then
139       restore_environment ();
140     Http_daemon.start'
141       ~addr:my_own_addr ~port:my_own_port ~mode:`Thread (callback mqi_handle);
142     MQIC.close mqi_handle
143   with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
144 ;;
145
146 main ()
147