module Parser (
  parseType,
  parseTerm
) where

import Syntax

import Text.ParserCombinators.Parsec hiding (char)
import qualified Text.ParserCombinators.Parsec.Token as P
import Text.ParserCombinators.Parsec.Language (haskellStyle)

parseType :: String -> Either ParseError Type
parseType str = parse (wholeInp type_) "" str
parseTerm :: String -> Either ParseError Term
parseTerm str = parse (wholeInp term) "" str

wholeInp :: (Show tok) => GenParser tok st t -> GenParser tok st t
wholeInp p = do
  x <- p
  eof
  return x

lexer :: P.TokenParser ()
lexer  = P.makeTokenParser haskellStyle
        {
                P.reservedNames = ["true", "false", "not", "if", "fix", "Int", "Bool"],
                P.reservedOpNames = ["<=>", "<=>#", "+", "+#", "=", "=#", "/", "/#", "->",
                         "\\", ".", ":", "<", "|>", ">"]
        }

whiteSpace :: CharParser () ()
whiteSpace  = P.whiteSpace lexer
lexeme :: CharParser () a -> CharParser () a
lexeme      = P.lexeme lexer
symbol :: String -> CharParser () String
symbol      = P.symbol lexer
natural :: CharParser () Integer
natural     = P.natural lexer
parens :: CharParser () a -> CharParser () a
parens      = P.parens lexer
semi :: CharParser () String
semi        = P.semi lexer
identifier :: CharParser () String
identifier  = P.identifier lexer
reserved :: String -> CharParser () ()
reserved    = P.reserved lexer
reservedOp :: String -> CharParser () ()
reservedOp  = P.reservedOp lexer
float :: CharParser () Double
float       = P.float lexer
integer :: CharParser () Integer
integer     = P.integer lexer
charLiteral :: CharParser () Char
charLiteral = P.charLiteral lexer
commaSep :: CharParser () a -> CharParser () [a]
commaSep    = P.commaSep lexer
operator :: CharParser () String
operator    = P.operator lexer
angles :: CharParser () a -> CharParser () a
angles      = P.angles lexer
braces :: CharParser () a -> CharParser () a
braces      = P.braces lexer
brackets :: CharParser () a -> CharParser () a
brackets    = P.brackets lexer

con = fmap Con $
  choice [true, false, implication, not_, number, plus, div_, equals,
          if_, fix_, plusn, divn, equalsn, implb]

true :: GenParser Char () Constant
true        = reserved   "true"  >> return Ctrue
false :: GenParser Char () Constant
false       = reserved   "false" >> return Cfalse
implication :: GenParser Char () Constant
implication = reservedOp "<=>"   >> return Cimpl
not_ :: GenParser Char () Constant
not_        = reserved   "not"   >> return Cnot
plus :: GenParser Char () Constant
plus        = reservedOp "+"     >> return Cplus
equals :: GenParser Char () Constant
equals      = reservedOp "="     >> return Ceq
div_ :: GenParser Char () Constant
div_        = reservedOp "/"     >> return Cdiv
number :: GenParser Char () Constant
number      = try natural        >>= (return . Cint)

divn :: GenParser Char () Constant
divn = do
  reservedOp "/#"
  n <- natural
  return $ Cdivn n

plusn :: GenParser Char () Constant
plusn = do
  reservedOp "+#"
  n <- natural
  return $ Cplusn n

equalsn :: GenParser Char () Constant
equalsn = do
  reservedOp "=#"
  n <- natural
  return $ Ceqn n

implb :: GenParser Char () Constant
implb = do
  reservedOp "<=>#"
  (reserved "true" >> return (Cimplb True)) <|>
    (reserved "false" >> return (Cimplb False))

if_         = do
  reserved "if"
  t <- typeArg
  return (Cif t)

fix_ = do
  reserved "fix"
  t <- typeArg
  return (Cfix t)

typeArg :: CharParser () Type
type_ :: CharParser () Type
fun :: GenParser Char () Type
varOfType :: GenParser Char () (Name, Type)
ref :: GenParser Char () Type
term :: GenParser Char () Term
term1 :: GenParser Char () Term
con :: GenParser Char () Term
if_ :: GenParser Char () Constant
fix_ :: GenParser Char () Constant
lam :: GenParser Char () Term
cast :: GenParser Char () Term
typeArg = brackets type_

var :: GenParser Char () Term
var = do
  x <- identifier
  return (Var x)

lam = parens $ do
  reservedOp "\\"
  (x,t) <- varOfType
  reservedOp "."
  te <- term
  return (Lam x t te)

term = do
  ts <- many1 term1
  if length ts == 1
    then return (head ts)
    else return (foldApp ts)
  where
    foldApp ts = foldl1 (\t -> App t) ts

cast = do
  (t1, t2) <- angles $ do
    t1 <- type_
    reservedOp "|>"
    t2 <- type_
    return (t1, t2)

  te <- term1
  return (Cast t1 t2 te)

term1 = choice [try con, try lam, cast, var, parens term]


varOfType = do
  x <- identifier
  reservedOp ":"
  t <- type_
  return (x, t)

fun = do
  (x, t) <- varOfType
  reservedOp "->"
  t' <- fun <|> type_
  return (Fun x t t')

ref = braces $ do
  x <- identifier
  reservedOp ":"
  b <- base
  reservedOp "|"
  t <- term
  return (Ref x b t)

base :: GenParser Char () Base
base = int <|> bool

int :: GenParser Char () Base
int  = reserved "Int"  >> return BInt
bool :: GenParser Char () Base
bool = reserved "Bool" >> return BBool

baseT :: GenParser Char () Type
baseT = do
  b <- base
  return $ Ref "x" b (Con Ctrue)

type_ = choice $ map try [baseT, ref, fun, parens type_]

-- util
many2 :: GenParser tok st t -> GenParser tok st [t]
many2 t = do
  x  <- t
  xs <- many1 t
  return (x:xs)