Merge PR #11695: Refactor lookaheads

Reviewed-by: herbelin
Reviewed-by: ppedrot

3 files changed, 24 insertions, 59 deletions

diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 5835d75c79..f97c291c79 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -330,18 +330,10 @@ END
 {
 
 let local_test_lpar_id_colon =
-  let err () = raise Stream.Failure in
-  Pcoq.Entry.of_parser "lpar_id_colon"
-    (fun _ strm ->
-      match Util.stream_nth 0 strm with
-        | Tok.KEYWORD "(" ->
-            (match Util.stream_nth 1 strm with
-              | Tok.IDENT _ ->
-                  (match Util.stream_nth 2 strm with
-                    | Tok.KEYWORD ":" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "lpar_id_colon" begin
+    lk_kw "(" >> lk_ident >> lk_kw ":"
+  end
 
 let pr_lpar_id_colon _ _ _ _ = mt ()
 
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 7ea843ca69..c163438718 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -20,7 +20,6 @@ open Tacexpr
 open Namegen
 open Genarg
 open Genredexpr
-open Tok (* necessary for camlp5 *)
 open Names
 open Attributes
 
@@ -63,14 +62,10 @@ let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
 
 (* Hack to parse "[ id" without dropping [ *)
 let test_bracket_ident =
-  Pcoq.Entry.of_parser "test_bracket_ident"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "[" ->
-            (match stream_nth 1 strm with
-              | IDENT _ -> ()
-              | _ -> raise Stream.Failure)
-        | _ -> raise Stream.Failure)
+  let open Pcoq.Lookahead in
+  to_entry "test_bracket_ident" begin
+    lk_kw "[" >> lk_ident
+  end
 
 (* Tactics grammar rules *)
 
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index f0d6258cd1..3e4c7ba782 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -38,45 +38,24 @@ let err () = raise Stream.Failure
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
 let test_lpar_id_coloneq =
-  Pcoq.Entry.of_parser "lpar_id_coloneq"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":=" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "lpar_id_coloneq" begin
+    lk_kw "(" >> lk_ident >> lk_kw ":="
+  end
 
 (* Hack to recognize "(x)" *)
 let test_lpar_id_rpar =
-  Pcoq.Entry.of_parser "lpar_id_coloneq"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ")" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "lpar_id_coloneq" begin
+    lk_kw "(" >> lk_ident >> lk_kw ")"
+  end
 
 (* idem for (x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
-  Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ | NUMERAL _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":=" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "test_lpar_idnum_coloneq" begin
+    lk_kw "(" >> (lk_ident <+> lk_nat) >> lk_kw ":="
+  end
 
 (* idem for (x:t) *)
 open Extraargs
@@ -107,11 +86,10 @@ let check_for_coloneq =
       | _ -> err ())
 
 let lookup_at_as_comma =
-  Pcoq.Entry.of_parser "lookup_at_as_comma"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD (","|"at"|"as") -> ()
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "lookup_at_as_comma" begin
+    lk_kws [",";"at";"as"]
+  end
 
 open Constr
 open Prim