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 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;;
  43
  44 let is_xml_element n = match n#node_type with T_element _ -> true | _ -> false
  45 let get_attr node name =
  46   try
  47     (match node#attribute name with
  48     | Value s -> s
  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 ->
  54       ()
  55   | _ -> raise (Parse_error ("", "Expected node: " ^ name))
  56
  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
  62     raise Empty_node;
  63   let buf = Buffer.create 10240 in
  64   let node_to_string (node: ('a node extension as 'a) node) =
  65     Buffer.clear buf;
  66     node#write (`Out_buffer buf) `Enc_utf8;
  67     let res = Buffer.contents buf in
  68     Buffer.clear buf;
  69     res
  70   in
  71   let (goal_node, type_node, body_node) =
  72     try
  73       (find_element "CurrentGoal" root,
  74        find_element "ConstantType" root,
  75        find_element "CurrentProof" root)
  76     with Not_found ->
  77       raise (Parse_error ("", "Malformed HBugs status XML document"))
  78   in
  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)
  86   in
  87   let goal =
  88     try
  89       int_of_string (goal_node#data)
  90     with Failure "int_of_string" ->
  91       raise (Parse_error (goal_node#data, "can't parse goal"))
  92   in
  93   (type_string, body_string, goal)
  94
  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 *)
  97 let parse_hint node =
  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" ->
 112        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? *)
 115  in
 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? *)
 119
 120 let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
 121 let parse_tutor_dscs n =
 122   List.map
 123     (fun n -> (get_attr n "id", n#data))
 124     (List.filter is_xml_element n#sub_nodes)
 125 let parse_tutor_ids node =
 126   List.map
 127     (fun n -> get_attr n "id") (List.filter is_xml_element node#sub_nodes)
 128
 129 let tutors_sep = Pcre.regexp ",\\s*"
 130
 131 let msg_of_string' s =
 132   let root =  (* xml tree's root *)
 133     parse_wfcontent_entity default_config (from_string s) default_spec
 134   in
 135   match root#node_type with
 136
 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)
 141
 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" ->
 150       let state_node =
 151         try
 152           Some (find_element ~deeply:false "gTopLevelStatus" root)
 153         with Not_found -> None
 154       in
 155       State_change
 156         (get_attr root "id",
 157         match state_node with
 158         | Some n -> (try Some (parse_state n) with Empty_node -> None)
 159         | None -> None)
 160   | T_element "wow" -> Wow (get_attr root "id")
 161
 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
 166       Register_tutor
 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" ->
 175       let main_node =
 176         try
 177           find_element "eureka" root
 178         with Not_found -> find_element "sorry" root
 179       in
 180       Musing_completed
 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 *)
 187
 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" ->
 196       State_accepted
 197         (get_attr root "id",
 198         List.map
 199           (fun n -> get_attr n "id")
 200           (List.filter is_xml_element (find_element "stopped" root)#sub_nodes),
 201         List.map
 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)
 205
 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" ->
 210       let state_node =
 211         try
 212           find_element ~deeply:false "gTopLevelStatus" root
 213         with Not_found -> raise (No_element_found "gTopLevelStatus")
 214       in
 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")
 221
 222   | _ -> raise (No_element_found s)
 223
 224 let msg_of_string s =
 225   try
 226     msg_of_string' s
 227   with e -> raise (Parse_error (s, Printexc.to_string e))
 228
 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
 233     DOCTYPE one *)
 234     "<gTopLevelStatus>\n" ^
 235     (sprintf "<CurrentGoal>%d</CurrentGoal>\n" goal) ^
 236     type_string ^ "\n" ^
 237     body_string ^ "\n" ^
 238     "</gTopLevelStatus>\n"
 239   | None -> "<gTopLevelStatus />\n"
 240
 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
 253   | Hints hints ->
 254       sprintf "<hints>\n%s\n</hints>"
 255         (String.concat "\n" (List.map pp_hint hints))
 256
 257 let pp_hint_type s = s   (* TODO pretty print hint_type *)
 258 let pp_tutor_dscs =
 259   List.fold_left
 260     (fun s (id, dsc) ->
 261       sprintf "%s<tutor_dsc id=\"%s\">%s</tutor_dsc>" s id dsc)
 262     ""
 263 let pp_tutor_ids =
 264   List.fold_left (fun s id -> sprintf "%s<tutor id=\"%s\" />" s id) ""
 265
 266 let string_of_msg = function
 267   | Help -> "<help />"
 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>"
 280         id (pp_state state)
 281   | Wow id -> sprintf "<wow id=\"%s\" />" id
 282   | Register_tutor (id, url, hint_type, dsc) ->
 283       sprintf
 284 "<register_tutor id=\"%s\" url=\"%s\">
 285 <hint_type>%s</hint_type>
 286 <description>%s</description>
 287 </register_tutor>"
 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) ->
 295       sprintf
 296         "<musing_completed id=\"%s\" musing_id=\"%s\">%s</musing_completed>"
 297         id musing_id
 298         (match result with
 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) ->
 310       sprintf
 311 "<state_accepted id=\"%s\">
 312 <stopped>%s</stopped>
 313 <started>%s</started>
 314 </state_accepted>"
 315         id
 316         (String.concat ""
 317           (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) stop_ids))
 318         (String.concat ""
 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
 332 ;;
 333
 334   (* debugging function that dump on stderr the sent messages *)
 335 let dump_msg msg =
 336   if debug then
 337     prerr_endline
 338       (sprintf "<SENDING_MESSAGE>\n%s\n</SENDING_MESSAGE>"
 339         (match msg with
 340         | State_change _ -> "<state_change>omissis ...</state_change>"
 341         | msg -> string_of_msg msg))
 342 ;;
 343
 344 let submit_req ~url msg =
 345   dump_msg msg;
 346   if debug then (prerr_string "Waiting for an answer ... "; flush stderr);
 347   let res =
 348     msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
 349   in
 350   if debug then (prerr_string "answer received!\n"; flush stderr);
 351   res
 352 ;;
 353 let return_xml_msg body outchan =
 354   Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan
 355 ;;
 356 let respond_msg msg outchan =
 357   dump_msg msg;
 358   return_xml_msg (string_of_msg msg) outchan
 359 (*   close_out outchan *)
 360 ;;
 361 let respond_exc name value = respond_msg (Exception (name, value));;
 362