module Type where

import qualified Term
import Term ( Term(Node), Identifier(Identifier) )
import IO ( Input, input )

import qualified Text.ParserCombinators.Parsec.Token as T
import qualified Text.ParserCombinators.Parsec.Language as L
import qualified Text.ParserCombinators.Parsec.Expr as Expr
import qualified Text.ParserCombinators.Parsec as Parsec
import Text.ParserCombinators.Parsec
           ( CharParser, Parser, (<|>), (<?>), )
import Text.ParserCombinators.Parsec.Expr
           ( Assoc(AssocRight) )

import Control.Monad.Exception.Synchronous ( Exceptional(Success,Exception) )
import Control.Monad ( liftM2 )


lexer :: T.TokenParser st
lexer =
   T.makeTokenParser $ L.emptyDef {
      L.commentStart = "{-",
      L.commentEnd = "-}",
      L.commentLine = "--",
      L.nestedComments = True,
      L.identStart = Term.identifierStart,
      L.identLetter = Term.identifierLetter,
      L.opStart = operatorStart,
      L.opLetter = operatorLetter,
      L.caseSensitive = True,
      L.reservedNames = [ "forall" ],
      L.reservedOpNames = [ "=", "::", "|" ]
      }


operators :: [[([Char], Assoc)]]
operators =
  [ [ ( "->", AssocRight ) ]
--  , [ ( ",", AssocRight) ]
  ]


parseBracket :: Parser Term
parseBracket = T.lexeme lexer $ do
    (rng,term) <-
        Term.ranged $
        Parsec.between (T.symbol lexer "[") (Parsec.char ']') parseExpression
    return (Node (Identifier { Term.name = "[]", Term.range = rng }) [term])

parseAtom :: Parser Term
parseAtom =
        T.parens lexer parseExpression
    <|> parseBracket
    <|> fmap (flip Node []) input

parseApply :: Parser Term
parseApply = do
    t <- liftM2 Term.appendArguments parseAtom $ Parsec.many parseAtom
    case t of
        Success t' -> return t'
        Exception e -> fail e


operatorStart, operatorLetter :: CharParser st Char
operatorStart  = Parsec.oneOf operatorSymbols
operatorLetter = Parsec.oneOf operatorSymbols

operatorSymbols :: [Char]
operatorSymbols = ":->"

table :: Expr.OperatorTable Char st Term
table = map ( map binary ) operators

binary :: (String, Assoc) -> Expr.Operator Char st Term
binary (s, assoc) = flip Expr.Infix assoc $ do
    rng <- Parsec.try $ T.lexeme lexer $ do
        (rng,_) <- Term.ranged $ Parsec.string s
        Parsec.notFollowedBy operatorLetter <?> ("end of " ++ show s)
        return rng
    return $ \ l r -> Node ( Identifier { Term.name = s, Term.range = rng } ) [ l, r ]


parseContext :: Parsec.GenParser Char () [Term]
parseContext = do
    constraints <-
        T.parens lexer $
            T.commaSep lexer input
    T.reservedOp lexer "=>"
    return constraints

parseExpression :: Parsec.GenParser Char () Term
parseExpression =
    Expr.buildExpressionParser table parseApply