]> matita.cs.unibo.it Git - helm.git/blob - helm/hbugs/common/hbugs_messages.ml
0cc0f1b1fe599d079c21f79248a7253ebe361e10
[helm.git] / helm / hbugs / common / hbugs_messages.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 open Pxp_document;;
32 open Pxp_dtd;;
33 open Pxp_types;;
34 open Pxp_yacc;;
35
36 let debug = true;;
37
38 exception Attribute_not_found of string;;
39 exception No_element_found of string;;
40 exception Parse_error of string * string;;  (* parsing subject, reason *)
41 exception Unexpected_message of message;;
42
43 let is_xml_element n = match n#node_type with T_element _ -> true | _ -> false
44 let get_attr node name =
45   try
46     (match node#attribute name with
47     | Value s -> s
48     | _ -> raise Not_found)
49   with Not_found -> raise (Attribute_not_found name)
50
51   (** given a string representation of a proof asistant state (e.g. the first
52   child of the XML root of a State_change or Start_musing message), build from
53   it an HBugs view of a proof assistant state *)
54 let parse_state (root: ('a node extension as 'a) node) =
55   let assert_element n name =
56     match n#node_type with
57     | T_element n when n = name ->
58         ()
59     | _ -> raise (Parse_error ("", "Expected node: " ^ name))
60   in
61   let buf = Buffer.create 10240 in
62   let node_to_string (node: ('a node extension as 'a) node) =
63     Buffer.clear buf;
64     node#write (`Out_buffer buf) `Enc_utf8;
65     let res = Buffer.contents buf in
66     Buffer.clear buf;
67     res
68   in
69   let (goal_node, type_node, body_node) =
70     try
71       (find_element "CurrentGoal" root,
72        find_element "ConstantType" root,  (* TODO e' sempre ConstantType? *)
73        find_element "CurrentProof" root)
74     with Not_found ->
75       raise (Parse_error ("", "Malformed HBugs status XML document"))
76   in
77   assert_element root "gTopLevelStatus";
78   assert_element goal_node "CurrentGoal";
79   assert_element type_node "ConstantType";  (* TODO: tutti gli xml 'type' hanno
80                                             come root element "ConstantType"? *)
81   assert_element body_node "CurrentProof";
82   goal_node#write (`Out_buffer buf) `Enc_utf8;
83   let (type_string, body_string) =
84     (node_to_string type_node, node_to_string body_node)
85   in
86   let goal =
87     try
88       int_of_string (goal_node#data)
89     with Failure "int_of_string" ->
90       raise (Parse_error (goal_node#data, "can't parse goal"))
91   in
92   (type_string, body_string, goal)
93
94   (** parse an hint from an XML node, XML node should have type 'T_element _'
95   (the name is ignored), attributes on it are ignored *)
96 let parse_hint node =
97  let rec parse_hint_node node =
98    match node#node_type with
99    | T_element "ring" -> Use_ring_Luke
100    | T_element "fourier" -> Use_fourier_Luke
101    | T_element "reflexivity" -> Use_reflexivity_Luke
102    | T_element "symmetry" -> Use_symmetry_Luke
103    | T_element "assumption" -> Use_assumption_Luke
104    | T_element "contradiction" -> Use_contradiction_Luke
105    | T_element "exists" -> Use_exists_Luke
106    | T_element "split" -> Use_split_Luke
107    | T_element "left" -> Use_left_Luke
108    | T_element "right" -> Use_right_Luke
109    | T_element "apply" -> Use_apply_Luke node#data
110    | T_element "hints" ->
111        Hints
112         (List.map parse_hint_node (List.filter is_xml_element node#sub_nodes))
113    | _ -> assert false (* CSC: should this assert false be a raise something? *)
114  in
115   match List.filter is_xml_element node#sub_nodes with
116      [node] -> parse_hint_node node
117    | _ -> assert false (* CSC: should this assert false be a raise something? *)
118
119 let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
120 let parse_tutor_dscs n =
121   List.map
122     (fun n -> (get_attr n "id", n#data))
123     (List.filter is_xml_element n#sub_nodes)
124 let parse_tutor_ids node =
125   List.map
126     (fun n -> get_attr n "id") (List.filter is_xml_element node#sub_nodes)
127
128 let tutors_sep = Pcre.regexp ",\\s*"
129
130 let msg_of_string' s =
131   let root =  (* xml tree's root *)
132     parse_wfcontent_entity default_config (from_string s) default_spec
133   in
134   match root#node_type with
135
136     (* general purpose *)
137   | T_element "help" -> Help
138   | T_element "usage" -> Usage root#data
139   | T_element "exception" -> Exception (get_attr root "name", root#data)
140
141     (* client -> broker *)
142   | T_element "register_client" ->
143       Register_client (get_attr root "id", get_attr root "url")
144   | T_element "unregister_client" -> Unregister_client (get_attr root "id")
145   | T_element "list_tutors" -> List_tutors (get_attr root "id")
146   | T_element "subscribe" ->
147       Subscribe (get_attr root "id", parse_tutor_ids root)
148   | T_element "state_change" ->
149       let state_node =
150         try
151           find_element ~deeply:false "gTopLevelStatus" root
152         with Not_found -> raise (No_element_found "gTopLevelStatus")
153       in
154       State_change (get_attr root "id", parse_state state_node)
155   | T_element "wow" -> Wow (get_attr root "id")
156
157     (* tutor -> broker *)
158   | T_element "register_tutor" ->
159       let hint_node = find_element "hint_type" root in
160       let dsc_node = find_element "description" root in
161       Register_tutor
162         (get_attr root "id", get_attr root "url",
163         parse_hint_type hint_node, dsc_node#data)
164   | T_element "unregister_tutor" -> Unregister_tutor (get_attr root "id")
165   | T_element "musing_started" ->
166       Musing_started (get_attr root "id", get_attr root "musing_id")
167   | T_element "musing_aborted" ->
168       Musing_started (get_attr root "id", get_attr root "musing_id")
169   | T_element "musing_completed" ->
170       let main_node =
171         try
172           find_element "eureka" root
173         with Not_found -> find_element "sorry" root
174       in
175       Musing_completed
176         (get_attr root "id", get_attr root "musing_id",
177         (match main_node#node_type with
178         | T_element "eureka" ->
179             Eureka (parse_hint main_node)
180         | T_element "sorry" -> Sorry
181         | _ -> assert false)) (* can't be there, see 'find_element' above *)
182
183     (* broker -> client *)
184   | T_element "client_registered" -> Client_registered (get_attr root "id")
185   | T_element "client_unregistered" -> Client_unregistered (get_attr root "id")
186   | T_element "tutor_list" ->
187       Tutor_list (get_attr root "id", parse_tutor_dscs root)
188   | T_element "subscribed" ->
189       Subscribed (get_attr root "id", parse_tutor_ids root)
190   | T_element "state_accepted" ->
191       State_accepted
192         (get_attr root "id",
193         List.map
194           (fun n -> get_attr n "id")
195           (List.filter is_xml_element (find_element "stopped" root)#sub_nodes),
196         List.map
197           (fun n -> get_attr n "id")
198           (List.filter is_xml_element (find_element "started" root)#sub_nodes))
199   | T_element "hint" -> Hint (get_attr root "id", parse_hint root)
200
201     (* broker -> tutor *)
202   | T_element "tutor_registered" -> Tutor_registered (get_attr root "id")
203   | T_element "tutor_unregistered" -> Tutor_unregistered (get_attr root "id")
204   | T_element "start_musing" ->
205       let state_node =
206         try
207           find_element ~deeply:false "gTopLevelStatus" root
208         with Not_found -> raise (No_element_found "gTopLevelStatus")
209       in
210       Start_musing (get_attr root "id", parse_state state_node)
211   | T_element "abort_musing" ->
212       Abort_musing (get_attr root "id", get_attr root "musing_id")
213   | T_element "thanks" -> Thanks (get_attr root "id", get_attr root "musing_id")
214
215   | _ -> raise (No_element_found s)
216
217 let msg_of_string s =
218   try
219     msg_of_string' s
220   with e -> raise (Parse_error (s, Printexc.to_string e))
221
222 let pp_state (type_string, body_string, goal) =
223   (* ASSUMPTION: type_string and body_string are well formed XML document
224   contents (i.e. they don't contain heading <?xml ... ?> declaration nor DOCTYPE
225   one *)
226   let res =
227     "<gTopLevelStatus>\n" ^
228     (sprintf "<CurrentGoal>%d</CurrentGoal>\n" goal) ^
229     type_string ^ "\n" ^
230     body_string ^ "\n" ^
231     "</gTopLevelStatus>\n"
232   in
233   res
234
235 let rec pp_hint = function
236   | Use_ring_Luke -> sprintf "<ring />"
237   | Use_fourier_Luke -> sprintf "<fourier />"
238   | Use_reflexivity_Luke -> sprintf "<reflexivity />"
239   | Use_symmetry_Luke -> sprintf "<symmetry />"
240   | Use_assumption_Luke -> sprintf "<assumption />"
241   | Use_contradiction_Luke -> sprintf "<contradiction />"
242   | Use_exists_Luke -> sprintf "<exists />"
243   | Use_split_Luke -> sprintf "<split />"
244   | Use_left_Luke -> sprintf "<left />"
245   | Use_right_Luke -> sprintf "<right />"
246   | Use_apply_Luke term -> sprintf "<apply>%s</apply>" term
247   | Hints hints ->
248       sprintf "<hints>\n%s\n</hints>"
249         (String.concat "\n" (List.map pp_hint hints))
250
251 let pp_hint_type s = s   (* TODO pretty print hint_type *)
252 let pp_tutor_dscs =
253   List.fold_left
254     (fun s (id, dsc) ->
255       sprintf "%s<tutor_dsc id=\"%s\">%s</tutor_dsc>" s id dsc)
256     ""
257 let pp_tutor_ids =
258   List.fold_left (fun s id -> sprintf "%s<tutor id=\"%s\" />" s id) ""
259
260 let string_of_msg = function
261   | Help -> "<help />"
262   | Usage usage_string -> sprintf "<usage>%s</usage>" usage_string
263   | Exception (name, value) ->
264       sprintf "<exception name=\"%s\">%s</exception>" name value
265   | Register_client (id, url) ->
266       sprintf "<register_client id=\"%s\" url=\"%s\" />" id url
267   | Unregister_client id -> sprintf "<unregister_client id=\"%s\" />" id
268   | List_tutors id -> sprintf "<list_tutors id=\"%s\" />" id
269   | Subscribe (id, tutor_ids) ->
270       sprintf "<subscribe id=\"%s\">%s</subscribe>"
271         id (pp_tutor_ids tutor_ids)
272   | State_change (id, state) ->
273       sprintf "<state_change id=\"%s\">%s</state_change>"
274         id (pp_state state)
275   | Wow id -> sprintf "<wow id=\"%s\" />" id
276   | Register_tutor (id, url, hint_type, dsc) ->
277       sprintf
278 "<register_tutor id=\"%s\" url=\"%s\">
279 <hint_type>%s</hint_type>
280 <description>%s</description>
281 </register_tutor>"
282         id url (pp_hint_type hint_type) dsc
283   | Unregister_tutor id -> sprintf "<unregister_tutor id=\"%s\" />" id
284   | Musing_started (id, musing_id) ->
285       sprintf "<musing_started id=\"%s\" musing_id=\"%s\" />" id musing_id
286   | Musing_aborted (id, musing_id) ->
287       sprintf "<musing_aborted id=\"%s\" musing_id=\"%s\" />" id musing_id
288   | Musing_completed (id, musing_id, result) ->
289       sprintf
290         "<musing_completed id=\"%s\" musing_id=\"%s\">%s</musing_completed>"
291         id musing_id
292         (match result with
293         | Sorry -> "<sorry />"
294         | Eureka hint -> sprintf "<eureka>%s</eureka>" (pp_hint hint))
295   | Client_registered id -> sprintf "<client_registered id=\"%s\" />" id
296   | Client_unregistered id -> sprintf "<client_unregistered id=\"%s\" />" id
297   | Tutor_list (id, tutor_dscs) ->
298       sprintf "<tutor_list id=\"%s\">%s</tutor_list>"
299         id (pp_tutor_dscs tutor_dscs)
300   | Subscribed (id, tutor_ids) ->
301       sprintf "<subscribed id=\"%s\">%s</subscribed>"
302         id (pp_tutor_ids tutor_ids)
303   | State_accepted (id, stop_ids, start_ids) ->
304       sprintf
305 "<state_accepted id=\"%s\">
306 <stopped>%s</stopped>
307 <started>%s</started>
308 </state_accepted>"
309         id
310         (String.concat ""
311           (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) stop_ids))
312         (String.concat ""
313           (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) start_ids))
314   | Hint (id, hint) -> sprintf "<hint id=\"%s\">%s</hint>" id (pp_hint hint)
315   | Tutor_registered id -> sprintf "<tutor_registered id=\"%s\" />" id
316   | Tutor_unregistered id -> sprintf "<tutor_unregistered id=\"%s\" />" id
317   | Start_musing (id, state) ->
318       sprintf "<start_musing id=\"%s\">%s</start_musing>" id (pp_state state)
319   | Abort_musing (id, musing_id) ->
320       sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
321   | Thanks (id, musing_id) ->
322       sprintf "<thanks id=\"%s\" musing_id=\"%s\" />" id musing_id
323   | Too_late (id, musing_id) ->
324       sprintf "<too_late id=\"%s\" musing_id=\"%s\" />" id musing_id
325 ;;
326
327   (* debugging function that dump on stderr the sent messages *)
328 let dump_msg msg =
329   if debug then
330     prerr_endline
331       (sprintf "<SENDING_MESSAGE>\n%s\n</SENDING_MESSAGE>"
332         (match msg with
333         | State_change _ -> "<state_change>omissis ...</state_change>"
334         | msg -> string_of_msg msg))
335 ;;
336
337 let submit_req ~url msg =
338   dump_msg msg;
339   if debug then (prerr_string "Waiting for an answer ... "; flush stderr);
340   let res =
341     msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
342   in
343   if debug then (prerr_string "answer received!\n"; flush stderr);
344   res
345 ;;
346 let return_xml_msg body outchan =
347   Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan
348 ;;
349 let respond_msg msg outchan =
350   dump_msg msg;
351   return_xml_msg (string_of_msg msg) outchan
352 (*   close_out outchan *)
353 ;;
354 let respond_exc name value = respond_msg (Exception (name, value));;
355