@@ -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)
@@ -23,11 +24,11 @@ public export
2324inf : Bool -> Type -> Type
2425inf True t = Inf t
2526inf False t = t
26−
27+
2728||| Sequence two recognisers. If either consumes a character, the sequence
2829||| is guaranteed to consume a character.
2930export %inline
30−(<+>) : {c1 : Bool} ->
31+(<+>) : {c1 : Bool} ->
3132 Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
3233(<+>) {c1 = False} = SeqEmpty
3334(<+>) {c1 = True} = SeqEat
@@ -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
@@ -48,22 +65,46 @@ export
4865isNot : Char -> Lexer
4966isNot x = Pred (/=x)
5067
68+||| Recognise a lexer or recognise no input. This is not guaranteed
69+||| to consume input
70+export
71+opt : Lexer -> Recognise False
72+opt l = l <|> Empty
73+
5174||| Recognise a sequence of at least one sub-lexers
5275export
5376some : Lexer -> Lexer
54−some l = l <+> (some l <|> Empty)
77+some l = l <+> opt (some l)
5578
5679||| Recognise a sequence of at zero or more sub-lexers. This is not
5780||| guaranteed to consume input
5881export
5982many : Lexer -> Recognise False
60−many l = some l <|> Empty
83+many l = opt (some l)
84+
85+||| Recognise the first matching lexer from a non-empty list.
86+export
87+choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
88+choice (x :: []) = x
89+choice (x :: xs@(_ :: _)) = x <|> choice xs
90+
91+||| Recognise many instances of `l` until an instance of `end` is
92+||| encountered.
93+|||
94+||| Useful for defining comments.
95+export
96+manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
97+manyTill l end = end <|> opt (l <+> manyTill l end)
6198
6299||| Recognise any character
63100export
64101any : Lexer
65102any = Pred (const True)
66103
104+||| Recognise any character if the sub-lexer `l` fails.
105+non : (l : Lexer) -> Lexer
106+non l = reject l <+> any
107+
67108||| Recognise no input (doesn't consume any input)
68109export
69110empty : Recognise False
@@ -86,7 +127,7 @@ getString : StrLen -> String
86127getString (MkStrLen str n) = str
87128
88129strIndex : StrLen -> Nat -> Maybe Char
89−strIndex (MkStrLen str len) i
130+strIndex (MkStrLen str len) i
90131 = if i >= len then Nothing
91132 else Just (assert_total (prim__strIndex str (cast i)))
92133
@@ -102,70 +143,159 @@ strTail start (MkStrLen str len)
102143scan : Recognise c -> Nat -> StrLen -> Maybe Nat
103144scan Empty idx str = pure idx
104145scan Fail idx str = Nothing
105−scan (Pred f) idx str
146+scan (Expect r) idx str
147+ = case scan r idx str of
148+ Just _ => pure idx
149+ Nothing => Nothing
150+scan (Pred f) idx str
106151 = do c <- strIndex str idx
107152 if f c
108153 then Just (idx + 1)
109154 else Nothing
110−scan (SeqEat r1 r2) idx str
155+scan (SeqEat r1 r2) idx str
111156 = do idx' <- scan r1 idx str
112157 -- TODO: Can we prove totality instead by showing idx has increased?
113158 assert_total (scan r2 idx' str)
114−scan (SeqEmpty r1 r2) idx str
159+scan (SeqEmpty r1 r2) idx str
115160 = do idx' <- scan r1 idx str
116161 scan r2 idx' str
117−scan (Alt r1 r2) idx str
162+scan (Alt r1 r2) idx str
118163 = case scan r1 idx str of
119164 Nothing => scan r2 idx str
120165 Just idx => Just idx
121166
122167takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
123−takeToken lex str
168+takeToken lex str
124169 = do i <- scan lex 0 str -- i must be > 0 if successful
125170 pure (substr 0 i (getString str), strTail i str)
126171
127−||| Recognise a digit 0-9
172+||| Recognise a single digit 0-9
173+export
174+digit : Lexer
175+digit = pred isDigit
176+
177+||| Recognise one or more digits
128178export
129179digits : Lexer
130−digits = some (Pred isDigit)
180+digits = some digit
131181
132182||| Recognise a specific string
133183export
134184exact : String -> Lexer
135185exact str with (unpack str)
136186 exact str | [] = Fail -- Not allowed, Lexer has to consume
137− exact str | (x :: xs)
187+ exact str | (x :: xs)
138188 = foldl SeqEmpty (is x) (map is xs)
139189
140−||| Recognise a whitespace character
190+||| Recognise a single hexidecimal digit
191+export
192+hexDigit : Lexer
193+hexDigit = digit <|> oneOf "abcdefABCDEF"
194+
195+||| Recognise one or more hexidecimal digits
196+export
197+hexDigits : Lexer
198+hexDigits = some hexDigit
199+
200+||| Recognise a single alpha character
201+export
202+alpha : Lexer
203+alpha = pred isAlpha
204+
205+||| Recognise one or more alpha characters
206+export
207+alphas : Lexer
208+alphas = some alpha
209+
210+||| Recognise a lowercase alpha character
211+export
212+lower : Lexer
213+lower = pred isLower
214+
215+||| Recognise one or more lowercase alpha characters
216+export
217+lowers : Lexer
218+lowers = some lower
219+
220+||| Recognise an uppercase alpha character
221+export
222+upper : Lexer
223+upper = pred isUpper
224+
225+||| Recognise one or more uppercase alpha characters
226+export
227+uppers : Lexer
228+uppers = some upper
229+
230+||| Recognise an alphanumeric character
231+export
232+alphaNum : Lexer
233+alphaNum = pred isAlphaNum
234+
235+||| Recognise one or more alphanumeric characters
236+export
237+alphaNums : Lexer
238+alphaNums = some alphaNum
239+
240+||| Recognise a single whitespace character
141241export
142242space : Lexer
143−space = some (pred isSpace)
243+space = pred isSpace
244+
245+||| Recognise one or more whitespace characters
246+export
247+spaces : Lexer
248+spaces = some space
144249
145−||| Recognise a non-alphanumeric, non-whitespace character
250+||| Recognise a single non-whitespace, non-alphanumeric character
146251export
147252symbol : Lexer
148−symbol = some (pred (\x => not (isAlphaNum x) && not (isSpace x)))
253+symbol = pred (\x => not (isSpace x || isAlphaNum x))
254+
255+||| Recognise one or more non-whitespace, non-alphanumeric characters
256+export
257+symbols : Lexer
258+symbols = some symbol
149259
150−strChar : Lexer
151−strChar = (is '\\' <+> any) <|> isNot '"'
260+||| Recognise zero or more occurrences of a sub-lexer between
261+||| delimiting lexers
262+export
263+surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
264+surround start end l = start <+> manyTill l end
265+
266+||| Recognise zero or more occurrences of a sub-lexer surrounded
267+||| by the same quote lexer on both sides (useful for strings)
268+export
269+quote : (q : Lexer) -> (l : Lexer) -> Lexer
270+quote q l = surround q q l
271+
272+||| Recognise an escape character (often '\\') followed by a sub-lexer
273+export
274+escape : (esc : Char) -> Lexer -> Lexer
275+escape esc l = is esc <+> l
152276
153277||| Recognise a string literal, including escaped characters.
154278||| (Note: doesn't yet handle escape sequences such as \123)
155279export
156280stringLit : Lexer
157−stringLit = is '"' <+> many strChar <+> is '"'
281+stringLit = quote (is '"') (escape '\\' any <|> any)
158282
159283||| Recognise a character literal, including escaped characters.
160284||| (Note: doesn't yet handle escape sequences such as \123)
161285export
162286charLit : Lexer
163−charLit = is '\'' <+> strChar <+> is '\''
287+charLit = let q = '\'' in
288+ is q <+> (escape '\\' any <|> isNot q) <+> is q
164289
165290||| Recognise an integer literal (possibly with a '-' prefix)
166291export
167292intLit : Lexer
168−intLit = (is '-' <|> Empty) <+> digits
293+intLit = opt (is '-') <+> digits
294+
295+||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
296+export
297+hexLit : Lexer
298+hexLit = is '0' <+> oneOf "xX" <+> hexDigits
169299
170300||| A mapping from lexers to the tokens they produce.
171301||| This is a list of pairs `(Lexer, String -> tokenType)`
@@ -185,8 +315,8 @@ record TokenData a where
185315
186316fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
187317fspanEnd k p "" = (k, "")
188−fspanEnd k p xxs
189− = assert_total $
318+fspanEnd k p xxs
319+ = assert_total $
190320 let x = prim__strHead xxs
191321 xs = prim__strTail xxs in
192322 if p x then fspanEnd (S k) p xs
@@ -195,14 +325,14 @@ fspanEnd k p xxs
195325-- Faster version of 'span' from the prelude (avoids unpacking)
196326export
197327fspan : (Char -> Bool) -> String -> (String, String)
198−fspan p xs
328+fspan p xs
199329 = let (end, rest) = fspanEnd 0 p xs in
200330 (substr 0 end xs, rest)
201331
202332tokenise : (line : Int) -> (col : Int) ->
203− List (TokenData a) -> TokenMap a ->
333+ List (TokenData a) -> TokenMap a ->
204334 StrLen -> (List (TokenData a), (Int, Int, StrLen))
205−tokenise line col acc tmap str
335+tokenise line col acc tmap str
206336 = case getFirstToken tmap str of
207337 Just (tok, line', col', rest) =>
208338 -- assert total because getFirstToken must consume something
@@ -213,7 +343,7 @@ tokenise line col acc tmap str
213343 countNLs str = List.length (filter (== '\n') str)
214344
215345 getCols : String -> Int -> Int
216− getCols x c
346+ getCols x c
217347 = case fspan (/= '\n') (reverse x) of
218348 (incol, "") => c + cast (length incol)
219349 (incol, _) => cast (length incol)
@@ -223,7 +353,7 @@ tokenise line col acc tmap str
223353 getFirstToken ((lex, fn) :: ts) str
224354 = case takeToken lex str of
225355 Just (tok, rest) => Just (MkToken line col (fn tok),
226− line + cast (countNLs (unpack tok)),
356+ line + cast (countNLs (unpack tok)),
227357 getCols tok col, rest)
228358 Nothing => getFirstToken ts str
229359
@@ -235,4 +365,3 @@ export
235365lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
236366lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
237367 (ts, (l, c, getString str'))
238−