git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4036 from msmorgan/feature/lexer-lookahead
4251ad8Jan de Muijnck-Hughes
libs/contrib/Text/Lexer.idr+27−2
compare with master
unifiedsplit
@@ -3,12 +3,13 @@ module Text.Lexer
3%default total
3%default total
4
4
5||| A language of token recognisers.
5||| A language of token recognisers.
6−||| The `consumes` flag is True is the recogniser is guaranteed to consume
6+||| @ consumes If `True`, this recogniser is guaranteed to consume at
7−||| at least one character
7+||| least one character of input when it succeeds.
8export
8export
9data Recognise : (consumes : Bool) -> Type where
9data Recognise : (consumes : Bool) -> Type where
10 Empty : Recognise False
10 Empty : Recognise False
11 Fail : Recognise c
11 Fail : Recognise c
12+ Expect : Recognise c -> Recognise False
12 Pred : (Char -> Bool) -> Recognise True
13 Pred : (Char -> Bool) -> Recognise True
13 SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
14 SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
14 SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
15 SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
@@ -38,6 +39,22 @@ export
38(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
39(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
39(<|>) = Alt
40(<|>) = Alt
40
41
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+
41||| Recognise a specific character
58||| Recognise a specific character
42export
59export
43is : Char -> Lexer
60is : Char -> Lexer
@@ -84,6 +101,10 @@ export
84any : Lexer
101any : Lexer
85any = Pred (const True)
102any = Pred (const True)
86
103
104+||| Recognise any character if the sub-lexer `l` fails.
105+non : (l : Lexer) -> Lexer
106+non l = reject l <+> any
107+
87||| Recognise no input (doesn't consume any input)
108||| Recognise no input (doesn't consume any input)
88export
109export
89empty : Recognise False
110empty : Recognise False
@@ -122,6 +143,10 @@ strTail start (MkStrLen str len)
122scan : Recognise c -> Nat -> StrLen -> Maybe Nat
143scan : Recognise c -> Nat -> StrLen -> Maybe Nat
123scan Empty idx str = pure idx
144scan Empty idx str = pure idx
124scan Fail idx str = Nothing
145scan Fail idx str = Nothing
146+scan (Expect r) idx str
147+ = case scan r idx str of
148+ Just _ => pure idx
149+ Nothing => Nothing
125scan (Pred f) idx str
150scan (Pred f) idx str
126 = do c <- strIndex str idx
151 = do c <- strIndex str idx
127 if f c
152 if f c