@@ -3,12 +3,13 @@ module Text.Lexer
33%default total
44
55||| A language of token recognisers.
6−||| The `consumes` flag is True is the recogniser is guaranteed to consume
7−||| at least one character
6+||| @ consumes If `True`, this recogniser is guaranteed to consume at
7+||| least one character of input when it succeeds.
88export
99data Recognise : (consumes : Bool) -> Type where
1010 Empty : Recognise False
1111 Fail : Recognise c
12+ Expect : Recognise c -> Recognise False
1213 Pred : (Char -> Bool) -> Recognise True
1314 SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
1415 SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
@@ -38,6 +39,22 @@ export
3839(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
3940(<|>) = Alt
4041
42+||| Positive lookahead. Never consumes input.
43+export
44+expect : Recognise c -> Recognise False
45+expect = Expect
46+
47+||| Negative lookahead. Never consumes input.
48+export
49+reject : Recognise c -> Recognise False
50+reject Empty = Fail
51+reject Fail = Empty
52+reject (Expect x) = reject x
53+reject (Pred f) = Expect (Pred (not . f))
54+reject (SeqEat r1 r2) = reject r1 <|> Expect (SeqEat r1 (reject r2))
55+reject (SeqEmpty r1 r2) = reject r1 <|> Expect (SeqEmpty r1 (reject r2))
56+reject (Alt r1 r2) = reject r1 <+> reject r2
57+
4158||| Recognise a specific character
4259export
4360is : Char -> Lexer
@@ -122,6 +139,10 @@ strTail start (MkStrLen str len)
122139scan : Recognise c -> Nat -> StrLen -> Maybe Nat
123140scan Empty idx str = pure idx
124141scan Fail idx str = Nothing
142+scan (Expect r) idx str
143+ = case scan r idx str of
144+ Just _ => pure idx
145+ Nothing => Nothing
125146scan (Pred f) idx str
126147 = do c <- strIndex str idx
127148 if f c