From 4651ed901a51659c31dbcb9a8b4f75d17321be14 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 19 Feb 2003 14:17:24 +0000 Subject: [PATCH] - 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 --- helm/hbugs/common/hbugs_messages.ml | 151 +++++++++++++++++++++++++-- helm/hbugs/common/hbugs_messages.mli | 9 ++ 2 files changed, 149 insertions(+), 11 deletions(-) diff --git a/helm/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml index 0eac0b149..c0f709484 100644 --- 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 declaration nor DOCTYPE + one *) + let res = + "\n" ^ + (sprintf "%d\n" goal) ^ + type_string ^ "\n" ^ + body_string ^ "\n" ^ + "\n" + in + res + +let rec pp_hint = function + | Use_ring_Luke -> sprintf "" + | Use_fourier_Luke -> sprintf "" + | Use_reflexivity_Luke -> sprintf "" + | Use_symmetry_Luke -> sprintf "" + | Use_assumption_Luke -> sprintf "" + | Use_contradiction_Luke -> sprintf "" + | Use_exists_Luke -> sprintf "" + | Use_split_Luke -> sprintf "" + | Use_left_Luke -> sprintf "" + | Use_right_Luke -> sprintf "" + | Use_apply_Luke term -> sprintf "%s" term + | Hints hints -> + sprintf "\n%s\n" + (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 "%s" id (pp_state state) + | Wow id -> sprintf "" id | Register_tutor (id, url, hint_type, dsc) -> sprintf " @@ -181,7 +285,7 @@ let string_of_msg = function id musing_id (match result with | Sorry -> "" - | Eureka s -> sprintf "%s" s) + | Eureka hint -> sprintf "%s" (pp_hint hint)) | Client_registered id -> sprintf "" id | Client_unregistered id -> sprintf "" id | Tutor_list (id, tutor_dscs) -> @@ -210,11 +314,36 @@ let string_of_msg = function sprintf "" id musing_id | Thanks (id, musing_id) -> sprintf "" id musing_id + | Too_late (id, musing_id) -> + sprintf "" id musing_id +;; + + (* debugging function that dump on stderr the sent messages *) +let dump_msg msg = + if debug then + prerr_endline + (sprintf "\n%s\n" + (match msg with + | State_change _ -> "omissis ..." + | 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 d035dcff1..85ffe66c9 100644 --- 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 + -- 2.39.2