quox/src/Quox/Lexer.idr

module Quox.Lexer

import Quox.Error

import Data.String
import public Text.Lexer
import public Text.Lexer.Tokenizer
import Generics.Derive

%default total
%language ElabReflection


public export
record Error where
  constructor Err
  reason    : StopReason
  line, col : Int
  char      : Char

public export
data Punc
= LParen  | RParen
| LSquare | RSquare
| LBrace  | RBrace
| Comma
| Colon | DblColon
| Arrow | DblArrow
| Times | Triangle
| Wild

%runElab derive "Punc" [Generic, Meta, Eq, Ord, DecEq, Show]



public export
data Token
= P Punc
| Name String | Symbol String

%runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]


nameStart = pred $ \c => isAlpha c || c == '_'
nameCont  = pred $ \c => isAlphaNum c || c == '_' || c == '\''

name = nameStart <+> many nameCont <+> reject nameCont

wild = exact "_" <+> reject nameCont

%hide Text.Lexer.symbol
symbol = exact "'" <+> name


skip : Lexer -> Tokenizer (Maybe a)
skip lex = match lex $ const Nothing

simple : List String -> a -> Tokenizer (Maybe a)
simple str x = match (choice $ map exact str) $ const $ Just x

choice : (xs : List (Tokenizer a)) -> {auto 0 _ : So (isCons xs)} -> Tokenizer a
choice (t :: ts) = foldl (\a, b => a <|> b) t ts

tokens : Tokenizer (Maybe Token)
tokens = choice [
  skip $ lineComment $ exact "--",
  skip $ blockComment (exact "{-") (exact "-}"),
  skip spaces,

  simple ["("] $ P LParen,  simple [")"] $ P RParen,
  simple ["["] $ P LSquare, simple ["]"] $ P RSquare,
  simple ["{"] $ P LBrace,  simple ["}"] $ P RBrace,
  simple [","] $ P Comma,
  simple ["::", "∷"] $ P DblColon,
  simple [":"] $ P Colon,

  simple ["->", "→"] $ P Arrow,
  simple ["=>", "⇒"] $ P DblArrow,
  simple ["**", "×"] $ P Times,
  simple ["<<", "⊲"] $ P Triangle,
  match wild $ const $ Just $ P Wild,

  match name   $ Just . Name,
  match symbol $ Just . Symbol . assert_total strTail
]

export
lex : MonadThrow Error m => String -> m (List (WithBounds Token))
lex str =
  let (res, (reason, line, col, str)) = lex tokens str in
  case reason of
       EndInput => pure $ mapMaybe sequence res
       _        => let char = assert_total strIndex str 0 in
                   throw $ Err {reason, line, col, char}