]> matita.cs.unibo.it Git - helm.git/blob - helm/hbugs/tutors/hbugs_tutors_common.ml
- addead autoconf-iguration. Actually it only set the default runtime
[helm.git] / helm / hbugs / tutors / hbugs_tutors_common.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 open Hbugs_types;;
30 open Printf;;
31
32 let broker_url = "localhost:49081/act";;
33 let dump_environment_on_exit = false;;
34
35 let init_tutor = Hbugs_id_generator.new_tutor_id;;
36
37   (** register a tutor to broker *)
38 let register_to_broker id url hint_type dsc =
39   try
40     let res =
41       Hbugs_messages.submit_req
42         ~url:broker_url (Register_tutor (id, url, hint_type, dsc))
43     in
44     (match res with
45     | Tutor_registered id ->
46         prerr_endline (sprintf "Tutor registered, broker id: %s" id);
47         id
48     | unexpected_msg ->
49         raise (Hbugs_messages.Unexpected_message unexpected_msg))
50   with e ->
51     failwith (sprintf "Can't register tutor to broker: uncaught exception: %s"
52       (Printexc.to_string e))
53 ;;
54   (** unregister a tutor from the broker *)
55 let unregister_from_broker id =
56   let res = Hbugs_messages.submit_req ~url:broker_url (Unregister_tutor id) in
57   match res with
58   | Tutor_unregistered _ -> prerr_endline "Tutor unregistered!"
59   | unexpected_msg ->
60       failwith
61         (sprintf "Can't unregister from broker, received unexpected msg: %s"
62           (Hbugs_messages.string_of_msg unexpected_msg))
63 ;;
64
65   (* typecheck a loaded proof *)
66   (* TODO this is a cut and paste from gTopLevel.ml *)
67 let typecheck_loaded_proof metasenv bo ty =
68  let module T = CicTypeChecker in
69   ignore (
70    List.fold_left
71     (fun metasenv ((_,context,ty) as conj) ->
72       ignore (T.type_of_aux' metasenv context ty) ;
73       metasenv @ [conj]
74     ) [] metasenv) ;
75   ignore (T.type_of_aux' metasenv [] ty) ;
76   ignore (T.type_of_aux' metasenv [] bo)
77 ;;
78
79 type xml_kind = Body | Type;;
80 let mk_dtdname ~ask_dtd_to_the_getter dtd =
81  if ask_dtd_to_the_getter then
82   Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
83  else
84   "http://mowgli.cs.unibo.it/dtd/" ^ dtd
85 ;;  
86   (** this function must be the inverse function of GTopLevel.strip_xml_headings
87   *)
88 let add_xml_headings ~kind s =
89   let dtdname = mk_dtdname ~ask_dtd_to_the_getter:true "cic.dtd" in
90   let root =
91     match kind with
92     | Body -> "CurrentProof"
93     | Type -> "ConstantType"
94   in
95   "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n" ^
96   "<!DOCTYPE " ^ root ^ " SYSTEM \""^ dtdname ^ "\">\n\n" ^
97   s
98 ;;
99
100 let load_state (type_string, body_string, goal) =
101   prerr_endline "a0";
102   let ((tmp1, oc1), (tmp2, oc2)) =
103     (Filename.open_temp_file "" "", Filename.open_temp_file "" "")
104   in
105   prerr_endline "a1";
106   output_string oc1 (add_xml_headings ~kind:Type type_string);
107   output_string oc2 (add_xml_headings ~kind:Body body_string);
108   close_out oc1; close_out oc2;
109   prerr_endline (sprintf "Proof Type available in %s" tmp1);
110   prerr_endline (sprintf "Proof Body available in %s" tmp2);
111   let (proof, goal) =
112     prerr_endline "a2";
113     (match CicParser.obj_of_xml tmp1 (Some tmp2) with
114     | Cic.CurrentProof (_,metasenv,bo,ty,_) ->  (* TODO il primo argomento e' una URI valida o e' casuale? *)
115         prerr_endline "a3";
116         let uri = UriManager.uri_of_string "cic:/foo.con" in
117         prerr_endline "a4";
118         typecheck_loaded_proof metasenv bo ty;
119         prerr_endline "a5";
120         ((uri, metasenv, bo, ty), goal)
121     | _ -> assert false)
122   in
123   prerr_endline "a6";
124   Sys.remove tmp1; Sys.remove tmp2;
125   (proof, goal)
126
127 (* tutors creation stuff from now on *)
128
129 module type HbugsTutor =
130   sig
131     val start: unit -> unit
132   end
133
134 module type HbugsTutorDescription =
135   sig
136     val addr: string
137     val port: int
138     val tactic: ProofEngineTypes.tactic
139     val hint: hint
140     val hint_type: hint_type
141     val description: string
142     val environment_file: string
143   end
144
145 module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
146   struct
147     let broker_id = ref None
148     let my_own_id = init_tutor ()
149     let my_own_addr, my_own_port = Dsc.addr, Dsc.port
150     let my_own_url = sprintf "%s:%d" my_own_addr my_own_port
151
152     let is_authenticated id =
153       match !broker_id with
154       | None -> false
155       | Some broker_id -> id = broker_id
156
157       (* thread who do the dirty work *)
158     let slave (state, musing_id) =
159       prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
160       let (proof, goal) = load_state state in
161       let success =
162         try
163           ignore (Dsc.tactic (proof, goal));
164           true
165         with e -> false
166       in
167       let answer = 
168         Musing_completed
169           (my_own_id, musing_id, (if success then Eureka Dsc.hint else Sorry))
170       in
171       ignore (Hbugs_messages.submit_req ~url:broker_url answer);
172       prerr_endline
173         (sprintf "Bye, I've completed my duties (success = %b)" success)
174
175     let hbugs_callback =
176         (* hashtbl mapping musings ids to PID of threads doing the related (dirty)
177         work *)
178       let slaves = Hashtbl.create 17 in
179       let forbidden () =
180         prerr_endline "ignoring request from unauthorized broker";
181         Exception ("forbidden", "")
182       in
183       function  (* _the_ callback *)
184       | Start_musing (broker_id, state) ->
185           if is_authenticated broker_id then begin
186             prerr_endline "received Start_musing";
187             let new_musing_id = Hbugs_id_generator.new_musing_id () in
188             prerr_endline
189               (sprintf "starting a new musing (id = %s)" new_musing_id);
190 (*             let slave_thread = Thread.create slave (state, new_musing_id) in *)
191             let slave_thread =
192               Hbugs_deity.create slave (state, new_musing_id)
193             in
194             Hashtbl.add slaves new_musing_id slave_thread;
195             Musing_started (my_own_id, new_musing_id)
196           end else  (* broker unauthorized *)
197             forbidden ();
198       | Abort_musing (broker_id, musing_id) ->
199           if is_authenticated broker_id then begin
200             (try  (* kill thread responsible for "musing_id" *)
201               let slave_thread = Hashtbl.find slaves musing_id in
202               Hbugs_deity.kill slave_thread;
203               Hashtbl.remove slaves musing_id
204             with
205             | Hbugs_deity.Can_t_kill (_, reason) ->
206                 prerr_endline (sprintf "Unable to kill slave: %s" reason)
207             | Not_found ->
208                 prerr_endline (sprintf
209                   "Can't find slave corresponding to musing %s, can't kill it"
210                   musing_id));
211             Musing_aborted (my_own_id, musing_id)
212           end else (* broker unauthorized *)
213             forbidden ();
214       | unexpected_msg ->
215           Exception ("unexpected_msg",
216             Hbugs_messages.string_of_msg unexpected_msg)
217
218     let callback (req: Http_types.request) outchan =
219       try
220         let req_msg = Hbugs_messages.msg_of_string req#body in
221         let answer = hbugs_callback req_msg in
222         Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan
223       with Hbugs_messages.Parse_error (subj, reason) ->
224         Http_daemon.respond
225           ~body:(Hbugs_messages.string_of_msg
226             (Exception ("parse_error", reason)))
227           outchan
228
229     let restore_environment () =
230       let ic = open_in Dsc.environment_file in
231       prerr_endline "Restoring environment ...";
232       CicEnvironment.restore_from_channel
233         ~callback:(fun uri -> prerr_endline uri) ic;
234       prerr_endline "... done!";
235       close_in ic
236
237     let dump_environment () =
238       let oc = open_out Dsc.environment_file in
239       prerr_endline "Dumping environment ...";
240       CicEnvironment.dump_to_channel
241         ~callback:(fun uri -> prerr_endline uri) oc;
242       prerr_endline "... done!";
243       close_out oc
244
245     let main () =
246       try
247         Sys.catch_break true;
248         at_exit (fun () ->
249           if dump_environment_on_exit then
250             dump_environment ();
251           unregister_from_broker my_own_id);
252         broker_id :=
253           Some (register_to_broker
254             my_own_id my_own_url Dsc.hint_type Dsc.description);
255         if Sys.file_exists Dsc.environment_file then
256           restore_environment ();
257         Http_daemon.start'
258           ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback
259       with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
260
261     let start = main
262
263   end
264