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

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

import Fmt (Buildable(..), listF, 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)

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

-- | 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
  | UnsupportedTypes [T.T]
  -- ^ Error that happens when type cannot be used in the corresponding scope.
  -- Argument of this constructor carries types which, in the aggregate, violate
  -- the restriction (e.g. @timestamp@ and @timestamp@ passed to @MUL@ instruction).
  | 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
  deriving stock (Show, Eq)

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 |+ ""
    UnsupportedTypes types ->
      "Unsupported types: " +| listF types |+ ""
    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"

-- | Type check error
data TCError
  = TCFailedOnInstr U.ExpandedInstr SomeHST Text InstrCallStack (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)

-- TODO pva701: an instruction position should be used in
-- Buildable instance within TM-151.
instance Buildable TCError where
  build = \case
    TCFailedOnInstr instr (SomeHST t) custom _ mbTCTypeError ->
      "Error checking expression "
      +| instr |+ " against input stack type "
      +| t ||+ bool (": " +| custom |+ " ") "" (null custom)
      +| (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 occured 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)

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

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