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

import Fmt (Buildable(..), pretty, (+|), (|+))
import Prelude hiding (empty, (<$>))
import Text.PrettyPrint.Leijen.Text
  (Doc, cat, enclose, indent, line, list, punctuate, textStrict, (<$$>), (<$>), (<+>))

import Morley.Michelson.ErrorPos (ErrorSrcPos(..))
import Morley.Michelson.Printer.Util
  (RenderDoc(..), buildRenderDoc, buildRenderDocExtended, doesntNeedParens, renderAnyBuildable,
  renderDoc, renderDocList)
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
  | LambdaCode
  | 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 RenderDoc TypeContext where
  renderDoc _ = \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"
    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 = buildRenderDoc

instance RenderDoc TopLevelType where
  renderDoc _ = \case
    TltParameterType -> "parameter"
    TltStorageType -> "storage"

instance Buildable TypeContext where
  build = buildRenderDoc

-- | 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.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 ContractAddress
  -- ^ Contract with given address is not originated.
  | TxRollupContract TxRollupAddress
  -- ^ Provided txr1 address as contract.
  | 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 = buildRenderDocExtended

instance RenderDoc TCTypeError where
  renderDoc context = \case
    TypeEqError merr ->
      "Types not equal:" <$> renderDoc context merr
    StackEqError merr ->
      "Stacks not equal:" <$> renderDoc context merr
    UnsupportedTypeForScope typ reason ->
      "Type '" <> (renderDoc context typ) <> "' is unsupported here because it"
      <+> (renderDoc context reason)
    NotNumericTypes t1 t2 ->
      "Some of the types in an arithmetic operation are not numeric:"
      <+> (renderDoc context t1) <+> "and" <+> (renderDoc context t2)
    UnexpectedType (t :| ts) ->
      "Wrong stack type for instruction, expect stack type to begin with " <+>
        (cat $ punctuate "or"
          $ fmap (\(x :| xs) -> list $ fmap (renderAnyBuildable) (x:xs))
          $ (t:ts)
        )
    UnexpectedTopLevelType tyDesc mmerr ->
      "Unexpected" <+> renderDoc context tyDesc <+> "type."
      <$$> renderDoc doesntNeedParens mmerr
    InvalidInstruction instr reason ->
      "Invalid instruction" <+> (renderDoc context instr)
      <$$> "Reason:" <+> textStrict reason
    InvalidValueType t ->
      "Value type is never a valid" <+> enclose "`" "`" (renderDoc context t)
    NotEnoughItemsOnStack ->
      "Not enough items on stack"
    UnknownContract addr ->
      "Contract is not registered:" <+> (renderAnyBuildable addr)
    TxRollupContract addr ->
      "txr1 address can not be used as a contract:" <+> (renderAnyBuildable addr)
    IllegalEntrypoint err -> renderDoc context err
    EntrypointNotFound ep ->
      "No such entrypoint" <+> enclose "`" "`" (renderAnyBuildable ep)
    IllegalParamDecl err -> renderDoc context err
    NegativeNat -> "Natural number cannot be negative"
    MutezOverflow -> "Exceeds maximal value for mutez"
    InvalidAddress e -> renderDoc context e
    InvalidKeyHash e -> renderDoc context e
    InvalidBls12381Object e -> renderDoc context 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 ->
      "No big_map with ID" <+> renderAnyBuildable bigMapId <+> "was found."
    UnexpectedBigMapType bigMapId mismatchError ->
      "A big_map with the ID" <+> renderAnyBuildable bigMapId <+> "was found, but it does not have the expected type."
      <$$> renderDoc context mismatchError

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

instance NFData TCError

instance Buildable TCError where
  build = buildRenderDocExtended

instance RenderDoc TCError where
  renderDoc context = \case
    TCFailedOnInstr instr (SomeHST t) ics mbTCTypeContext mbTCTypeError -> line
      <> "Error checking expression:"
      <> surroundWithNewLines (renderDoc context instr)
      <> "against input stack type:"
      <> surroundWithNewLines (renderDoc context t)
      <> maybe "" (\c -> "Error in" <+> renderDoc context c) mbTCTypeContext
      <> maybe "" (\e -> ":" <+> (renderDoc context e) <> "." <$$> line) mbTCTypeError
      <> (renderDoc context ics)
    TCFailedOnValue v t custom ics mbTCTypeError ->
      "Error checking value"
      <$$> (renderDoc context v) <+> "against type"
      <+> (renderDoc context t) <> (bool (":" <+> (renderAnyBuildable custom)) "." (null custom))
      <+> (maybe "" (\e -> line <> (renderDoc context e) <> line) mbTCTypeError)
      <+> (renderDoc context ics)
    TCContractError msg typeError ->
      "Error occurred during contract typecheck:"
      <$$> (renderAnyBuildable msg) <> (maybe "" (\e -> " " <> (renderDoc context e)) typeError)
    TCViewError msg viewName typeError ->
      "Error occurred during typecheck of view " <> renderDoc context viewName <> ":"
      <$$> (renderAnyBuildable msg) <> (maybe "" (\e -> " " <> (renderDoc context e)) typeError)
    TCUnreachableCode ics instrs ->
      "Unreachable code:" <$$> buildTruncated 3 (toList instrs) <> "."
      <+> (renderDoc context ics)
    TCExtError (SomeHST t) ics e ->
      "Error occurred during Morley extension typecheck:" <>
      (renderAnyBuildable e) <+> "on stack" <+> (renderDoc context t) <> "."
      <+> (renderDoc context ics)
    TCIncompletelyTyped err contract ->
      line
      <> renderDoc doesntNeedParens contract
      <$> renderDoc context err
    TCIncompletelyTypedView err _view ->
      line
      <> renderDoc context err
    where
    buildTruncated k l
      | null (drop k l) = renderDocList context l
      | otherwise = (renderDocList context (take k l)) <> " ..."

    -- | Helper to format a line using empty lines at the end and at the beginning,
    -- and 4-space indents for the line itself
    surroundWithNewLines :: Doc -> Doc
    surroundWithNewLines l =
      line
      <$$> indent 4 l
      <$$> line

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))