Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t`

7 files changed, 22 insertions, 108 deletions

diff --git a/gramlib/dune b/gramlib/dune
index 6a9e622b4c..8ca6aff25a 100644
--- a/gramlib/dune
+++ b/gramlib/dune
@@ -1,3 +1,4 @@
 (library
  (name gramlib)
- (public_name coq.gramlib))
+ (public_name coq.gramlib)
+ (libraries coq.lib))
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 285c14ec62..8f7953b714 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -130,7 +130,7 @@ let loc_of_token_interval bp ep =
   if bp == ep then
     if bp == 0 then Ploc.dummy else Ploc.after (!floc (bp - 1)) 0 1
   else
-    let loc1 = !floc bp in let loc2 = !floc (pred ep) in Ploc.encl loc1 loc2
+    let loc1 = !floc bp in let loc2 = !floc (pred ep) in Loc.merge loc1 loc2
 
 let name_of_symbol entry =
   function
@@ -816,7 +816,7 @@ let parse_parsable entry p =
       let cnt = Stream.count ts in
       let loc = fun_loc cnt in
       if !token_count - 1 <= cnt then loc
-      else Ploc.encl loc (fun_loc (!token_count - 1))
+      else Loc.merge loc (fun_loc (!token_count - 1))
     with Failure _ -> Ploc.make_unlined (Stream.count cs, Stream.count cs + 1)
   in
   floc := fun_loc;
@@ -884,7 +884,7 @@ module type S =
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
         ('self, 'b -> 'a, 'r) ty_rule
-    val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production
+    val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
     module Unsafe :
       sig
         val clear_entry : 'a Entry.e -> unit
@@ -946,7 +946,7 @@ module GMake (L : GLexerType) =
     let r_stop = []
     let r_next r s = r @ [s]
     let production
-        (p : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f) : 'a ty_production =
+        (p : ('a, 'f, Loc.t -> 'a) ty_rule * 'f) : 'a ty_production =
       Obj.magic p
     module Unsafe =
       struct
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 0c585a7c0d..4b61286859 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -58,7 +58,7 @@ module type S =
     val r_next :
       ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
         ('self, 'b -> 'a, 'r) ty_rule
-    val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production
+    val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
 
     module Unsafe :
       sig
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index 986363ec1f..7b8618fd20 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -6,8 +6,7 @@ type pattern = string * string
 
 exception Error of string
 
-type location = Ploc.t
-type location_function = int -> location
+type location_function = int -> Loc.t
 type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
 
 type 'te lexer =
@@ -16,4 +15,4 @@ type 'te lexer =
     tok_removing : pattern -> unit;
     mutable tok_match : pattern -> 'te -> string;
     tok_text : pattern -> string;
-    mutable tok_comm : location list option }
+    mutable tok_comm : Loc.t list option }
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 96b432a8ad..63c89dac28 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -30,8 +30,8 @@ type 'te lexer =
     tok_removing : pattern -> unit;
     mutable tok_match : pattern -> 'te -> string;
     tok_text : pattern -> string;
-    mutable tok_comm : Ploc.t list option }
+    mutable tok_comm : Loc.t list option }
 and 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
-and location_function = int -> Ploc.t
+and location_function = int -> Loc.t
   (** The type of a function giving the location of a token in the
       source from the token number in the stream (starting from zero). *)
diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml
index 082686db01..9342fc6c1d 100644
--- a/gramlib/ploc.ml
+++ b/gramlib/ploc.ml
@@ -2,60 +2,23 @@
 (* ploc.ml,v *)
 (* Copyright (c) INRIA 2007-2017 *)
 
-type t =
-  { fname : string;
-    line_nb : int;
-    bol_pos : int;
-    line_nb_last : int;
-    bol_pos_last : int;
-    bp : int;
-    ep : int;
-    comm : string;
-    ecomm : string }
-
-let make_loc fname line_nb bol_pos (bp, ep) comm =
-  {fname = fname; line_nb = line_nb; bol_pos = bol_pos;
-   line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep;
-   comm = comm; ecomm = ""}
+open Loc
 
 let make_unlined (bp, ep) =
-  {fname = ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+  {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
    bp = bp; ep = ep; comm = ""; ecomm = ""}
 
 let dummy =
-  {fname = ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+  {fname = InFile ""; line_nb = 1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
    bp = 0; ep = 0; comm = ""; ecomm = ""}
 
-let file_name loc = loc.fname
-let first_pos loc = loc.bp
-let last_pos loc = loc.ep
-let line_nb loc = loc.line_nb
-let bol_pos loc = loc.bol_pos
-let line_nb_last loc = loc.line_nb_last
-let bol_pos_last loc = loc.bol_pos_last
-let comment loc = loc.comm
-let comment_last loc = loc.ecomm
-
 (* *)
 
-let encl loc1 loc2 =
-  if loc1.bp < loc2.bp then
-    if loc1.ep < loc2.ep then
-      {fname = loc1.fname; line_nb = loc1.line_nb; bol_pos = loc1.bol_pos;
-       line_nb_last = loc2.line_nb_last; bol_pos_last = loc2.bol_pos_last;
-       bp = loc1.bp; ep = loc2.ep; comm = loc1.comm; ecomm = loc2.comm}
-    else loc1
-  else if loc2.ep < loc1.ep then
-    {fname = loc2.fname; line_nb = loc2.line_nb; bol_pos = loc2.bol_pos;
-     line_nb_last = loc1.line_nb_last; bol_pos_last = loc1.bol_pos_last;
-     bp = loc2.bp; ep = loc1.ep; comm = loc2.comm; ecomm = loc1.comm}
-  else loc2
-let shift sh loc = {loc with bp = sh + loc.bp; ep = sh + loc.ep}
 let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len}
 let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len}
 let with_comment loc comm = {loc with comm = comm}
 
-exception Exc of t * exn
+exception Exc of Loc.t * exn
 
 let raise loc exc =
   match exc with
diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli
index 2ce6382183..766e96fdfc 100644
--- a/gramlib/ploc.mli
+++ b/gramlib/ploc.mli
@@ -2,85 +2,36 @@
 (* ploc.mli,v *)
 (* Copyright (c) INRIA 2007-2017 *)
 
-(** Locations and some pervasive type and value. *)
-
-type t
-
 (* located exceptions *)
 
-exception Exc of t * exn
+exception Exc of Loc.t * exn
    (** [Ploc.Exc loc e] is an encapsulation of the exception [e] with
        the input location [loc]. To be used to specify a location
        for an error. This exception must not be raised by [raise] but
        rather by [Ploc.raise] (see below), to prevent the risk of several
        encapsulations of [Ploc.Exc]. *)
-val raise : t -> exn -> 'a
+val raise : Loc.t -> exn -> 'a
    (** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc],
        re-raise it (ignoring the new location [loc]), else raise the
        exception [Ploc.Exc loc e]. *)
 
-(* making locations *)
-
-val make_loc : string -> int -> int -> int * int -> string -> t
-   (** [Ploc.make_loc fname line_nb bol_pos (bp, ep) comm] creates a location
-       starting at line number [line_nb], where the position of the beginning
-       of the line is [bol_pos] and between the positions [bp] (included) and
-       [ep] excluded. And [comm] is the comment before the location. The
-       positions are in number of characters since the begin of the stream. *)
-val make_unlined : int * int -> t
+val make_unlined : int * int -> Loc.t
    (** [Ploc.make_unlined] is like [Ploc.make] except that the line number
        is not provided (to be used e.g. when the line number is unknown. *)
 
-val dummy : t
+val dummy : Loc.t
    (** [Ploc.dummy] is a dummy location, used in situations when location
        has no meaning. *)
 
-(* getting location info *)
-
-val file_name : t -> string
-   (** [Ploc.file_name loc] returns the file name of the location. *)
-val first_pos : t -> int
-   (** [Ploc.first_pos loc] returns the position of the begin of the location
-       in number of characters since the beginning of the stream. *)
-val last_pos : t -> int
-   (** [Ploc.last_pos loc] returns the position of the first character not
-       in the location in number of characters since the beginning of the
-       stream. *)
-val line_nb : t -> int
-   (** [Ploc.line_nb loc] returns the line number of the location or [-1] if
-       the location does not contain a line number (i.e. built with
-       [Ploc.make_unlined]. *)
-val bol_pos : t -> int
-   (** [Ploc.bol_pos loc] returns the position of the beginning of the line
-       of the location in number of characters since the beginning of
-       the stream, or [0] if the location does not contain a line number
-       (i.e. built with [Ploc.make_unlined]. *)
-val line_nb_last : t -> int
-val bol_pos_last : t -> int
-   (** Return the line number and the position of the beginning of the line
-       of the last position. *)
-val comment : t -> string
-   (** [Ploc.comment loc] returns the comment before the location. *)
-val comment_last : t -> string
-   (** [Ploc.comment loc] returns the last comment of the location. *)
-
 (* combining locations *)
 
-val encl : t -> t -> t
-   (** [Ploc.encl loc1 loc2] returns the location starting at the
-       smallest start of [loc1] and [loc2] and ending at the greatest end
-       of them. In other words, it is the location enclosing [loc1] and
-       [loc2]. *)
-val shift : int -> t -> t
-   (** [Ploc.shift sh loc] returns the location [loc] shifted with [sh]
-       characters. The line number is not recomputed. *)
-val sub : t -> int -> int -> t
+val sub : Loc.t -> int -> int -> Loc.t
    (** [Ploc.sub loc sh len] is the location [loc] shifted with [sh]
        characters and with length [len]. The previous ending position
        of the location is lost. *)
-val after : t -> int -> int -> t
+val after : Loc.t -> int -> int -> Loc.t
    (** [Ploc.after loc sh len] is the location just after loc (starting at
        the end position of [loc]) shifted with [sh] characters and of length
        [len]. *)
-val with_comment : t -> string -> t
+val with_comment : Loc.t -> string -> Loc.t
    (** Change the comment part of the given location *)