@@ -41,6 +41,16 @@ export
41fail : Recognise c
41fail : Recognise c
42fail = Fail
42fail = Fail
44+||| Recognise no input (doesn't consume any input)
46+empty : Recognise False
49+||| Recognise a character that matches a predicate
51+pred : (Char -> Bool) -> Lexer
44||| Positive lookahead. Never consumes input.
54||| Positive lookahead. Never consumes input.
46expect : Recognise c -> Recognise False
56expect : Recognise c -> Recognise False
@@ -51,6 +61,124 @@ export
51reject : Recognise c -> Recognise False
61reject : Recognise c -> Recognise False
52reject = Lookahead False
62reject = Lookahead False
64+data StrLen : Type where
65+ MkStrLen : String -> Nat -> StrLen
67+getString : StrLen -> String
68+getString (MkStrLen str n) = str
70+strIndex : StrLen -> Nat -> Maybe Char
71+strIndex (MkStrLen str len) i
72+ = if i >= len then Nothing
73+ else Just (assert_total (prim__strIndex str (cast i)))
75+mkStr : String -> StrLen
76+mkStr str = MkStrLen str (length str)
78+strTail : Nat -> StrLen -> StrLen
79+strTail start (MkStrLen str len)
80+ = MkStrLen (substr start len str) (minus len start)
82+-- If the string is recognised, returns the index at which the token
84+scan : Recognise c -> Nat -> StrLen -> Maybe Nat
85+scan Empty idx str = pure idx
86+scan Fail idx str = Nothing
87+scan (Lookahead positive r) idx str
88+ = if isJust (scan r idx str) == positive
92+ = do c <- strIndex str idx
96+scan (SeqEat r1 r2) idx str
97+ = do idx' <- scan r1 idx str
98+ -- TODO: Can we prove totality instead by showing idx has increased?
99+ assert_total (scan r2 idx' str)
100+scan (SeqEmpty r1 r2) idx str
101+ = do idx' <- scan r1 idx str
103+scan (Alt r1 r2) idx str
104+ = case scan r1 idx str of
105+ Nothing => scan r2 idx str
106+ Just idx => Just idx
108+takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
110+ = do i <- scan lex 0 str -- i must be > 0 if successful
111+ pure (substr 0 i (getString str), strTail i str)
113+||| A mapping from lexers to the tokens they produce.
114+||| This is a list of pairs `(Lexer, String -> tokenType)`
115+||| For each Lexer in the list, if a substring in the input matches, run
116+||| the associated function to produce a token of type `tokenType`
118+TokenMap : (tokenType : Type) -> Type
119+TokenMap tokenType = List (Lexer, String -> tokenType)
121+||| A token, and the line and column where it was in the input
123+record TokenData a where
129+fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
130+fspanEnd k p "" = (k, "")
133+ let x = prim__strHead xxs
134+ xs = prim__strTail xxs in
135+ if p x then fspanEnd (S k) p xs
138+-- Faster version of 'span' from the prelude (avoids unpacking)
140+fspan : (Char -> Bool) -> String -> (String, String)
142+ = let (end, rest) = fspanEnd 0 p xs in
143+ (substr 0 end xs, rest)
145+tokenise : (line : Int) -> (col : Int) ->
146+ List (TokenData a) -> TokenMap a ->
147+ StrLen -> (List (TokenData a), (Int, Int, StrLen))
148+tokenise line col acc tmap str
149+ = case getFirstToken tmap str of
150+ Just (tok, line', col', rest) =>
151+ -- assert total because getFirstToken must consume something
152+ assert_total (tokenise line' col' (tok :: acc) tmap rest)
153+ Nothing => (reverse acc, (line, col, str))
155+ countNLs : List Char -> Nat
156+ countNLs str = List.length (filter (== '\n') str)
158+ getCols : String -> Int -> Int
160+ = case fspan (/= '\n') (reverse x) of
161+ (incol, "") => c + cast (length incol)
162+ (incol, _) => cast (length incol)
164+ getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)
165+ getFirstToken [] str = Nothing
166+ getFirstToken ((lex, fn) :: ts) str
167+ = case takeToken lex str of
168+ Just (tok, rest) => Just (MkToken line col (fn tok),
169+ line + cast (countNLs (unpack tok)),
170+ getCols tok col, rest)
171+ Nothing => getFirstToken ts str
173+||| Given a mapping from lexers to token generating functions (the
174+||| TokenMap a) and an input string, return a list of recognised tokens,
175+||| and the line, column, and remainder of the input at the first point in the
176+||| string where there are no recognised tokens.
178+lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
179+lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
180+ (ts, (l, c, getString str'))
54||| Recognise a specific character
182||| Recognise a specific character
56is : Char -> Lexer
184is : Char -> Lexer
@@ -172,70 +300,11 @@ export
172non : (l : Lexer) -> Lexer
300non : (l : Lexer) -> Lexer
173non l = reject l <+> any
301non l = reject l <+> any
175−||| Recognise no input (doesn't consume any input)
177−empty : Recognise False
180−||| Recognise a character that matches a predicate
182−pred : (Char -> Bool) -> Lexer
185||| Recognise any of the characters in the given string
303||| Recognise any of the characters in the given string
187oneOf : String -> Lexer
305oneOf : String -> Lexer
188oneOf cs = pred (\x => x `elem` unpack cs)
306oneOf cs = pred (\x => x `elem` unpack cs)
190−data StrLen : Type where
191− MkStrLen : String -> Nat -> StrLen
193−getString : StrLen -> String
194−getString (MkStrLen str n) = str
196−strIndex : StrLen -> Nat -> Maybe Char
197−strIndex (MkStrLen str len) i
198− = if i >= len then Nothing
199− else Just (assert_total (prim__strIndex str (cast i)))
201−mkStr : String -> StrLen
202−mkStr str = MkStrLen str (length str)
204−strTail : Nat -> StrLen -> StrLen
205−strTail start (MkStrLen str len)
206− = MkStrLen (substr start len str) (minus len start)
208−-- If the string is recognised, returns the index at which the token
210−scan : Recognise c -> Nat -> StrLen -> Maybe Nat
211−scan Empty idx str = pure idx
212−scan Fail idx str = Nothing
213−scan (Lookahead positive r) idx str
214− = if isJust (scan r idx str) == positive
217−scan (Pred f) idx str
218− = do c <- strIndex str idx
222−scan (SeqEat r1 r2) idx str
223− = do idx' <- scan r1 idx str
224− -- TODO: Can we prove totality instead by showing idx has increased?
225− assert_total (scan r2 idx' str)
226−scan (SeqEmpty r1 r2) idx str
227− = do idx' <- scan r1 idx str
229−scan (Alt r1 r2) idx str
230− = case scan r1 idx str of
231− Nothing => scan r2 idx str
232− Just idx => Just idx
234−takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
236− = do i <- scan lex 0 str -- i must be > 0 if successful
237− pure (substr 0 i (getString str), strTail i str)
239||| Recognise a character range [`a`-`b`]. Also works in reverse!
308||| Recognise a character range [`a`-`b`]. Also works in reverse!
241range : (start : Char) -> (end : Char) -> Lexer
310range : (start : Char) -> (end : Char) -> Lexer
@@ -391,72 +460,3 @@ blockComment start end = start <+> middle <+> end
392 middle : Recognise False
461 middle : Recognise False
393 middle = manyUntil end (blockComment start end <|> any)
462 middle = manyUntil end (blockComment start end <|> any)
395−||| A mapping from lexers to the tokens they produce.
396−||| This is a list of pairs `(Lexer, String -> tokenType)`
397−||| For each Lexer in the list, if a substring in the input matches, run
398−||| the associated function to produce a token of type `tokenType`
400−TokenMap : (tokenType : Type) -> Type
401−TokenMap tokenType = List (Lexer, String -> tokenType)
403−||| A token, and the line and column where it was in the input
405−record TokenData a where
411−fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
412−fspanEnd k p "" = (k, "")
415− let x = prim__strHead xxs
416− xs = prim__strTail xxs in
417− if p x then fspanEnd (S k) p xs
420−-- Faster version of 'span' from the prelude (avoids unpacking)
422−fspan : (Char -> Bool) -> String -> (String, String)
424− = let (end, rest) = fspanEnd 0 p xs in
425− (substr 0 end xs, rest)
427−tokenise : (line : Int) -> (col : Int) ->
428− List (TokenData a) -> TokenMap a ->
429− StrLen -> (List (TokenData a), (Int, Int, StrLen))
430−tokenise line col acc tmap str
431− = case getFirstToken tmap str of
432− Just (tok, line', col', rest) =>
433− -- assert total because getFirstToken must consume something
434− assert_total (tokenise line' col' (tok :: acc) tmap rest)
435− Nothing => (reverse acc, (line, col, str))
437− countNLs : List Char -> Nat
438− countNLs str = List.length (filter (== '\n') str)
440− getCols : String -> Int -> Int
442− = case fspan (/= '\n') (reverse x) of
443− (incol, "") => c + cast (length incol)
444− (incol, _) => cast (length incol)
446− getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)
447− getFirstToken [] str = Nothing
448− getFirstToken ((lex, fn) :: ts) str
449− = case takeToken lex str of
450− Just (tok, rest) => Just (MkToken line col (fn tok),
451− line + cast (countNLs (unpack tok)),
452− getCols tok col, rest)
453− Nothing => getFirstToken ts str
455−||| Given a mapping from lexers to token generating functions (the
456−||| TokenMap a) and an input string, return a list of recognised tokens,
457−||| and the line, column, and remainder of the input at the first point in the
458−||| string where there are no recognised tokens.
460−lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
461−lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
462− (ts, (l, c, getString str'))