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 *)
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" ->
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? *)
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? *)
119 let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
120 let parse_tutor_dscs n =
122 (fun n -> (get_attr n "id", n#data))
123 (List.filter is_xml_element n#sub_nodes)
124 let parse_tutor_ids node =
126 (fun n -> get_attr n "id") (List.filter is_xml_element node#sub_nodes)
128 let tutors_sep = Pcre.regexp ",\\s*"
130 let msg_of_string' s =
131 let root = (* xml tree's root *)
132 parse_wfcontent_entity default_config (from_string s) default_spec
134 match root#node_type with
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)
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" ->
151 find_element ~deeply:false "gTopLevelStatus" root
152 with Not_found -> raise (No_element_found "gTopLevelStatus")
154 State_change (get_attr root "id", parse_state state_node)
155 | T_element "wow" -> Wow (get_attr root "id")
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
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" ->
172 find_element "eureka" root
173 with Not_found -> find_element "sorry" root
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 *)
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" ->
194 (fun n -> get_attr n "id")
195 (List.filter is_xml_element (find_element "stopped" root)#sub_nodes),
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)
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" ->
207 find_element ~deeply:false "gTopLevelStatus" root
208 with Not_found -> raise (No_element_found "gTopLevelStatus")
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")
215 | _ -> raise (No_element_found s)
217 let msg_of_string s =
220 with e -> raise (Parse_error (s, Printexc.to_string e))
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
227 "<gTopLevelStatus>\n" ^
228 (sprintf "<CurrentGoal>%d</CurrentGoal>\n" goal) ^
231 "</gTopLevelStatus>\n"
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
248 sprintf "<hints>\n%s\n</hints>"
249 (String.concat "\n" (List.map pp_hint hints))
251 let pp_hint_type s = s (* TODO pretty print hint_type *)
255 sprintf "%s<tutor_dsc id=\"%s\">%s</tutor_dsc>" s id dsc)
258 List.fold_left (fun s id -> sprintf "%s<tutor id=\"%s\" />" s id) ""
260 let string_of_msg = function
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>"
275 | Wow id -> sprintf "<wow id=\"%s\" />" id
276 | Register_tutor (id, url, hint_type, dsc) ->
278 "<register_tutor id=\"%s\" url=\"%s\">
279 <hint_type>%s</hint_type>
280 <description>%s</description>
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) ->
290 "<musing_completed id=\"%s\" musing_id=\"%s\">%s</musing_completed>"
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) ->
305 "<state_accepted id=\"%s\">
306 <stopped>%s</stopped>
307 <started>%s</started>
311 (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) stop_ids))
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
327 (* debugging function that dump on stderr the sent messages *)
331 (sprintf "<SENDING_MESSAGE>\n%s\n</SENDING_MESSAGE>"
333 | State_change _ -> "<state_change>omissis ...</state_change>"
334 | msg -> string_of_msg msg))
337 let submit_req ~url msg =
339 if debug then (prerr_string "Waiting for an answer ... "; flush stderr);
341 msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
343 if debug then (prerr_string "answer received!\n"; flush stderr);
346 let return_xml_msg body outchan =
347 Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan
349 let respond_msg msg outchan =
351 return_xml_msg (string_of_msg msg) outchan
352 (* close_out outchan *)
354 let respond_exc name value = respond_msg (Exception (name, value));;