From 8e3c2182d0c43530fc2cf62e63f5474773d04604 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 15 Aug 2015 19:43:22 +0200 Subject: Fixing richpp behaviour w.r.t. its specification. Contrarily to what was described in the API, nodes without annotations were not ignored by the printer but left there instead. --- lib/richpp.ml | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) (limited to 'lib') diff --git a/lib/richpp.ml b/lib/richpp.ml index c4a9c39d5a..b02d9903b4 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -85,18 +85,23 @@ let rich_pp annotate ppcmds = try Int.Map.find (int_of_string node) context.annotations with _ -> None in - let annotation = { - annotation = annotation; - startpos = pos; - endpos = context.offset; - } in - let xml = Element (node, annotation, List.rev child) in + let child = List.rev child in + let xml = match annotation with + | None -> child (** Ignore the node *) + | Some annotation -> + let annotation = { + annotation = Some annotation; + startpos = pos; + endpos = context.offset; + } in + [Element (node, annotation, child)] + in match ctx with | Leaf -> (** Final node: we keep the result in a dummy context *) - context.stack <- Node ("", [xml], 0, Leaf) + context.stack <- Node ("", List.rev xml, 0, Leaf) | Node (node, child, pos, ctx) -> - context.stack <- Node (node, xml :: child, pos, ctx) + context.stack <- Node (node, List.rev_append xml child, pos, ctx) in let open Format in -- cgit v1.2.3 From 2c1882815e7877bfc574f9f71eff6ce099145df5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 15 Aug 2015 19:51:50 +0200 Subject: Statically ensure that we omit null annotations in Richpp. --- lib/richpp.ml | 19 +++++-------------- lib/richpp.mli | 2 +- 2 files changed, 6 insertions(+), 15 deletions(-) (limited to 'lib') diff --git a/lib/richpp.ml b/lib/richpp.ml index b02d9903b4..45173ff307 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -10,7 +10,7 @@ open Util open Xml_datatype type 'annotation located = { - annotation : 'annotation option; + annotation : 'annotation; startpos : int; endpos : int } @@ -90,7 +90,7 @@ let rich_pp annotate ppcmds = | None -> child (** Ignore the node *) | Some annotation -> let annotation = { - annotation = Some annotation; + annotation = annotation; startpos = pos; endpos = context.offset; } in @@ -134,10 +134,8 @@ let rich_pp annotate ppcmds = let annotations_positions xml = let rec node accu = function - | Element (_, { annotation = Some annotation; startpos; endpos }, cs) -> + | Element (_, { annotation = annotation; startpos; endpos }, cs) -> children ((annotation, (startpos, endpos)) :: accu) cs - | Element (_, _, cs) -> - children accu cs | _ -> accu and children accu cs = @@ -152,16 +150,9 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = [ "startpos", string_of_int startpos; "endpos", string_of_int endpos ] - @ (match annotation with - | None -> [] - | Some annotation -> attributes_of_annotation annotation - ) - in - let tag = - match annotation with - | None -> index - | Some annotation -> tag_of_annotation annotation + @ (attributes_of_annotation annotation) in + let tag = tag_of_annotation annotation in Element (tag, attributes, List.map node cs) | PCData s -> PCData s diff --git a/lib/richpp.mli b/lib/richpp.mli index bf80c8dc8c..2c20197893 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -11,7 +11,7 @@ (** Each annotation of the semi-structured document refers to the substring it annotates. *) type 'annotation located = { - annotation : 'annotation option; + annotation : 'annotation; startpos : int; endpos : int } -- cgit v1.2.3 From 98618cfb6b326b70da29348bc5d212e41086f473 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 15 Aug 2015 19:17:26 +0200 Subject: More parametric type for generalized XML. --- lib/richpp.ml | 2 +- lib/richpp.mli | 6 +++--- lib/xml_datatype.mli | 14 ++++++-------- 3 files changed, 10 insertions(+), 12 deletions(-) (limited to 'lib') diff --git a/lib/richpp.ml b/lib/richpp.ml index 45173ff307..087c247299 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -17,7 +17,7 @@ type 'annotation located = { type 'a stack = | Leaf -| Node of string * 'a located gxml list * int * 'a stack +| Node of string * (string, 'a located) gxml list * int * 'a stack type 'a context = { mutable stack : 'a stack; diff --git a/lib/richpp.mli b/lib/richpp.mli index 2c20197893..5eb0e7b3b0 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -23,13 +23,13 @@ type 'annotation located = { annotation. If this function returns [None], then no annotation is put. *) val rich_pp : (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds -> - 'annotation located Xml_datatype.gxml + (string, 'annotation located) Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is built. *) val annotations_positions : - 'annotation located Xml_datatype.gxml -> + ('a, 'annotation located) Xml_datatype.gxml -> ('annotation * (int * int)) list (** [xml_of_rich_pp ssdoc] returns an XML representation of the @@ -37,5 +37,5 @@ val annotations_positions : val xml_of_rich_pp : ('annotation -> string) -> ('annotation -> (string * string) list) -> - 'annotation located Xml_datatype.gxml -> + (string, 'annotation located) Xml_datatype.gxml -> Xml_datatype.xml diff --git a/lib/xml_datatype.mli b/lib/xml_datatype.mli index f61ba032a2..f822080a6d 100644 --- a/lib/xml_datatype.mli +++ b/lib/xml_datatype.mli @@ -7,13 +7,11 @@ (************************************************************************) (** ['a gxml] is the type for semi-structured documents. They generalize - XML by allowing any kind of attributes. *) -type 'a gxml = - | Element of (string * 'a * 'a gxml list) + XML by allowing any kind of tags and attributes. *) +type ('a, 'b) gxml = + | Element of ('a * 'b * ('a, 'b) gxml list) | PCData of string -(** [xml] is a semi-structured documents where attributes are association - lists from string to string. *) -type xml = (string * string) list gxml - - +(** [xml] is a semi-structured documents where tags are strings and attributes + are association lists from string to string. *) +type xml = (string, (string * string) list) gxml -- cgit v1.2.3 From 54fb2cdf7bb5c45f5a237b2559fd26d90d8f4df1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 15 Aug 2015 19:27:43 +0200 Subject: More invariants in Richpp. We ensure statically by typing that the tags used by the rich printer are integers. Furthermore, we also expose through typing that tags are irrelevants in the returned XML. --- lib/richpp.ml | 16 +++++++++------- lib/richpp.mli | 4 ++-- 2 files changed, 11 insertions(+), 9 deletions(-) (limited to 'lib') diff --git a/lib/richpp.ml b/lib/richpp.ml index 087c247299..7f14ca992e 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -17,7 +17,7 @@ type 'annotation located = { type 'a stack = | Leaf -| Node of string * (string, 'a located) gxml list * int * 'a stack +| Node of int * (unit, 'a located) gxml list * int * 'a stack type 'a context = { mutable stack : 'a stack; @@ -72,6 +72,7 @@ let rich_pp annotate ppcmds = let open_xml_tag tag = let () = push_pcdata () in + let tag = try int_of_string tag with _ -> assert false in context.stack <- Node (tag, [], context.offset, context.stack) in @@ -80,10 +81,11 @@ let rich_pp annotate ppcmds = match context.stack with | Leaf -> assert false | Node (node, child, pos, ctx) -> - let () = assert (String.equal tag node) in + let tag = try int_of_string tag with _ -> assert false in + let () = assert (Int.equal tag node) in let annotation = - try Int.Map.find (int_of_string node) context.annotations - with _ -> None + try Int.Map.find node context.annotations + with _ -> assert false in let child = List.rev child in let xml = match annotation with @@ -94,12 +96,12 @@ let rich_pp annotate ppcmds = startpos = pos; endpos = context.offset; } in - [Element (node, annotation, child)] + [Element ((), annotation, child)] in match ctx with | Leaf -> (** Final node: we keep the result in a dummy context *) - context.stack <- Node ("", List.rev xml, 0, Leaf) + context.stack <- Node ((-1), List.rev xml, 0, Leaf) | Node (node, child, pos, ctx) -> context.stack <- Node (node, List.rev_append xml child, pos, ctx) in @@ -128,7 +130,7 @@ let rich_pp annotate ppcmds = let () = pp_print_flush ft () in let () = assert (Buffer.length pp_buffer = 0) in match context.stack with - | Node ("", [xml], 0, Leaf) -> xml + | Node ((-1), [xml], 0, Leaf) -> xml | _ -> assert false diff --git a/lib/richpp.mli b/lib/richpp.mli index 5eb0e7b3b0..3f6463c88a 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -23,7 +23,7 @@ type 'annotation located = { annotation. If this function returns [None], then no annotation is put. *) val rich_pp : (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds -> - (string, 'annotation located) Xml_datatype.gxml + (unit, 'annotation located) Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is @@ -37,5 +37,5 @@ val annotations_positions : val xml_of_rich_pp : ('annotation -> string) -> ('annotation -> (string * string) list) -> - (string, 'annotation located) Xml_datatype.gxml -> + ('a, 'annotation located) Xml_datatype.gxml -> Xml_datatype.xml -- cgit v1.2.3 From 2f5bc3148579ff359f179c758a7f4e724a14adf7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 15 Aug 2015 21:49:22 +0200 Subject: Revert the four previous commits and update the description of Richpp. Correcting the code w.r.t. to the API was not the right solution. Instead, the API comment had to be corrected. --- lib/richpp.ml | 50 ++++++++++++++++++++++++++------------------------ lib/richpp.mli | 10 +++++----- lib/xml_datatype.mli | 14 ++++++++------ 3 files changed, 39 insertions(+), 35 deletions(-) (limited to 'lib') diff --git a/lib/richpp.ml b/lib/richpp.ml index 7f14ca992e..c4a9c39d5a 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -10,14 +10,14 @@ open Util open Xml_datatype type 'annotation located = { - annotation : 'annotation; + annotation : 'annotation option; startpos : int; endpos : int } type 'a stack = | Leaf -| Node of int * (unit, 'a located) gxml list * int * 'a stack +| Node of string * 'a located gxml list * int * 'a stack type 'a context = { mutable stack : 'a stack; @@ -72,7 +72,6 @@ let rich_pp annotate ppcmds = let open_xml_tag tag = let () = push_pcdata () in - let tag = try int_of_string tag with _ -> assert false in context.stack <- Node (tag, [], context.offset, context.stack) in @@ -81,29 +80,23 @@ let rich_pp annotate ppcmds = match context.stack with | Leaf -> assert false | Node (node, child, pos, ctx) -> - let tag = try int_of_string tag with _ -> assert false in - let () = assert (Int.equal tag node) in + let () = assert (String.equal tag node) in let annotation = - try Int.Map.find node context.annotations - with _ -> assert false - in - let child = List.rev child in - let xml = match annotation with - | None -> child (** Ignore the node *) - | Some annotation -> - let annotation = { - annotation = annotation; - startpos = pos; - endpos = context.offset; - } in - [Element ((), annotation, child)] + try Int.Map.find (int_of_string node) context.annotations + with _ -> None in + let annotation = { + annotation = annotation; + startpos = pos; + endpos = context.offset; + } in + let xml = Element (node, annotation, List.rev child) in match ctx with | Leaf -> (** Final node: we keep the result in a dummy context *) - context.stack <- Node ((-1), List.rev xml, 0, Leaf) + context.stack <- Node ("", [xml], 0, Leaf) | Node (node, child, pos, ctx) -> - context.stack <- Node (node, List.rev_append xml child, pos, ctx) + context.stack <- Node (node, xml :: child, pos, ctx) in let open Format in @@ -130,14 +123,16 @@ let rich_pp annotate ppcmds = let () = pp_print_flush ft () in let () = assert (Buffer.length pp_buffer = 0) in match context.stack with - | Node ((-1), [xml], 0, Leaf) -> xml + | Node ("", [xml], 0, Leaf) -> xml | _ -> assert false let annotations_positions xml = let rec node accu = function - | Element (_, { annotation = annotation; startpos; endpos }, cs) -> + | Element (_, { annotation = Some annotation; startpos; endpos }, cs) -> children ((annotation, (startpos, endpos)) :: accu) cs + | Element (_, _, cs) -> + children accu cs | _ -> accu and children accu cs = @@ -152,9 +147,16 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = [ "startpos", string_of_int startpos; "endpos", string_of_int endpos ] - @ (attributes_of_annotation annotation) + @ (match annotation with + | None -> [] + | Some annotation -> attributes_of_annotation annotation + ) + in + let tag = + match annotation with + | None -> index + | Some annotation -> tag_of_annotation annotation in - let tag = tag_of_annotation annotation in Element (tag, attributes, List.map node cs) | PCData s -> PCData s diff --git a/lib/richpp.mli b/lib/richpp.mli index 3f6463c88a..a0d3c374b2 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -11,7 +11,7 @@ (** Each annotation of the semi-structured document refers to the substring it annotates. *) type 'annotation located = { - annotation : 'annotation; + annotation : 'annotation option; startpos : int; endpos : int } @@ -20,16 +20,16 @@ type 'annotation located = { of [ppcmds] as a semi-structured document that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired - annotation. If this function returns [None], then no annotation is put. *) + annotation. *) val rich_pp : (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds -> - (unit, 'annotation located) Xml_datatype.gxml + 'annotation located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is built. *) val annotations_positions : - ('a, 'annotation located) Xml_datatype.gxml -> + 'annotation located Xml_datatype.gxml -> ('annotation * (int * int)) list (** [xml_of_rich_pp ssdoc] returns an XML representation of the @@ -37,5 +37,5 @@ val annotations_positions : val xml_of_rich_pp : ('annotation -> string) -> ('annotation -> (string * string) list) -> - ('a, 'annotation located) Xml_datatype.gxml -> + 'annotation located Xml_datatype.gxml -> Xml_datatype.xml diff --git a/lib/xml_datatype.mli b/lib/xml_datatype.mli index f822080a6d..f61ba032a2 100644 --- a/lib/xml_datatype.mli +++ b/lib/xml_datatype.mli @@ -7,11 +7,13 @@ (************************************************************************) (** ['a gxml] is the type for semi-structured documents. They generalize - XML by allowing any kind of tags and attributes. *) -type ('a, 'b) gxml = - | Element of ('a * 'b * ('a, 'b) gxml list) + XML by allowing any kind of attributes. *) +type 'a gxml = + | Element of (string * 'a * 'a gxml list) | PCData of string -(** [xml] is a semi-structured documents where tags are strings and attributes - are association lists from string to string. *) -type xml = (string, (string * string) list) gxml +(** [xml] is a semi-structured documents where attributes are association + lists from string to string. *) +type xml = (string * string) list gxml + + -- cgit v1.2.3