@@ -3,12 +3,13 @@ module Text.Lexer
3%default total
3%default total
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.
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)
@@ -23,11 +24,11 @@ public export
23inf : Bool -> Type -> Type
24inf : Bool -> Type -> Type
24inf True t = Inf t
25inf True t = Inf t
25inf False t = t
26inf False t = t
27||| Sequence two recognisers. If either consumes a character, the sequence
28||| Sequence two recognisers. If either consumes a character, the sequence
28||| is guaranteed to consume a character.
29||| is guaranteed to consume a character.
29export %inline
30export %inline
30−(<+>) : {c1 : Bool} ->
31+(<+>) : {c1 : Bool} ->
31 Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
32 Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
32(<+>) {c1 = False} = SeqEmpty
33(<+>) {c1 = False} = SeqEmpty
33(<+>) {c1 = True} = SeqEat
34(<+>) {c1 = True} = SeqEat
@@ -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
42+||| Positive lookahead. Never consumes input.
44+expect : Recognise c -> Recognise False
47+||| Negative lookahead. Never consumes input.
49+reject : Recognise c -> Recognise False
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
41||| Recognise a specific character
58||| Recognise a specific character
43is : Char -> Lexer
60is : Char -> Lexer
@@ -48,22 +65,46 @@ export
48isNot : Char -> Lexer
65isNot : Char -> Lexer
49isNot x = Pred (/=x)
66isNot x = Pred (/=x)
68+||| Recognise a lexer or recognise no input. This is not guaranteed
71+opt : Lexer -> Recognise False
51||| Recognise a sequence of at least one sub-lexers
74||| Recognise a sequence of at least one sub-lexers
53some : Lexer -> Lexer
76some : Lexer -> Lexer
54−some l = l <+> (some l <|> Empty)
77+some l = l <+> opt (some l)
56||| Recognise a sequence of at zero or more sub-lexers. This is not
79||| Recognise a sequence of at zero or more sub-lexers. This is not
57||| guaranteed to consume input
80||| guaranteed to consume input
59many : Lexer -> Recognise False
82many : Lexer -> Recognise False
60−many l = some l <|> Empty
83+many l = opt (some l)
85+||| Recognise the first matching lexer from a non-empty list.
87+choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
89+choice (x :: xs@(_ :: _)) = x <|> choice xs
91+||| Recognise many instances of `l` until an instance of `end` is
94+||| Useful for defining comments.
96+manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
97+manyTill l end = end <|> opt (l <+> manyTill l end)
62||| Recognise any character
99||| Recognise any character
64any : Lexer
101any : Lexer
65any = Pred (const True)
102any = Pred (const True)
104+||| Recognise any character if the sub-lexer `l` fails.
105+non : (l : Lexer) -> Lexer
106+non l = reject l <+> any
67||| Recognise no input (doesn't consume any input)
108||| Recognise no input (doesn't consume any input)
69empty : Recognise False
110empty : Recognise False
@@ -86,7 +127,7 @@ getString : StrLen -> String
86getString (MkStrLen str n) = str
127getString (MkStrLen str n) = str
88strIndex : StrLen -> Nat -> Maybe Char
129strIndex : StrLen -> Nat -> Maybe Char
89−strIndex (MkStrLen str len) i
130+strIndex (MkStrLen str len) i
90 = if i >= len then Nothing
131 = if i >= len then Nothing
91 else Just (assert_total (prim__strIndex str (cast i)))
132 else Just (assert_total (prim__strIndex str (cast i)))
@@ -102,70 +143,159 @@ strTail start (MkStrLen str len)
102scan : Recognise c -> Nat -> StrLen -> Maybe Nat
143scan : Recognise c -> Nat -> StrLen -> Maybe Nat
103scan Empty idx str = pure idx
144scan Empty idx str = pure idx
104scan Fail idx str = Nothing
145scan Fail idx str = Nothing
146+scan (Expect r) idx str
147+ = case scan r idx str of
105−scan (Pred f) idx str
150+scan (Pred f) idx str
106 = do c <- strIndex str idx
151 = do c <- strIndex str idx
108 then Just (idx + 1)
153 then Just (idx + 1)
109 else Nothing
154 else Nothing
110−scan (SeqEat r1 r2) idx str
155+scan (SeqEat r1 r2) idx str
111 = do idx' <- scan r1 idx str
156 = do idx' <- scan r1 idx str
112 -- TODO: Can we prove totality instead by showing idx has increased?
157 -- TODO: Can we prove totality instead by showing idx has increased?
113 assert_total (scan r2 idx' str)
158 assert_total (scan r2 idx' str)
114−scan (SeqEmpty r1 r2) idx str
159+scan (SeqEmpty r1 r2) idx str
115 = do idx' <- scan r1 idx str
160 = do idx' <- scan r1 idx str
116 scan r2 idx' str
161 scan r2 idx' str
117−scan (Alt r1 r2) idx str
162+scan (Alt r1 r2) idx str
118 = case scan r1 idx str of
163 = case scan r1 idx str of
119 Nothing => scan r2 idx str
164 Nothing => scan r2 idx str
120 Just idx => Just idx
165 Just idx => Just idx
122takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
167takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
123−takeToken lex str
168+takeToken lex str
124 = do i <- scan lex 0 str -- i must be > 0 if successful
169 = do i <- scan lex 0 str -- i must be > 0 if successful
125 pure (substr 0 i (getString str), strTail i str)
170 pure (substr 0 i (getString str), strTail i str)
127−||| Recognise a digit 0-9
172+||| Recognise a single digit 0-9
177+||| Recognise one or more digits
129digits : Lexer
179digits : Lexer
130−digits = some (Pred isDigit)
180+digits = some digit
132||| Recognise a specific string
182||| Recognise a specific string
134exact : String -> Lexer
184exact : String -> Lexer
135exact str with (unpack str)
185exact str with (unpack str)
136 exact str | [] = Fail -- Not allowed, Lexer has to consume
186 exact str | [] = Fail -- Not allowed, Lexer has to consume
137− exact str | (x :: xs)
187+ exact str | (x :: xs)
138 = foldl SeqEmpty (is x) (map is xs)
188 = foldl SeqEmpty (is x) (map is xs)
190+||| Recognise a single hexidecimal digit
193+hexDigit = digit <|> oneOf "abcdefABCDEF"
195+||| Recognise one or more hexidecimal digits
198+hexDigits = some hexDigit
200+||| Recognise a single alpha character
205+||| Recognise one or more alpha characters
210+||| Recognise a lowercase alpha character
215+||| Recognise one or more lowercase alpha characters
220+||| Recognise an uppercase alpha character
225+||| Recognise one or more uppercase alpha characters
230+||| Recognise an alphanumeric character
233+alphaNum = pred isAlphaNum
235+||| Recognise one or more alphanumeric characters
238+alphaNums = some alphaNum
140−||| Recognise a whitespace character
240+||| Recognise a single whitespace character
142space : Lexer
242space : Lexer
143−space = some (pred isSpace)
243+space = pred isSpace
245+||| Recognise one or more whitespace characters
145−||| Recognise a non-alphanumeric, non-whitespace character
250+||| Recognise a single non-whitespace, non-alphanumeric character
147symbol : Lexer
252symbol : Lexer
148−symbol = some (pred (\x => not (isAlphaNum x) && not (isSpace x)))
253+symbol = pred (\x => not (isSpace x || isAlphaNum x))
255+||| Recognise one or more non-whitespace, non-alphanumeric characters
258+symbols = some symbol
150−strChar : Lexer
260+||| Recognise zero or more occurrences of a sub-lexer between
151−strChar = (is '\\' <+> any) <|> isNot '"'
261+||| delimiting lexers
263+surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
264+surround start end l = start <+> manyTill l end
266+||| Recognise zero or more occurrences of a sub-lexer surrounded
267+||| by the same quote lexer on both sides (useful for strings)
269+quote : (q : Lexer) -> (l : Lexer) -> Lexer
270+quote q l = surround q q l
272+||| Recognise an escape character (often '\\') followed by a sub-lexer
274+escape : (esc : Char) -> Lexer -> Lexer
275+escape esc l = is esc <+> l
153||| Recognise a string literal, including escaped characters.
277||| Recognise a string literal, including escaped characters.
154||| (Note: doesn't yet handle escape sequences such as \123)
278||| (Note: doesn't yet handle escape sequences such as \123)
156stringLit : Lexer
280stringLit : Lexer
157−stringLit = is '"' <+> many strChar <+> is '"'
281+stringLit = quote (is '"') (escape '\\' any <|> any)
159||| Recognise a character literal, including escaped characters.
283||| Recognise a character literal, including escaped characters.
160||| (Note: doesn't yet handle escape sequences such as \123)
284||| (Note: doesn't yet handle escape sequences such as \123)
162charLit : Lexer
286charLit : Lexer
163−charLit = is '\'' <+> strChar <+> is '\''
287+charLit = let q = '\'' in
288+ is q <+> (escape '\\' any <|> isNot q) <+> is q
165||| Recognise an integer literal (possibly with a '-' prefix)
290||| Recognise an integer literal (possibly with a '-' prefix)
167intLit : Lexer
292intLit : Lexer
168−intLit = (is '-' <|> Empty) <+> digits
293+intLit = opt (is '-') <+> digits
295+||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
298+hexLit = is '0' <+> oneOf "xX" <+> hexDigits
170||| A mapping from lexers to the tokens they produce.
300||| A mapping from lexers to the tokens they produce.
171||| This is a list of pairs `(Lexer, String -> tokenType)`
301||| This is a list of pairs `(Lexer, String -> tokenType)`
@@ -185,8 +315,8 @@ record TokenData a where
186fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
316fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
187fspanEnd k p "" = (k, "")
317fspanEnd k p "" = (k, "")
188−fspanEnd k p xxs
318+fspanEnd k p xxs
189− = assert_total $
319+ = assert_total $
190 let x = prim__strHead xxs
320 let x = prim__strHead xxs
191 xs = prim__strTail xxs in
321 xs = prim__strTail xxs in
192 if p x then fspanEnd (S k) p xs
322 if p x then fspanEnd (S k) p xs
@@ -195,14 +325,14 @@ fspanEnd k p xxs
195-- Faster version of 'span' from the prelude (avoids unpacking)
325-- Faster version of 'span' from the prelude (avoids unpacking)
197fspan : (Char -> Bool) -> String -> (String, String)
327fspan : (Char -> Bool) -> String -> (String, String)
198−fspan p xs
328+fspan p xs
199 = let (end, rest) = fspanEnd 0 p xs in
329 = let (end, rest) = fspanEnd 0 p xs in
200 (substr 0 end xs, rest)
330 (substr 0 end xs, rest)
202tokenise : (line : Int) -> (col : Int) ->
332tokenise : (line : Int) -> (col : Int) ->
203− List (TokenData a) -> TokenMap a ->
333+ List (TokenData a) -> TokenMap a ->
204 StrLen -> (List (TokenData a), (Int, Int, StrLen))
334 StrLen -> (List (TokenData a), (Int, Int, StrLen))
205−tokenise line col acc tmap str
335+tokenise line col acc tmap str
206 = case getFirstToken tmap str of
336 = case getFirstToken tmap str of
207 Just (tok, line', col', rest) =>
337 Just (tok, line', col', rest) =>
208 -- assert total because getFirstToken must consume something
338 -- assert total because getFirstToken must consume something
@@ -213,7 +343,7 @@ tokenise line col acc tmap str
213 countNLs str = List.length (filter (== '\n') str)
343 countNLs str = List.length (filter (== '\n') str)
215 getCols : String -> Int -> Int
345 getCols : String -> Int -> Int
216− getCols x c
346+ getCols x c
217 = case fspan (/= '\n') (reverse x) of
347 = case fspan (/= '\n') (reverse x) of
218 (incol, "") => c + cast (length incol)
348 (incol, "") => c + cast (length incol)
219 (incol, _) => cast (length incol)
349 (incol, _) => cast (length incol)
@@ -223,7 +353,7 @@ tokenise line col acc tmap str
223 getFirstToken ((lex, fn) :: ts) str
353 getFirstToken ((lex, fn) :: ts) str
224 = case takeToken lex str of
354 = case takeToken lex str of
225 Just (tok, rest) => Just (MkToken line col (fn tok),
355 Just (tok, rest) => Just (MkToken line col (fn tok),
226− line + cast (countNLs (unpack tok)),
356+ line + cast (countNLs (unpack tok)),
227 getCols tok col, rest)
357 getCols tok col, rest)
228 Nothing => getFirstToken ts str
358 Nothing => getFirstToken ts str
@@ -235,4 +365,3 @@ export
235lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
365lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
236lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
366lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
237 (ts, (l, c, getString str'))
367 (ts, (l, c, getString str'))