- implemented status {,de}serialization

- implemented hint {,de}serialization
- added support for new Wow and Too_late messages
- added dump_msg debugging function
- added Unexpected_message exception

diff --git a/helm/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml
index 0eac0b149aa26a685a4617c79a7321a8c31828d0..c0f70948462badd3f2a6678a7fafea2e365ce758 100644 (file)
--- a/helm/hbugs/common/hbugs_messages.ml
+++ b/helm/hbugs/common/hbugs_messages.ml
@@ -29,12 +29,16 @@
 open Hbugs_types;;
 open Printf;;
 open Pxp_document;;
+open Pxp_dtd;;
 open Pxp_types;;
 open Pxp_yacc;;
 
+let debug = true;;
+
 exception Attribute_not_found of string;;
 exception No_element_found of string;;
 exception Parse_error of string * string;;  (* parsing subject, reason *)
+exception Unexpected_message of message;;
 
 let is_xml_element n = match n#node_type with T_element _ -> true | _ -> false
 let get_attr node name =
@@ -44,8 +48,68 @@ let get_attr node name =
     | _ -> raise Not_found)
   with Not_found -> raise (Attribute_not_found name)
 
-let parse_state s = s (* TODO parsare lo stato del proof assistant! *)
-let parse_hint s = s (* TODO parsare il possibile suggerimento *)
+  (** given a string representation of a proof asistant state (e.g. the first
+  child of the XML root of a State_change or Start_musing message), build from
+  it an HBugs view of a proof assistant state *)
+let parse_state (root: ('a node extension as 'a) node) =
+  let assert_element n name =
+    match n#node_type with
+    | T_element n when n = name ->
+        ()
+    | _ -> raise (Parse_error ("", "Expected node: " ^ name))
+  in
+  let buf = Buffer.create 10240 in
+  let node_to_string (node: ('a node extension as 'a) node) =
+    Buffer.clear buf;
+    node#write (`Out_buffer buf) `Enc_utf8;
+    let res = Buffer.contents buf in
+    Buffer.clear buf;
+    res
+  in
+  let (goal_node, type_node, body_node) =
+    try
+      (find_element "CurrentGoal" root,
+       find_element "ConstantType" root,  (* TODO e' sempre ConstantType? *)
+       find_element "CurrentProof" root)
+    with Not_found ->
+      raise (Parse_error ("", "Malformed HBugs status XML document"))
+  in
+  assert_element root "gTopLevelStatus";
+  assert_element goal_node "CurrentGoal";
+  assert_element type_node "ConstantType";  (* TODO: tutti gli xml 'type' hanno
+                                            come root element "ConstantType"? *)
+  assert_element body_node "CurrentProof";
+  goal_node#write (`Out_buffer buf) `Enc_utf8;
+  let (type_string, body_string) =
+    (node_to_string type_node, node_to_string body_node)
+  in
+  let goal =
+    try
+      int_of_string (goal_node#data)
+    with Failure "int_of_string" ->
+      raise (Parse_error (goal_node#data, "can't parse goal"))
+  in
+  (type_string, body_string, goal)
+
+  (** parse an hint from an XML node, XML node should have type 'T_element _'
+  (the name is ignored), attributes on it are ignored *)
+let rec parse_hint node =
+  let child = node#nth_node 0 in
+  match child#node_type with
+  | T_element "ring" -> Use_ring_Luke
+  | T_element "fourier" -> Use_fourier_Luke
+  | T_element "reflexivity" -> Use_reflexivity_Luke
+  | T_element "symmetry" -> Use_symmetry_Luke
+  | T_element "assumption" -> Use_assumption_Luke
+  | T_element "contradiction" -> Use_contradiction_Luke
+  | T_element "exists" -> Use_exists_Luke
+  | T_element "split" -> Use_split_Luke
+  | T_element "left" -> Use_left_Luke
+  | T_element "right" -> Use_right_Luke
+  | T_element "apply" -> Use_apply_Luke node#data
+  | T_element "hints" ->
+      Hints (List.map parse_hint (List.filter is_xml_element node#sub_nodes))
+  | _ -> assert false
 let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
 let parse_tutor_dscs n =
   List.map
@@ -76,7 +140,13 @@ let msg_of_string' s =
   | T_element "subscribe" ->
       Subscribe (get_attr root "id", parse_tutor_ids root)
   | T_element "state_change" ->
-      State_change (get_attr root "id", parse_state root#data)
+      let state_node =
+        try
+          find_element ~deeply:false "gTopLevelStatus" root
+        with Not_found -> raise (No_element_found "gTopLevelStatus")
+      in
+      State_change (get_attr root "id", parse_state state_node)
+  | T_element "wow" -> Wow (get_attr root "id")
 
     (* tutor -> broker *)
   | T_element "register_tutor" ->
@@ -99,7 +169,8 @@ let msg_of_string' s =
       Musing_completed
         (get_attr root "id", get_attr root "musing_id",
         (match main_node#node_type with
-        | T_element "eureka" -> Eureka main_node#data (* TODO come parsare sta roba? *)
+        | T_element "eureka" ->
+            Eureka (parse_hint main_node)
         | T_element "sorry" -> Sorry
         | _ -> assert false)) (* can't be there, see 'find_element' above *)
 
@@ -119,13 +190,18 @@ let msg_of_string' s =
         List.map
           (fun n -> get_attr n "id")
           (List.filter is_xml_element (find_element "started" root)#sub_nodes))
-  | T_element "hint" -> Hint (get_attr root "id", parse_hint root#data)
+  | T_element "hint" -> Hint (get_attr root "id", parse_hint root)
 
     (* broker -> tutor *)
   | T_element "tutor_registered" -> Tutor_registered (get_attr root "id")
   | T_element "tutor_unregistered" -> Tutor_unregistered (get_attr root "id")
   | T_element "start_musing" ->
-      Start_musing (get_attr root "id", parse_state root#data)
+      let state_node =
+        try
+          find_element ~deeply:false "gTopLevelStatus" root
+        with Not_found -> raise (No_element_found "gTopLevelStatus")
+      in
+      Start_musing (get_attr root "id", parse_state state_node)
   | T_element "abort_musing" ->
       Abort_musing (get_attr root "id", get_attr root "musing_id")
   | T_element "thanks" -> Thanks (get_attr root "id", get_attr root "musing_id")
@@ -137,8 +213,35 @@ let msg_of_string s =
     msg_of_string' s
   with e -> raise (Parse_error (s, Printexc.to_string e))
 
-let pp_state s = s  (* TODO pretty print state *)
-let pp_hint s = s   (* TODO pretty print hint *)
+let pp_state (type_string, body_string, goal) =
+  (* ASSUMPTION: type_string and body_string are well formed XML document
+  contents (i.e. they don't contain heading <?xml ... ?> declaration nor DOCTYPE
+  one *)
+  let res =
+    "<gTopLevelStatus>\n" ^
+    (sprintf "<CurrentGoal>%d</CurrentGoal>\n" goal) ^
+    type_string ^ "\n" ^
+    body_string ^ "\n" ^
+    "</gTopLevelStatus>\n"
+  in
+  res
+
+let rec pp_hint = function
+  | Use_ring_Luke -> sprintf "<ring />"
+  | Use_fourier_Luke -> sprintf "<fourier />"
+  | Use_reflexivity_Luke -> sprintf "<reflexivity />"
+  | Use_symmetry_Luke -> sprintf "<symmetry />"
+  | Use_assumption_Luke -> sprintf "<assumption />"
+  | Use_contradiction_Luke -> sprintf "<contradiction />"
+  | Use_exists_Luke -> sprintf "<exists />"
+  | Use_split_Luke -> sprintf "<split />"
+  | Use_left_Luke -> sprintf "<left />"
+  | Use_right_Luke -> sprintf "<right />"
+  | Use_apply_Luke term -> sprintf "<apply>%s</apply>" term
+  | Hints hints ->
+      sprintf "<hints>\n%s\n</hints>"
+        (String.concat "\n" (List.map pp_hint hints))
+
 let pp_hint_type s = s   (* TODO pretty print hint_type *)
 let pp_tutor_dscs =
   List.fold_left
@@ -163,6 +266,7 @@ let string_of_msg = function
   | State_change (id, state) ->
       sprintf "<state_change id=\"%s\">%s</state_change>"
         id (pp_state state)
+  | Wow id -> sprintf "<wow id=\"%s\" />" id
   | Register_tutor (id, url, hint_type, dsc) ->
       sprintf
 "<register_tutor id=\"%s\" url=\"%s\">
@@ -181,7 +285,7 @@ let string_of_msg = function
         id musing_id
         (match result with
         | Sorry -> "<sorry />"
-        | Eureka s -> sprintf "<eureka>%s</eureka>" s)
+        | Eureka hint -> sprintf "<eureka>%s</eureka>" (pp_hint hint))
   | Client_registered id -> sprintf "<client_registered id=\"%s\" />" id
   | Client_unregistered id -> sprintf "<client_unregistered id=\"%s\" />" id
   | Tutor_list (id, tutor_dscs) ->
@@ -210,11 +314,36 @@ let string_of_msg = function
       sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
   | Thanks (id, musing_id) ->
       sprintf "<thanks id=\"%s\" musing_id=\"%s\" />" id musing_id
+  | Too_late (id, musing_id) ->
+      sprintf "<too_late id=\"%s\" musing_id=\"%s\" />" id musing_id
+;;
+
+  (* debugging function that dump on stderr the sent messages *)
+let dump_msg msg =
+  if debug then
+    prerr_endline
+      (sprintf "<SENDING_MESSAGE>\n%s\n</SENDING_MESSAGE>"
+        (match msg with
+        | State_change _ -> "<state_change>omissis ...</state_change>"
+        | msg -> string_of_msg msg))
+;;
 
 let submit_req ~url msg =
-  msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
+  dump_msg msg;
+  if debug then (prerr_string "Waiting for an answer ... "; flush stderr);
+  let res =
+    msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
+  in
+  if debug then (prerr_string "answer received!\n"; flush stderr);
+  res
+;;
 let return_xml_msg body outchan =
   Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan
-let respond_msg msg = return_xml_msg (string_of_msg msg);;
+;;
+let respond_msg msg outchan =
+  dump_msg msg;
+  return_xml_msg (string_of_msg msg) outchan
+(*   close_out outchan *)
+;;
 let respond_exc name value = respond_msg (Exception (name, value));;
 

diff --git a/helm/hbugs/common/hbugs_messages.mli b/helm/hbugs/common/hbugs_messages.mli
index d035dcff11899651950196627b569438e545e9b8..85ffe66c9e53b3ad232747fa15c469f3ff3b37ed 100644 (file)
--- a/helm/hbugs/common/hbugs_messages.mli
+++ b/helm/hbugs/common/hbugs_messages.mli
@@ -29,12 +29,21 @@
 open Hbugs_types;;
 
 exception Parse_error of string * string  (* parsing subject, reason *)
+exception Unexpected_message of message;;
 
 val msg_of_string: string -> message
 val string_of_msg: message -> string
 
 val submit_req: url:string -> message -> message
+  (** close outchan afterwards *)
 val respond_msg: message -> out_channel -> unit
+  (** close outchan afterwards *)
   (* exception_name, exception_value, output_channel *)
 val respond_exc: string -> string -> out_channel -> unit
 
+(* TODO the below functions are for debugging only and shouldn't be exposed *)
+val parse_state:
+  ('a Pxp_document.node Pxp_document.extension as 'a) Pxp_document.node ->
+    (string * string * int)
+val pp_state: (string * string * int) -> string
+