diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_prim.mlg | 35 |
1 files changed, 30 insertions, 5 deletions
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index c1f52c5b39..020501aedf 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -31,10 +31,35 @@ let my_int_of_string loc s = with Failure _ -> CErrors.user_err ~loc (Pp.str "This number is too large.") -let check_nospace loc expected = - let (bp, ep) = Loc.unloc loc in - if ep = bp + String.length expected then () else - Gramlib.Ploc.raise loc (Stream.Error ("'" ^ expected ^ "' expected")) +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 -> + 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 contiguous tok n (n + List.length m - 1) then () + else raise Stream.Failure) + +let test_nospace_pipe_closedcurly = + test_nospace ["|"; "}"] + } @@ -130,6 +155,6 @@ GRAMMAR EXTEND Gram [ [ i = NUMERAL -> { check_int loc i } ] ] ; bar_cbrace: - [ [ "|"; "}" -> { check_nospace loc "|}" } ] ] + [ [ test_nospace_pipe_closedcurly; "|"; "}" -> { () } ] ] ; END |