0 | module Parser.Lexer.Source

  2 | import public Parser.Lexer.Common

  4 | import Data.Either

  5 | import Data.Maybe

  6 | import Data.String

  7 | import Libraries.Data.String.Extra

  8 | import public Libraries.Text.Bounded

  9 | import Libraries.Text.Lexer.Tokenizer

 10 | import Libraries.Text.PrettyPrint.Prettyprinter

 11 | import Libraries.Text.PrettyPrint.Prettyprinter.Util

 13 | import Protocol.Hex

 14 | import Libraries.Utils.Octal

 15 | import Libraries.Utils.String

 17 | import Core.Name

 19 | %default total

 21 | public export

 22 | data IsMultiline = Multi | Single

 24 | public export

 25 | data DebugInfo

 26 |   = DebugLoc

 27 |   | DebugFile

 28 |   | DebugLine

 29 |   | DebugCol

 32 | Eq DebugInfo where

 33 |   DebugLoc == DebugLoc = True

 34 |   DebugFile == DebugFile = True

 35 |   DebugLine == DebugLine = True

 36 |   DebugCol == DebugCol = True

 37 |   _ == _ = False

 39 | public export

 40 | data Token

 41 |   -- Literals

 42 |   = CharLit String

 43 |   | DoubleLit Double

 44 |   | IntegerLit Integer

 45 |   -- String

 46 |   | StringBegin Nat IsMultiline -- The escape depth and whether is multiline string

 47 |   | StringEnd

 48 |   | InterpBegin

 49 |   | InterpEnd

 50 |   | StringLit String

 51 |   -- Identifiers

 52 |   | HoleIdent String

 53 |   | Ident String

 54 |   | DotSepIdent Namespace String -- ident.ident

 55 |   | DotIdent String               -- .ident

 56 |   | Symbol String

 57 |   -- Whitespace

 58 |   | Space

 59 |   -- Comments

 60 |   | Comment

 61 |   | DocComment String

 62 |   -- Special

 63 |   | CGDirective String

 64 |   | EndInput

 65 |   | Keyword String

 66 |   | Pragma String

 67 |   | MagicDebugInfo DebugInfo

 68 |   | Unrecognised String

 71 | Show DebugInfo where

 72 |   show DebugLoc = "__LOC__"

 73 |   show DebugFile = "__FILE__"

 74 |   show DebugLine = "__LINE__"

 75 |   show DebugCol = "__COL__"

 78 | Show Token where

 79 |   -- Literals

 80 |   show (CharLit x) = "character " ++ show x

 81 |   show (DoubleLit x) = "double " ++ show x

 82 |   show (IntegerLit x) = "literal " ++ show x

 83 |   -- String

 84 |   show (StringBegin hashtag Single) = "string begin"

 85 |   show (StringBegin hashtag Multi) = "multiline string begin"

 86 |   show StringEnd = "string end"

 87 |   show InterpBegin = "string interp begin"

 88 |   show InterpEnd = "string interp end"

 89 |   show (StringLit x) = "string " ++ show x

 90 |   -- Identifiers

 91 |   show (HoleIdent x) = "hole identifier " ++ x

 92 |   show (Ident x) = "identifier " ++ x

 93 |   show (DotSepIdent ns n) = "namespaced identifier " ++ show ns ++ "." ++ show n

 94 |   show (DotIdent x) = "dot+identifier " ++ x

 95 |   show (Symbol x) = "symbol " ++ x

 96 |   -- Whitespace

 97 |   show Space = "whitespace"

 98 |   -- Comments

 99 |   show Comment = "comment"

100 |   show (DocComment c) = "doc comment: \"" ++ c ++ "\""

101 |   -- Special

102 |   show (CGDirective x) = "CGDirective " ++ x

103 |   show EndInput = "end of input"

104 |   show (Keyword x) = x

105 |   show (Pragma x) = "pragma " ++ x

106 |   show (MagicDebugInfo di) = show di

107 |   show (Unrecognised x) = "Unrecognised " ++ x

110 | Pretty Void Token where

111 |   -- Literals

112 |   pretty (CharLit x) = pretty "character" <++> squotes (pretty x)

113 |   pretty (DoubleLit x) = pretty "double" <++> pretty (show x)

114 |   pretty (IntegerLit x) = pretty "literal" <++> pretty (show x)

115 |   -- String

116 |   pretty (StringBegin hashtag Single) = reflow "string begin"

117 |   pretty (StringBegin hashtag Multi) = reflow "multiline string begin"

118 |   pretty StringEnd = reflow "string end"

119 |   pretty InterpBegin = reflow "string interp begin"

120 |   pretty InterpEnd = reflow "string interp end"

121 |   pretty (StringLit x) = pretty "string" <++> dquotes (pretty x)

122 |   -- Identifiers

123 |   pretty (HoleIdent x) = reflow "hole identifier" <++> pretty x

124 |   pretty (Ident x) = pretty "identifier" <++> pretty x

125 |   pretty (DotSepIdent ns n) = reflow "namespaced identifier" <++> pretty ns <+> dot <+> pretty n

126 |   pretty (DotIdent x) = pretty "dot+identifier" <++> pretty x

127 |   pretty (Symbol x) = pretty "symbol" <++> pretty x

128 |   -- Whitespace

129 |   pretty Space = pretty "space"

130 |   -- Comments

131 |   pretty Comment = pretty "comment"

132 |   pretty (DocComment c) = reflow "doc comment:" <++> dquotes (pretty c)

133 |   -- Special

134 |   pretty (CGDirective x) = pretty "CGDirective" <++> pretty x

135 |   pretty EndInput = reflow "end of input"

136 |   pretty (Keyword x) = pretty x

137 |   pretty (Pragma x) = pretty "pragma" <++> pretty x

138 |   pretty (MagicDebugInfo di) = pretty (show di)

139 |   pretty (Unrecognised x) = pretty "Unrecognised" <++> pretty x

141 | docComment : Lexer

142 | docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n')

144 | holeIdent : Lexer

145 | holeIdent = is '?' <+> identNormal

147 | dotIdent : Lexer

148 | dotIdent = is '.' <+> identNormal

150 | pragma : Lexer

151 | pragma = is '%' <+> identNormal

153 | doubleLit : Lexer

155 |     = digits <+> is '.' <+> digits <+> opt

156 |            (is 'e' <+> opt (is '-' <|> is '+') <+> digits)

158 | stringBegin : Lexer

159 | stringBegin = many (is '#') <+> (is '"')

161 | stringEnd : Nat -> String

162 | stringEnd hashtag = "\"" ++ replicate hashtag '#'

164 | multilineBegin : Lexer

165 | multilineBegin = many (is '#') <+> (exact "\"\"\"") <+>

166 |                     manyUntil newline space <+> newline

168 | multilineEnd : Nat -> String

169 | multilineEnd hashtag = "\"\"\"" ++ replicate hashtag '#'

173 | cgDirective : Lexer

175 |     = exact "%cg" <+>

176 |       ((some space <+>

177 |            some (pred isAlphaNum) <+> many space <+>

178 |            is '{' <+> many (isNot '}') <+>

179 |            is '}')

180 |          <|> many (isNot '\n'))

182 | mkDirective : String -> Token

183 | mkDirective str = CGDirective (trim (substr 3 (length str) str))

185 | public export

186 | fixityKeywords : List String

187 | fixityKeywords = ["infixl", "infixr", "infix", "prefix"]

192 | public export

193 | keywords : List String

194 | keywords = ["data", "module", "where", "let", "in", "do", "record",

195 |             "auto", "default", "implicit", "failing", "mutual", "namespace",

196 |             "parameters", "with", "proof", "impossible", "case", "of",

197 |             "if", "then", "else", "forall", "rewrite", "typebind", "autobind",

198 |             "using", "interface", "implementation", "open", "import",

199 |             "public", "export", "private"] ++

200 |             fixityKeywords ++

201 |             ["total", "partial", "covering"]

203 | public export

204 | debugInfo : List (String, DebugInfo)

205 | debugInfo = map (\ di => (show di, di))

206 |           [ DebugLoc, DebugFile, DebugLine, DebugCol ]

209 | special : List String

210 | special = ["%lam", "%pi", "%imppi", "%let"]

212 | public export

213 | symbols : List String

214 | symbols = [",", ";", "_", "`"]

217 | groupSymbols : List String

218 | groupSymbols = [".(", -- for things such as Foo.Bar.(+)

219 |     ".[|", -- for namespaced brackets such as Foo.Bar.[| x + y |]

220 |     "@{", "[|", "(", "{", "[<", "[>", "[", "`(", "`{", "`["]

223 | groupClose : String -> String

224 | groupClose ".(" = ")"

225 | groupClose "@{" = "}"

226 | groupClose "[|" = "|]"

227 | groupClose ".[|" = "|]"

228 | groupClose "(" = ")"

229 | groupClose "[" = "]"

230 | groupClose "[<" = "]"

231 | groupClose "[>" = "]"

232 | groupClose "{" = "}"

233 | groupClose "`(" = ")"

234 | groupClose "`{" = "}"

235 | groupClose "`[" = "]"

236 | groupClose _ = ""

238 | validSymbol : Lexer

239 | validSymbol = some (pred isOpChar)

242 | public export

243 | reservedInfixSymbols : List String

245 |     = ["%", "\\", ":", "=", ":=", "$=", "|", "|||", "<-", "->", "=>", "?", "!",

246 |        "&", "**", "..", "~", "@"]

249 | public export

250 | reservedSymbols : List String

252 |     = symbols

253 |     ++ groupSymbols ++ (groupClose <$> groupSymbols)

254 |     ++ reservedInfixSymbols

256 | fromBinLit : String -> Integer

257 | fromBinLit str

258 |     = if length str <= 2

259 |          then 0

260 |          else let num = assert_total (strTail (strTail str)) in

261 |                 fromBin . reverse . map castBin . unpack $ num

262 |     where

263 |       castBin : Char -> Integer

264 |       castBin '1' = 1; castBin _ = 0 -- This can only be '1' and '0' once lexed

265 |       fromBin : List Integer -> Integer

266 |       fromBin [] = 0

267 |       fromBin (0 :: xs) = 2 * fromBin xs

268 |       fromBin (x :: xs) = x + (2 * fromBin xs)

270 | fromHexLit : String -> Integer

271 | fromHexLit str

272 |   = if length str <= 2

273 |        then 0

274 |        else let num = assert_total (strTail (strTail str)) in

275 |              fromMaybe 0 (fromHex (reverse num))

276 |              --        ^-- can't happen if the literal was lexed correctly

278 | fromOctLit : String -> Integer

279 | fromOctLit str

280 |   = if length str <= 2

281 |        then 0

282 |        else let num = assert_total (strTail (strTail str)) in

283 |              fromMaybe 0 (fromOct (reverse num))

284 |              --        ^-- can't happen if the literal lexed correctly

287 |   stringTokens : Bool -> Nat -> Tokenizer Token

288 |   stringTokens multi hashtag

289 |       = let escapeChars = "\\" ++ replicate hashtag '#'

290 |             interpStart = escapeChars ++ "{"

291 |             escapeLexer = escape (exact escapeChars) any

292 |             charLexer = if multi

293 |                            then non $ exact (multilineEnd hashtag)

294 |                            else non (newline <|> exact (stringEnd hashtag))

295 |           in

296 |             match (someUntil (exact interpStart) (escapeLexer <|> charLexer)) (\x => StringLit x)

297 |         <|> compose (exact interpStart)

298 |                     (const InterpBegin)

299 |                     (const ())

300 |                     (\_ => rawTokens)

301 |                     (const $ is '}')

302 |                     (const InterpEnd)

304 |   rawTokens : Tokenizer Token

305 |   rawTokens =

306 |           match comment (const Comment)

307 |       <|> match blockComment (const Comment)

308 |       <|> match docComment (DocComment . removeOptionalLeadingSpace . drop 3)

309 |       <|> match cgDirective mkDirective

310 |       <|> match holeIdent (\x => HoleIdent (assert_total (strTail x)))

311 |       <|> compose (choice $ exact <$> groupSymbols)

312 |                   Symbol

313 |                   id

314 |                   (\_ => rawTokens)

315 |                   (exact . groupClose)

316 |                   Symbol

317 |       <|> match (choice $ (exact . fst) <$> debugInfo) (MagicDebugInfo . fromMaybe DebugLoc . flip lookup debugInfo)

318 |       <|> match (choice $ exact <$> symbols) Symbol

319 |       <|> match doubleLit (DoubleLit . cast)

320 |       <|> match binUnderscoredLit (IntegerLit . fromBinLit . removeUnderscores)

321 |       <|> match hexUnderscoredLit (IntegerLit . fromHexLit . removeUnderscores)

322 |       <|> match octUnderscoredLit (IntegerLit . fromOctLit . removeUnderscores)

323 |       <|> match digitsUnderscoredLit (IntegerLit . cast . removeUnderscores)

324 |       <|> compose multilineBegin

325 |                   (\begin => StringBegin (countHashtag begin) Multi)

326 |                   countHashtag

327 |                   (stringTokens True)

328 |                   (exact . multilineEnd)

329 |                   (const StringEnd)

330 |       <|> compose stringBegin

331 |                   (\begin => StringBegin (countHashtag begin) Single)

332 |                   countHashtag

333 |                   (stringTokens False)

334 |                   (\hashtag => exact (stringEnd hashtag) <+> reject (is '"'))

335 |                   (const StringEnd)

336 |       <|> match charLit (CharLit . stripQuotes)

337 |       <|> match dotIdent (\x => DotIdent (assert_total $ strTail x))

338 |       <|> match namespacedIdent parseNamespace

339 |       <|> match identNormal parseIdent

340 |       <|> match pragma (\x => Pragma (assert_total $ strTail x))

341 |       <|> match space (const Space)

342 |       <|> match validSymbol Symbol

343 |       <|> match symbol Unrecognised

344 |     where

345 |       parseIdent : String -> Token

346 |       parseIdent x = if x `elem` keywords then Keyword x

347 |                      else Ident x

349 |       parseNamespace : String -> Token

350 |       parseNamespace ns = case mkNamespacedIdent ns of

351 |                                (Nothing, ident) => parseIdent ident

352 |                                (Just ns, n)     => DotSepIdent ns n

354 |       countHashtag : String -> Nat

355 |       countHashtag = count (== '#') . unpack

357 |       removeOptionalLeadingSpace : String -> String

358 |       removeOptionalLeadingSpace str = case strM str of

359 |                                             StrCons ' ' tail => tail

360 |                                             _ => str

362 |       removeUnderscores : String -> String

363 |       removeUnderscores s = fastPack $ filter (/= '_') (fastUnpack s)

366 | lexTo : Lexer ->

367 |         String ->

368 |         Either (StopReason, Int, Int, String)

369 |                ( List (WithBounds ())     -- bounds of comments

370 |                , List (WithBounds Token)) -- tokens

371 | lexTo reject str

372 |     = case lexTo reject rawTokens str of

373 |            (toks, (EndInput, l, c, _)) =>

374 |              -- Add the EndInput token so that we'll have a line and column

375 |              -- number to read when storing spans in the file

376 |              let end = [MkBounded EndInput False (MkBounds l c l c)] in

377 |              Right $ map (++ end)

378 |                    $ partitionEithers

379 |                    $ map spotComment

380 |                    $ filter isNotSpace toks

381 |            (_, fail) => Left fail

382 |     where

384 |       isNotSpace : WithBounds Token -> Bool

385 |       isNotSpace t = case t.val of

386 |         Space => False

387 |         _ => True

389 |       spotComment : WithBounds Token ->

390 |                     Either (WithBounds ()) (WithBounds Token)

391 |       spotComment t = case t.val of

392 |         Comment => Left (() <$ t)

393 |         _ => Right t

396 | lex : String ->

397 |       Either (StopReason, Int, Int, String)

398 |              ( List (WithBounds ())     -- bounds of comments

399 |              , List (WithBounds Token)) -- tokens

400 | lex = lexTo (pred $ const False)