Move lookahead combinators to Pcoq

They were in Ltac2, but they are of general interest

1 files changed, 7 insertions, 40 deletions

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