Refactor lookaheads using DSL

4 files changed, 52 insertions, 84 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 bd3fc26e4e..5f61b9a047 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -31,28 +31,11 @@ let my_int_of_string loc s =
   with Failure _ ->
     CErrors.user_err ~loc (Pp.str "This number is too large.")
 
-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 Pcoq.Lookahead.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
 
 }
 
@@ -148,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 ea1ed53a0b..4b42c59d54 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -123,7 +123,7 @@ struct
 
   let err () = raise Stream.Failure
 
-  type lookahead = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option
+  type t = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option
 
   let rec contiguous tok n m =
     n == m ||
@@ -135,15 +135,15 @@ struct
     let n = Stream.count strm in
     if contiguous tok n (n+m-1) then Some m else None
 
-  let entry_of_lookahead s (lk : lookahead) =
+  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 : lookahead) lk2 tok n strm = match lk1 tok n strm with
+  let (>>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with
   | None -> None
   | Some n -> lk2 tok n strm
 
-  let (<+>) (lk1 : lookahead) lk2 tok n strm = match lk1 tok n strm with
+  let (<+>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with
   | None -> lk2 tok n strm
   | Some n -> Some n
 
@@ -153,18 +153,26 @@ struct
   | 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_int tok n strm = match stream_nth n strm with
   | Tok.NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
   | _ -> None
 
-  let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident >> check_no_space)
+  let rec lk_list lk_elem n strm =
+    ((lk_elem >> lk_list lk_elem) <+> lk_empty) n strm
 
-  let rec lk_ident_list n strm =
-    ((lk_ident >> lk_ident_list) <+> lk_empty) n strm
+  let lk_ident_list = lk_list lk_ident
 
 end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 832cb8341d..746510b911 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -35,17 +35,18 @@ module Entry : sig
 end
 
 module Lookahead : sig
-  type lookahead
-  val entry_of_lookahead : string -> lookahead -> unit Entry.t
-  val contiguous : (int -> Loc.t) -> int -> int -> bool
-  val (>>) : lookahead -> lookahead -> lookahead
-  val (<+>) : lookahead -> lookahead -> lookahead
-  val check_no_space : lookahead
-  val lk_kw : string -> lookahead
-  val lk_ident_or_anti : lookahead
-  val lk_int : lookahead
-  val lk_ident : lookahead
-  val lk_ident_list : lookahead
+  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_int : 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: