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