]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/hbugs/search_pattern_apply_tutor.ml
removed a comment/bug report about let..in rendering, now fixed
[helm.git] / helm / ocaml / hbugs / 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.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.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 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.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 = ExtThread.create (slave mqi_handle) (state, new_musing_id) in
75         prerr_endline (sprintf "starting a new musing (id = %s)" new_musing_id);
76         Hashtbl.add ids new_musing_id id;
77         (*ignore (Thread.create slave (state, new_musing_id));*)
78         Musing_started (my_own_id, new_musing_id)
79       end else  (* broker unauthorized *)
80         forbidden ();
81   | Abort_musing (broker_id, musing_id) ->
82       prerr_endline "CSC: Abort_musing received" ;
83       if is_authenticated broker_id then begin
84         (* prerr_endline "Ignoring 'Abort_musing' message ..."; *)
85         (try
86           ExtThread.kill (Hashtbl.find ids musing_id) ;
87           Hashtbl.remove ids musing_id ;
88          with
89             Not_found
90           | ExtThread.Can_t_kill _ ->
91              prerr_endline ("Can not kill slave " ^ musing_id)) ;
92         Musing_aborted (my_own_id, musing_id)
93       end else (* broker unauthorized *)
94         forbidden ();
95   | unexpected_msg ->
96       Exception ("unexpected_msg",
97         Hbugs_messages.string_of_msg unexpected_msg)
98
99 let callback mqi_handle (req: Http_types.request) outchan =
100   try
101     let req_msg = Hbugs_messages.msg_of_string req#body in
102     let answer = hbugs_callback mqi_handle req_msg in
103     Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan
104   with Hbugs_messages.Parse_error (subj, reason) ->
105     Http_daemon.respond
106       ~body:(Hbugs_messages.string_of_msg
107         (Exception ("parse_error", reason)))
108       outchan
109
110 let restore_environment () =
111   let ic = open_in environment_file in
112   prerr_endline "Restoring environment ...";
113   CicEnvironment.restore_from_channel
114     ~callback:(fun uri -> prerr_endline uri) ic;
115   prerr_endline "... done!";
116   close_in ic
117
118 let dump_environment () =
119   let oc = open_out environment_file in
120   prerr_endline "Dumping environment ...";
121   CicEnvironment.dump_to_channel
122     ~callback:(fun uri -> prerr_endline uri) oc;
123   prerr_endline "... done!";
124   close_out oc
125
126 let main () =
127   try
128     Sys.catch_break true;
129     at_exit (fun () ->
130       if dump_environment_on_exit then
131         dump_environment ();
132       Hbugs_tutors.unregister_from_broker my_own_id);
133     broker_id :=
134       Some (Hbugs_tutors.register_to_broker
135         my_own_id my_own_url "FOO" "Search_pattern_apply tutor");
136     let mqi_handle = MQIC.init ~log:prerr_string () in 
137     if Sys.file_exists environment_file then
138       restore_environment ();
139     Http_daemon.start'
140       ~addr:my_own_addr ~port:my_own_port ~mode:`Thread (callback mqi_handle);
141     MQIC.close mqi_handle
142   with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
143 ;;
144
145 main ()
146