X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fhbugs%2Fcommon%2Fhbugs_messages.ml;h=b7e6f5ddc59a5cd7bdbed32c0d91df5fbe668b17;hb=8bc543384089a7da61d49d336afa23caaa8cb26e;hp=c0f70948462badd3f2a6678a7fafea2e365ce758;hpb=4651ed901a51659c31dbcb9a8b4f75d17321be14;p=helm.git
diff --git a/helm/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml
index c0f709484..b7e6f5ddc 100644
--- a/helm/hbugs/common/hbugs_messages.ml
+++ b/helm/hbugs/common/hbugs_messages.ml
@@ -36,6 +36,7 @@ open Pxp_yacc;;
let debug = true;;
exception Attribute_not_found of string;;
+exception Empty_node;; (** found a node with no _element_ children *)
exception No_element_found of string;;
exception Parse_error of string * string;; (* parsing subject, reason *)
exception Unexpected_message of message;;
@@ -47,17 +48,18 @@ let get_attr node name =
| Value s -> s
| _ -> raise Not_found)
with Not_found -> raise (Attribute_not_found name)
+let assert_element n name =
+ match n#node_type with
+ | T_element n when n = name ->
+ ()
+ | _ -> raise (Parse_error ("", "Expected node: " ^ name))
(** 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
+ if (List.filter is_xml_element root#sub_nodes) = [] then
+ raise Empty_node;
let buf = Buffer.create 10240 in
let node_to_string (node: ('a node extension as 'a) node) =
Buffer.clear buf;
@@ -69,15 +71,14 @@ let parse_state (root: ('a node extension as 'a) node) =
let (goal_node, type_node, body_node) =
try
(find_element "CurrentGoal" root,
- find_element "ConstantType" root, (* TODO e' sempre ConstantType? *)
+ find_element "ConstantType" root,
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 type_node "ConstantType";
assert_element body_node "CurrentProof";
goal_node#write (`Out_buffer buf) `Enc_utf8;
let (type_string, body_string) =
@@ -93,23 +94,29 @@ let parse_state (root: ('a node extension as 'a) node) =
(** 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 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
@@ -142,10 +149,14 @@ let msg_of_string' s =
| T_element "state_change" ->
let state_node =
try
- find_element ~deeply:false "gTopLevelStatus" root
- with Not_found -> raise (No_element_found "gTopLevelStatus")
+ Some (find_element ~deeply:false "gTopLevelStatus" root)
+ with Not_found -> None
in
- State_change (get_attr root "id", parse_state state_node)
+ State_change
+ (get_attr root "id",
+ match state_node with
+ | Some n -> (try Some (parse_state n) with Empty_node -> None)
+ | None -> None)
| T_element "wow" -> Wow (get_attr root "id")
(* tutor -> broker *)
@@ -205,6 +216,8 @@ let msg_of_string' s =
| 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")
+ | T_element "too_late" ->
+ Too_late (get_attr root "id", get_attr root "musing_id")
| _ -> raise (No_element_found s)
@@ -213,18 +226,17 @@ let msg_of_string s =
msg_of_string' s
with e -> raise (Parse_error (s, Printexc.to_string e))
-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 =
+let pp_state = function
+ | Some (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 *)
"\n" ^
(sprintf "%d\n" goal) ^
type_string ^ "\n" ^
body_string ^ "\n" ^
"\n"
- in
- res
+ | None -> "\n"
let rec pp_hint = function
| Use_ring_Luke -> sprintf ""
@@ -309,7 +321,8 @@ let string_of_msg = function
| Tutor_registered id -> sprintf "" id
| Tutor_unregistered id -> sprintf "" id
| Start_musing (id, state) ->
- sprintf "%s" id (pp_state state)
+ sprintf "%s"
+ id (pp_state (Some state))
| Abort_musing (id, musing_id) ->
sprintf "" id musing_id
| Thanks (id, musing_id) ->