module TypeChecking.Expressions.Utils where

import Data.Bifunctor
import Data.Void

import Syntax
import Syntax.ErrorDoc
import Semantics
import Semantics.Value
import TypeChecking.Context
import TypeChecking.Monad.Warn

data Error = Error { errorType :: ErrorType, errorMsg :: EMsg (Term Syntax) }

instance Eq Error where
    Error e _ == Error e' _ = e == e'

data ErrorType
    = NotInScope
    | Inference
    | TooManyArgs
    | NotEnoughArgs
    | Coverage
    | TypeMismatch
    | Conditions
    | Other
    deriving Eq

data Argument = Argument Int Posn (Maybe Name) | NoArgument Int [Error]

argumentIndex :: Argument -> Int
argumentIndex (Argument k _ _) = k
argumentIndex (NoArgument k _) = k

instance Eq Argument where
    arg == arg' = argumentIndex arg == argumentIndex arg'

notInScope :: Show a => Posn -> String -> a -> Error
notInScope pos s a = Error NotInScope $ emsgLC pos ("Not in scope: " ++ (if null s then "" else s ++ " ") ++ show a) enull

inferErrorMsg :: Posn -> String -> Error
inferErrorMsg pos s = Error Inference $ emsgLC pos ("Cannot infer type of " ++ s) enull

inferExprErrorMsg :: Posn -> Error
inferExprErrorMsg pos = Error Inference $ emsgLC pos "Cannot infer an expressions" enull

inferArgErrorMsg :: Argument -> [Error]
inferArgErrorMsg (Argument k pos mname) = [Error Inference $ emsgLC pos
    ("Cannot infer " ++ nth (k + 1) ++ " argument" ++ maybe "" (\name -> " for " ++ nameToPrefix name) mname) enull]
  where
    nth 1 = "first"
    nth 2 = "second"
    nth 3 = "third"
    nth n = show n ++ "th"
inferArgErrorMsg (NoArgument _ errs) = errs

inferParamsErrorMsg :: Show a => Posn -> a -> Error
inferParamsErrorMsg pos d = Error Inference $ emsgLC pos ("Cannot infer parameters of data constructor " ++ show d) enull

argsErrorMsg :: Posn -> String -> Error
argsErrorMsg pos s = Error TooManyArgs $ emsgLC pos (s ++ " is applied to arguments") enull

expectedArgErrorMsg :: Show a => Posn -> a -> Error
expectedArgErrorMsg lc d = Error NotEnoughArgs $ emsgLC lc ("Expected an argument to " ++ show d) enull

coverageErrorMsg :: Posn -> Maybe [Posn] -> [Error]
coverageErrorMsg pos Nothing = [Error Coverage $ emsgLC pos "Incomplete pattern matching" enull]
coverageErrorMsg _ (Just uc) = map (\pos -> Error Coverage $ emsgLC pos "Unreachable clause" enull) uc

notEnoughArgs :: Show a => Posn -> a -> Error
notEnoughArgs pos a = Error NotEnoughArgs $ emsgLC pos ("Not enough arguments to " ++ show a) enull

tooManyArgs :: Posn -> Error
tooManyArgs pos = Error TooManyArgs $ emsgLC pos "Too many arguments" enull

conditionsErrorMsg :: Posn -> Ctx String f Void a -> ([String], Term Semantics a, Term Semantics a, Term Semantics a) -> Error
conditionsErrorMsg pos ctx (vs, t1, t2, t3) = Error Conditions $ emsgLC pos "Conditions check failed:"
    $  scopeToEDoc ctx vs t1 <+> pretty "equals to" <+> scopeToEDoc ctx vs t2
    $$ pretty "but should be equal to" <+> scopeToEDoc ctx vs t3
  where
    scopeToEDoc :: Ctx String f Void a -> [String] -> Term Semantics a -> EDoc (Term Syntax)
    scopeToEDoc ctx vs t = epretty $ bimap syntax pretty $ apps (vacuous $ abstractTerm ctx t) $ map cvar (ctxVars ctx ++ vs)

prettyOpen :: Ctx String (Type Semantics) Void a -> Term Semantics a -> EDoc (Term Syntax)
prettyOpen ctx term = epretty $ fmap (pretty . either id absurd) $ close ctx (bimap syntax Right term)

checkIsType :: Monad m => Ctx String (Type Semantics) Void a -> Posn -> Term Semantics a -> WarnT [Error] m Sort
checkIsType _ _ (Apply (Semantics _ (Universe k)) _) = return k
checkIsType ctx pos t = throwError [Error TypeMismatch $ emsgLC pos "" $ pretty "Expected type: Type"
                                                                      $$ pretty "Actual type:" <+> prettyOpen ctx t]

termPos :: Term (Posn, s) a -> Posn
termPos (Apply (pos, _) _) = pos
termPos _ = error "termPos"

catchErrorType :: Monad m => [ErrorType] -> WarnT [Error] m a -> ([Error] -> WarnT [Error] m a) -> WarnT [Error] m a
catchErrorType errs = catchErrorBy $ \(Error err _) -> err `elem` errs