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 No_element_found of string;;
40 exception Parse_error of string * string;; (* parsing subject, reason *)
41 exception Unexpected_message of message;;
43 let is_xml_element n = match n#node_type with T_element _ -> true | _ -> false
44 let get_attr node name =
46 (match node#attribute name with
48 | _ -> raise Not_found)
49 with Not_found -> raise (Attribute_not_found name)
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 ->
59 | _ -> raise (Parse_error ("", "Expected node: " ^ name))
61 let buf = Buffer.create 10240 in
62 let node_to_string (node: ('a node extension as 'a) node) =
64 node#write (`Out_buffer buf) `Enc_utf8;
65 let res = Buffer.contents buf in
69 let (goal_node, type_node, body_node) =
71 (find_element "CurrentGoal" root,
72 find_element "ConstantType" root, (* TODO e' sempre ConstantType? *)
73 find_element "CurrentProof" root)
75 raise (Parse_error ("", "Malformed HBugs status XML document"))
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)
88 int_of_string (goal_node#data)
89 with Failure "int_of_string" ->
90 raise (Parse_error (goal_node#data, "can't parse goal"))
92 (type_string, body_string, goal)
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 rec parse_hint node =
97 let child = node#nth_node 0 in
98 match child#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 (List.map parse_hint (List.filter is_xml_element node#sub_nodes))
113 let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
114 let parse_tutor_dscs n =
116 (fun n -> (get_attr n "id", n#data))
117 (List.filter is_xml_element n#sub_nodes)
118 let parse_tutor_ids node =
120 (fun n -> get_attr n "id") (List.filter is_xml_element node#sub_nodes)
122 let tutors_sep = Pcre.regexp ",\\s*"
124 let msg_of_string' s =
125 let root = (* xml tree's root *)
126 parse_wfcontent_entity default_config (from_string s) default_spec
128 match root#node_type with
130 (* general purpose *)
131 | T_element "help" -> Help
132 | T_element "usage" -> Usage root#data
133 | T_element "exception" -> Exception (get_attr root "name", root#data)
135 (* client -> broker *)
136 | T_element "register_client" ->
137 Register_client (get_attr root "id", get_attr root "url")
138 | T_element "unregister_client" -> Unregister_client (get_attr root "id")
139 | T_element "list_tutors" -> List_tutors (get_attr root "id")
140 | T_element "subscribe" ->
141 Subscribe (get_attr root "id", parse_tutor_ids root)
142 | T_element "state_change" ->
145 find_element ~deeply:false "gTopLevelStatus" root
146 with Not_found -> raise (No_element_found "gTopLevelStatus")
148 State_change (get_attr root "id", parse_state state_node)
149 | T_element "wow" -> Wow (get_attr root "id")
151 (* tutor -> broker *)
152 | T_element "register_tutor" ->
153 let hint_node = find_element "hint_type" root in
154 let dsc_node = find_element "description" root in
156 (get_attr root "id", get_attr root "url",
157 parse_hint_type hint_node, dsc_node#data)
158 | T_element "unregister_tutor" -> Unregister_tutor (get_attr root "id")
159 | T_element "musing_started" ->
160 Musing_started (get_attr root "id", get_attr root "musing_id")
161 | T_element "musing_aborted" ->
162 Musing_started (get_attr root "id", get_attr root "musing_id")
163 | T_element "musing_completed" ->
166 find_element "eureka" root
167 with Not_found -> find_element "sorry" root
170 (get_attr root "id", get_attr root "musing_id",
171 (match main_node#node_type with
172 | T_element "eureka" ->
173 Eureka (parse_hint main_node)
174 | T_element "sorry" -> Sorry
175 | _ -> assert false)) (* can't be there, see 'find_element' above *)
177 (* broker -> client *)
178 | T_element "client_registered" -> Client_registered (get_attr root "id")
179 | T_element "client_unregistered" -> Client_unregistered (get_attr root "id")
180 | T_element "tutor_list" ->
181 Tutor_list (get_attr root "id", parse_tutor_dscs root)
182 | T_element "subscribed" ->
183 Subscribed (get_attr root "id", parse_tutor_ids root)
184 | T_element "state_accepted" ->
188 (fun n -> get_attr n "id")
189 (List.filter is_xml_element (find_element "stopped" root)#sub_nodes),
191 (fun n -> get_attr n "id")
192 (List.filter is_xml_element (find_element "started" root)#sub_nodes))
193 | T_element "hint" -> Hint (get_attr root "id", parse_hint root)
195 (* broker -> tutor *)
196 | T_element "tutor_registered" -> Tutor_registered (get_attr root "id")
197 | T_element "tutor_unregistered" -> Tutor_unregistered (get_attr root "id")
198 | T_element "start_musing" ->
201 find_element ~deeply:false "gTopLevelStatus" root
202 with Not_found -> raise (No_element_found "gTopLevelStatus")
204 Start_musing (get_attr root "id", parse_state state_node)
205 | T_element "abort_musing" ->
206 Abort_musing (get_attr root "id", get_attr root "musing_id")
207 | T_element "thanks" -> Thanks (get_attr root "id", get_attr root "musing_id")
209 | _ -> raise (No_element_found s)
211 let msg_of_string s =
214 with e -> raise (Parse_error (s, Printexc.to_string e))
216 let pp_state (type_string, body_string, goal) =
217 (* ASSUMPTION: type_string and body_string are well formed XML document
218 contents (i.e. they don't contain heading <?xml ... ?> declaration nor DOCTYPE
221 "<gTopLevelStatus>\n" ^
222 (sprintf "<CurrentGoal>%d</CurrentGoal>\n" goal) ^
225 "</gTopLevelStatus>\n"
229 let rec pp_hint = function
230 | Use_ring_Luke -> sprintf "<ring />"
231 | Use_fourier_Luke -> sprintf "<fourier />"
232 | Use_reflexivity_Luke -> sprintf "<reflexivity />"
233 | Use_symmetry_Luke -> sprintf "<symmetry />"
234 | Use_assumption_Luke -> sprintf "<assumption />"
235 | Use_contradiction_Luke -> sprintf "<contradiction />"
236 | Use_exists_Luke -> sprintf "<exists />"
237 | Use_split_Luke -> sprintf "<split />"
238 | Use_left_Luke -> sprintf "<left />"
239 | Use_right_Luke -> sprintf "<right />"
240 | Use_apply_Luke term -> sprintf "<apply>%s</apply>" term
242 sprintf "<hints>\n%s\n</hints>"
243 (String.concat "\n" (List.map pp_hint hints))
245 let pp_hint_type s = s (* TODO pretty print hint_type *)
249 sprintf "%s<tutor_dsc id=\"%s\">%s</tutor_dsc>" s id dsc)
252 List.fold_left (fun s id -> sprintf "%s<tutor id=\"%s\" />" s id) ""
254 let string_of_msg = function
256 | Usage usage_string -> sprintf "<usage>%s</usage>" usage_string
257 | Exception (name, value) ->
258 sprintf "<exception name=\"%s\">%s</exception>" name value
259 | Register_client (id, url) ->
260 sprintf "<register_client id=\"%s\" url=\"%s\" />" id url
261 | Unregister_client id -> sprintf "<unregister_client id=\"%s\" />" id
262 | List_tutors id -> sprintf "<list_tutors id=\"%s\" />" id
263 | Subscribe (id, tutor_ids) ->
264 sprintf "<subscribe id=\"%s\">%s</subscribe>"
265 id (pp_tutor_ids tutor_ids)
266 | State_change (id, state) ->
267 sprintf "<state_change id=\"%s\">%s</state_change>"
269 | Wow id -> sprintf "<wow id=\"%s\" />" id
270 | Register_tutor (id, url, hint_type, dsc) ->
272 "<register_tutor id=\"%s\" url=\"%s\">
273 <hint_type>%s</hint_type>
274 <description>%s</description>
276 id url (pp_hint_type hint_type) dsc
277 | Unregister_tutor id -> sprintf "<unregister_tutor id=\"%s\" />" id
278 | Musing_started (id, musing_id) ->
279 sprintf "<musing_started id=\"%s\" musing_id=\"%s\" />" id musing_id
280 | Musing_aborted (id, musing_id) ->
281 sprintf "<musing_aborted id=\"%s\" musing_id=\"%s\" />" id musing_id
282 | Musing_completed (id, musing_id, result) ->
284 "<musing_completed id=\"%s\" musing_id=\"%s\">%s</musing_completed>"
287 | Sorry -> "<sorry />"
288 | Eureka hint -> sprintf "<eureka>%s</eureka>" (pp_hint hint))
289 | Client_registered id -> sprintf "<client_registered id=\"%s\" />" id
290 | Client_unregistered id -> sprintf "<client_unregistered id=\"%s\" />" id
291 | Tutor_list (id, tutor_dscs) ->
292 sprintf "<tutor_list id=\"%s\">%s</tutor_list>"
293 id (pp_tutor_dscs tutor_dscs)
294 | Subscribed (id, tutor_ids) ->
295 sprintf "<subscribed id=\"%s\">%s</subscribed>"
296 id (pp_tutor_ids tutor_ids)
297 | State_accepted (id, stop_ids, start_ids) ->
299 "<state_accepted id=\"%s\">
300 <stopped>%s</stopped>
301 <started>%s</started>
305 (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) stop_ids))
307 (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) start_ids))
308 | Hint (id, hint) -> sprintf "<hint id=\"%s\">%s</hint>" id (pp_hint hint)
309 | Tutor_registered id -> sprintf "<tutor_registered id=\"%s\" />" id
310 | Tutor_unregistered id -> sprintf "<tutor_unregistered id=\"%s\" />" id
311 | Start_musing (id, state) ->
312 sprintf "<start_musing id=\"%s\">%s</start_musing>" id (pp_state state)
313 | Abort_musing (id, musing_id) ->
314 sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
315 | Thanks (id, musing_id) ->
316 sprintf "<thanks id=\"%s\" musing_id=\"%s\" />" id musing_id
317 | Too_late (id, musing_id) ->
318 sprintf "<too_late id=\"%s\" musing_id=\"%s\" />" id musing_id
321 (* debugging function that dump on stderr the sent messages *)
325 (sprintf "<SENDING_MESSAGE>\n%s\n</SENDING_MESSAGE>"
327 | State_change _ -> "<state_change>omissis ...</state_change>"
328 | msg -> string_of_msg msg))
331 let submit_req ~url msg =
333 if debug then (prerr_string "Waiting for an answer ... "; flush stderr);
335 msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
337 if debug then (prerr_string "answer received!\n"; flush stderr);
340 let return_xml_msg body outchan =
341 Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan
343 let respond_msg msg outchan =
345 return_xml_msg (string_of_msg msg) outchan
346 (* close_out outchan *)
348 let respond_exc name value = respond_msg (Exception (name, value));;