aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/extraargs.mlg16
-rw-r--r--plugins/ltac/g_ltac.mlg13
-rw-r--r--plugins/ltac/g_tactic.mlg54
-rw-r--r--plugins/ssr/ssrparser.mlg76
4 files changed, 48 insertions, 111 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 5835d75c79..f97c291c79 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -330,18 +330,10 @@ END
{
let local_test_lpar_id_colon =
- let err () = raise Stream.Failure in
- Pcoq.Entry.of_parser "lpar_id_colon"
- (fun _ strm ->
- match Util.stream_nth 0 strm with
- | Tok.KEYWORD "(" ->
- (match Util.stream_nth 1 strm with
- | Tok.IDENT _ ->
- (match Util.stream_nth 2 strm with
- | Tok.KEYWORD ":" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+ let open Pcoq.Lookahead in
+ to_entry "lpar_id_colon" begin
+ lk_kw "(" >> lk_ident >> lk_kw ":"
+ end
let pr_lpar_id_colon _ _ _ _ = mt ()
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 7ea843ca69..c163438718 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -20,7 +20,6 @@ open Tacexpr
open Namegen
open Genarg
open Genredexpr
-open Tok (* necessary for camlp5 *)
open Names
open Attributes
@@ -63,14 +62,10 @@ let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
(* Hack to parse "[ id" without dropping [ *)
let test_bracket_ident =
- Pcoq.Entry.of_parser "test_bracket_ident"
- (fun _ strm ->
- match stream_nth 0 strm with
- | KEYWORD "[" ->
- (match stream_nth 1 strm with
- | IDENT _ -> ()
- | _ -> raise Stream.Failure)
- | _ -> raise Stream.Failure)
+ let open Pcoq.Lookahead in
+ to_entry "test_bracket_ident" begin
+ lk_kw "[" >> lk_ident
+ end
(* Tactics grammar rules *)
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index f0d6258cd1..517c0d59e1 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -38,45 +38,24 @@ let err () = raise Stream.Failure
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
(* admissible notation "(x t)" *)
let test_lpar_id_coloneq =
- Pcoq.Entry.of_parser "lpar_id_coloneq"
- (fun _ strm ->
- match stream_nth 0 strm with
- | KEYWORD "(" ->
- (match stream_nth 1 strm with
- | IDENT _ ->
- (match stream_nth 2 strm with
- | KEYWORD ":=" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+ let open Pcoq.Lookahead in
+ to_entry "lpar_id_coloneq" begin
+ lk_kw "(" >> lk_ident >> lk_kw ":="
+ end
(* Hack to recognize "(x)" *)
let test_lpar_id_rpar =
- Pcoq.Entry.of_parser "lpar_id_coloneq"
- (fun _ strm ->
- match stream_nth 0 strm with
- | KEYWORD "(" ->
- (match stream_nth 1 strm with
- | IDENT _ ->
- (match stream_nth 2 strm with
- | KEYWORD ")" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+ let open Pcoq.Lookahead in
+ to_entry "lpar_id_coloneq" begin
+ lk_kw "(" >> lk_ident >> lk_kw ")"
+ end
(* idem for (x:=t) and (1:=t) *)
let test_lpar_idnum_coloneq =
- Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
- (fun _ strm ->
- match stream_nth 0 strm with
- | KEYWORD "(" ->
- (match stream_nth 1 strm with
- | IDENT _ | NUMERAL _ ->
- (match stream_nth 2 strm with
- | KEYWORD ":=" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+ let open Pcoq.Lookahead in
+ to_entry "test_lpar_idnum_coloneq" begin
+ lk_kw "(" >> (lk_ident <+> lk_int) >> lk_kw ":="
+ end
(* idem for (x:t) *)
open Extraargs
@@ -107,11 +86,10 @@ let check_for_coloneq =
| _ -> err ())
let lookup_at_as_comma =
- Pcoq.Entry.of_parser "lookup_at_as_comma"
- (fun _ strm ->
- match stream_nth 0 strm with
- | KEYWORD (","|"at"|"as") -> ()
- | _ -> err ())
+ let open Pcoq.Lookahead in
+ to_entry "lookup_at_as_comma" begin
+ lk_kws [",";"at";"as"]
+ end
open Constr
open Prim
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 3f67d55e73..cd7c7d660e 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -142,25 +142,6 @@ let add_genarg tag pr =
Pptactic.declare_extra_genarg_pprule wit gen_pr gen_pr gen_pr;
wit
-(** Primitive parsing to avoid syntax conflicts with basic tactics. *)
-
-let accept_before_syms syms strm =
- match Util.stream_nth 1 strm with
- | Tok.KEYWORD sym when List.mem sym syms -> ()
- | _ -> raise Stream.Failure
-
-let accept_before_syms_or_any_id syms strm =
- match Util.stream_nth 1 strm with
- | Tok.KEYWORD sym when List.mem sym syms -> ()
- | Tok.IDENT _ -> ()
- | _ -> raise Stream.Failure
-
-let accept_before_syms_or_ids syms ids strm =
- match Util.stream_nth 1 strm with
- | Tok.KEYWORD sym when List.mem sym syms -> ()
- | Tok.IDENT id when List.mem id ids -> ()
- | _ -> raise Stream.Failure
-
open Ssrast
let pr_id = Ppconstr.pr_id
let pr_name = function Name id -> pr_id id | Anonymous -> str "_"
@@ -746,13 +727,11 @@ let pushIPatNoop = function
| pats :: orpat -> (IPatNoop :: pats) :: orpat
| [] -> []
-let test_ident_no_do _ strm =
- match Util.stream_nth 0 strm with
- | Tok.IDENT s when s <> "do" -> ()
- | _ -> raise Stream.Failure
-
let test_ident_no_do =
- Pcoq.Entry.of_parser "test_ident_no_do" test_ident_no_do
+ let open Pcoq.Lookahead in
+ to_entry "test_ident_no_do" begin
+ lk_ident_except ["do"]
+ end
}
@@ -1005,12 +984,11 @@ END
{
-let accept_ssrfwdid _ strm =
- match stream_nth 0 strm with
- | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm
- | _ -> raise Stream.Failure
-
-let test_ssrfwdid = Pcoq.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid
+let test_ssrfwdid =
+ let open Pcoq.Lookahead in
+ to_entry "test_ssrfwdid" begin
+ lk_ident >> (lk_ident <+> lk_kws [":"; ":="; "("])
+ end
}
@@ -1589,13 +1567,12 @@ END
let sq_brace_tacnames =
["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"]
(* "by" is a keyword *)
-let accept_ssrseqvar _ strm =
- match stream_nth 0 strm with
- | Tok.IDENT id when not (List.mem id sq_brace_tacnames) ->
- accept_before_syms_or_ids ["["] ["first";"last"] strm
- | _ -> raise Stream.Failure
-let test_ssrseqvar = Pcoq.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
+let test_ssrseqvar =
+ let open Pcoq.Lookahead in
+ to_entry "test_ssrseqvar" begin
+ lk_ident_except sq_brace_tacnames >> (lk_kws ["[";"first";"last"])
+ end
let swaptacarg (loc, b) = (b, []), Some (TacId [])
@@ -1985,15 +1962,11 @@ END
{
-let accept_ssreqid _ strm =
- match Util.stream_nth 0 strm with
- | Tok.IDENT _ -> accept_before_syms [":"] strm
- | Tok.KEYWORD ":" -> ()
- | Tok.KEYWORD pat when List.mem pat ["_"; "?"; "->"; "<-"] ->
- accept_before_syms [":"] strm
- | _ -> raise Stream.Failure
-
-let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid
+let test_ssreqid =
+ let open Pcoq.Lookahead in
+ to_entry "test_ssreqid" begin
+ ((lk_ident <+> lk_kws ["_"; "?"; "->"; "<-"]) >> lk_kw ":") <+> lk_kw ":"
+ end
}
@@ -2614,12 +2587,11 @@ END
{
-let accept_idcomma _ strm =
- match stream_nth 0 strm with
- | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm
- | _ -> raise Stream.Failure
-
-let test_idcomma = Pcoq.Entry.of_parser "test_idcomma" accept_idcomma
+let test_idcomma =
+ let open Pcoq.Lookahead in
+ to_entry "test_idcomma" begin
+ (lk_ident <+> lk_kw "_") >> lk_kw ","
+ end
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:13:20 +0000