X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fcommon%2Fhbugs_messages.ml;h=0cc0f1b1fe599d079c21f79248a7253ebe361e10;hb=d2c60bae1c4badba0a0f29e3fd2faed6d3a1869e;hp=d0a6fe1dbad25b1d5274f25f335e3b97eb6c561d;hpb=5d7d6bd5090f3f82279bef0b93b4b361a5b1d751;p=helm.git
diff --git a/helm/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml
index d0a6fe1db..0cc0f1b1f 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,74 @@ 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 parse_hint node =
+ let rec parse_hint_node node =
+ match node#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_node (List.filter is_xml_element node#sub_nodes))
+ | _ -> assert false (* CSC: should this assert false be a raise something? *)
+ in
+ match List.filter is_xml_element node#sub_nodes with
+ [node] -> parse_hint_node node
+ | _ -> assert false (* CSC: should this assert false be a raise something? *)
+
let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
let parse_tutor_dscs n =
List.map
@@ -76,7 +146,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 +175,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 +196,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 +219,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 +272,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 +291,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,7 +320,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 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));;