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