@@ -3,24 +3,21 @@ module Text.Lexer
33import public Text.Lexer.Core
44
55%default total
6+%access export
67
78||| Recognise a specific character
8−export
99is : Char -> Lexer
1010is x = pred (==x)
1111
1212||| Recognise anything but the given character
13−export
1413isNot : Char -> Lexer
1514isNot x = pred (/=x)
1615
1716||| Recognise a character case-insensitively
18−export
1917like : Char -> Lexer
2018like x = pred (\y => toUpper x == toUpper y)
2119
2220||| Recognise anything but the given character case-insensitively
23−export
2421notLike : Char -> Lexer
2522notLike x = pred (\y => toUpper x /= toUpper y)
2623
@@ -40,38 +37,32 @@ approx str = case map like (unpack str) of
4037
4138||| Recognise a lexer or recognise no input. This is not guaranteed
4239||| to consume input
43−export
4440opt : Lexer -> Recognise False
4541opt l = l <|> empty
4642
4743||| Recognise a sequence of at least one sub-lexers
48−export
4944some : Lexer -> Lexer
5045some l = l <+> opt (some l)
5146
5247||| Recognise a sequence of at zero or more sub-lexers. This is not
5348||| guaranteed to consume input
54−export
5549many : Lexer -> Recognise False
5650many l = opt (some l)
5751
5852||| Recognise the first matching lexer from a Foldable. Always consumes input
5953||| if one of the options succeeds. Fails if the foldable is empty.
60−export
6154choice : Foldable t => t Lexer -> Lexer
6255choice xs = foldr (<|>) fail xs
6356
6457||| Repeat the sub-lexer `l` zero or more times until the lexer
6558||| `stopBefore` is encountered. `stopBefore` will not be consumed.
6659||| Not guaranteed to consume input.
67−export
6860manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
6961manyUntil stopBefore l = many (reject stopBefore <+> l)
7062
7163||| Repeat the sub-lexer `l` zero or more times until the lexer
7264||| `stopAfter` is encountered, and consume it. Guaranteed to
7365||| consume if `stopAfter` consumes.
74−export
7566manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
7667manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
7768
@@ -79,7 +70,6 @@ manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
7970||| encountered.
8071|||
8172||| Useful for defining comments.
82−export
8373manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
8474manyTill l end = end <|> opt (l <+> manyTill l end)
8575%deprecate manyTill
@@ -87,21 +77,18 @@ manyTill l end = end <|> opt (l <+> manyTill l end)
8777
8878||| Recognise a sub-lexer at least `min` times. Consumes input unless
8979||| min is zero.
90−export
9180atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)
9281atLeast Z l = many l
9382atLeast (S min) l = l <+> atLeast min l
9483
9584||| Recognise a sub-lexer at most `max` times. Not guaranteed to
9685||| consume input.
97−export
9886atMost : (max : Nat) -> (l : Lexer) -> Recognise False
9987atMost Z _ = empty
10088atMost (S k) l = atMost k l <+> opt l
10189
10290||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
10391||| if the inputs are out of order. Consumes input unless min is zero.
104−export
10592between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
10693between Z max l = atMost max l
10794between (S min) Z _ = fail
@@ -109,166 +96,135 @@ between (S min) (S max) l = l <+> between min max l
10996
11097||| Recognise exactly `count` repeated occurrences of a sub-lexer.
11198||| Consumes input unless count is zero.
112−export
11399exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
114100exactly n l = between n n l
115101
116102||| Recognise any character
117−export
118103any : Lexer
119104any = pred (const True)
120105
121106||| Recognise any character if the sub-lexer `l` fails.
122−export
123107non : (l : Lexer) -> Lexer
124108non l = reject l <+> any
125109
126110||| Recognise any of the characters in the given string
127−export
128111oneOf : String -> Lexer
129112oneOf cs = pred (\x => x `elem` unpack cs)
130113
131114||| Recognise a character range [`a`-`b`]. Also works in reverse!
132−export
133115range : (start : Char) -> (end : Char) -> Lexer
134116range start end = pred (\x => (x >= min start end)
135117 && (x <= max start end))
136118
137119||| Recognise a single digit 0-9
138−export
139120digit : Lexer
140121digit = pred isDigit
141122
142123||| Recognise one or more digits
143−export
144124digits : Lexer
145125digits = some digit
146126
147127||| Recognise a single hexidecimal digit
148−export
149128hexDigit : Lexer
150129hexDigit = pred isHexDigit
151130
152131||| Recognise one or more hexidecimal digits
153−export
154132hexDigits : Lexer
155133hexDigits = some hexDigit
156134
157135||| Recognise a single alpha character
158−export
159136alpha : Lexer
160137alpha = pred isAlpha
161138
162139||| Recognise one or more alpha characters
163−export
164140alphas : Lexer
165141alphas = some alpha
166142
167143||| Recognise a lowercase alpha character
168−export
169144lower : Lexer
170145lower = pred isLower
171146
172147||| Recognise one or more lowercase alpha characters
173−export
174148lowers : Lexer
175149lowers = some lower
176150
177151||| Recognise an uppercase alpha character
178−export
179152upper : Lexer
180153upper = pred isUpper
181154
182155||| Recognise one or more uppercase alpha characters
183−export
184156uppers : Lexer
185157uppers = some upper
186158
187159||| Recognise an alphanumeric character
188−export
189160alphaNum : Lexer
190161alphaNum = pred isAlphaNum
191162
192163||| Recognise one or more alphanumeric characters
193−export
194164alphaNums : Lexer
195165alphaNums = some alphaNum
196166
197167||| Recognise a single whitespace character
198−export
199168space : Lexer
200169space = pred isSpace
201170
202171||| Recognise one or more whitespace characters
203−export
204172spaces : Lexer
205173spaces = some space
206174
207175||| Recognise a single newline sequence. Understands CRLF, CR, and LF
208−export
209176newline : Lexer
210177newline = let crlf = "\r\n" in
211178 exact crlf <|> oneOf crlf
212179
213180||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
214−export
215181newlines : Lexer
216182newlines = some newline
217183
218184||| Recognise a single non-whitespace, non-alphanumeric character
219−export
220185symbol : Lexer
221186symbol = pred (\x => not (isSpace x || isAlphaNum x))
222187
223188||| Recognise one or more non-whitespace, non-alphanumeric characters
224−export
225189symbols : Lexer
226190symbols = some symbol
227191
228192||| Recognise zero or more occurrences of a sub-lexer between
229193||| delimiting lexers
230−export
231194surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
232195surround start end l = start <+> manyThen end l
233196
234197||| Recognise zero or more occurrences of a sub-lexer surrounded
235198||| by the same quote lexer on both sides (useful for strings)
236−export
237199quote : (q : Lexer) -> (l : Lexer) -> Lexer
238200quote q l = surround q q l
239201
240202||| Recognise an escape character (often '\\') followed by a sub-lexer
241−export
242203escape : (esc : Char) -> Lexer -> Lexer
243204escape esc l = is esc <+> l
244205
245206||| Recognise a string literal, including escaped characters.
246207||| (Note: doesn't yet handle escape sequences such as \123)
247−export
248208stringLit : Lexer
249209stringLit = quote (is '"') (escape '\\' any <|> any)
250210
251211||| Recognise a character literal, including escaped characters.
252212||| (Note: doesn't yet handle escape sequences such as \123)
253−export
254213charLit : Lexer
255214charLit = let q = '\'' in
256215 is q <+> (escape '\\' any <|> isNot q) <+> is q
257216
258217||| Recognise an integer literal (possibly with a '-' prefix)
259−export
260218intLit : Lexer
261219intLit = opt (is '-') <+> digits
262220
263221||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
264−export
265222hexLit : Lexer
266223hexLit = approx "0x" <+> hexDigits
267224
268225||| Recognise `start`, then recognise all input until a newline is encountered,
269226||| and consume the newline. Will succeed if end-of-input is encountered before
270227||| a newline.
271−export
272228lineComment : (start : Lexer) -> Lexer
273229lineComment start = start <+> manyUntil newline any <+> opt newline
274230
@@ -277,7 +233,6 @@ lineComment start = start <+> manyUntil newline any <+> opt newline
277233|||
278234||| For block comments that don't support nesting (such as C-style comments),
279235||| use `surround`.
280−export
281236blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
282237blockComment start end = start <+> middle <+> end
283238 where