diff options
| -rw-r--r-- | parsing/g_prim.mlg | 9 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 50 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 14 | ||||
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 47 |
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 |