Merge PR #11695: Refactor lookaheads

Reviewed-by: herbelin
Reviewed-by: ppedrot

4 files changed, 98 insertions, 73 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index d6c6c365cb..48e6f1f213 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -17,7 +17,6 @@ open Glob_term
 open Constrexpr
 open Constrexpr_ops
 open Util
-open Tok
 open Namegen
 
 open Pcoq
@@ -54,48 +53,25 @@ let err () = raise Stream.Failure
 
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
-let lpar_id_coloneq =
-  Pcoq.Entry.of_parser "test_lpar_id_coloneq"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT s ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":=" ->
-                        stream_njunk 3 strm;
-                        Names.Id.of_string s
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+let test_lpar_id_coloneq =
+  let open Pcoq.Lookahead in
+  to_entry "test_lpar_id_coloneq" begin
+    lk_kw "(" >> lk_ident >> lk_kw ":="
+  end
 
 let ensure_fixannot =
-  Pcoq.Entry.of_parser "check_fixannot"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "{" ->
-            (match stream_nth 1 strm with
-              | IDENT ("wf"|"struct"|"measure") -> ()
-              | _ -> err ())
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "check_fixannot" begin
+    lk_kw "{" >> lk_kws ["wf"; "struct"; "measure"]
+  end
 
-let name_colon =
-  Pcoq.Entry.of_parser "name_colon"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | IDENT s ->
-            (match stream_nth 1 strm with
-              | KEYWORD ":" ->
-                  stream_njunk 2 strm;
-                  Name (Names.Id.of_string s)
-              | _ -> err ())
-        | KEYWORD "_" ->
-          (match stream_nth 1 strm with
-              | KEYWORD ":" ->
-                  stream_njunk 2 strm;
-                  Anonymous
-              | _ -> err ())
-        | _ -> err ())
+let lk_name = Pcoq.Lookahead.(lk_ident <+> lk_kw "_")
+
+let test_name_colon =
+  let open Pcoq.Lookahead in
+  to_entry "test_name_colon" begin
+    lk_name >> lk_kw ":"
+  end
 
 let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None
 
@@ -266,7 +242,7 @@ GRAMMAR EXTEND Gram
       | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ]
   ;
   appl_arg:
-    [ [ id = lpar_id_coloneq; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) }
+    [ [ test_lpar_id_coloneq; "("; id = ident; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) }
       | c=operconstr LEVEL "9" -> { (c,None) } ] ]
   ;
   atomic_constr:
@@ -464,8 +440,8 @@ GRAMMAR EXTEND Gram
     [ [ "!" ; c = operconstr LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c }
       | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
           { id, expl, c }
-      | iid = name_colon ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
-          { (CAst.make ~loc iid), expl, c }
+      | test_name_colon; iid = name; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
+          { iid, expl, c }
       | c = operconstr LEVEL "200" ->
           { (CAst.make ~loc Anonymous), false, c } ] ]
   ;
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 020501aedf..5f61b9a047 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -31,35 +31,11 @@ let my_int_of_string loc s =
   with Failure _ ->
     CErrors.user_err ~loc (Pp.str "This number is too large.")
 
-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 ["|"; "}"]
-
+let test_pipe_closedcurly =
+  let open Pcoq.Lookahead in
+  to_entry "test_pipe_closedcurly" begin
+    lk_kw "|" >> lk_kw "}" >> check_no_space
+  end
 
 }
 
@@ -155,6 +131,6 @@ GRAMMAR EXTEND Gram
     [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
   bar_cbrace:
-    [ [ test_nospace_pipe_closedcurly; "|"; "}" -> { () } ] ]
+    [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ]
   ;
 END
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 92c3b7c6e8..d1a6e0eda2 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -118,6 +118,64 @@ struct
 
 end
 
+module Lookahead =
+struct
+
+  let err () = raise Stream.Failure
+
+  type t = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option
+
+  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 check_no_space tok m strm =
+    let n = Stream.count strm in
+    if contiguous tok n (n+m-1) then Some m else None
+
+  let to_entry s (lk : t) =
+    let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in
+    Entry.of_parser s run
+
+  let (>>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with
+  | None -> None
+  | Some n -> lk2 tok n strm
+
+  let (<+>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with
+  | None -> lk2 tok n strm
+  | Some n -> Some n
+
+  let lk_empty tok n strm = Some n
+
+  let lk_kw kw tok n strm = match stream_nth n strm with
+  | Tok.KEYWORD kw' | Tok.IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None
+  | _ -> None
+
+  let lk_kws kws tok n strm = match stream_nth n strm with
+  | Tok.KEYWORD kw | Tok.IDENT kw -> if List.mem_f String.equal kw kws then Some (n + 1) else None
+  | _ -> None
+
+  let lk_ident tok n strm = match stream_nth n strm with
+  | Tok.IDENT _ -> Some (n + 1)
+  | _ -> None
+
+  let lk_ident_except idents tok n strm = match stream_nth n strm with
+  | Tok.IDENT ident when not (List.mem_f String.equal ident idents) -> Some (n + 1)
+  | _ -> None
+
+  let lk_nat tok n strm = match stream_nth n strm with
+  | Tok.NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
+  | _ -> None
+
+  let rec lk_list lk_elem n strm =
+    ((lk_elem >> lk_list lk_elem) <+> lk_empty) n strm
+
+  let lk_ident_list = lk_list lk_ident
+
+end
+
 (** Grammar extensions *)
 
 (** NB: [extend_statement =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f2fc007a7b..6543a69b50 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -34,6 +34,21 @@ module Entry : sig
   val name : 'a t -> string
 end
 
+module Lookahead : sig
+  type t
+  val to_entry : string -> t -> unit Entry.t
+  val (>>) : t -> t -> t
+  val (<+>) : t -> t -> t
+  val lk_list : t -> t
+  val check_no_space : t
+  val lk_kw : string -> t
+  val lk_kws : string list -> t
+  val lk_nat : t
+  val lk_ident : t
+  val lk_ident_except : string list -> t
+  val lk_ident_list : t
+end
+
 (** The parser of Coq is built from three kinds of rule declarations:
 
    - dynamic rules declared at the evaluation of Coq files (using