on master help sign in
Merge pull request #4036 from msmorgan/feature/lexer-lookahead

Text.Lexer: positive and negative lookahead

commit4251ad87a3e48811324741701e61a4a20b85a989 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateSat 2 Sep 2017, 08:53 (9 years ago) parente69ce018c6a569
1 file changed+27−2
libs/contrib/Text/Lexer.idr+27−2
libs/contrib/Text/Lexer.idr+27−2
@@ -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
@@ -84,6 +101,10 @@ export
84101any : Lexer
85102any = Pred (const True)
86103
104+||| Recognise any character if the sub-lexer `l` fails.
105+non : (l : Lexer) -> Lexer
106+non l = reject l <+> any
107+
87108||| Recognise no input (doesn't consume any input)
88109export
89110empty : Recognise False
@@ -122,6 +143,10 @@ strTail start (MkStrLen str len)
122143scan : Recognise c -> Nat -> StrLen -> Maybe Nat
123144scan Empty idx str = pure idx
124145scan Fail idx str = Nothing
146+scan (Expect r) idx str
147+ = case scan r idx str of
148+ Just _ => pure idx
149+ Nothing => Nothing
125150scan (Pred f) idx str
126151 = do c <- strIndex str idx
127152 if f c