-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | Errors that can occur when some code is being typechecked.

module Michelson.TypeCheck.Error
  ( ExpectType (..)
  , TypeContext (..)
  , TCTypeError (..)
  , TCError (..)
  , ExtError (..)
  , StackSize (..)
  ) where

import Fmt (Buildable(..), listF, pretty, (+|), (+||), (|+), (||+))
import qualified Text.Show (show)

import Michelson.ErrorPos (InstrCallStack(..), Pos(..), SrcPos(..))
import Michelson.Printer.Util (doesntNeedParens, printDocB, renderDoc)
import Michelson.TypeCheck.TypeCheckedOp (TypeCheckedOp)
import Michelson.TypeCheck.Types (SomeHST(..))
import qualified Michelson.Typed as T
import Michelson.Typed.Annotation (AnnConvergeError(..))
import Michelson.Typed.Extract (toUType)
import Michelson.Typed.T (buildStack)
import Michelson.Untyped (StackFn, Type, Var)
import qualified Michelson.Untyped as U
import Tezos.Address (Address)
import Tezos.Crypto (CryptoParseError)

-- | Description of the type to be expected by certain instruction.
data ExpectType
  = ExpectTypeVar
  | ExpectStackVar
  | ExpectBool
  | ExpectInt
  | ExpectNat
  | ExpectByte
  | ExpectString
  | ExpectAddress
  | ExpectKey
  | ExpectKeyHash
  | ExpectSignature
  | ExpectContract
  | ExpectMutez
  | ExpectList (Maybe ExpectType)
  | ExpectSet (Maybe ExpectType)
  | ExpectMap
  | ExpectBigMap
  | ExpectOption (Maybe ExpectType)
  | ExpectPair (Maybe ExpectType)  (Maybe ExpectType)
  | ExpectOr (Maybe ExpectType)  (Maybe ExpectType)
  | ExpectLambda (Maybe ExpectType)  (Maybe ExpectType)
  deriving stock (Show, Eq, Generic)

instance NFData ExpectType

instance Buildable ExpectType where
  build = \case
    ExpectTypeVar -> "'a"
    ExpectStackVar -> "'A"
    ExpectBool -> "bool"
    ExpectInt -> "int"
    ExpectNat -> "nat"
    ExpectByte -> "byte"
    ExpectString -> "string"
    ExpectAddress -> "address"
    ExpectKey -> "key"
    ExpectKeyHash -> "key_hash"
    ExpectSignature -> "signature"
    ExpectMutez -> "mutez"
    ExpectContract -> "contract 'p"
    ExpectList expType ->
      "list "
        +| maybe "'a" build expType
    ExpectSet expType ->
      "set "
        +| maybe "'a" build expType
    ExpectMap -> "map 'key 'val"
    ExpectBigMap -> "big_map 'key 'val"
    ExpectOption expType ->
      "option "
        +| maybe "'a" build expType
    ExpectPair expType1 expType2 ->
      "pair "
        +| (maybe "'a" build expType1) +| " "
        +| (maybe "'b" build expType2) +| ""
    ExpectOr expType1 expType2 ->
      "or "
        +| (maybe "'a" build expType1) +| " "
        +| (maybe "'b" build expType2) +| ""
    ExpectLambda expType1 expType2 ->
      "lambda "
        +| (maybe "'a"
            (\case
              ExpectPair a b -> "(" +| ExpectPair a b |+ ")" -- bracket is needed for APPLY
              x -> build x
            ) expType1
           ) +| " "
        +| (maybe "'b" build expType2) +| ""

-- | Contexts where type error can occur.
data TypeContext
  = LambdaArgument
  | LambdaCode
  | DipCode
  | ConsArgument
  | ComparisonArguments
  | ContractParameter
  | ContractStorage
  | ArithmeticOperation
  | Iteration
  | Cast
  | CarArgument
  | CdrArgument
  | If
  | ConcatArgument
  | ContainerKeyType
  | ContainerValueType
  deriving stock (Show, Eq, Generic)
  deriving anyclass (NFData)

instance Buildable TypeContext where
  build = \case
    LambdaArgument -> "argument to some lambda"
    LambdaCode -> "code in LAMBDA"
    DipCode -> "code in DIP"
    ConsArgument -> "argument to CONS"
    ComparisonArguments -> "arguments to comparison function"
    ContractParameter -> "contract parameter"
    ContractStorage -> "contract storage"
    ArithmeticOperation -> "arguments to arithmetic operation"
    Iteration -> "iteration (ITER / MAP / etc) code"
    Cast -> "argument to CAST"
    CarArgument -> "argument to CAR"
    CdrArgument -> "argument to CDR"
    If -> "conditional expression"
    ConcatArgument -> "argument to CONCAT"
    ContainerKeyType -> "container key type"
    ContainerValueType -> "container value type"

-- | Data type that represents various errors
-- which are related to type system.
-- These errors are used to specify info about type check errors
-- in @TCError@ data type.
data TCTypeError
  = AnnError AnnConvergeError
  -- ^ Annotation unify error
  | TypeEqError T.T T.T
  -- ^ Type equality error
  | StackEqError [T.T] [T.T]
  -- ^ Stacks equality error
  | UnsupportedTypeForScope T.T T.BadTypeForScope
  -- ^ Error that happens when type cannot be used in the corresponding scope.
  -- Argument of this constructor carries type which violates
  -- the restriction, e.g. @big_map@ in @UNPACK@, and a concrete reason why the
  -- type is unsuported.
  | NotNumericTypes T.T T.T
  -- ^ Arithmetic operation is applied to types, at least one of which is not numeric
  -- (e.g. @timestamp@ and @timestamp@ passed to @MUL@ instruction).
  | UnexpectedType (NonEmpty (NonEmpty ExpectType))
  -- ^ Error that happens when actual types are different from the type that instruction expects.
  -- The param is an non-empty list of all expected stack types that the instruction would accept.
  -- Each expected stack types is represented as non-empty list as well.
  | InvalidInstruction U.ExpandedInstr
  -- ^ Some instruction can not be used in a specific context, like @SELF@ in @LAMBDA@.
  | InvalidValueType T.T
  -- ^ Error that happens when a `U.Value` is never a valid source for this type
  -- (e.g. @timestamp@ cannot be obtained from a `U.ValueTrue`)
  | NotEnoughItemsOnStack
  -- ^ There are not enough items on stack to perform a certain instruction.
  | IllegalEntrypoint T.EpNameFromRefAnnError
  -- ^ Invalid entrypoint name provided
  | UnknownContract Address
  -- ^ Contract with given address is not originated.
  | EntrypointNotFound T.EpName
  -- ^ Given entrypoint is not present.
  | IllegalParamDecl T.ParamEpError
  -- ^ Incorrect parameter declaration (with respect to entrypoints feature).
  | NegativeNat
  -- ^ Natural numbers cannot be negative
  | MutezOverflow
  -- ^ Exceeds the maximal mutez value
  | InvalidAddress T.ParseEpAddressError
  -- ^ Address couldn't be parsed from its textual representation
  | InvalidKeyHash CryptoParseError
  -- ^ KeyHash couldn't be parsed from its textual representation
  | InvalidTimestamp
  -- ^ Timestamp is not RFC339 compliant
  | CodeAlwaysFails
  -- ^ Code always fails, but shouldn't, like ITER body.
  | EmptyCode
  -- ^ Empty block of code, like ITER body.
  | AnyError
  -- ^ Generic error when instruction does not match something sensible.
  deriving stock (Show, Eq, Generic)
  deriving anyclass (NFData)

instance Buildable TCTypeError where
  build = \case
    AnnError e -> build e
    TypeEqError type1 type2 ->
      "Types not equal: " +| type1 |+ " /= " +| type2 |+ ""
    StackEqError st1 st2 ->
      "Stacks not equal: " +| buildStack st1 |+ " /= " +| buildStack st2 |+ ""
    UnsupportedTypeForScope typ reason ->
      "Type '" +| typ |+ "' is unsupported here because it "
      +| reason |+ ""
    NotNumericTypes t1 t2 ->
      "Some of the types in an arithmetic operation are not numeric: "
      +| t1 |+ " and " +| t2 |+ ""
    UnexpectedType (t :| ts) ->
      "Wrong stack type for instruction, expect stack type to begin with " +|
        ( intercalate " or "
          $ fmap (\(x :| xs) -> "" +| listF (x:xs) |+ "")
          $ (t:ts)
        ) |+ ""
    InvalidInstruction instr ->
      "Forbidden instruction " +| instr |+ ""
    InvalidValueType t ->
      "Value type is never a valid `" +| t |+ "`"
    NotEnoughItemsOnStack ->
      "Not enough items on stack"
    UnknownContract addr ->
      "Contract is not registered: " +| addr |+ ""
    IllegalEntrypoint err -> build err
    EntrypointNotFound ep ->
      "No such entrypoint '" +| ep |+ "'"
    IllegalParamDecl err -> build err
    NegativeNat -> "Natural number cannot be negative"
    MutezOverflow -> "Exceeds maximal value for mutez"
    InvalidAddress e -> build e
    InvalidKeyHash e -> build e
    InvalidTimestamp -> "Is not a valid RFC3339 timestamp"
    CodeAlwaysFails -> "Code always fails, but is not supposed to"
    EmptyCode -> "Code block is empty"
    AnyError -> "Some of the arguments have invalid types"

-- | Type check error
data TCError
  = TCFailedOnInstr U.ExpandedInstr SomeHST InstrCallStack (Maybe TypeContext) (Maybe TCTypeError)
  | TCFailedOnValue U.Value T.T Text InstrCallStack (Maybe TCTypeError)
  | TCContractError Text (Maybe TCTypeError)
  | TCUnreachableCode InstrCallStack (NonEmpty U.ExpandedOp)
  | TCExtError SomeHST InstrCallStack ExtError
  | TCIncompletelyTyped TCError (U.Contract' TypeCheckedOp)
  deriving stock (Eq, Generic)

instance NFData TCError

instance Buildable TCError where
  build = \case
    TCFailedOnInstr instr (SomeHST t) ics mbTCTypeContext mbTCTypeError ->
      "Error checking expression "
      +| instr |+ " against input stack type "
      +| t |+ maybe "" (\c -> ". Error in " +| c |+ "") mbTCTypeContext
      +| maybe ". " (\e -> ": " +| e |+ ". ") mbTCTypeError
      +| buildCallStack ics
    TCFailedOnValue v t custom ics mbTCTypeError ->
      "Error checking value "
      +| v |+ " against type "
      +| toUType t |+ bool (": " +| custom |+ " ") "." (null custom)
      +| (maybe "" (\e -> "\n" +| e |+ ".\n") mbTCTypeError)
      +| buildCallStack ics
    TCContractError msg typeError ->
      "Error occured during contract typecheck: "
      +|| msg ||+ (maybe "" (\e -> " " +| e |+ "") typeError)
    TCUnreachableCode ics instrs ->
      "Unreachable code: " +| buildTruncated 3 (toList instrs) |+ ". "
      +| buildCallStack ics
    TCExtError (SomeHST t) ics e ->
      "Error occurred during Morley extension typecheck: "
      +| e |+ " on stack " +| t |+ ". "
      +| buildCallStack ics
    TCIncompletelyTyped err contract ->
      "\n"
      +| printDocB False (renderDoc doesntNeedParens contract) |+ "\n"
      +| build err
    where
    buildTruncated k l
      | null (drop k l) = build l
      | otherwise = build (take k l) <> " ..."
    buildCallStack InstrCallStack{icsCallStack, icsSrcPos = SrcPos (Pos line) (Pos col)} =
      "Error occured on line " +| line + 1 |+ " char " +| col + 1 |+ ""
      +| case icsCallStack of
           [] -> "."
           _ -> " inside these let defenitions: " +| listF icsCallStack |+ "."

instance Show TCError where
  show = pretty

instance Exception TCError

newtype StackSize = StackSize Natural
  deriving stock (Show, Eq, Generic)

instance NFData StackSize

-- | Various type errors possible when checking Morley extension commands
data ExtError =
    LengthMismatch U.StackTypePattern
  | VarError Text StackFn
  | TypeMismatch U.StackTypePattern Int TCTypeError
  | TyVarMismatch Var Type U.StackTypePattern Int TCTypeError
  | StkRestMismatch U.StackTypePattern SomeHST SomeHST TCTypeError
  | TestAssertError Text
  | InvalidStackReference U.StackRef StackSize
  deriving stock (Eq, Generic)

instance NFData ExtError

instance Buildable ExtError where
  build = \case
    LengthMismatch stk ->
      "Unexpected length of stack: pattern "
      +| stk |+ " has length "
      +| (length . fst . U.stackTypePatternToList) stk |+ ""
    VarError t sf ->
      "In defenition of " +| t |+ ": VarError "
      +| sf |+ ""
    TypeMismatch stk i e ->
      "TypeMismatch: Pattern " +| stk |+ " at index "
      +| i |+ " with error: " +| e |+ ""
    TyVarMismatch v t stk i e ->
      "TyVarMismach: Variable " +| v |+ " is bound to type "
      +| t |+ " but pattern " +| stk |+ " failed at index "
      +| i |+ " with error: " +| e |+ ""
    StkRestMismatch stk (SomeHST r) (SomeHST r') e ->
      "StkRestMismatch in pattern " +| stk |+
      " against stacks " +| r ||+ " and " +| r' ||+
      " with error: " +| e |+ ""
    TestAssertError t ->
      "TestAssertError: " +| t |+ ""
    InvalidStackReference i lhs ->
      "InvalidStackReference: reference is out of the stack: "
      +| i ||+ " >= " +| lhs ||+ ""