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