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

3 files changed, 30 insertions, 71 deletions

diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index d81ee475b5..c327f8aa43 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -13,28 +13,6 @@ open Util
 open Tok
 open Gramlib
 
-(** Location utilities  *)
-let ploc_file_of_coq_file = function
-| Loc.ToplevelInput -> ""
-| Loc.InFile f -> f
-
-let coq_file_of_ploc_file s =
-  if s = "" then Loc.ToplevelInput else Loc.InFile s
-
-let from_coqloc fname line_nb bol_pos bp ep =
-  Ploc.make_loc (ploc_file_of_coq_file fname) line_nb bol_pos (bp, ep) ""
-
-let to_coqloc loc =
-  { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
-    Loc.line_nb = Ploc.line_nb loc;
-    Loc.bol_pos = Ploc.bol_pos loc;
-    Loc.bp = Ploc.first_pos loc;
-    Loc.ep = Ploc.last_pos loc;
-    Loc.line_nb_last = Ploc.line_nb_last loc;
-    Loc.bol_pos_last = Ploc.bol_pos_last loc; }
-
-let (!@) = to_coqloc
-
 (* Dictionaries: trees annotated with string options, each node being a map
    from chars to dictionaries (the subtrees). A trie, in other words. *)
 
@@ -128,18 +106,22 @@ module Error = struct
 end
 open Error
 
-let err loc str = Loc.raise ~loc:(to_coqloc loc) (Error.E str)
+let err loc str = Loc.raise ~loc (Error.E str)
 
 let bad_token str = raise (Error.E (Bad_token str))
 
 (* Update a loc without allocating an intermediate pair *)
 let set_loc_pos loc bp ep =
-  Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp)
+  Ploc.sub loc (bp - loc.Loc.bp) (ep - bp)
 
 (* Increase line number by 1 and update position of beginning of line *)
 let bump_loc_line loc bol_pos =
-  Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos
-		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
+  Loc.{ loc with
+        line_nb      = loc.line_nb + 1;
+        line_nb_last = loc.line_nb + 1;
+        bol_pos;
+        bol_pos_last = bol_pos;
+      }
 
 (* Same as [bump_loc_line], but for the last line in location *)
 (* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop,
@@ -147,19 +129,25 @@ let bump_loc_line loc bol_pos =
 (* Warning: [bump_loc_line_last] changes the end position. You may need to call
    [set_loc_pos] to fix it. *)
 let bump_loc_line_last loc bol_pos =
-  let loc' =
-    Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos
-		  (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc)
-  in
-  Ploc.encl loc loc'
+  let open Loc in
+  let loc' = { loc with
+               line_nb      = loc.line_nb_last + 1;
+               line_nb_last = loc.line_nb_last + 1;
+               bol_pos;
+               bol_pos_last = bol_pos;
+               bp = loc.bp + 1;
+               ep = loc.ep + 1;
+             } in
+  Loc.merge loc loc'
 
 (* For some reason, the [Ploc.after] function of Camlp5 does not update line
    numbers, so we define our own function that does it. *)
 let after loc =
-  let line_nb = Ploc.line_nb_last loc in
-  let bol_pos = Ploc.bol_pos_last loc in
-  Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos
-		(Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
+  Loc.{ loc with
+        line_nb = loc.line_nb_last;
+        bol_pos = loc.bol_pos_last;
+        bp      = loc.ep;
+      }
 
 (** Lexer conventions on tokens *)
 
@@ -324,7 +312,7 @@ let rec ident_tail loc len s = match Stream.peek s with
       | Utf8Token (st, n) when Unicode.is_unknown st ->
           let id = get_buff len in
           let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in
-          warn_unrecognized_unicode ~loc:!@loc (u,id); len
+          warn_unrecognized_unicode ~loc (u,id); len
       | _ -> len
 
 let rec number len s = match Stream.peek s with
@@ -368,7 +356,7 @@ let rec string loc ~comm_level bp len s = match Stream.peek s with
             Stream.junk s;
             let () = match comm_level with
             | Some 0 ->
-              warn_comment_terminator_in_string ~loc:!@loc ()
+              warn_comment_terminator_in_string ~loc ()
             | _ -> ()
             in
             let comm_level = Option.map pred comm_level in
@@ -757,7 +745,7 @@ let token_text = function
 
 let func cs =
   let loct = loct_create () in
-  let cur_loc = ref (from_coqloc !current_file 1 0 0 0) in
+  let cur_loc = ref (Loc.create !current_file 1 0 0 0) in
   let ts =
     Stream.from
       (fun i ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 816a02a6aa..923147ba2e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -14,29 +14,6 @@ open Extend
 open Genarg
 open Gramlib
 
-(** Location Utils  *)
-let ploc_file_of_coq_file = function
-| Loc.ToplevelInput -> ""
-| Loc.InFile f -> f
-
-let coq_file_of_ploc_file s =
-  if s = "" then Loc.ToplevelInput else Loc.InFile s
-
-let of_coqloc loc =
-  let open Loc in
-  Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) ""
-
-let to_coqloc loc =
-  { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
-    Loc.line_nb = Ploc.line_nb loc;
-    Loc.bol_pos = Ploc.bol_pos loc;
-    Loc.bp = Ploc.first_pos loc;
-    Loc.ep = Ploc.last_pos loc;
-    Loc.line_nb_last = Ploc.line_nb_last loc;
-    Loc.bol_pos_last = Ploc.bol_pos_last loc; }
-
-let (!@) = to_coqloc
-
 (** The parser of Coq *)
 module G : sig
 
@@ -112,7 +89,7 @@ end with type 'a Entry.e = 'a Extend.entry = struct
     with Ploc.Exc (loc,e) ->
       CLexer.drop_lexer_state ();
       let loc' = Loc.get_loc (Exninfo.info e) in
-      let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
+      let loc = match loc' with None -> loc | Some loc -> loc in
       Loc.raise ~loc e
 
   let comment_state (p,state) =
@@ -197,8 +174,8 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol
   let warning msg = Feedback.msg_warning Pp.(str msg) in
   G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)
 
-and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function
-| Stop -> Casted (G.r_stop, fun act loc -> act (!@loc))
+and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Loc.t -> r) casted_rule = function
+| Stop -> Casted (G.r_stop, fun act loc -> act loc)
 | Next (r, s) ->
   let Casted (r, cast) = symbol_of_rule r in
   Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x)))
@@ -209,7 +186,7 @@ and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function
   G.production (symb, cast act)
 
 (** FIXME: This is a hack around a deficient camlp5 API *)
-type 'a any_production = AnyProduction : ('a, 'f, Ploc.t -> 'a) G.ty_rule * 'f -> 'a any_production
+type 'a any_production = AnyProduction : ('a, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production
 
 let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function
 | Rule (toks, act) ->
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 69ba57d516..352857d4cd 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -13,7 +13,6 @@ open Extend
 open Genarg
 open Constrexpr
 open Libnames
-open Gramlib
 
 (** The parser of Coq *)
 
@@ -261,11 +260,6 @@ val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t
 
 val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
 
-(** Location Utils  *)
-val of_coqloc : Loc.t -> Ploc.t
-val to_coqloc : Ploc.t -> Loc.t
-val (!@) : Ploc.t -> Loc.t
-
 type frozen_t
 val parser_summary_tag : frozen_t Summary.Dyn.tag