-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

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

module Morley.Michelson.TypeCheck.Error
  ( TypeContext (..)
  , TopLevelType (..)
  , TcTypeError (..)
  , TcError
  , TcError' (..)
  , ExtError (..)
  , StackSize (..)
  , TCOpSeq (..)
  , pairWithNodeIndex
  , pairWithElems
  ) where

import Prelude hiding (empty, (<$>))

import Fmt (Buildable(..), Doc, isEmpty, nameF, pretty, (+|), (<$>), (<+>), (<//>), (</>), (|+))
import Fmt.Utils qualified as PP
import Prettyprinter (flatAlt, hardline)
import Prettyprinter qualified as PP
import Prettyprinter.Util (reflow)

import Morley.Michelson.ErrorPos (ErrorSrcPos(..))
import Morley.Michelson.Printer.Util
import Morley.Michelson.TypeCheck.TypeCheckedOp (TypeCheckedOp)
import Morley.Michelson.TypeCheck.Types (SomeHST(..))
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Untyped qualified as U
import Morley.Tezos.Address
import Morley.Tezos.Crypto (CryptoParseError)
import Morley.Tezos.Crypto.BLS12381 qualified as BLS
import Morley.Util.MismatchError

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

instance Buildable TypeContext where
  build = \case
    LambdaArgument -> "argument to some lambda"
    LambdaCodeCtx -> "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"
    UnpairArgument -> "argument to UNPAIR"
    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"
    TicketsJoin -> "join of two tickets"
    ViewBlock -> "top-level view block"
    EmitArgument -> "argument to EMIT"

data TopLevelType
  = TltParameterType
  | TltStorageType
  deriving stock (Show, Eq, Generic)
  deriving anyclass (NFData)

instance Buildable TopLevelType where
  build = \case
    TltParameterType -> "parameter"
    TltStorageType -> "storage"

-- | 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
  = TypeEqError (MismatchError T.T)
  -- ^ Type equality error
  | StackEqError (MismatchError [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.
  | UnexpectedTopLevelType TopLevelType (MismatchError T.T)
  -- ^ Error that happens when the caller expected one top-level type, but
  -- the contract has another type specified.
  | InvalidInstruction (U.InstrAbstract [] ()) 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.
  --
  -- Since this makes sense only for primitive instructions, we keep
  -- @U.InstrAbstract@ with @()@ type argument.
  | 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 ContractAddress
  -- ^ 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.
  | InvalidBigMapId Integer
  -- ^ A big_map with the given ID was not found.
  | UnexpectedBigMapType
  -- ^ We found a big_map with the given big_map ID, but
  -- its key and/or value types are not the same as the requested types.
      Integer -- ^ The big_map ID we used to lookup a big_map value.
      (MismatchError T.T)
  deriving stock (Show, Eq, Generic)
  deriving anyclass (NFData)

instance Buildable TcTypeError where
  build = \case
    TypeEqError merr -> nameF "Types not equal" $ build merr
    StackEqError merr -> nameF "Stacks not equal" $ build merr
    UnsupportedTypeForScope typ reason -> PP.group
      ("Type" <$>
        let res = build typ in flatAlt (PP.indent 2 res) (PP.squotes res) <> PP.line)
      <//> reflow "is unsupported here because it" </> build reason
    NotNumericTypes t1 t2 ->
      nameF (reflow "Some of the types in an arithmetic operation are not numeric") $
        PP.sep
          [ build t1 <+> "and"
          , build t2
          ]
    UnexpectedType stacks -> "Wrong stack type for instruction."
      </> nameF "Expected stack type to begin with"
        (PP.sep $ PP.punctuate " or" (fmap build $ toList stacks))
    UnexpectedTopLevelType tyDesc mmerr -> nameF
      ("Unexpected" <+> build tyDesc <+> "type")
      (build mmerr)
    InvalidInstruction instr reason -> PP.vsep
      [ nameF "Invalid instruction" $ build (instr $> ("..." :: Text))
      , nameF "Reason" $ build reason
      ]
    InvalidValueType t -> nameF "Value type is never a valid" $ build t
    NotEnoughItemsOnStack -> "Not enough items on stack"
    UnknownContract addr -> nameF "Contract is not registered" $ build addr
    IllegalEntrypoint err -> build err
    EntrypointNotFound ep -> nameF "No such entrypoint" $ build 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) in this block"
    EmptyCode -> "Code block is empty"
    AnyError -> "Some of the arguments have invalid types"
    InvalidBigMapId bigMapId -> PP.nest 2 $
      reflow "No big_map with ID"
      </> build bigMapId
      </> reflow "was found."
    UnexpectedBigMapType bigMapId mismatchError -> PP.nest 2 $ PP.vsep
      [ reflow "A big_map with the ID"
        </> build bigMapId
        </> reflow "was found, but it does not have the expected type."
      , build mismatchError
      ]

instance Exception TcTypeError where
  displayException = pretty

-- | Type check error
data TcError' op
  = TcFailedOnInstr (U.InstrAbstract [] op) SomeHST ErrorSrcPos (Maybe TypeContext) (Maybe TcTypeError)
  | TcFailedOnValue (U.Value' [] op) T.T Text ErrorSrcPos (Maybe TcTypeError)
  | TcContractError Text (Maybe TcTypeError)
  | TcViewError Text U.ViewName (Maybe TcTypeError)
  | TcUnreachableCode ErrorSrcPos (NonEmpty op)
  | TcExtError SomeHST ErrorSrcPos ExtError
  | TcIncompletelyTyped (TcError' op) (U.Contract' (TCOpSeq op))
  | TcIncompletelyTypedView (TcError' op) (U.View' (TCOpSeq op))
  | TcDeprecatedType Text T.T
  deriving stock (Show, Eq, Generic)

-- | Used to smooth out the impedance mismatch between instruction arguments,
-- which must be sequences, and contract/view code which can be a singular
-- instruction. Only used for error reporting, as in general this isn't valid.
newtype TCOpSeq op = TCOpSeq [TypeCheckedOp op]
  deriving newtype (Show, Eq)
  deriving stock (Functor, Generic)
  deriving anyclass NFData

instance RenderDoc op => RenderDoc (TCOpSeq op) where
  renderDoc _ (TCOpSeq ops) = renderOpsListNoBraces False ops

type TcError = TcError' U.ExpandedOp

instance (NFData op, NFData (TypeCheckedOp op)) => NFData (TcError' op)

instance (RenderDoc op, Buildable op) => Buildable (TcError' op) where
  build = \case
    TcFailedOnInstr instr (SomeHST t) ics mbTCTypeContext mbTcTypeError -> PP.vsep
      [ PP.nest 2 $ "Error checking expression:"
          <$> surroundWithNewLines (build instr)
      , PP.nest 2 $ "against input stack type:"
          <$> surroundWithNewLines (build t)
      , nameF
          (maybe mempty (("Error in" <+>) . build) mbTCTypeContext)
          (build mbTcTypeError)
      , build ics
      ]
    TcFailedOnValue v t custom ics mbTcTypeError -> PP.nest 2 $ PP.vsep $ filter (not . isEmpty)
      [ nameF "Error checking value" $ build v
      , nameF "Against type" $ build t
      , build custom
      , build mbTcTypeError
      , build ics
      ]
    TcContractError msg typeError -> nameF "Error occurred during contract typecheck" $
      build msg <$> build typeError
    TcViewError msg viewName typeError -> nameF
      ("Error occurred during typecheck of view " <> build viewName) $
      build msg <$> build typeError
    TcUnreachableCode ics instrs -> nameF "Unreachable code" $
      buildTruncated 3 (toList instrs) <> hardline <> build ics
    TcExtError (SomeHST t) ics e -> nameF
      "Error occurred during Morley extension typecheck" $ PP.vsep
        [ build e
        , "on stack"
        , build t
        , build ics
        ]
    TcIncompletelyTyped err contract ->
      renderDoc doesntNeedParens contract <> PP.linebreak
        <$> build err
    TcIncompletelyTypedView err _view -> build err
    TcDeprecatedType err ty ->
      nameF "Found deprecated type" (renderDoc doesntNeedParens ty)
      <$> renderDoc doesntNeedParens err
    where
      buildTruncated k =
        PP.align . renderOpsListNoBraces False . trunc . fmap (renderDoc doesntNeedParens)
        where
          trunc (splitAt k -> (h, t))
            | null t = h
            | otherwise = h <> ["..."]

      surroundWithNewLines :: Doc -> Doc
      surroundWithNewLines = PP.enclose PP.linebreak PP.linebreak

instance Exception TcError where
  displayException = pretty

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

instance NFData StackSize

instance Buildable StackSize where
  build (StackSize n) = "stack size " +| n |+ ""

-- | Various type errors possible when checking Morley extension commands
data ExtError =
    LengthMismatch U.StackTypePattern
  | TypeMismatch U.StackTypePattern Int TcTypeError
  | StkRestMismatch U.StackTypePattern SomeHST SomeHST TcTypeError
  | TestAssertError Text
  | InvalidStackReference U.StackRef StackSize
  deriving stock (Show, 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 |+ ""
    TypeMismatch stk i e ->
      "TypeMismatch: Pattern " +| stk |+ " 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))