@@ -41,6 +41,16 @@ export
4141fail : Recognise c
4242fail = Fail
4343
44+||| Recognise no input (doesn't consume any input)
45+export
46+empty : Recognise False
47+empty = Empty
48+
49+||| Recognise a character that matches a predicate
50+export
51+pred : (Char -> Bool) -> Lexer
52+pred = Pred
53+
4454||| Positive lookahead. Never consumes input.
4555export
4656expect : Recognise c -> Recognise False
@@ -51,6 +61,124 @@ export
5161reject : Recognise c -> Recognise False
5262reject = Lookahead False
5363
64+data StrLen : Type where
65+ MkStrLen : String -> Nat -> StrLen
66+
67+getString : StrLen -> String
68+getString (MkStrLen str n) = str
69+
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)))
74+
75+mkStr : String -> StrLen
76+mkStr str = MkStrLen str (length str)
77+
78+strTail : Nat -> StrLen -> StrLen
79+strTail start (MkStrLen str len)
80+ = MkStrLen (substr start len str) (minus len start)
81+
82+-- If the string is recognised, returns the index at which the token
83+-- ends
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
89+ then Just idx
90+ else Nothing
91+scan (Pred f) idx str
92+ = do c <- strIndex str idx
93+ if f c
94+ then Just (idx + 1)
95+ else Nothing
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
102+ scan r2 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
107+
108+takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
109+takeToken lex str
110+ = do i <- scan lex 0 str -- i must be > 0 if successful
111+ pure (substr 0 i (getString str), strTail i str)
112+
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`
117+public export
118+TokenMap : (tokenType : Type) -> Type
119+TokenMap tokenType = List (Lexer, String -> tokenType)
120+
121+||| A token, and the line and column where it was in the input
122+public export
123+record TokenData a where
124+ constructor MkToken
125+ line : Int
126+ col : Int
127+ tok : a
128+
129+fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
130+fspanEnd k p "" = (k, "")
131+fspanEnd k p xxs
132+ = assert_total $
133+ let x = prim__strHead xxs
134+ xs = prim__strTail xxs in
135+ if p x then fspanEnd (S k) p xs
136+ else (k, xxs)
137+
138+-- Faster version of 'span' from the prelude (avoids unpacking)
139+export
140+fspan : (Char -> Bool) -> String -> (String, String)
141+fspan p xs
142+ = let (end, rest) = fspanEnd 0 p xs in
143+ (substr 0 end xs, rest)
144+
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))
154+ where
155+ countNLs : List Char -> Nat
156+ countNLs str = List.length (filter (== '\n') str)
157+
158+ getCols : String -> Int -> Int
159+ getCols x c
160+ = case fspan (/= '\n') (reverse x) of
161+ (incol, "") => c + cast (length incol)
162+ (incol, _) => cast (length incol)
163+
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
172+
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.
177+export
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'))
181+
54182||| Recognise a specific character
55183export
56184is : Char -> Lexer
@@ -172,70 +300,11 @@ export
172300non : (l : Lexer) -> Lexer
173301non l = reject l <+> any
174302
175−||| Recognise no input (doesn't consume any input)
176−export
177−empty : Recognise False
178−empty = Empty
179−
180−||| Recognise a character that matches a predicate
181−export
182−pred : (Char -> Bool) -> Lexer
183−pred = Pred
184−
185303||| Recognise any of the characters in the given string
186304export
187305oneOf : String -> Lexer
188306oneOf cs = pred (\x => x `elem` unpack cs)
189307
190−data StrLen : Type where
191− MkStrLen : String -> Nat -> StrLen
192−
193−getString : StrLen -> String
194−getString (MkStrLen str n) = str
195−
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)))
200−
201−mkStr : String -> StrLen
202−mkStr str = MkStrLen str (length str)
203−
204−strTail : Nat -> StrLen -> StrLen
205−strTail start (MkStrLen str len)
206− = MkStrLen (substr start len str) (minus len start)
207−
208−-- If the string is recognised, returns the index at which the token
209−-- ends
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
215− then Just idx
216− else Nothing
217−scan (Pred f) idx str
218− = do c <- strIndex str idx
219− if f c
220− then Just (idx + 1)
221− else Nothing
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
228− scan r2 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
233−
234−takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
235−takeToken lex str
236− = do i <- scan lex 0 str -- i must be > 0 if successful
237− pure (substr 0 i (getString str), strTail i str)
238−
239308||| Recognise a character range [`a`-`b`]. Also works in reverse!
240309export
241310range : (start : Char) -> (end : Char) -> Lexer
@@ -391,72 +460,3 @@ blockComment start end = start <+> middle <+> end
391460 where
392461 middle : Recognise False
393462 middle = manyUntil end (blockComment start end <|> any)
394−
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`
399−public export
400−TokenMap : (tokenType : Type) -> Type
401−TokenMap tokenType = List (Lexer, String -> tokenType)
402−
403−||| A token, and the line and column where it was in the input
404−public export
405−record TokenData a where
406− constructor MkToken
407− line : Int
408− col : Int
409− tok : a
410−
411−fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
412−fspanEnd k p "" = (k, "")
413−fspanEnd k p xxs
414− = assert_total $
415− let x = prim__strHead xxs
416− xs = prim__strTail xxs in
417− if p x then fspanEnd (S k) p xs
418− else (k, xxs)
419−
420−-- Faster version of 'span' from the prelude (avoids unpacking)
421−export
422−fspan : (Char -> Bool) -> String -> (String, String)
423−fspan p xs
424− = let (end, rest) = fspanEnd 0 p xs in
425− (substr 0 end xs, rest)
426−
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))
436− where
437− countNLs : List Char -> Nat
438− countNLs str = List.length (filter (== '\n') str)
439−
440− getCols : String -> Int -> Int
441− getCols x c
442− = case fspan (/= '\n') (reverse x) of
443− (incol, "") => c + cast (length incol)
444− (incol, _) => cast (length incol)
445−
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
454−
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.
459−export
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'))