[parsing] unify checks for contiguity of tokens in Ltac2 and G_prim

2 files changed, 31 insertions, 8 deletions

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/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 8e5aae4900..adc1606016 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -82,9 +82,7 @@ let test_lpar_id_rpar =
 
 let check_no_space tok m strm =
   let n = Stream.count strm in
-  let (_, ep) = Loc.unloc (tok n) in
-  let (bp, _) = Loc.unloc (tok (n + 1)) in
-  if Int.equal ep bp then Some m else None
+  if G_prim.contiguous tok n (n+m-1) then Some m else None
 
 let test_ampersand_ident =
   entry_of_lookahead "test_ampersand_ident" begin