{-# LANGUAGE CPP #-}

-- | Lexer from Strings into Tokens
module L3.Parse.Lexer (Token (..), alternatives, comment, lexSrc, grammar) where

import Control.Applicative hiding (many)
import L3.Log
import L3.Parse.Parsec
import L3.Parse.Parser
import L3.Parse.StringParsec
import L3.Util

trace :: String -> a -> a
trace = String -> String -> a -> a
forall a. String -> String -> a -> a
traceU String
"Parse::Lexer"

-- | Lex strings into tokens, canonical form for the syntax definitition
data Token
  = OpenParen
  | CloseParen
  | OpenBracket
  | CloseBracket
  | HasType
  | At
  | StarT
  | BoxT
  | Arrow
  | LambdaT
  | PiT
  | AutoT
  | Symbol String
  | Number Int
  | Comment String
  | EOL
  deriving (Int -> Token -> ShowS
[Token] -> ShowS
Token -> String
(Int -> Token -> ShowS)
-> (Token -> String) -> ([Token] -> ShowS) -> Show Token
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Token] -> ShowS
$cshowList :: [Token] -> ShowS
show :: Token -> String
$cshow :: Token -> String
showsPrec :: Int -> Token -> ShowS
$cshowsPrec :: Int -> Token -> ShowS
Show, Token -> Token -> Bool
(Token -> Token -> Bool) -> (Token -> Token -> Bool) -> Eq Token
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Token -> Token -> Bool
$c/= :: Token -> Token -> Bool
== :: Token -> Token -> Bool
$c== :: Token -> Token -> Bool
Eq)

-- | A list of Alternatives that may be used to lex a string into tokens.
alternatives :: [Parser String Token]
alternatives :: [Parser String Token]
alternatives =
  [ String -> Parser String String
reserved String
"(" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"open-paren" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
OpenParen),
    String -> Parser String String
reserved String
")" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"close-paren" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
CloseParen),
    String -> Parser String String
reserved String
"[" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"open-bracket" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
OpenBracket),
    String -> Parser String String
reserved String
"]" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"close-bracket" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
CloseBracket),
    String -> Parser String String
reserved String
"*" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"star" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
StarT),
    String -> Parser String String
reserved String
"#" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"box" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
BoxT),
    String -> Parser String String
reserved String
":" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"has-type" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
HasType),
    String -> Parser String String
reserved String
"." Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"arrow" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
Arrow),
    String -> Parser String String
reserved String
"→" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"arrow" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
Arrow),
    String -> Parser String String
reserved String
"->" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"arrow" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
Arrow),
    String -> Parser String String
reserved String
"λ" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"lambda" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
LambdaT),
    String -> Parser String String
reserved String
"π" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"pi" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
PiT),
#ifdef SETNOTATION
    String -> Parser String String
reserved String
"⊤" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"star" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
StarT),
    String -> Parser String String
reserved String
"⊥" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"box" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
BoxT),
    String -> Parser String String
reserved String
"∈" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"has-type" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
HasType),
    String -> Parser String String
reserved String
"∃" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"lambda" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
LambdaT),
    String -> Parser String String
reserved String
"∀" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"pi" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
PiT),
#endif
    String -> Parser String String
reserved String
"@" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"at" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
At),
    String -> Parser String String
reserved String
"--" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"comment" Parser String Token
comment,
    String -> Parser String String
reserved String
"\n" Parser String String -> Parser String Token -> Parser String Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"end-of-line" (Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure Token
EOL),
    Int -> Token
Number (Int -> Token) -> Parser String Int -> Parser String Token
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String Int
number,
    String -> Token
Symbol (String -> Token) -> Parser String String -> Parser String Token
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String String
word
  ]

-- | Parse a comment, taking characters until an End-Of-Line
comment :: Parser String Token
comment :: Parser String Token
comment = String -> Parser String Token -> Parser String Token
forall a. String -> a -> a
trace String
"comment" (Parser String Token -> Parser String Token)
-> Parser String Token -> Parser String Token
forall a b. (a -> b) -> a -> b
$ do
  String
cs <- Parser String Char -> Parser String String
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Parser String Char -> Parser String String)
-> Parser String Char -> Parser String String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Parser String Char
satisfy (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\n')
  Token -> Parser String Token
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Token -> Parser String Token) -> Token -> Parser String Token
forall a b. (a -> b) -> a -> b
$ String -> Token
Comment String
cs

-- | Parse a string into canonical form using tokens
lexSrc :: String -> Result [Token]
lexSrc :: String -> Result [Token]
lexSrc = Parser String [Token] -> String -> Result [Token]
forall (f :: * -> *) i o.
(Alternative f, Show (f i), Show o, Eq (f i)) =>
Parser (f i) o -> f i -> Result o
runParser Parser String [Token]
grammar

-- | The grammar for this parser is the collection of Alternatives
grammar :: Parser String [Token]
grammar :: Parser String [Token]
grammar = Parser String Token -> Parser String [Token]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Parser String Token -> Parser String [Token])
-> Parser String Token -> Parser String [Token]
forall a b. (a -> b) -> a -> b
$ (Parser String Token -> Parser String Token -> Parser String Token)
-> [Parser String Token] -> Parser String Token
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Parser String Token -> Parser String Token -> Parser String Token
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) [Parser String Token]
alternatives