{-  CAO Compiler
    Copyright (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>. -}

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}

{- |
Module      :  $Header$
Description :  Functions to handle errors and warnings.
Copyright   :  (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
License     :  GPL

Maintainer  :  Paulo Silva <paufil@di.uminho.pt>
Stability   :  experimental
Portability :  non-portable

This module provides error and warning messages, as well as functions to
throw errors.

-}

module Language.CAO.Common.Error 
    ( mkCaoWarningInfo
    , WarningCode(..)
    , CaoWarning
    , mkCaoWarning
    , CaoError
    , mkCaoError
    , ParserException(..)
    , ErrorCode(..)
    , TypeMismatchException(..)
    , DeclException(..)
    , CardinalityException(..)
    , AssignmentKind(..)
    , ScopeKind(..)
    , TypeKind(..)
    , showCaoError
    , showCaoWarnings
    , noWarning
    , mkUnknownErr
    ) where

import Text.Read
import Control.Monad.Error
import Control.Monad.Writer

import Language.CAO.Index
import Language.CAO.Type

import Language.CAO.Common.Outputable ( PP, showPpr )
import Language.CAO.Common.Polynomial
import Language.CAO.Common.SrcLoc
import Language.CAO.Common.Utils
import Language.CAO.Common.Var

-- CaoWarning ------------------------------------------------------------------

data WarningInfo = forall id . PP id 
                 => WarningInfo !SrcLoc !String !(WarningCode id)

mkCaoWarningInfo :: PP id => SrcLoc -> String -> WarningCode id -> WarningInfo
mkCaoWarningInfo = WarningInfo

data WarningCode id =
      BaseExtensionWarn !(Pol id)
    | PolExtensionWarn !(Pol id)
    -- | Warnings for transformations/optimizations
    | IndistFail id id
    | DeadCodeReturn
    | NoProverWarning (ICond id)

showWarningCode :: PP id => WarningCode id -> String
showWarningCode warn = case warn of
    BaseExtensionWarn b -> 
        "Base `" ++ showPpr b ++ "' must be a prime number"
    PolExtensionWarn p  -> 
        "Polynomial `" ++ showPpr p ++ "' must be irreducible"
    IndistFail i1 i2    -> 
        "Could not apply side-channel countermeasures: `" 
            ++ showPpr i1 ++ ", " ++ showPpr i2
    DeadCodeReturn ->
        "Removing dead code after return"
    NoProverWarning c -> 
        "Yices prover not available. The following restriction was admitted without proof:\n" ++ showPpr c

newtype CaoWarning = CaoWarning [WarningInfo]

mkCaoWarning :: WarningInfo -> CaoWarning
mkCaoWarning i = CaoWarning [i]

instance Monoid CaoWarning where
    mempty = CaoWarning []
    (CaoWarning l) `mappend` (CaoWarning l') = CaoWarning $! l `mappend` l'

showWarningInfo :: WarningInfo -> String
showWarningInfo (WarningInfo sl fln w) =
    fln ++ ":" ++ showPpr sl ++ ":\n" ++
        nestStr 4 ("[Warning] " ++ showWarningCode w)

showCaoWarnings :: CaoWarning -> String
showCaoWarnings (CaoWarning l) = unlines $ map showWarningInfo l

noWarning :: CaoWarning -> Bool
noWarning (CaoWarning w) = null w

-- CaoError --------------------------------------------------------------------

data CaoError = forall id . (Show id, Read id, PP id) 
              => CaoError SrcLoc String (ErrorCode id)

instance Show CaoError where
    show (CaoError loc s e) = 
        "CaoError " ++ '(': show loc ++ ") " ++ show s ++ " (" ++ show e ++ ")"

instance Read CaoError where
    readsPrec i s = case [ x | (x,"") <- readPrec_to_S (readAsT errcds) i s ] of
                      []    -> []
                      (x:_) -> [(x, "")]

errcds :: (String, (Name, (Var, ())))
errcds = undefined

class ReadAsT t e where
    readAsT :: t -> ReadPrec e

instance ReadAsT () e where
    readAsT ~() = mzero

instance (Read t, Show t, PP t, ReadAsT ts CaoError)
      => ReadAsT (t,ts) CaoError where
    readAsT ~(t,ts)
        = goR t `mplus` readAsT ts
        where 
        goR :: t -> ReadPrec CaoError
        goR _ = prec 5 $ do
            Ident "CaoError" <- lexP
            l  <- parens $ step readPrec
            s  <- step readPrec
            cd <- parens $ step readPrec
            return $ CaoError l s (cd :: ErrorCode t)

mkCaoError 
    :: (Show id, Read id, PP id) 
    => SrcLoc -> String -> ErrorCode id 
    -> CaoError
mkCaoError = CaoError

instance Error CaoError where
    noMsg       = CaoError defSrcLoc "<unknown>" 
        ((UnknownErr "noMsg")::ErrorCode String)
    strMsg mstr = CaoError defSrcLoc "<unknonw>" 
        ((UnknownErr mstr)::ErrorCode String)

showCaoError :: CaoError -> String
showCaoError (CaoError sl fln e) =
    fln ++ ":" ++ showPpr sl ++ ":\n" ++ nestStr 4 (showErrorCode e)

-- Error Messages --------------------------------------------------------------

data ErrorCode id 
    = IntEvalErr
    | TimesMatrixErr
    | PowerMatrixErr
    | FuncReturnErr
    | SeqRangeErr
    | LiteralModErr (Mon id) (Type id)
    | UnknownLiteralErr (Mon id)
    | PolynomialErr (Pol id)
    | ExpressionErr id
    | NotDefinedCodeErr
    | UnknownErr String
    | MultipleErr [CaoError]
    | StrictModeErr

    | ContainerInitErr

    | NestedModpolErr (Type id)
    | NotSupportedTypeErr (Type id)
    | NotSupportedOp String (Type id)
    | NotSupportedVar String (Type id)

    -- XXX: Not supported is not the best name....
    | NotSupportedIndexTyp
    | NotSupportedIndexOp
    | NotSupportedIndexLit

    | ParserException ParserException
    | ScopeException id ScopeKind 
    | BadUseException id ScopeKind
    | TypeMismatchException (Type id) (Type id) TypeMismatchException
    | WrongTypeException (Type id) TypeKind
    | SemanticException SemanticException
    | DeclException (DeclException id)
    | RangeException TypeKind
    | CardinalityException CardinalityException
    deriving (Show, Read)

data TypeMismatchException
    = CastException
    | MatchException
    | UnificationException
    deriving (Show, Read)

data ScopeKind
    = GenericScope
    | IndScope
    | VarScope
    | TypeScope
    | ProcScope
    | FuncScope
    | IndetScope
    | SFieldScope Name
    deriving (Show, Read)

data TypeKind
    = AlgebraicType
    | ModType
    | IntOrModType
    | BitsType
    | BitsOrVectorType
    | VectorType
    | MatrixType
    | StructType
    deriving (Show, Read)

data SemanticException
    = DivByZeroException
    | ModDivException
    | RemByZeroException
    | NegativeExponentException
    | VectorAccessException
    | MatrixRowAccessException
    | MatrixColAccessException
    deriving (Show, Read)

data ParserException 
    = LexicalException String
    | ParsingException String 
    | EOFException
    deriving (Show, Read)

data DeclException id
    = SizeDeclException (IExpr id) (Maybe (IExpr id)) TypeKind
    | BaseDeclException (IExpr id)
    | MultipleDeclException id
    deriving (Show, Read)

data CardinalityException
    = AssignCardinalityException AssignmentKind
    | ParamsCardinalityException
    | InitCardinalityException TypeKind
    deriving (Show, Read)

data AssignmentKind
    = MultipleAssign
    | TupleAssign
    deriving (Show, Read)

mkUnknownErr :: String -> ErrorCode String
mkUnknownErr = UnknownErr

showErrorCode :: PP id => ErrorCode id -> String
showErrorCode err = case err of
    IntEvalErr -> 
        "Expression could not be evaluated during compilation"
    TimesMatrixErr ->
        "Multiplication only is possible if the number of columns of left matrix\n" ++
        "    is the same as the number of rows of right matrix"
    PowerMatrixErr -> 
        "Exponentiation only is possible on square matrices"
    FuncReturnErr -> 
        "Function must return a value"
    SeqRangeErr -> 
        "Invalid bounds or stepping distance in seq statement"
    LiteralModErr lit t ->
        "Literal `[" ++ showPpr lit ++ "]' is not a valid literal of type `" ++
            showPpr t ++ "'"
    UnknownLiteralErr lit -> 
        "Literal `[" ++ showPpr lit ++ "]' has unknown type"
    PolynomialErr pol ->
        "Polynomial literal `[" ++ showPpr pol ++ "]' is not in canonical form"
    ExpressionErr cmd -> 
        "Not an expression: `" ++ showPpr cmd ++ "'"
    NotDefinedCodeErr -> 
        "The specification of the current platform does not define type codes"
    UnknownErr str -> 
        "Unexpected error occurred:\n" ++ str
    MultipleErr lst -> 
        unlines $ map showCaoError lst
    StrictModeErr -> 
        "Unexpected declaration on non dependent type checking mode"

    NotSupportedIndexTyp -> 
        "Not valid index type"
    NotSupportedIndexOp -> 
        "Not supported operations on indexes"
    NotSupportedIndexLit -> 
        "Not supported index literal"

    ContainerInitErr ->
        "Initialization with multiple values only is possible for container types"

    NestedModpolErr t -> 
        "Translation does not support nested polynomial extensions:\n\t`" ++ 
            showPpr t ++ "'"
    NotSupportedTypeErr t -> 
        "Translation for the current platform does not support the type:\n\t`" ++
            showPpr t ++ "'"
    NotSupportedOp op t -> 
        "Translation for the current platform does not support the operation `" 
        ++ op ++ "' for type:\n\t`" ++ showPpr t ++ "'"
    NotSupportedVar op t -> 
        "Translation for the current platform does not support variables of type `" 
        ++ showPpr t ++ "' in operation `" ++ op 
        ++ "'. Only constants are allowed."


    ParserException k -> showParserException k
    ScopeException a k  -> showScopeException a k
    BadUseException a k -> showBadUseException a k
    TypeMismatchException t1 t2 k -> showTypeMismatchException t1 t2 k
    WrongTypeException t k -> showWrongTypeException t k
    SemanticException k -> showSemanticException k
    DeclException e -> showDeclException e
    RangeException k -> showRangeException k
    CardinalityException e -> showCardinalityException e

showParserException :: ParserException -> String
showParserException k = case k of
    LexicalException s -> 
        "Lexical error at character '" ++ s ++ "'"
    ParsingException tok -> 
        "Parse error on input `" ++ tok ++ "'"
    EOFException  -> 
        "Parse error at end of input"

showScopeKind :: ScopeKind -> String
showScopeKind k = case k of
    GenericScope  -> ""
    VarScope      -> "variable"
    IndScope      -> "index"
    FuncScope     -> "function"
    ProcScope     -> "procedure"
    TypeScope     -> "type or struct"
    IndetScope    -> "indeterminate"
    SFieldScope s -> "field of struct `" ++ showPpr s ++ "'"
    
showTypeMismatchException :: PP id => Type id -> Type id -> TypeMismatchException -> String
showTypeMismatchException it et kind = case kind of
    CastException -> 
        "Couldn't cast inferred type `" ++ showPpr it ++ "'\n" ++
        "            to casting type `" ++ showPpr et ++ "'"
    MatchException -> 
        "Couldn't match expected type `" ++ showPpr et ++ "'\n" ++
        "       against inferred type `" ++ showPpr it ++ "'"
    UnificationException -> 
        "Couldn't unify type `" ++ showPpr it ++ "'\n" ++
        "          with type `" ++ showPpr et ++ "'"

showScopeException :: PP id => id -> ScopeKind -> String
showScopeException v kind = "Symbol not found in current scope: " 
    ++ showScopeKind kind ++ " `" ++ showPpr v ++ "'"

showBadUseException :: PP id => id -> ScopeKind -> String
showBadUseException v kind = 
    "Bad use of " ++ showScopeKind kind ++ " `" ++ showPpr v ++ "'"

showWrongTypeException :: PP id => Type id -> TypeKind -> String
showWrongTypeException t kind = 
    "Couldn't match expected " ++ showTypeKind kind ++ " type\n" ++
    "       against inferred type `" ++ showPpr t ++ "'"

showTypeKind :: TypeKind -> String
showTypeKind k = case k of
    AlgebraicType    -> "algebraic"
    ModType          -> "mod"
    IntOrModType     -> "int or mod"
    BitsType         -> "bits"
    BitsOrVectorType -> "bits or vector"
    VectorType       -> "vector"
    MatrixType       -> "matrix"
    StructType       -> "struct"

showSemanticException :: SemanticException -> String
showSemanticException k = case k of
    VectorAccessException -> 
        "Invalid index in vector selection"
    MatrixRowAccessException -> 
        "Invalid row index in matrix selection"
    MatrixColAccessException -> 
        "Invalid column index in matrix selection"
    DivByZeroException -> 
        "Invalid division by zero"
    NegativeExponentException -> 
        "Negative exponent"
    ModDivException -> 
        "Invalid mod division"
    RemByZeroException -> 
        "Invalid remainder by zero"

showDeclException :: PP id => DeclException id -> String
showDeclException e = case e of
    SizeDeclException i mi k -> 
        "Invalid size [" ++
            showPpr i ++ maybe "" ((", " ++) . showPpr) mi ++ 
            "] in " ++ showTypeKind k ++ " type declaration"
    BaseDeclException i ->
        "Invalid modulus `" ++ showPpr i ++ "' in mod type declaration"
    MultipleDeclException v ->
        "Multiple declarations of `" ++ showPpr v ++ "'"

showRangeException :: TypeKind -> String
showRangeException kind =
    "Invalid range in " ++ showTypeKind kind ++ " selection"

showCardinalityException :: CardinalityException -> String
showCardinalityException e = case e of
    AssignCardinalityException k ->
        "The number of left values does not match the number of right " ++ showAssignmentKind k
    ParamsCardinalityException -> 
        "Invalid number of parameters"
    InitCardinalityException k ->
        "Initialization doesn't match " ++ showTypeKind k ++ "dimension"
    where
    showAssignmentKind k = case k of
        MultipleAssign -> "expresions"
        TupleAssign -> " values returned by the function"