Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involving &

Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Ack-by: ggonthier
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: vbgl

4 files changed, 38 insertions, 11 deletions

diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index a27d6450b7..de23f05a9e 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -785,12 +785,14 @@ let next_token ~diff_mode loc s =
 (* Location table system for creating tables associating a token count
    to its location in a char stream (the source) *)
 
-let locerr () = invalid_arg "Lexer: location function"
+let locerr i =
+  let m = "Lexer: location function called on token "^string_of_int i in
+  invalid_arg m
 
 let loct_create () = Hashtbl.create 207
 
 let loct_func loct i =
-  try Hashtbl.find loct i with Not_found -> locerr ()
+  try Hashtbl.find loct i with Not_found -> locerr i
 
 let loct_add loct i loc = Hashtbl.add loct i loc
 
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 8fdec7d1a8..78a12a2e7d 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -84,7 +84,7 @@ let err () = raise Stream.Failure
 (* admissible notation "(x t)" *)
 let lpar_id_coloneq =
   Pcoq.Entry.of_parser "test_lpar_id_coloneq"
-    (fun strm ->
+    (fun _ strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
             (match stream_nth 1 strm with
@@ -99,7 +99,7 @@ let lpar_id_coloneq =
 
 let impl_ident_head =
   Pcoq.Entry.of_parser "impl_ident_head"
-    (fun strm ->
+    (fun _ strm ->
       match stream_nth 0 strm with
 	| KEYWORD "{" ->
 	    (match stream_nth 1 strm with
@@ -112,7 +112,7 @@ let impl_ident_head =
 
 let name_colon =
   Pcoq.Entry.of_parser "name_colon"
-    (fun strm ->
+    (fun _ strm ->
       match stream_nth 0 strm with
 	| IDENT s ->
             (match stream_nth 1 strm with
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index c1f52c5b39..020501aedf 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -31,10 +31,35 @@ let my_int_of_string loc s =
   with Failure _ ->
     CErrors.user_err ~loc (Pp.str "This number is too large.")
 
-let check_nospace loc expected =
-  let (bp, ep) = Loc.unloc loc in
-  if ep = bp + String.length expected then () else
-  Gramlib.Ploc.raise loc (Stream.Error ("'" ^ expected ^ "' expected"))
+let rec contiguous tok n m =
+    n == m
+  ||
+    let (_, ep) = Loc.unloc (tok n) in
+    let (bp, _) = Loc.unloc (tok (n + 1)) in
+    Int.equal ep bp && contiguous tok (succ n) m
+
+let rec lookahead_kwds strm n = function
+  | [] -> ()
+  | x :: xs ->
+      let toks = Stream.npeek (n+1) strm in
+      match List.nth toks n with
+      | Tok.KEYWORD y ->
+          if String.equal x y then lookahead_kwds strm (succ n) xs
+          else raise Stream.Failure
+      | _ -> raise Stream.Failure
+      | exception (Failure _) -> raise Stream.Failure
+
+(* [test_nospace m] fails if the next m tokens are not contiguous keywords *)
+let test_nospace m = assert(m <> []); Pcoq.Entry.of_parser "test_nospace"
+   (fun tok strm ->
+      let n = Stream.count strm in
+      lookahead_kwds strm 0 m;
+      if contiguous tok n (n + List.length m - 1) then ()
+      else raise Stream.Failure)
+
+let test_nospace_pipe_closedcurly =
+  test_nospace ["|"; "}"]
+
 
 }
 
@@ -130,6 +155,6 @@ GRAMMAR EXTEND Gram
     [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
   bar_cbrace:
-    [ [ "|"; "}" -> { check_nospace loc "|}" } ] ]
+    [ [ test_nospace_pipe_closedcurly; "|"; "}" -> { () } ] ]
   ;
 END
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index cde867d2ef..7efeab6ba0 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -29,7 +29,7 @@ module Entry : sig
   val create : string -> 'a t
   val parse : 'a t -> Parsable.t -> 'a
   val print : Format.formatter -> 'a t -> unit
-  val of_parser : string -> (Tok.t Stream.t -> 'a) -> 'a t
+  val of_parser : string -> (Gramlib.Plexing.location_function -> Tok.t Stream.t -> 'a) -> 'a t
   val parse_token_stream : 'a t -> Tok.t Stream.t -> 'a
   val name : 'a t -> string
 end