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

-- | 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 hiding (bool, pretty)
import qualified Text.Show (show)

import Morley.Michelson.ErrorPos (InstrCallStack(..))
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 qualified Morley.Michelson.Typed as T
import Morley.Michelson.Typed.Annotation (AnnConvergeError(..))
import Morley.Michelson.Untyped (StackFn, Ty, Var)
import qualified Morley.Michelson.Untyped as U
import Morley.Tezos.Address (Address)
import Morley.Tezos.Crypto (CryptoParseError)
import qualified Morley.Tezos.Crypto.BLS12381 as BLS
import Morley.Util.Named

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

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
  = 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.
  | UnexpectedTopLevelType TopLevelType ("expected" :! T.T) ("got" :! 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 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 = buildRenderDocExtended

instance RenderDoc TCTypeError where
  renderDoc context = \case
    AnnError e -> renderAnyBuildable e
    TypeEqError type1 type2 ->
      "Types not equal:" <+> (renderDoc context type1) <+> "/=" <+> (renderDoc context type2)
    StackEqError st1 st2 ->
      "Stacks not equal:"<+> (renderDocList context st1) <+> "/=" <+> (renderDocList context st2)
    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 (N expected) (N got) ->
      "Unexpected" <+> renderDoc context tyDesc <+> "type:"
      <$$> renderLargeType got
      <$$> "Expected:"
      <$$> renderLargeType expected
    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)
    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"
    where
      renderLargeType :: T.T -> Doc
      renderLargeType = indent 2 . renderDoc doesntNeedParens . T.toUType

-- | 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)
  | TCViewError Text U.ViewName (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 = 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
    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 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 Ty 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))