Move lookahead combinators to Pcoq

They were in Ltac2, but they are of general interest

4 files changed, 72 insertions, 48 deletions

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
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index e95ac3b02b..c32d95de7c 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -13,7 +13,6 @@
 open Pp
 open Util
 open Names
-open Tok
 open Pcoq
 open Attributes
 open Constrexpr
@@ -21,80 +20,48 @@ open Tac2expr
 open Tac2qexpr
 open Ltac_plugin
 
-let err () = raise Stream.Failure
-
-type lookahead = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option
-
-let check_no_space tok m strm =
-  let n = Stream.count strm in
-  if G_prim.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
-  Pcoq.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
-| KEYWORD kw' | 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
-| IDENT _ -> Some (n + 1)
-| _ -> None
-
-let lk_int tok n strm = match stream_nth n strm with
-| 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
-
 (* lookahead for (x:=t), (?x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
+  let open Pcoq.Lookahead in
   entry_of_lookahead "test_lpar_idnum_coloneq" begin
     lk_kw "(" >> (lk_ident_or_anti <+> lk_int) >> lk_kw ":="
   end
 
 (* lookahead for (x:t), (?x:t) *)
 let test_lpar_id_colon =
+  let open Pcoq.Lookahead in
   entry_of_lookahead "test_lpar_id_colon" begin
     lk_kw "(" >> lk_ident_or_anti >> lk_kw ":"
   end
 
 (* Hack to recognize "(x := t)" and "($x := t)" *)
 let test_lpar_id_coloneq =
+  let open Pcoq.Lookahead in
   entry_of_lookahead "test_lpar_id_coloneq" begin
     lk_kw "(" >> lk_ident_or_anti >> lk_kw ":="
   end
 
 (* Hack to recognize "(x)" *)
 let test_lpar_id_rpar =
+  let open Pcoq.Lookahead in
   entry_of_lookahead "test_lpar_id_rpar" begin
     lk_kw "(" >> lk_ident >> lk_kw ")"
   end
 
 let test_ampersand_ident =
+  let open Pcoq.Lookahead in
   entry_of_lookahead "test_ampersand_ident" begin
     lk_kw "&" >> lk_ident >> check_no_space
   end
 
 let test_dollar_ident =
+  let open Pcoq.Lookahead in
   entry_of_lookahead "test_dollar_ident" begin
     lk_kw "$" >> lk_ident >> check_no_space
   end
 
 let test_ltac1_env =
+  let open Pcoq.Lookahead in
   entry_of_lookahead "test_ltac1_env" begin
     lk_ident_list >> lk_kw "|-"
   end