3 * Stefano Zacchiroli <zack@cs.unibo.it>
4 * for the HELM Team http://helm.cs.unibo.it/
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.
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.
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.
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,
25 * For details, see the HELM World-Wide-Web page,
26 * http://helm.cs.unibo.it/
38 exception Attribute_not_found of string;;
39 exception Empty_node;; (** found a node with no _element_ children *)
40 exception No_element_found of string;;
41 exception Parse_error of string * string;; (* parsing subject, reason *)
42 exception Unexpected_message of message;;
44 let is_xml_element n = match n#node_type with T_element _ -> true | _ -> false
45 let get_attr node name =
47 (match node#attribute name with
49 | _ -> raise Not_found)
50 with Not_found -> raise (Attribute_not_found name)
51 let assert_element n name =
52 match n#node_type with
53 | T_element n when n = name ->
55 | _ -> raise (Parse_error ("", "Expected node: " ^ name))
57 (** given a string representation of a proof asistant state (e.g. the first
58 child of the XML root of a State_change or Start_musing message), build from
59 it an HBugs view of a proof assistant state *)
60 let parse_state (root: ('a node extension as 'a) node) =
61 if (List.filter is_xml_element root#sub_nodes) = [] then
63 let buf = Buffer.create 10240 in
64 let node_to_string (node: ('a node extension as 'a) node) =
66 node#write (`Out_buffer buf) `Enc_utf8;
67 let res = Buffer.contents buf in
71 let (goal_node, type_node, body_node) =
73 (find_element "CurrentGoal" root,
74 find_element "ConstantType" root,
75 find_element "CurrentProof" root)
77 raise (Parse_error ("", "Malformed HBugs status XML document"))
79 assert_element root "gTopLevelStatus";
80 assert_element goal_node "CurrentGoal";
81 assert_element type_node "ConstantType";
82 assert_element body_node "CurrentProof";
83 goal_node#write (`Out_buffer buf) `Enc_utf8;
84 let (type_string, body_string) =
85 (node_to_string type_node, node_to_string body_node)
89 int_of_string (goal_node#data)
90 with Failure "int_of_string" ->
91 raise (Parse_error (goal_node#data, "can't parse goal"))
93 (type_string, body_string, goal)
95 (** parse an hint from an XML node, XML node should have type 'T_element _'
96 (the name is ignored), attributes on it are ignored *)
98 let rec parse_hint_node node =
99 match node#node_type with
100 | T_element "ring" -> Use_ring_Luke
101 | T_element "fourier" -> Use_fourier_Luke
102 | T_element "reflexivity" -> Use_reflexivity_Luke
103 | T_element "symmetry" -> Use_symmetry_Luke
104 | T_element "assumption" -> Use_assumption_Luke
105 | T_element "contradiction" -> Use_contradiction_Luke
106 | T_element "exists" -> Use_exists_Luke
107 | T_element "split" -> Use_split_Luke
108 | T_element "left" -> Use_left_Luke
109 | T_element "right" -> Use_right_Luke
110 | T_element "apply" -> Use_apply_Luke node#data
111 | T_element "hints" ->
113 (List.map parse_hint_node (List.filter is_xml_element node#sub_nodes))
114 | _ -> assert false (* CSC: should this assert false be a raise something? *)
116 match List.filter is_xml_element node#sub_nodes with
117 [node] -> parse_hint_node node
118 | _ -> assert false (* CSC: should this assert false be a raise something? *)
120 let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
121 let parse_tutor_dscs n =
123 (fun n -> (get_attr n "id", n#data))
124 (List.filter is_xml_element n#sub_nodes)
125 let parse_tutor_ids node =
127 (fun n -> get_attr n "id") (List.filter is_xml_element node#sub_nodes)
129 let tutors_sep = Pcre.regexp ",\\s*"
131 let msg_of_string' s =
132 let root = (* xml tree's root *)
133 parse_wfcontent_entity default_config (from_string s) default_spec
135 match root#node_type with
137 (* general purpose *)
138 | T_element "help" -> Help
139 | T_element "usage" -> Usage root#data
140 | T_element "exception" -> Exception (get_attr root "name", root#data)
142 (* client -> broker *)
143 | T_element "register_client" ->
144 Register_client (get_attr root "id", get_attr root "url")
145 | T_element "unregister_client" -> Unregister_client (get_attr root "id")
146 | T_element "list_tutors" -> List_tutors (get_attr root "id")
147 | T_element "subscribe" ->
148 Subscribe (get_attr root "id", parse_tutor_ids root)
149 | T_element "state_change" ->
152 Some (find_element ~deeply:false "gTopLevelStatus" root)
153 with Not_found -> None
157 match state_node with
158 | Some n -> (try Some (parse_state n) with Empty_node -> None)
160 | T_element "wow" -> Wow (get_attr root "id")
162 (* tutor -> broker *)
163 | T_element "register_tutor" ->
164 let hint_node = find_element "hint_type" root in
165 let dsc_node = find_element "description" root in
167 (get_attr root "id", get_attr root "url",
168 parse_hint_type hint_node, dsc_node#data)
169 | T_element "unregister_tutor" -> Unregister_tutor (get_attr root "id")
170 | T_element "musing_started" ->
171 Musing_started (get_attr root "id", get_attr root "musing_id")
172 | T_element "musing_aborted" ->
173 Musing_started (get_attr root "id", get_attr root "musing_id")
174 | T_element "musing_completed" ->
177 find_element "eureka" root
178 with Not_found -> find_element "sorry" root
181 (get_attr root "id", get_attr root "musing_id",
182 (match main_node#node_type with
183 | T_element "eureka" ->
184 Eureka (parse_hint main_node)
185 | T_element "sorry" -> Sorry
186 | _ -> assert false)) (* can't be there, see 'find_element' above *)
188 (* broker -> client *)
189 | T_element "client_registered" -> Client_registered (get_attr root "id")
190 | T_element "client_unregistered" -> Client_unregistered (get_attr root "id")
191 | T_element "tutor_list" ->
192 Tutor_list (get_attr root "id", parse_tutor_dscs root)
193 | T_element "subscribed" ->
194 Subscribed (get_attr root "id", parse_tutor_ids root)
195 | T_element "state_accepted" ->
199 (fun n -> get_attr n "id")
200 (List.filter is_xml_element (find_element "stopped" root)#sub_nodes),
202 (fun n -> get_attr n "id")
203 (List.filter is_xml_element (find_element "started" root)#sub_nodes))
204 | T_element "hint" -> Hint (get_attr root "id", parse_hint root)
206 (* broker -> tutor *)
207 | T_element "tutor_registered" -> Tutor_registered (get_attr root "id")
208 | T_element "tutor_unregistered" -> Tutor_unregistered (get_attr root "id")
209 | T_element "start_musing" ->
212 find_element ~deeply:false "gTopLevelStatus" root
213 with Not_found -> raise (No_element_found "gTopLevelStatus")
215 Start_musing (get_attr root "id", parse_state state_node)
216 | T_element "abort_musing" ->
217 Abort_musing (get_attr root "id", get_attr root "musing_id")
218 | T_element "thanks" -> Thanks (get_attr root "id", get_attr root "musing_id")
219 | T_element "too_late" ->
220 Too_late (get_attr root "id", get_attr root "musing_id")
222 | _ -> raise (No_element_found s)
224 let msg_of_string s =
227 with e -> raise (Parse_error (s, Printexc.to_string e))
229 let pp_state = function
230 | Some (type_string, body_string, goal) ->
231 (* ASSUMPTION: type_string and body_string are well formed XML document
232 contents (i.e. they don't contain heading <?xml ... ?> declaration nor
234 "<gTopLevelStatus>\n" ^
235 (sprintf "<CurrentGoal>%d</CurrentGoal>\n" goal) ^
238 "</gTopLevelStatus>\n"
239 | None -> "<gTopLevelStatus />\n"
241 let rec pp_hint = function
242 | Use_ring_Luke -> sprintf "<ring />"
243 | Use_fourier_Luke -> sprintf "<fourier />"
244 | Use_reflexivity_Luke -> sprintf "<reflexivity />"
245 | Use_symmetry_Luke -> sprintf "<symmetry />"
246 | Use_assumption_Luke -> sprintf "<assumption />"
247 | Use_contradiction_Luke -> sprintf "<contradiction />"
248 | Use_exists_Luke -> sprintf "<exists />"
249 | Use_split_Luke -> sprintf "<split />"
250 | Use_left_Luke -> sprintf "<left />"
251 | Use_right_Luke -> sprintf "<right />"
252 | Use_apply_Luke term -> sprintf "<apply>%s</apply>" term
254 sprintf "<hints>\n%s\n</hints>"
255 (String.concat "\n" (List.map pp_hint hints))
257 let pp_hint_type s = s (* TODO pretty print hint_type *)
261 sprintf "%s<tutor_dsc id=\"%s\">%s</tutor_dsc>" s id dsc)
264 List.fold_left (fun s id -> sprintf "%s<tutor id=\"%s\" />" s id) ""
266 let string_of_msg = function
268 | Usage usage_string -> sprintf "<usage>%s</usage>" usage_string
269 | Exception (name, value) ->
270 sprintf "<exception name=\"%s\">%s</exception>" name value
271 | Register_client (id, url) ->
272 sprintf "<register_client id=\"%s\" url=\"%s\" />" id url
273 | Unregister_client id -> sprintf "<unregister_client id=\"%s\" />" id
274 | List_tutors id -> sprintf "<list_tutors id=\"%s\" />" id
275 | Subscribe (id, tutor_ids) ->
276 sprintf "<subscribe id=\"%s\">%s</subscribe>"
277 id (pp_tutor_ids tutor_ids)
278 | State_change (id, state) ->
279 sprintf "<state_change id=\"%s\">%s</state_change>"
281 | Wow id -> sprintf "<wow id=\"%s\" />" id
282 | Register_tutor (id, url, hint_type, dsc) ->
284 "<register_tutor id=\"%s\" url=\"%s\">
285 <hint_type>%s</hint_type>
286 <description>%s</description>
288 id url (pp_hint_type hint_type) dsc
289 | Unregister_tutor id -> sprintf "<unregister_tutor id=\"%s\" />" id
290 | Musing_started (id, musing_id) ->
291 sprintf "<musing_started id=\"%s\" musing_id=\"%s\" />" id musing_id
292 | Musing_aborted (id, musing_id) ->
293 sprintf "<musing_aborted id=\"%s\" musing_id=\"%s\" />" id musing_id
294 | Musing_completed (id, musing_id, result) ->
296 "<musing_completed id=\"%s\" musing_id=\"%s\">%s</musing_completed>"
299 | Sorry -> "<sorry />"
300 | Eureka hint -> sprintf "<eureka>%s</eureka>" (pp_hint hint))
301 | Client_registered id -> sprintf "<client_registered id=\"%s\" />" id
302 | Client_unregistered id -> sprintf "<client_unregistered id=\"%s\" />" id
303 | Tutor_list (id, tutor_dscs) ->
304 sprintf "<tutor_list id=\"%s\">%s</tutor_list>"
305 id (pp_tutor_dscs tutor_dscs)
306 | Subscribed (id, tutor_ids) ->
307 sprintf "<subscribed id=\"%s\">%s</subscribed>"
308 id (pp_tutor_ids tutor_ids)
309 | State_accepted (id, stop_ids, start_ids) ->
311 "<state_accepted id=\"%s\">
312 <stopped>%s</stopped>
313 <started>%s</started>
317 (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) stop_ids))
319 (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) start_ids))
320 | Hint (id, hint) -> sprintf "<hint id=\"%s\">%s</hint>" id (pp_hint hint)
321 | Tutor_registered id -> sprintf "<tutor_registered id=\"%s\" />" id
322 | Tutor_unregistered id -> sprintf "<tutor_unregistered id=\"%s\" />" id
323 | Start_musing (id, state) ->
324 sprintf "<start_musing id=\"%s\">%s</start_musing>"
325 id (pp_state (Some state))
326 | Abort_musing (id, musing_id) ->
327 sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
328 | Thanks (id, musing_id) ->
329 sprintf "<thanks id=\"%s\" musing_id=\"%s\" />" id musing_id
330 | Too_late (id, musing_id) ->
331 sprintf "<too_late id=\"%s\" musing_id=\"%s\" />" id musing_id
334 (* debugging function that dump on stderr the sent messages *)
338 (sprintf "<SENDING_MESSAGE>\n%s\n</SENDING_MESSAGE>"
340 | State_change _ -> "<state_change>omissis ...</state_change>"
341 | msg -> string_of_msg msg))
344 let submit_req ~url msg =
346 if debug then (prerr_string "Waiting for an answer ... "; flush stderr);
348 msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
350 if debug then (prerr_string "answer received!\n"; flush stderr);
353 let return_xml_msg body outchan =
354 Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan
356 let respond_msg msg outchan =
358 return_xml_msg (string_of_msg msg) outchan
359 (* close_out outchan *)
361 let respond_exc name value = respond_msg (Exception (name, value));;