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

import Fmt (Buildable(..), listF, pretty, (+|), (+||), (|+), (||+))
import qualified Text.Show (show)

import Michelson.ErrorPos (InstrCallStack(..), Pos(..), SrcPos(..))
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 type to be expected by certain instruction.
data ExpectType
  = ExpectTypeVar
  | ExpectStackVar
  | ExpectBool
  | ExpectInt
  | ExpectNat
  | ExpectByte
  | ExpectString
  | ExpectAddress
  | ExpectKey
  | ExpectKeyHash
  | ExpectSignature
  | ExpectContract
  | ExpectMutez
  | ExpectList (Maybe ExpectType)
  | ExpectSet (Maybe ExpectType)
  | ExpectMap
  | ExpectBigMap
  | ExpectOption (Maybe ExpectType)
  | ExpectPair (Maybe ExpectType)  (Maybe ExpectType)
  | ExpectOr (Maybe ExpectType)  (Maybe ExpectType)
  | ExpectLambda (Maybe ExpectType)  (Maybe ExpectType)
  deriving stock (Int -> ExpectType -> ShowS
[ExpectType] -> ShowS
ExpectType -> String
(Int -> ExpectType -> ShowS)
-> (ExpectType -> String)
-> ([ExpectType] -> ShowS)
-> Show ExpectType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExpectType] -> ShowS
$cshowList :: [ExpectType] -> ShowS
show :: ExpectType -> String
$cshow :: ExpectType -> String
showsPrec :: Int -> ExpectType -> ShowS
$cshowsPrec :: Int -> ExpectType -> ShowS
Show, ExpectType -> ExpectType -> Bool
(ExpectType -> ExpectType -> Bool)
-> (ExpectType -> ExpectType -> Bool) -> Eq ExpectType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExpectType -> ExpectType -> Bool
$c/= :: ExpectType -> ExpectType -> Bool
== :: ExpectType -> ExpectType -> Bool
$c== :: ExpectType -> ExpectType -> Bool
Eq, (forall x. ExpectType -> Rep ExpectType x)
-> (forall x. Rep ExpectType x -> ExpectType) -> Generic ExpectType
forall x. Rep ExpectType x -> ExpectType
forall x. ExpectType -> Rep ExpectType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ExpectType x -> ExpectType
$cfrom :: forall x. ExpectType -> Rep ExpectType x
Generic)

instance NFData ExpectType

instance Buildable ExpectType where
  build :: ExpectType -> Builder
build = \case
    ExpectTypeVar -> "'a"
    ExpectStackVar -> "'A"
    ExpectBool -> "bool"
    ExpectInt -> "int"
    ExpectNat -> "nat"
    ExpectByte -> "byte"
    ExpectString -> "string"
    ExpectAddress -> "address"
    ExpectKey -> "key"
    ExpectKeyHash -> "key_hash"
    ExpectSignature -> "signature"
    ExpectMutez -> "mutez"
    ExpectContract -> "contract 'p"
    ExpectList expType :: Maybe ExpectType
expType ->
      "list "
        Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Builder -> (ExpectType -> Builder) -> Maybe ExpectType -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "'a" ExpectType -> Builder
forall p. Buildable p => p -> Builder
build Maybe ExpectType
expType
    ExpectSet expType :: Maybe ExpectType
expType ->
      "set "
        Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Builder -> (ExpectType -> Builder) -> Maybe ExpectType -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "'a" ExpectType -> Builder
forall p. Buildable p => p -> Builder
build Maybe ExpectType
expType
    ExpectMap -> "map 'key 'val"
    ExpectBigMap -> "big_map 'key 'val"
    ExpectOption expType :: Maybe ExpectType
expType ->
      "option "
        Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Builder -> (ExpectType -> Builder) -> Maybe ExpectType -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "'a" ExpectType -> Builder
forall p. Buildable p => p -> Builder
build Maybe ExpectType
expType
    ExpectPair expType1 :: Maybe ExpectType
expType1 expType2 :: Maybe ExpectType
expType2 ->
      "pair "
        Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| (Builder -> (ExpectType -> Builder) -> Maybe ExpectType -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "'a" ExpectType -> Builder
forall p. Buildable p => p -> Builder
build Maybe ExpectType
expType1) Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| " "
        Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| (Builder -> (ExpectType -> Builder) -> Maybe ExpectType -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "'b" ExpectType -> Builder
forall p. Buildable p => p -> Builder
build Maybe ExpectType
expType2) Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| ""
    ExpectOr expType1 :: Maybe ExpectType
expType1 expType2 :: Maybe ExpectType
expType2 ->
      "or "
        Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| (Builder -> (ExpectType -> Builder) -> Maybe ExpectType -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "'a" ExpectType -> Builder
forall p. Buildable p => p -> Builder
build Maybe ExpectType
expType1) Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| " "
        Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| (Builder -> (ExpectType -> Builder) -> Maybe ExpectType -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "'b" ExpectType -> Builder
forall p. Buildable p => p -> Builder
build Maybe ExpectType
expType2) Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| ""
    ExpectLambda expType1 :: Maybe ExpectType
expType1 expType2 :: Maybe ExpectType
expType2 ->
      "lambda "
        Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| (Builder -> (ExpectType -> Builder) -> Maybe ExpectType -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "'a"
            (\case
              ExpectPair a :: Maybe ExpectType
a b :: Maybe ExpectType
b -> "(" Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Maybe ExpectType -> Maybe ExpectType -> ExpectType
ExpectPair Maybe ExpectType
a Maybe ExpectType
b ExpectType -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ")" -- bracket is needed for APPLY
              x :: ExpectType
x -> ExpectType -> Builder
forall p. Buildable p => p -> Builder
build ExpectType
x
            ) Maybe ExpectType
expType1
           ) Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| " "
        Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| (Builder -> (ExpectType -> Builder) -> Maybe ExpectType -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "'b" ExpectType -> Builder
forall p. Buildable p => p -> Builder
build Maybe ExpectType
expType2) Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| ""

-- | Contexts where type error can occur.
data TypeContext
  = LambdaArgument
  | LambdaCode
  | DipCode
  | ConsArgument
  | ComparisonArguments
  | ContractParameter
  | ContractStorage
  | ArithmeticOperation
  | Iteration
  | Cast
  | CarArgument
  | CdrArgument
  | If
  | ConcatArgument
  | ContainerKeyType
  | ContainerValueType
  deriving stock (Int -> TypeContext -> ShowS
[TypeContext] -> ShowS
TypeContext -> String
(Int -> TypeContext -> ShowS)
-> (TypeContext -> String)
-> ([TypeContext] -> ShowS)
-> Show TypeContext
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeContext] -> ShowS
$cshowList :: [TypeContext] -> ShowS
show :: TypeContext -> String
$cshow :: TypeContext -> String
showsPrec :: Int -> TypeContext -> ShowS
$cshowsPrec :: Int -> TypeContext -> ShowS
Show, TypeContext -> TypeContext -> Bool
(TypeContext -> TypeContext -> Bool)
-> (TypeContext -> TypeContext -> Bool) -> Eq TypeContext
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeContext -> TypeContext -> Bool
$c/= :: TypeContext -> TypeContext -> Bool
== :: TypeContext -> TypeContext -> Bool
$c== :: TypeContext -> TypeContext -> Bool
Eq, (forall x. TypeContext -> Rep TypeContext x)
-> (forall x. Rep TypeContext x -> TypeContext)
-> Generic TypeContext
forall x. Rep TypeContext x -> TypeContext
forall x. TypeContext -> Rep TypeContext x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TypeContext x -> TypeContext
$cfrom :: forall x. TypeContext -> Rep TypeContext x
Generic)
  deriving anyclass (TypeContext -> ()
(TypeContext -> ()) -> NFData TypeContext
forall a. (a -> ()) -> NFData a
rnf :: TypeContext -> ()
$crnf :: TypeContext -> ()
NFData)

instance Buildable TypeContext where
  build :: TypeContext -> Builder
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"

-- | 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 ExpectType))
  -- ^ 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
  -- ^ Some instruction can not be used in a specific context, like @SELF@ in @LAMBDA@.
  | 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
  | InvalidTimestamp
  -- ^ Timestamp is not RFC339 compliant
  | CodeAlwaysFails
  -- ^ Code always fails, but shouldn't, like ITER body.
  | EmptyCode
  -- ^ Empty block of code, like ITER body.
  | AnyError
  -- ^ Generic error when instruction does not match something sensible.
  deriving stock (Int -> TCTypeError -> ShowS
[TCTypeError] -> ShowS
TCTypeError -> String
(Int -> TCTypeError -> ShowS)
-> (TCTypeError -> String)
-> ([TCTypeError] -> ShowS)
-> Show TCTypeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TCTypeError] -> ShowS
$cshowList :: [TCTypeError] -> ShowS
show :: TCTypeError -> String
$cshow :: TCTypeError -> String
showsPrec :: Int -> TCTypeError -> ShowS
$cshowsPrec :: Int -> TCTypeError -> ShowS
Show, TCTypeError -> TCTypeError -> Bool
(TCTypeError -> TCTypeError -> Bool)
-> (TCTypeError -> TCTypeError -> Bool) -> Eq TCTypeError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TCTypeError -> TCTypeError -> Bool
$c/= :: TCTypeError -> TCTypeError -> Bool
== :: TCTypeError -> TCTypeError -> Bool
$c== :: TCTypeError -> TCTypeError -> Bool
Eq, (forall x. TCTypeError -> Rep TCTypeError x)
-> (forall x. Rep TCTypeError x -> TCTypeError)
-> Generic TCTypeError
forall x. Rep TCTypeError x -> TCTypeError
forall x. TCTypeError -> Rep TCTypeError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TCTypeError x -> TCTypeError
$cfrom :: forall x. TCTypeError -> Rep TCTypeError x
Generic)
  deriving anyclass (TCTypeError -> ()
(TCTypeError -> ()) -> NFData TCTypeError
forall a. (a -> ()) -> NFData a
rnf :: TCTypeError -> ()
$crnf :: TCTypeError -> ()
NFData)

instance Buildable TCTypeError where
  build :: TCTypeError -> Builder
build = \case
    AnnError e :: AnnConvergeError
e -> AnnConvergeError -> Builder
forall p. Buildable p => p -> Builder
build AnnConvergeError
e
    TypeEqError type1 :: T
type1 type2 :: T
type2 ->
      "Types not equal: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| T
type1 T -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " /= " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| T
type2 T -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    StackEqError st1 :: [T]
st1 st2 :: [T]
st2 ->
      "Stacks not equal: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| [T] -> Builder
buildStack [T]
st1 Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " /= " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| [T] -> Builder
buildStack [T]
st2 Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    UnsupportedTypeForScope typ :: T
typ reason :: BadTypeForScope
reason ->
      "Type '" Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| T
typ T -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ "' is unsupported here because it "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| BadTypeForScope
reason BadTypeForScope -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    NotNumericTypes t1 :: T
t1 t2 :: T
t2 ->
      "Some of the types in an arithmetic operation are not numeric: "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| T
t1 T -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " and " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| T
t2 T -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    UnexpectedType (t :: NonEmpty ExpectType
t :| ts :: [NonEmpty ExpectType]
ts) ->
      "Wrong stack type for instruction, expect stack type to begin with " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+|
        ( String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate " or "
          ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (NonEmpty ExpectType -> String)
-> [NonEmpty ExpectType] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(x :: ExpectType
x :| xs :: [ExpectType]
xs) -> "" Builder -> Builder -> String
forall b. FromBuilder b => Builder -> Builder -> b
+| [ExpectType] -> Builder
forall (f :: * -> *) a. (Foldable f, Buildable a) => f a -> Builder
listF (ExpectType
xExpectType -> [ExpectType] -> [ExpectType]
forall a. a -> [a] -> [a]
:[ExpectType]
xs) Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ "")
          ([NonEmpty ExpectType] -> [String])
-> [NonEmpty ExpectType] -> [String]
forall a b. (a -> b) -> a -> b
$ (NonEmpty ExpectType
tNonEmpty ExpectType
-> [NonEmpty ExpectType] -> [NonEmpty ExpectType]
forall a. a -> [a] -> [a]
:[NonEmpty ExpectType]
ts)
        ) String -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    InvalidInstruction instr :: ExpandedInstr
instr ->
      "Forbidden instruction " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| ExpandedInstr
instr ExpandedInstr -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    InvalidValueType t :: T
t ->
      "Value type is never a valid `" Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| T
t T -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ "`"
    NotEnoughItemsOnStack ->
      "Not enough items on stack"
    UnknownContract addr :: Address
addr ->
      "Contract is not registered: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Address
addr Address -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    IllegalEntrypoint err :: EpNameFromRefAnnError
err -> EpNameFromRefAnnError -> Builder
forall p. Buildable p => p -> Builder
build EpNameFromRefAnnError
err
    EntrypointNotFound ep :: EpName
ep ->
      "No such entrypoint '" Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| EpName
ep EpName -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ "'"
    IllegalParamDecl err :: ParamEpError
err -> ParamEpError -> Builder
forall p. Buildable p => p -> Builder
build ParamEpError
err
    NegativeNat -> "Natural number cannot be negative"
    MutezOverflow -> "Exceeds maximal value for mutez"
    InvalidAddress e :: ParseEpAddressError
e -> ParseEpAddressError -> Builder
forall p. Buildable p => p -> Builder
build ParseEpAddressError
e
    InvalidKeyHash e :: CryptoParseError
e -> CryptoParseError -> Builder
forall p. Buildable p => p -> Builder
build CryptoParseError
e
    InvalidTimestamp -> "Is not a valid RFC3339 timestamp"
    CodeAlwaysFails -> "Code always fails, but is not supposed to"
    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
  deriving stock (TCError -> TCError -> Bool
(TCError -> TCError -> Bool)
-> (TCError -> TCError -> Bool) -> Eq TCError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TCError -> TCError -> Bool
$c/= :: TCError -> TCError -> Bool
== :: TCError -> TCError -> Bool
$c== :: TCError -> TCError -> Bool
Eq, (forall x. TCError -> Rep TCError x)
-> (forall x. Rep TCError x -> TCError) -> Generic TCError
forall x. Rep TCError x -> TCError
forall x. TCError -> Rep TCError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TCError x -> TCError
$cfrom :: forall x. TCError -> Rep TCError x
Generic)

instance NFData TCError

instance Buildable TCError where
  build :: TCError -> Builder
build = \case
    TCFailedOnInstr instr :: ExpandedInstr
instr (SomeHST t :: HST ts
t) ics :: InstrCallStack
ics mbTCTypeContext :: Maybe TypeContext
mbTCTypeContext mbTCTypeError :: Maybe TCTypeError
mbTCTypeError ->
      "Error checking expression "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| ExpandedInstr
instr ExpandedInstr -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " against input stack type "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| HST ts
t HST ts -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder -> (TypeContext -> Builder) -> Maybe TypeContext -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (\c :: TypeContext
c -> ". Error in " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| TypeContext
c TypeContext -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ "") Maybe TypeContext
mbTCTypeContext
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Builder -> (TCTypeError -> Builder) -> Maybe TCTypeError -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ". " (\e :: TCTypeError
e -> ": " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| TCTypeError
e TCTypeError -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ". ") Maybe TCTypeError
mbTCTypeError
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| InstrCallStack -> Builder
forall b. FromBuilder b => InstrCallStack -> b
buildCallStack InstrCallStack
ics
    TCFailedOnValue v :: Value
v t :: T
t custom :: Text
custom ics :: InstrCallStack
ics mbTCTypeError :: Maybe TCTypeError
mbTCTypeError ->
      "Error checking value "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Value
v Value -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " against type "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| T -> Type
toUType T
t Type -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder -> Builder -> Bool -> Builder
forall a. a -> a -> Bool -> a
bool (": " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Text
custom Text -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " ") "." (Text -> Bool
forall t. Container t => t -> Bool
null Text
custom)
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| (Builder -> (TCTypeError -> Builder) -> Maybe TCTypeError -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (\e :: TCTypeError
e -> "\n" Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| TCTypeError
e TCTypeError -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ".\n") Maybe TCTypeError
mbTCTypeError)
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| InstrCallStack -> Builder
forall b. FromBuilder b => InstrCallStack -> b
buildCallStack InstrCallStack
ics
    TCContractError msg :: Text
msg typeError :: Maybe TCTypeError
typeError ->
      "Error occured during contract typecheck: "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+|| Text
msg Text -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ (Builder -> (TCTypeError -> Builder) -> Maybe TCTypeError -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (\e :: TCTypeError
e -> " " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| TCTypeError
e TCTypeError -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ "") Maybe TCTypeError
typeError)
    TCUnreachableCode ics :: InstrCallStack
ics instrs :: NonEmpty ExpandedOp
instrs ->
      "Unreachable code: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Int -> [ExpandedOp] -> Builder
forall a. Buildable [a] => Int -> [a] -> Builder
buildTruncated 3 (NonEmpty ExpandedOp -> [Element (NonEmpty ExpandedOp)]
forall t. Container t => t -> [Element t]
toList NonEmpty ExpandedOp
instrs) Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ". "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| InstrCallStack -> Builder
forall b. FromBuilder b => InstrCallStack -> b
buildCallStack InstrCallStack
ics
    TCExtError (SomeHST t :: HST ts
t) ics :: InstrCallStack
ics e :: ExtError
e ->
      "Error occurred during Morley extension typecheck: "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| ExtError
e ExtError -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " on stack " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| HST ts
t HST ts -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ". "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| InstrCallStack -> Builder
forall b. FromBuilder b => InstrCallStack -> b
buildCallStack InstrCallStack
ics
    where
    buildTruncated :: Int -> [a] -> Builder
buildTruncated k :: Int
k l :: [a]
l
      | [a] -> Bool
forall t. Container t => t -> Bool
null (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
k [a]
l) = [a] -> Builder
forall p. Buildable p => p -> Builder
build [a]
l
      | Bool
otherwise = [a] -> Builder
forall p. Buildable p => p -> Builder
build (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
k [a]
l) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> " ..."
    buildCallStack :: InstrCallStack -> b
buildCallStack InstrCallStack{LetCallStack
icsCallStack :: InstrCallStack -> LetCallStack
icsCallStack :: LetCallStack
icsCallStack, icsSrcPos :: InstrCallStack -> SrcPos
icsSrcPos = SrcPos (Pos line :: Word
line) (Pos col :: Word
col)} =
      "Error occured on line " Builder -> Builder -> b
forall b. FromBuilder b => Builder -> Builder -> b
+| Word
line Word -> Word -> Word
forall a. Num a => a -> a -> a
+ 1 Word -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " char " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Word
col Word -> Word -> Word
forall a. Num a => a -> a -> a
+ 1 Word -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| case LetCallStack
icsCallStack of
           [] -> "."
           _ -> " inside these let defenitions: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| LetCallStack -> Builder
forall (f :: * -> *) a. (Foldable f, Buildable a) => f a -> Builder
listF LetCallStack
icsCallStack Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ "."

instance Buildable U.ExpandedInstr => Show TCError where
  show :: TCError -> String
show = TCError -> String
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty

instance Buildable U.ExpandedInstr => Exception TCError

newtype StackSize = StackSize Natural
  deriving stock (Int -> StackSize -> ShowS
[StackSize] -> ShowS
StackSize -> String
(Int -> StackSize -> ShowS)
-> (StackSize -> String)
-> ([StackSize] -> ShowS)
-> Show StackSize
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [StackSize] -> ShowS
$cshowList :: [StackSize] -> ShowS
show :: StackSize -> String
$cshow :: StackSize -> String
showsPrec :: Int -> StackSize -> ShowS
$cshowsPrec :: Int -> StackSize -> ShowS
Show, StackSize -> StackSize -> Bool
(StackSize -> StackSize -> Bool)
-> (StackSize -> StackSize -> Bool) -> Eq StackSize
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StackSize -> StackSize -> Bool
$c/= :: StackSize -> StackSize -> Bool
== :: StackSize -> StackSize -> Bool
$c== :: StackSize -> StackSize -> Bool
Eq, (forall x. StackSize -> Rep StackSize x)
-> (forall x. Rep StackSize x -> StackSize) -> Generic StackSize
forall x. Rep StackSize x -> StackSize
forall x. StackSize -> Rep StackSize x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep StackSize x -> StackSize
$cfrom :: forall x. StackSize -> Rep StackSize x
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 (ExtError -> ExtError -> Bool
(ExtError -> ExtError -> Bool)
-> (ExtError -> ExtError -> Bool) -> Eq ExtError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExtError -> ExtError -> Bool
$c/= :: ExtError -> ExtError -> Bool
== :: ExtError -> ExtError -> Bool
$c== :: ExtError -> ExtError -> Bool
Eq, (forall x. ExtError -> Rep ExtError x)
-> (forall x. Rep ExtError x -> ExtError) -> Generic ExtError
forall x. Rep ExtError x -> ExtError
forall x. ExtError -> Rep ExtError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ExtError x -> ExtError
$cfrom :: forall x. ExtError -> Rep ExtError x
Generic)

instance NFData ExtError

instance Buildable ExtError where
  build :: ExtError -> Builder
build = \case
    LengthMismatch stk :: StackTypePattern
stk ->
      "Unexpected length of stack: pattern "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackTypePattern
stk StackTypePattern -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " has length "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| ([TyVar] -> Int
forall t. Container t => t -> Int
length ([TyVar] -> Int)
-> (StackTypePattern -> [TyVar]) -> StackTypePattern -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([TyVar], Bool) -> [TyVar]
forall a b. (a, b) -> a
fst (([TyVar], Bool) -> [TyVar])
-> (StackTypePattern -> ([TyVar], Bool))
-> StackTypePattern
-> [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StackTypePattern -> ([TyVar], Bool)
U.stackTypePatternToList) StackTypePattern
stk Int -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    VarError t :: Text
t sf :: StackFn
sf ->
      "In defenition of " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Text
t Text -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ": VarError "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackFn
sf StackFn -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    TypeMismatch stk :: StackTypePattern
stk i :: Int
i e :: TCTypeError
e ->
      "TypeMismatch: Pattern " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackTypePattern
stk StackTypePattern -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " at index "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Int
i Int -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " with error: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| TCTypeError
e TCTypeError -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    TyVarMismatch v :: Var
v t :: Type
t stk :: StackTypePattern
stk i :: Int
i e :: TCTypeError
e ->
      "TyVarMismach: Variable " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Var
v Var -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " is bound to type "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Type
t Type -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " but pattern " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackTypePattern
stk StackTypePattern -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " failed at index "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Int
i Int -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " with error: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| TCTypeError
e TCTypeError -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    StkRestMismatch stk :: StackTypePattern
stk (SomeHST r :: HST ts
r) (SomeHST r' :: HST ts
r') e :: TCTypeError
e ->
      "StkRestMismatch in pattern " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackTypePattern
stk StackTypePattern -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+
      " against stacks " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| HST ts
r HST ts -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ " and " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| HST ts
r' HST ts -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+
      " with error: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| TCTypeError
e TCTypeError -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    TestAssertError t :: Text
t ->
      "TestAssertError: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Text
t Text -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""
    InvalidStackReference i :: StackRef
i lhs :: StackSize
lhs ->
      "InvalidStackReference: reference is out of the stack: "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackRef
i StackRef -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ " >= " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackSize
lhs StackSize -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ ""