]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/hbugs/hbugs_tutors.ml
we were generating a name for the main fix twice
[helm.git] / helm / software / components / hbugs / hbugs_tutors.ml
1 (*
2  * Copyright (C) 2003:
3  *    Stefano Zacchiroli <zack@cs.unibo.it>
4  *    for the HELM Team http://helm.cs.unibo.it/
5  *
6  *  This file is part of HELM, an Hypertextual, Electronic
7  *  Library of Mathematics, developed at the Computer Science
8  *  Department, University of Bologna, Italy.
9  *
10  *  HELM is free software; you can redistribute it and/or
11  *  modify it under the terms of the GNU General Public License
12  *  as published by the Free Software Foundation; either version 2
13  *  of the License, or (at your option) any later version.
14  *
15  *  HELM is distributed in the hope that it will be useful,
16  *  but WITHOUT ANY WARRANTY; without even the implied warranty of
17  *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
18  *  GNU General Public License for more details.
19  *
20  *  You should have received a copy of the GNU General Public License
21  *  along with HELM; if not, write to the Free Software
22  *  Foundation, Inc., 59 Temple Place - Suite 330, Boston,
23  *  MA  02111-1307, USA.
24  *
25  *  For details, see the HELM World-Wide-Web page,
26  *  http://helm.cs.unibo.it/
27  *)
28
29 (* $Id$ *)
30
31 open Hbugs_types;;
32 open Printf;;
33
34 let broker_url = "localhost:49081/act";;
35 let dump_environment_on_exit = false;;
36
37 let init_tutor = Hbugs_id_generator.new_tutor_id;;
38
39   (** register a tutor to broker *)
40 let register_to_broker id url hint_type dsc =
41   try
42     let res =
43       Hbugs_messages.submit_req
44         ~url:broker_url (Register_tutor (id, url, hint_type, dsc))
45     in
46     (match res with
47     | Tutor_registered id ->
48         prerr_endline (sprintf "Tutor registered, broker id: %s" id);
49         id
50     | unexpected_msg ->
51         raise (Hbugs_messages.Unexpected_message unexpected_msg))
52   with e ->
53     failwith (sprintf "Can't register tutor to broker: uncaught exception: %s"
54       (Printexc.to_string e))
55 ;;
56   (** unregister a tutor from the broker *)
57 let unregister_from_broker id =
58   let res = Hbugs_messages.submit_req ~url:broker_url (Unregister_tutor id) in
59   match res with
60   | Tutor_unregistered _ -> prerr_endline "Tutor unregistered!"
61   | unexpected_msg ->
62       failwith
63         (sprintf "Can't unregister from broker, received unexpected msg: %s"
64           (Hbugs_messages.string_of_msg unexpected_msg))
65 ;;
66
67   (* typecheck a loaded proof *)
68   (* TODO this is a cut and paste from gTopLevel.ml *)
69 let typecheck_loaded_proof metasenv bo ty =
70  let module T = CicTypeChecker in
71   ignore (
72    List.fold_left
73     (fun metasenv ((_,context,ty) as conj) ->
74       ignore (T.type_of_aux' metasenv context ty) ;
75       metasenv @ [conj]
76     ) [] metasenv) ;
77   ignore (T.type_of_aux' metasenv [] ty) ;
78   ignore (T.type_of_aux' metasenv [] bo)
79 ;;
80
81 type xml_kind = Body | Type;;
82 let mk_dtdname ~ask_dtd_to_the_getter dtd =
83  if ask_dtd_to_the_getter then
84   Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
85  else
86   "http://mowgli.cs.unibo.it/dtd/" ^ dtd
87 ;;  
88   (** this function must be the inverse function of GTopLevel.strip_xml_headings
89   *)
90 let add_xml_headings ~kind s =
91   let dtdname = mk_dtdname ~ask_dtd_to_the_getter:true "cic.dtd" in
92   let root =
93     match kind with
94     | Body -> "CurrentProof"
95     | Type -> "ConstantType"
96   in
97   "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n" ^
98   "<!DOCTYPE " ^ root ^ " SYSTEM \""^ dtdname ^ "\">\n\n" ^
99   s
100 ;;
101
102 let load_state (type_string, body_string, goal) =
103   prerr_endline "a0";
104   let ((tmp1, oc1), (tmp2, oc2)) =
105     (Filename.open_temp_file "" "", Filename.open_temp_file "" "")
106   in
107   prerr_endline "a1";
108   output_string oc1 (add_xml_headings ~kind:Type type_string);
109   output_string oc2 (add_xml_headings ~kind:Body body_string);
110   close_out oc1; close_out oc2;
111   prerr_endline (sprintf "Proof Type available in %s" tmp1);
112   prerr_endline (sprintf "Proof Body available in %s" tmp2);
113   let (proof, goal) =
114     prerr_endline "a2";
115     (match CicParser.obj_of_xml tmp1 (Some tmp2) with
116     | Cic.CurrentProof (_,metasenv,bo,ty,attrs) ->  (* TODO il primo argomento e' una URI valida o e' casuale? *)
117         prerr_endline "a3";
118         let uri = UriManager.uri_of_string "cic:/foo.con" in
119         prerr_endline "a4";
120         typecheck_loaded_proof metasenv bo ty;
121         prerr_endline "a5";
122         ((uri, metasenv, bo, ty, attrs), goal)
123     | _ -> assert false)
124   in
125   prerr_endline "a6";
126   Sys.remove tmp1; Sys.remove tmp2;
127   (proof, goal)
128
129 (* tutors creation stuff from now on *)
130
131 module type HbugsTutor =
132   sig
133     val start: unit -> unit
134   end
135
136 module type HbugsTutorDescription =
137   sig
138     val addr: string
139     val port: int
140     val tactic: ProofEngineTypes.tactic
141     val hint: hint
142     val hint_type: hint_type
143     val description: string
144     val environment_file: string
145   end
146
147 module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
148   struct
149     let broker_id = ref None
150     let my_own_id = init_tutor ()
151     let my_own_addr, my_own_port = Dsc.addr, Dsc.port
152     let my_own_url = sprintf "%s:%d" my_own_addr my_own_port
153
154     let is_authenticated id =
155       match !broker_id with
156       | None -> false
157       | Some broker_id -> id = broker_id
158
159       (* thread who do the dirty work *)
160     let slave (state, musing_id) =
161       prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
162       let (proof, goal) = load_state state in
163       let success =
164         try
165           ignore (Dsc.tactic (proof, goal));
166           true
167         with e -> false
168       in
169       let answer = 
170         Musing_completed
171           (my_own_id, musing_id, (if success then Eureka Dsc.hint else Sorry))
172       in
173       ignore (Hbugs_messages.submit_req ~url:broker_url answer);
174       prerr_endline
175         (sprintf "Bye, I've completed my duties (success = %b)" success)
176
177     let hbugs_callback =
178         (* hashtbl mapping musings ids to PID of threads doing the related (dirty)
179         work *)
180       let slaves = Hashtbl.create 17 in
181       let forbidden () =
182         prerr_endline "ignoring request from unauthorized broker";
183         Exception ("forbidden", "")
184       in
185       function  (* _the_ callback *)
186       | Start_musing (broker_id, state) ->
187           if is_authenticated broker_id then begin
188             prerr_endline "received Start_musing";
189             let new_musing_id = Hbugs_id_generator.new_musing_id () in
190             prerr_endline
191               (sprintf "starting a new musing (id = %s)" new_musing_id);
192 (*             let slave_thread = Thread.create slave (state, new_musing_id) in *)
193             let slave_thread =
194               ExtThread.create slave (state, new_musing_id)
195             in
196             Hashtbl.add slaves new_musing_id slave_thread;
197             Musing_started (my_own_id, new_musing_id)
198           end else  (* broker unauthorized *)
199             forbidden ();
200       | Abort_musing (broker_id, musing_id) ->
201           if is_authenticated broker_id then begin
202             (try  (* kill thread responsible for "musing_id" *)
203               let slave_thread = Hashtbl.find slaves musing_id in
204               ExtThread.kill slave_thread;
205               Hashtbl.remove slaves musing_id
206             with
207             | ExtThread.Can_t_kill (_, reason) ->
208                 prerr_endline (sprintf "Unable to kill slave: %s" reason)
209             | Not_found ->
210                 prerr_endline (sprintf
211                   "Can't find slave corresponding to musing %s, can't kill it"
212                   musing_id));
213             Musing_aborted (my_own_id, musing_id)
214           end else (* broker unauthorized *)
215             forbidden ();
216       | unexpected_msg ->
217           Exception ("unexpected_msg",
218             Hbugs_messages.string_of_msg unexpected_msg)
219
220     let callback (req: Http_types.request) outchan =
221       try
222         let req_msg = Hbugs_messages.msg_of_string req#body in
223         let answer = hbugs_callback req_msg in
224         Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan
225       with Hbugs_messages.Parse_error (subj, reason) ->
226         Http_daemon.respond
227           ~body:(Hbugs_messages.string_of_msg
228             (Exception ("parse_error", reason)))
229           outchan
230
231     let restore_environment () =
232       let ic = open_in Dsc.environment_file in
233       prerr_endline "Restoring environment ...";
234       CicEnvironment.restore_from_channel
235         ~callback:(fun uri -> prerr_endline uri) ic;
236       prerr_endline "... done!";
237       close_in ic
238
239     let dump_environment () =
240       let oc = open_out Dsc.environment_file in
241       prerr_endline "Dumping environment ...";
242       CicEnvironment.dump_to_channel
243         ~callback:(fun uri -> prerr_endline uri) oc;
244       prerr_endline "... done!";
245       close_out oc
246
247     let main () =
248       try
249         Sys.catch_break true;
250         at_exit (fun () ->
251           if dump_environment_on_exit then
252             dump_environment ();
253           unregister_from_broker my_own_id);
254         broker_id :=
255           Some (register_to_broker
256             my_own_id my_own_url Dsc.hint_type Dsc.description);
257         if Sys.file_exists Dsc.environment_file then
258           restore_environment ();
259         Http_daemon.start'
260           ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback
261       with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
262
263     let start = main
264
265   end
266