module Language.Lexer (Token(..), lex) where

import Prelude hiding (lex)
import Data.Char (isAlpha, isAlphaNum, isSpace, isDigit)

data Token
  = TIdent String
  | TKeyword String
  | TLParen | TRParen
  | TNand
  | TColon | TSemicolon
  | TEquals
  | TArrow
  | TEOF
  deriving (Eq, Show)

keywords :: [String]
keywords = ["def", "assert", "prove", "module", "true", "false", "nand"]

lex :: String -> [Token]
lex [] = [TEOF]
lex ('-':'-':rest) = lex (dropWhile (/= '\n') rest)
lex (c:rest) | isSpace c = lex rest
lex ('(':rest) = TLParen : lex rest
lex (')':rest) = TRParen : lex rest
lex ('|':rest) = TNand : lex rest
lex (':':rest) = TColon : lex rest
lex (';':rest) = TSemicolon : lex rest
lex ('=':rest) = TEquals : lex rest
lex ('-':'>':rest) = TArrow : lex rest
lex (c:rest) | isAlpha c =
  let (word, remaining) = span isAlphaNum (c:rest)
  in (if word `elem` keywords then TKeyword word else TIdent word) : lex remaining
lex (_:rest) = lex rest