From fd38386b2aa19edf2df05f7b935d2273d9de8b00 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 25 Feb 2020 18:30:57 +0100
Subject: Move lookahead combinators to Pcoq

They were in Ltac2, but they are of general interest
---
 parsing/g_prim.mlg |  9 +--------
 parsing/pcoq.ml    | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 parsing/pcoq.mli   | 14 ++++++++++++++
 3 files changed, 65 insertions(+), 8 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 020501aedf..bd3fc26e4e 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -31,13 +31,6 @@ 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 ->
@@ -54,7 +47,7 @@ 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 ()
+      if Pcoq.Lookahead.contiguous tok n (n + List.length m - 1) then ()
       else raise Stream.Failure)
 
 let test_nospace_pipe_closedcurly =
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 92c3b7c6e8..ea1ed53a0b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -118,6 +118,56 @@ struct
 
 end
 
+module Lookahead =
+struct
+
+  let err () = raise Stream.Failure
+
+  type lookahead = 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 entry_of_lookahead s (lk : lookahead) =
+    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
+  | None -> None
+  | Some n -> lk2 tok n strm
+
+  let (<+>) (lk1 : lookahead) 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_ident tok n strm = match stream_nth n strm with
+  | Tok.IDENT _ -> 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_ident_list n strm =
+    ((lk_ident >> lk_ident_list) <+> lk_empty) n strm
+
+end
+
 (** Grammar extensions *)
 
 (** NB: [extend_statement =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f2fc007a7b..832cb8341d 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -34,6 +34,20 @@ module Entry : sig
   val name : 'a t -> string
 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
+end
+
 (** The parser of Coq is built from three kinds of rule declarations:
 
    - dynamic rules declared at the evaluation of Coq files (using
-- 
cgit v1.2.3


From 38e57715c086183250dd6176f9eaad01bfcde4c5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 27 Feb 2020 11:15:02 +0100
Subject: Refactor lookaheads using DSL

---
 parsing/g_constr.mlg | 62 ++++++++++++++++------------------------------------
 parsing/g_prim.mlg   | 29 +++++-------------------
 parsing/pcoq.ml      | 22 +++++++++++++------
 parsing/pcoq.mli     | 23 +++++++++----------
 4 files changed, 52 insertions(+), 84 deletions(-)

(limited to 'parsing')

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:
-- 
cgit v1.2.3


From 7ebcbc1cecca87619aa4b01606021c29c5d1f0a2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Feb 2020 20:19:00 +0100
Subject: [parser] lk_int -> lk_nat

---
 parsing/pcoq.ml  | 2 +-
 parsing/pcoq.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 4b42c59d54..d1a6e0eda2 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -165,7 +165,7 @@ struct
   | 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
+  let lk_nat tok n strm = match stream_nth n strm with
   | Tok.NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
   | _ -> None
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 746510b911..6543a69b50 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -43,7 +43,7 @@ module Lookahead : sig
   val check_no_space : t
   val lk_kw : string -> t
   val lk_kws : string list -> t
-  val lk_int : t
+  val lk_nat : t
   val lk_ident : t
   val lk_ident_except : string list -> t
   val lk_ident_list : t
-- 
cgit v1.2.3