-- 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
  ( TypeContext (..)
  , TCTypeError (..)
  , TCError (..)
  , ExtError (..)
  , StackSize (..)
  , pairWithNodeIndex
  , pairWithElems
  ) where

import Fmt (Buildable(..), listF, pretty, unlinesF, (+|), (+||), (|+), (||+))
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)
import qualified Tezos.Crypto.BLS12381 as BLS

-- | Contexts where type error can occur.
data TypeContext
  = LambdaArgument
  | LambdaCode
  | DipCode
  | ConsArgument
  | ComparisonArguments
  | ContractParameter
  | ContractStorage
  | ArithmeticOperation
  | Iteration
  | Cast
  | CarArgument
  | CdrArgument
  | If
  | ConcatArgument
  | ContainerKeyType
  | ContainerValueType
  | FailwithArgument
  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"
    FailwithArgument -> "argument to FAILWITH"

-- | 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 Text))
  -- ^ 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 Text
  -- ^ Some instruction is invalid or used in an invalid way.
  -- For example, @PAIR 0@ or @PAIR 1@, or a @SELF@ instruction was used in a @LAMBDA@.
  -- The 'Text' argument is a user-readable explanation of why this instruction is invalid.
  | 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
  | InvalidBls12381Object BLS.DeserializationError
  -- ^ BLS12-381 primitive couldn't be parsed
  | InvalidTimestamp
  -- ^ Timestamp is not RFC339 compliant
  | CodeAlwaysFails
  -- ^ Code always fails, but shouldn't, like in ITER body.
  -- This is actually more general, any instruction that allows no continuation
  -- (like @NEVER@) cannot appear as part of another instruction's 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 reason -> unlinesF
      [ "Invalid instruction " +| instr |+ ""
      , "Reason: " <> reason
      ]
    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
    InvalidBls12381Object e -> build e
    InvalidTimestamp -> "Is not a valid RFC3339 timestamp"
    CodeAlwaysFails ->
      "Cannot use a terminate instruction (like FAILWITH) as part of another \
      \instruction's body"
    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 occurred 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 occurred 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 ||+ ""

----------------------------------------------------------------------------
-- Helpers for formatting types
----------------------------------------------------------------------------

-- | Given a node index @ix@, creates a string representing the
-- smallest possible right-combed pair with at least @ix+1@ nodes.
--
-- Since the node index 0 is valid even for non-pair values
-- (e.g. we can run @GET 0@ on a @string@ or an @int@),
-- we simply return a type variable @'a@ in this case.
--
-- >>> pairWithNodeIndex 0
-- "'a"
--
-- >>> pairWithNodeIndex 4
-- "pair 'a1 'a2 'a3"
--
-- >>> pairWithNodeIndex 5
-- "pair 'a1 'a2 'a3 'a4"
pairWithNodeIndex :: Word -> Text
pairWithNodeIndex = \case
  0 -> "'a"
  ix -> pairWithElems (minPairLength ix)
  where
    -- | Given a node index @ix@, calculates the minimum number of
    -- elements a pair must have for that index to be valid.
    minPairLength :: Word -> Word
    minPairLength = \case
      0 -> 2
      ix -> (ix + 3) `div` 2

-- | Given a number @n@, creates a string representing a
-- right-combed pair of arity @n@.
--
-- > pairType 3 == "pair 'a1 'a2 'a3"
pairWithElems :: Word -> Text
pairWithElems n =
  "pair "
  <> mconcat (intersperse " " ([1 .. n] <&> \i -> "'a" <> show i))