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

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

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

import Michelson.ErrorPos (InstrCallStack)
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 instruction which wants more items on stack
-- than currently present.
data NotEnoughItemsInstr
  = NotEnoughDrop
  | NotEnoughDip
  | NotEnoughDig
  | NotEnoughDug
  deriving stock (Show, Eq, Generic)

instance NFData NotEnoughItemsInstr

instance Buildable NotEnoughItemsInstr where
  build = \case
    NotEnoughDrop -> "DROP"
    NotEnoughDip -> "DIP"
    NotEnoughDig -> "DIG"
    NotEnoughDug -> "DUG"

-- | 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).
  | 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 Word NotEnoughItemsInstr
  -- ^ 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 |+ ""
    InvalidInstruction instr ->
      "Forbidden instruction " +| instr |+ ""
    InvalidValueType t ->
      "Value type is never a valid `" +| t |+ "`"
    NotEnoughItemsOnStack n instr ->
      "Not enough items on stack to " +| instr |+ " " +| n |+ ""
    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
  deriving stock (Eq, Generic)

instance NFData TCError

-- TODO pva701: an instruction position should be used in
-- Buildable instance within TM-151.
instance Buildable TCError where
  build = \case
    TCFailedOnInstr instr (SomeHST t) _ mbTCTypeContext mbTCTypeError ->
      "Error checking expression "
      +| instr |+ " against input stack type "
      +| t |+ maybe "" (\c -> ". Error in " +| c |+ "") mbTCTypeContext
      +| maybe "" (\e -> ": " +| e |+ "") mbTCTypeError
      +| "."
    TCFailedOnValue v t custom _ mbTCTypeError ->
      "Error checking value "
      +| v |+ " against type "
      +| toUType t |+ bool (": " +| custom |+ " ") "" (null custom)
      +| (maybe "" (\e -> " " +| e |+ "") mbTCTypeError)
    TCContractError msg typeError ->
      "Error occured during contract typecheck: "
      +|| msg ||+ (maybe "" (\e -> " " +| e |+ "") typeError)
    TCUnreachableCode _ instrs ->
      "Unreachable code: " +| buildTruncated 3 (toList instrs)
    TCExtError (SomeHST t) _ e ->
      "Error occurred during Morley extension typecheck: "
      +| e |+ " on stack " +| t |+ ""
    where
    buildTruncated k l
      | null (drop k l) = build l
      | otherwise = build (take k l) <> " ..."

instance Buildable U.ExpandedInstr => Show TCError where
  show = pretty

instance Buildable U.ExpandedInstr => 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 ||+ ""