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