@@ -1,194 +1,9 @@
11module Text.Lexer
22
3−import Data.Bool.Extra
4−
5−import public Control.Delayed
3+import public Text.Lexer.Core
64
75%default total
86
9−||| A language of token recognisers.
10−||| @ consumes If `True`, this recogniser is guaranteed to consume at
11−||| least one character of input when it succeeds.
12−export
13−data Recognise : (consumes : Bool) -> Type where
14− Empty : Recognise False
15− Fail : Recognise c
16− Lookahead : (positive : Bool) -> Recognise c -> Recognise False
17− Pred : (Char -> Bool) -> Recognise True
18− SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
19− SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
20− Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)
21−
22−||| A token recogniser. Guaranteed to consume at least one character.
23−public export
24−Lexer : Type
25−Lexer = Recognise True
26−
27−||| Sequence two recognisers. If either consumes a character, the sequence
28−||| is guaranteed to consume a character.
29−export %inline
30−(<+>) : {c1 : Bool} ->
31− Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
32−(<+>) {c1 = False} = SeqEmpty
33−(<+>) {c1 = True} = SeqEat
34−
35−||| Alternative recognisers. If both consume, the combination is guaranteed
36−||| to consumer a character.
37−export
38−(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
39−(<|>) = Alt
40−
41−||| A recogniser that always fails.
42−export
43−fail : Recognise c
44−fail = Fail
45−
46−||| Recognise no input (doesn't consume any input)
47−export
48−empty : Recognise False
49−empty = Empty
50−
51−||| Recognise a character that matches a predicate
52−export
53−pred : (Char -> Bool) -> Lexer
54−pred = Pred
55−
56−||| Positive lookahead. Never consumes input.
57−export
58−expect : Recognise c -> Recognise False
59−expect = Lookahead True
60−
61−||| Negative lookahead. Never consumes input.
62−export
63−reject : Recognise c -> Recognise False
64−reject = Lookahead False
65−
66−||| Sequence a list of recognisers.
67−export
68−concat : {c : Bool} -> (xs : List (Recognise c)) -> Recognise (c && isCons xs)
69−concat {c} [] = rewrite andFalseFalse c in Empty
70−concat {c} (x :: xs) = rewrite andTrueNeutral c in
71− rewrite sym (orSameAndRightNeutral c (isCons xs)) in
72− SeqEmpty x (concat xs)
73−
74−data StrLen : Type where
75− MkStrLen : String -> Nat -> StrLen
76−
77−getString : StrLen -> String
78−getString (MkStrLen str n) = str
79−
80−strIndex : StrLen -> Nat -> Maybe Char
81−strIndex (MkStrLen str len) i
82− = if i >= len then Nothing
83− else Just (assert_total (prim__strIndex str (cast i)))
84−
85−mkStr : String -> StrLen
86−mkStr str = MkStrLen str (length str)
87−
88−strTail : Nat -> StrLen -> StrLen
89−strTail start (MkStrLen str len)
90− = MkStrLen (substr start len str) (minus len start)
91−
92−-- If the string is recognised, returns the index at which the token
93−-- ends
94−scan : Recognise c -> Nat -> StrLen -> Maybe Nat
95−scan Empty idx str = pure idx
96−scan Fail idx str = Nothing
97−scan (Lookahead positive r) idx str
98− = if isJust (scan r idx str) == positive
99− then Just idx
100− else Nothing
101−scan (Pred f) idx str
102− = do c <- strIndex str idx
103− if f c
104− then Just (idx + 1)
105− else Nothing
106−scan (SeqEat r1 r2) idx str
107− = do idx' <- scan r1 idx str
108− -- TODO: Can we prove totality instead by showing idx has increased?
109− assert_total (scan r2 idx' str)
110−scan (SeqEmpty r1 r2) idx str
111− = do idx' <- scan r1 idx str
112− scan r2 idx' str
113−scan (Alt r1 r2) idx str
114− = case scan r1 idx str of
115− Nothing => scan r2 idx str
116− Just idx => Just idx
117−
118−takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
119−takeToken lex str
120− = do i <- scan lex 0 str -- i must be > 0 if successful
121− pure (substr 0 i (getString str), strTail i str)
122−
123−||| A mapping from lexers to the tokens they produce.
124−||| This is a list of pairs `(Lexer, String -> tokenType)`
125−||| For each Lexer in the list, if a substring in the input matches, run
126−||| the associated function to produce a token of type `tokenType`
127−public export
128−TokenMap : (tokenType : Type) -> Type
129−TokenMap tokenType = List (Lexer, String -> tokenType)
130−
131−||| A token, and the line and column where it was in the input
132−public export
133−record TokenData a where
134− constructor MkToken
135− line : Int
136− col : Int
137− tok : a
138−
139−fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
140−fspanEnd k p "" = (k, "")
141−fspanEnd k p xxs
142− = assert_total $
143− let x = prim__strHead xxs
144− xs = prim__strTail xxs in
145− if p x then fspanEnd (S k) p xs
146− else (k, xxs)
147−
148−-- Faster version of 'span' from the prelude (avoids unpacking)
149−export
150−fspan : (Char -> Bool) -> String -> (String, String)
151−fspan p xs
152− = let (end, rest) = fspanEnd 0 p xs in
153− (substr 0 end xs, rest)
154−
155−tokenise : (line : Int) -> (col : Int) ->
156− List (TokenData a) -> TokenMap a ->
157− StrLen -> (List (TokenData a), (Int, Int, StrLen))
158−tokenise line col acc tmap str
159− = case getFirstToken tmap str of
160− Just (tok, line', col', rest) =>
161− -- assert total because getFirstToken must consume something
162− assert_total (tokenise line' col' (tok :: acc) tmap rest)
163− Nothing => (reverse acc, (line, col, str))
164− where
165− countNLs : List Char -> Nat
166− countNLs str = List.length (filter (== '\n') str)
167−
168− getCols : String -> Int -> Int
169− getCols x c
170− = case fspan (/= '\n') (reverse x) of
171− (incol, "") => c + cast (length incol)
172− (incol, _) => cast (length incol)
173−
174− getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)
175− getFirstToken [] str = Nothing
176− getFirstToken ((lex, fn) :: ts) str
177− = case takeToken lex str of
178− Just (tok, rest) => Just (MkToken line col (fn tok),
179− line + cast (countNLs (unpack tok)),
180− getCols tok col, rest)
181− Nothing => getFirstToken ts str
182−
183−||| Given a mapping from lexers to token generating functions (the
184−||| TokenMap a) and an input string, return a list of recognised tokens,
185−||| and the line, column, and remainder of the input at the first point in the
186−||| string where there are no recognised tokens.
187−export
188−lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
189−lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
190− (ts, (l, c, getString str'))
191−
1927||| Recognise a specific character
1938export
1949is : Char -> Lexer