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

module Morley.Michelson.TypeCheck.Value
    ( typeCheckValImpl
    , tcFailedOnValue
    ) where

import Control.Monad.Except (liftEither, throwError)
import Data.Constraint (Dict(..))
import Data.List.NonEmpty qualified as NE
import Data.Map qualified as M
import Data.Set qualified as S
import Data.Singletons (Sing, SingI(..), demote, fromSing, withSingI)
import Data.Typeable ((:~:)(..))
import Fmt (pretty)
import Prelude hiding (EQ, GT, LT)

import Morley.Michelson.Text
import Morley.Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))
import Morley.Michelson.TypeCheck.Helpers
import Morley.Michelson.TypeCheck.TypeCheck
  (SomeParamType(..), TcInstrHandler, TcOriginatedContracts, TypeCheckInstr, TypeCheckOptions(..),
  tcieErrorPos, tcieNotInView, throwingTCError)
import Morley.Michelson.TypeCheck.Types
import Morley.Michelson.Typed (EpAddress(..), Notes(..), SingT(..), Value'(..))
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Typed.Contract (giveNotInView)
import Morley.Michelson.Untyped qualified as U
import Morley.Tezos.Address (Address(..), TxRollupL2Address(..))
import Morley.Tezos.Core
import Morley.Tezos.Crypto
import Morley.Tezos.Crypto.BLS12381 qualified as BLS
import Morley.Tezos.Crypto.Timelock (chestFromBytes, chestKeyFromBytes)
import Morley.Util.Type (onFirst)

tcFailedOnValue :: U.Value -> T.T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue :: forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v T
t Text
msg Maybe TCTypeError
err = do
  ErrorSrcPos
loc <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT TypeCheckInstrEnv TypeCheck ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
  TCError -> TypeCheckInstr a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TypeCheckInstr a) -> TCError -> TypeCheckInstr a
forall a b. (a -> b) -> a -> b
$ Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
v T
t Text
msg ErrorSrcPos
loc Maybe TCTypeError
err

-- | Function @typeCheckValImpl@ converts a single Michelson value
-- given in representation from @Morley.Michelson.Type@ module to representation
-- in strictly typed GADT.
--
-- @typeCheckValImpl@ is polymorphic in the expected type of value.
--
-- Type checking algorithm pattern-matches on parse value representation,
-- expected type @t@ and constructs @Val t@ value.
--
-- If there was no match on a given pair of value and expected type,
-- that is interpreted as input of wrong type and type check finishes with
-- error.
--
-- @typeCheckValImpl@ also has a 'Maybe TcOriginatedContracts' argument that
-- should contain the originated contracts when typechecking a parameter and
-- 'Nothing' otherwise.
typeCheckValImpl
  :: forall ty.
     SingI ty
  => Maybe TcOriginatedContracts
  -> TcInstrHandler
  -> U.Value
  -> TypeCheckInstr (T.Value ty)
typeCheckValImpl :: forall (ty :: T).
SingI ty =>
Maybe TcOriginatedContracts
-> TcInstrHandler -> Value -> TypeCheckInstr (Value ty)
typeCheckValImpl Maybe TcOriginatedContracts
mOriginatedContracts TcInstrHandler
tcDo Value
uv = (Value, Sing ty) -> TypeCheckInstr (Value ty)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
uv, forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @ty)
  where
    doTypeCheckVal :: forall tz. (U.Value, Sing tz) -> TypeCheckInstr (T.Value tz)
    doTypeCheckVal :: forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
uvalue, Sing tz
sng) = case (Value
uvalue, Sing tz
SingT tz
sng) of
      (U.ValueInt Integer
i, SingT tz
STInt) -> Value' Instr 'TInt
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TInt)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TInt
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TInt))
-> Value' Instr 'TInt
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' Instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
T.VInt Integer
i
      (v :: Value
v@(U.ValueInt Integer
i), t :: SingT tz
t@SingT tz
STNat)
        | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 -> Value' Instr 'TNat
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TNat)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TNat
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TNat))
-> Value' Instr 'TNat
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TNat)
forall a b. (a -> b) -> a -> b
$ Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Integer -> Natural
forall a. (HasCallStack, Integral a) => Integer -> a
fromInteger Integer
i)
        | Bool
otherwise -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TNat -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TNat
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
NegativeNat)
      (v :: Value
v@(U.ValueInt Integer
i), t :: SingT tz
t@SingT tz
STMutez) -> case Integer -> Either Text Mutez
forall i. Integral i => i -> Either Text Mutez
mkMutez Integer
i of
        Right Mutez
m -> Value' Instr 'TMutez
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TMutez)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TMutez
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TMutez))
-> Value' Instr 'TMutez
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TMutez)
forall a b. (a -> b) -> a -> b
$ Mutez -> Value' Instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
m
        Left Text
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TMutez -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TMutez
SingT tz
t) Text
err (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
InvalidTimestamp)
      (U.ValueString MText
s, SingT tz
STString) -> Value' Instr 'TString
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TString
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TString))
-> Value' Instr 'TString
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TString)
forall a b. (a -> b) -> a -> b
$ MText -> Value' Instr 'TString
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString MText
s
      (v :: Value
v@(U.ValueString MText
s), t :: SingT tz
t@SingT tz
STAddress) -> case Text -> Either ParseEpAddressError EpAddress
T.parseEpAddress (MText -> Text
unMText MText
s) of
        Right EpAddress
addr -> Value' Instr 'TAddress
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TAddress)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TAddress
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TAddress))
-> Value' Instr 'TAddress
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TAddress)
forall a b. (a -> b) -> a -> b
$ EpAddress -> Value' Instr 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress EpAddress
addr
        Left ParseEpAddressError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TAddress -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TAddress
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ ParseEpAddressError -> TCTypeError
InvalidAddress ParseEpAddressError
err)
      (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STAddress) -> case ByteString -> Either ParseEpAddressError EpAddress
T.parseEpAddressRaw (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
        Right EpAddress
addr -> Value' Instr 'TAddress
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TAddress)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TAddress
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TAddress))
-> Value' Instr 'TAddress
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TAddress)
forall a b. (a -> b) -> a -> b
$ EpAddress -> Value' Instr 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress EpAddress
addr
        Left ParseEpAddressError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TAddress -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TAddress
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ ParseEpAddressError -> TCTypeError
InvalidAddress ParseEpAddressError
err)
      (v :: Value
v@(U.ValueString MText
s), t :: SingT tz
t@SingT tz
STKeyHash) -> case Text -> Either CryptoParseError (Hash 'HashKindPublicKey)
forall (kind :: HashKind).
AllTags kind =>
Text -> Either CryptoParseError (Hash kind)
parseHash (MText -> Text
unMText MText
s)  of
        Right Hash 'HashKindPublicKey
kHash -> Value' Instr 'TKeyHash
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKeyHash)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKeyHash
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKeyHash))
-> Value' Instr 'TKeyHash
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKeyHash)
forall a b. (a -> b) -> a -> b
$ Hash 'HashKindPublicKey -> Value' Instr 'TKeyHash
forall (instr :: [T] -> [T] -> *).
Hash 'HashKindPublicKey -> Value' instr 'TKeyHash
VKeyHash Hash 'HashKindPublicKey
kHash
        Left CryptoParseError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TKeyHash -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TKeyHash
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ CryptoParseError -> TCTypeError
InvalidKeyHash CryptoParseError
err)
      (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STKeyHash) ->
        case ByteString -> Either CryptoParseError (Hash 'HashKindPublicKey)
parseKeyHashRaw (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
          Right Hash 'HashKindPublicKey
kHash -> Value' Instr 'TKeyHash
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKeyHash)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKeyHash
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKeyHash))
-> Value' Instr 'TKeyHash
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKeyHash)
forall a b. (a -> b) -> a -> b
$ Hash 'HashKindPublicKey -> Value' Instr 'TKeyHash
forall (instr :: [T] -> [T] -> *).
Hash 'HashKindPublicKey -> Value' instr 'TKeyHash
VKeyHash Hash 'HashKindPublicKey
kHash
          Left CryptoParseError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TKeyHash -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TKeyHash
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ CryptoParseError -> TCTypeError
InvalidKeyHash CryptoParseError
err)
      (v :: Value
v@(U.ValueString MText
s), t :: SingT tz
t@SingT tz
STTxRollupL2Address) -> case Text -> Either CryptoParseError (Hash 'HashKindL2PublicKey)
forall (kind :: HashKind).
AllTags kind =>
Text -> Either CryptoParseError (Hash kind)
parseHash (MText -> Text
unMText MText
s)  of
        Right Hash 'HashKindL2PublicKey
kHash -> Value' Instr 'TTxRollupL2Address
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr 'TTxRollupL2Address)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTxRollupL2Address
 -> ReaderT
      TypeCheckInstrEnv TypeCheck (Value' Instr 'TTxRollupL2Address))
-> Value' Instr 'TTxRollupL2Address
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr 'TTxRollupL2Address)
forall a b. (a -> b) -> a -> b
$ TxRollupL2Address -> Value' Instr 'TTxRollupL2Address
forall (instr :: [T] -> [T] -> *).
TxRollupL2Address -> Value' instr 'TTxRollupL2Address
VTxRollupL2Address (TxRollupL2Address -> Value' Instr 'TTxRollupL2Address)
-> TxRollupL2Address -> Value' Instr 'TTxRollupL2Address
forall a b. (a -> b) -> a -> b
$ Hash 'HashKindL2PublicKey -> TxRollupL2Address
TxRollupL2Address Hash 'HashKindL2PublicKey
kHash
        Left CryptoParseError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TTxRollupL2Address -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TTxRollupL2Address
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ CryptoParseError -> TCTypeError
InvalidKeyHash CryptoParseError
err)
      (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STTxRollupL2Address) ->
        case ByteString -> Either CryptoParseError (Hash 'HashKindL2PublicKey)
parseKeyHashL2Raw (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
          Right Hash 'HashKindL2PublicKey
kHash -> Value' Instr 'TTxRollupL2Address
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr 'TTxRollupL2Address)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTxRollupL2Address
 -> ReaderT
      TypeCheckInstrEnv TypeCheck (Value' Instr 'TTxRollupL2Address))
-> Value' Instr 'TTxRollupL2Address
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr 'TTxRollupL2Address)
forall a b. (a -> b) -> a -> b
$ TxRollupL2Address -> Value' Instr 'TTxRollupL2Address
forall (instr :: [T] -> [T] -> *).
TxRollupL2Address -> Value' instr 'TTxRollupL2Address
VTxRollupL2Address (TxRollupL2Address -> Value' Instr 'TTxRollupL2Address)
-> TxRollupL2Address -> Value' Instr 'TTxRollupL2Address
forall a b. (a -> b) -> a -> b
$ Hash 'HashKindL2PublicKey -> TxRollupL2Address
TxRollupL2Address Hash 'HashKindL2PublicKey
kHash
          Left CryptoParseError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TTxRollupL2Address -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TTxRollupL2Address
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ CryptoParseError -> TCTypeError
InvalidKeyHash CryptoParseError
err)
      (U.ValueInt Integer
i, SingT tz
STBls12381Fr) ->
        Value' Instr 'TBls12381Fr
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381Fr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381Fr
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381Fr))
-> Value' Instr 'TBls12381Fr
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' Instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (forall a b. (Integral a, Num b) => a -> b
fromIntegralOverflowing @Integer @Bls12381Fr Integer
i)
      (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STBls12381Fr) ->
        case ByteString -> Either DeserializationError Bls12381Fr
forall a.
CurveObject a =>
ByteString -> Either DeserializationError a
BLS.fromMichelsonBytes (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
          Right Bls12381Fr
val -> Value' Instr 'TBls12381Fr
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381Fr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381Fr
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381Fr))
-> Value' Instr 'TBls12381Fr
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' Instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr Bls12381Fr
val
          Left DeserializationError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TBls12381Fr -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TBls12381Fr
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ DeserializationError -> TCTypeError
InvalidBls12381Object DeserializationError
err)
      (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STBls12381G1) ->
        case ByteString -> Either DeserializationError Bls12381G1
forall a.
CurveObject a =>
ByteString -> Either DeserializationError a
BLS.fromMichelsonBytes (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
          Right Bls12381G1
val -> Value' Instr 'TBls12381G1
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381G1)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381G1
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381G1))
-> Value' Instr 'TBls12381G1
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381G1)
forall a b. (a -> b) -> a -> b
$ Bls12381G1 -> Value' Instr 'TBls12381G1
forall (instr :: [T] -> [T] -> *).
Bls12381G1 -> Value' instr 'TBls12381G1
VBls12381G1 Bls12381G1
val
          Left DeserializationError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TBls12381G1 -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TBls12381G1
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ DeserializationError -> TCTypeError
InvalidBls12381Object DeserializationError
err)
      (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STBls12381G2) ->
        case ByteString -> Either DeserializationError Bls12381G2
forall a.
CurveObject a =>
ByteString -> Either DeserializationError a
BLS.fromMichelsonBytes (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
          Right Bls12381G2
val -> Value' Instr 'TBls12381G2
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381G2)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381G2
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381G2))
-> Value' Instr 'TBls12381G2
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBls12381G2)
forall a b. (a -> b) -> a -> b
$ Bls12381G2 -> Value' Instr 'TBls12381G2
forall (instr :: [T] -> [T] -> *).
Bls12381G2 -> Value' instr 'TBls12381G2
VBls12381G2 Bls12381G2
val
          Left DeserializationError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TBls12381G2 -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TBls12381G2
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ DeserializationError -> TCTypeError
InvalidBls12381Object DeserializationError
err)
      (v :: Value
v@(U.ValueString MText
s), t :: SingT tz
t@SingT tz
STTimestamp) -> case Text -> Maybe Timestamp
parseTimestamp (Text -> Maybe Timestamp) -> Text -> Maybe Timestamp
forall a b. (a -> b) -> a -> b
$ MText -> Text
unMText MText
s of
        Just Timestamp
tstamp -> Value' Instr 'TTimestamp
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TTimestamp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTimestamp
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TTimestamp))
-> Value' Instr 'TTimestamp
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TTimestamp)
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' Instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp Timestamp
tstamp
        Maybe Timestamp
Nothing -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TTimestamp -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TTimestamp
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
InvalidTimestamp)
      (U.ValueInt Integer
i, SingT tz
STTimestamp) -> Value' Instr 'TTimestamp
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TTimestamp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTimestamp
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TTimestamp))
-> Value' Instr 'TTimestamp
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TTimestamp)
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' Instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp (Integer -> Timestamp
timestampFromSeconds Integer
i)
      (U.ValueBytes (U.InternalByteString ByteString
s), SingT tz
STBytes) -> Value' Instr 'TBytes
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBytes)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBytes
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBytes))
-> Value' Instr 'TBytes
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBytes)
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes ByteString
s
      (Value
U.ValueTrue, SingT tz
STBool) -> Value' Instr 'TBool
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBool)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBool
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBool))
-> Value' Instr 'TBool
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBool)
forall a b. (a -> b) -> a -> b
$ Bool -> Value' Instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool Bool
True
      (Value
U.ValueFalse, SingT tz
STBool) -> Value' Instr 'TBool
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBool)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBool
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBool))
-> Value' Instr 'TBool
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TBool)
forall a b. (a -> b) -> a -> b
$ Bool -> Value' Instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool Bool
False

      (U.ValueString (Text -> Either CryptoParseError PublicKey
parsePublicKey (Text -> Either CryptoParseError PublicKey)
-> (MText -> Text) -> MText -> Either CryptoParseError PublicKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MText -> Text
unMText -> Right PublicKey
s), SingT tz
STKey) ->
        Value' Instr 'TKey
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKey)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKey
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKey))
-> Value' Instr 'TKey
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKey)
forall a b. (a -> b) -> a -> b
$ PublicKey -> Value' Instr 'TKey
forall (instr :: [T] -> [T] -> *). PublicKey -> Value' instr 'TKey
T.VKey PublicKey
s
      (U.ValueBytes (ByteString -> Either Text PublicKey
parsePublicKeyRaw (ByteString -> Either Text PublicKey)
-> (InternalByteString -> ByteString)
-> InternalByteString
-> Either Text PublicKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InternalByteString -> ByteString
U.unInternalByteString -> Right PublicKey
s), SingT tz
STKey) ->
        Value' Instr 'TKey
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKey)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKey
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKey))
-> Value' Instr 'TKey
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TKey)
forall a b. (a -> b) -> a -> b
$ PublicKey -> Value' Instr 'TKey
forall (instr :: [T] -> [T] -> *). PublicKey -> Value' instr 'TKey
VKey PublicKey
s

      (U.ValueString (Text -> Either CryptoParseError Signature
parseSignature (Text -> Either CryptoParseError Signature)
-> (MText -> Text) -> MText -> Either CryptoParseError Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MText -> Text
unMText -> Right Signature
s), SingT tz
STSignature) ->
        Value' Instr 'TSignature
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TSignature)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TSignature
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TSignature))
-> Value' Instr 'TSignature
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TSignature)
forall a b. (a -> b) -> a -> b
$ Signature -> Value' Instr 'TSignature
forall (instr :: [T] -> [T] -> *).
Signature -> Value' instr 'TSignature
VSignature Signature
s
      (U.ValueBytes (ByteString -> Either ParseSignatureRawError Signature
parseSignatureRaw (ByteString -> Either ParseSignatureRawError Signature)
-> (InternalByteString -> ByteString)
-> InternalByteString
-> Either ParseSignatureRawError Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InternalByteString -> ByteString
U.unInternalByteString  -> Right Signature
s), SingT tz
STSignature) ->
        Value' Instr 'TSignature
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TSignature)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TSignature
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TSignature))
-> Value' Instr 'TSignature
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TSignature)
forall a b. (a -> b) -> a -> b
$ Signature -> Value' Instr 'TSignature
forall (instr :: [T] -> [T] -> *).
Signature -> Value' instr 'TSignature
VSignature Signature
s

      (U.ValueString (Text -> Either ParseChainIdError ChainId
parseChainId (Text -> Either ParseChainIdError ChainId)
-> (MText -> Text) -> MText -> Either ParseChainIdError ChainId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MText -> Text
unMText -> Right ChainId
ci), SingT tz
STChainId) ->
        Value' Instr 'TChainId
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChainId)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChainId
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChainId))
-> Value' Instr 'TChainId
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChainId)
forall a b. (a -> b) -> a -> b
$ ChainId -> Value' Instr 'TChainId
forall (instr :: [T] -> [T] -> *).
ChainId -> Value' instr 'TChainId
VChainId ChainId
ci
      (U.ValueBytes (ByteString -> Either ParseChainIdError ChainId
mkChainId (ByteString -> Either ParseChainIdError ChainId)
-> (InternalByteString -> ByteString)
-> InternalByteString
-> Either ParseChainIdError ChainId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InternalByteString -> ByteString
U.unInternalByteString -> Right ChainId
ci), SingT tz
STChainId) ->
        Value' Instr 'TChainId
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChainId)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChainId
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChainId))
-> Value' Instr 'TChainId
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChainId)
forall a b. (a -> b) -> a -> b
$ ChainId -> Value' Instr 'TChainId
forall (instr :: [T] -> [T] -> *).
ChainId -> Value' instr 'TChainId
VChainId ChainId
ci

      (cv :: Value
cv@(U.ValueString (Text -> Either ParseEpAddressError EpAddress
T.parseEpAddress (Text -> Either ParseEpAddressError EpAddress)
-> (MText -> Text) -> MText -> Either ParseEpAddressError EpAddress
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MText -> Text
unMText -> Right EpAddress
addr))
        , STContract Sing n
pc) -> Value -> EpAddress -> Sing n -> TypeCheckInstr (Value tz)
forall (cp :: T) (tz :: T).
(tz ~ 'TContract cp) =>
Value -> EpAddress -> Sing cp -> TypeCheckInstr (Value tz)
typecheckContractValue Value
cv EpAddress
addr Sing n
pc
      (cv :: Value
cv@(U.ValueBytes (ByteString -> Either ParseEpAddressError EpAddress
T.parseEpAddressRaw (ByteString -> Either ParseEpAddressError EpAddress)
-> (InternalByteString -> ByteString)
-> InternalByteString
-> Either ParseEpAddressError EpAddress
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InternalByteString -> ByteString
U.unInternalByteString -> Right EpAddress
addr))
        , STContract Sing n
pc) -> Value -> EpAddress -> Sing n -> TypeCheckInstr (Value tz)
forall (cp :: T) (tz :: T).
(tz ~ 'TContract cp) =>
Value -> EpAddress -> Sing cp -> TypeCheckInstr (Value tz)
typecheckContractValue Value
cv EpAddress
addr Sing n
pc

      (Value
cv, s :: SingT tz
s@(STTicket Sing n
vt)) -> TypeCheck Bool -> ReaderT TypeCheckInstrEnv TypeCheck Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((TypeCheckOptions -> Bool) -> TypeCheck Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks TypeCheckOptions -> Bool
tcStrict) ReaderT TypeCheckInstrEnv TypeCheck Bool
-> (Bool -> TypeCheckInstr (Value tz)) -> TypeCheckInstr (Value tz)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        -- Note [Tickets forging]
        -- Normally, ticket values cannot be constructed manually (i.e. forged)
        -- by design, and the only valid way to make a ticket is calling
        -- @TICKET@ instruction.
        --
        -- However @tezos-client run@ adds an exception, it allows passing a
        -- manually constructed ticket value as parameter or initial storage.
        Bool
True ->
          Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
cv (Sing ('TTicket n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing tz
Sing ('TTicket n)
sng)
            Text
"ticket values cannot be forged in real operations"
            Maybe TCTypeError
forall a. Maybe a
Nothing
        Bool
False -> case Value
cv of
          U.ValuePair Value
addrV (U.ValuePair Value
datV Value
amV) -> Sing n
-> Value
-> Sing ('TTicket n)
-> (Comparable n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing n
vt Value
cv Sing ('TTicket n)
SingT tz
s ((Comparable n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
            Value' Instr 'TAddress
addrValue <- (Value, Sing 'TAddress)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TAddress)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
addrV, Sing 'TAddress
SingT 'TAddress
STAddress)
            Value n
dat <- (Value, Sing n) -> TypeCheckInstr (Value n)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
datV, Sing n
vt)
            Value' Instr 'TNat
amountValue <- (Value, Sing 'TNat)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TNat)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
amV, Sing 'TNat
SingT 'TNat
STNat)
            case (Value' Instr 'TAddress
addrValue, Value' Instr 'TNat
amountValue) of
              (VAddress (EpAddress Address
addr EpName
ep), VNat Natural
am) -> do
                Bool
-> ReaderT TypeCheckInstrEnv TypeCheck ()
-> ReaderT TypeCheckInstrEnv TypeCheck ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (EpName -> Bool
U.isDefEpName EpName
ep) (ReaderT TypeCheckInstrEnv TypeCheck ()
 -> ReaderT TypeCheckInstrEnv TypeCheck ())
-> ReaderT TypeCheckInstrEnv TypeCheck ()
-> ReaderT TypeCheckInstrEnv TypeCheck ()
forall a b. (a -> b) -> a -> b
$
                  Value
-> T
-> Text
-> Maybe TCTypeError
-> ReaderT TypeCheckInstrEnv TypeCheck ()
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
cv (Sing ('TTicket n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing tz
Sing ('TTicket n)
sng)
                    Text
"it is pointless to provide an address with entrypoint as a \
                    \ticketer, we do not support that"
                    Maybe TCTypeError
forall a. Maybe a
Nothing
                -- ↑ Tezos allows passing addresses with entrypoint, but it is
                -- not possible to sanely work with them after that anyway,
                -- since @TICKET@ instruction (the only valid way of constructing
                -- tickets in real run) uses @SELF_ADDRESS@ result as ticketer.
                return $ Address -> Value n -> Natural -> Value' Instr ('TTicket n)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Comparable arg =>
Address
-> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
VTicket Address
addr Value n
dat Natural
am
          Value
_ ->
            Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
cv (Sing ('TTicket n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing tz
Sing ('TTicket n)
sng)
              Text
"ticket type expects a value of type `(pair address <data> nat)`"
              Maybe TCTypeError
forall a. Maybe a
Nothing

      (Value
U.ValueUnit, SingT tz
STUnit) -> Value' Instr 'TUnit
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TUnit)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TUnit
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TUnit))
-> Value' Instr 'TUnit
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TUnit)
forall a b. (a -> b) -> a -> b
$ Value' Instr 'TUnit
forall (instr :: [T] -> [T] -> *). Value' instr 'TUnit
VUnit
      (U.ValuePair Value
ml Value
mr, STPair Sing n1
lt Sing n2
rt) -> do
        Value n1
l <- (Value, Sing n1) -> TypeCheckInstr (Value n1)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
ml, Sing n1
lt)
        Value n2
r <- (Value, Sing n2) -> TypeCheckInstr (Value n2)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
mr, Sing n2
rt)
        pure $ (Value n1, Value n2) -> Value' Instr ('TPair n1 n2)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value n1
l, Value n2
r)
      (U.ValueLeft Value
ml, STOr Sing n1
lt Sing n2
rt) -> do
        Value n1
l <- (Value, Sing n1) -> TypeCheckInstr (Value n1)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
ml, Sing n1
lt)
        Sing n1
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
lt ((SingI n1 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
rt ((SingI n2 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TOr n1 n2)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOr n1 n2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TOr n1 n2)
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOr n1 n2)))
-> Value' Instr ('TOr n1 n2)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOr n1 n2))
forall a b. (a -> b) -> a -> b
$ Either (Value n1) (Value' Instr n2) -> Value' Instr ('TOr n1 n2)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Value n1 -> Either (Value n1) (Value' Instr n2)
forall a b. a -> Either a b
Left Value n1
l)
      (U.ValueRight Value
mr, STOr Sing n1
lt Sing n2
rt) -> do
        Value n2
r <- (Value, Sing n2) -> TypeCheckInstr (Value n2)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
mr, Sing n2
rt)
        Sing n1
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
lt ((SingI n1 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
rt ((SingI n2 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TOr n1 n2)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOr n1 n2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TOr n1 n2)
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOr n1 n2)))
-> Value' Instr ('TOr n1 n2)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOr n1 n2))
forall a b. (a -> b) -> a -> b
$ Either (Value' Instr n1) (Value n2) -> Value' Instr ('TOr n1 n2)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Value n2 -> Either (Value' Instr n1) (Value n2)
forall a b. b -> Either a b
Right Value n2
r)
      (U.ValueSome Value
mv, STOption Sing n
op) -> do
        Value n
v <- (Value, Sing n) -> TypeCheckInstr (Value n)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
mv, Sing n
op)
        Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
op ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TOption n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOption n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TOption n)
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOption n)))
-> Value' Instr ('TOption n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOption n))
forall a b. (a -> b) -> a -> b
$ Maybe (Value n) -> Value' Instr ('TOption n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Value n -> Maybe (Value n)
forall a. a -> Maybe a
Just Value n
v)
      (Value
U.ValueNone, STOption Sing n
op) -> do
        Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
op ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TOption n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOption n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TOption n)
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOption n)))
-> Value' Instr ('TOption n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TOption n))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' Instr n) -> Value' Instr ('TOption n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption Maybe (Value' Instr n)
forall a. Maybe a
Nothing

      (Value
U.ValueNil, STList Sing n
l) -> Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
l ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$
        Value' Instr ('TList n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TList n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TList n)
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TList n)))
-> Value' Instr ('TList n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TList n))
forall a b. (a -> b) -> a -> b
$ [Value' Instr n] -> Value' Instr ('TList n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
T.VList []

      -- If ValueSeq contains at least 2 elements, it can be type checked as a
      -- right combed pair.
      (U.ValueSeq vals :: NonEmpty $ Value
vals@(Value
_ :| (Value
_ : [Value]
_)), STPair Sing n1
_ Sing n2
_) ->
        (Value, Sing tz) -> TypeCheckInstr (Value tz)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal ((NonEmpty $ Value) -> Value
seqToRightCombedPair NonEmpty $ Value
vals, Sing tz
sng)

      (U.ValueSeq ((NonEmpty $ Value) -> [Element (NonEmpty $ Value)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Value)]
mels), STList Sing n
l) -> do
        [Value n]
els <- ([Value], Sing n) -> TypeCheckInstr [Value n]
forall (t :: T). ([Value], Sing t) -> TypeCheckInstr [Value t]
typeCheckValsImpl ([Element (NonEmpty $ Value)]
[Value]
mels, Sing n
l)
        Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
l ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TList n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TList n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TList n)
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TList n)))
-> Value' Instr ('TList n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TList n))
forall a b. (a -> b) -> a -> b
$ [Value n] -> Value' Instr ('TList n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList [Value n]
els

      (Value
U.ValueNil, STSet Sing n
s) -> do
        ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT TypeCheckInstrEnv TypeCheck ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
        case Sing n -> Maybe (Dict (Comparable n))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
T.getComparableProofS Sing n
s of
          Just Dict (Comparable n)
Dict -> Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
s ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TSet n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TSet n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Value' Instr n) -> Value' Instr ('TSet n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
(SingI t1, Comparable t1) =>
Set (Value' instr t1) -> Value' instr ('TSet t1)
T.VSet Set (Value' Instr n)
forall a. Set a
S.empty)
          Maybe (Dict (Comparable n))
Nothing -> TCError -> TypeCheckInstr (Value tz)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TypeCheckInstr (Value tz))
-> TCError -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
uvalue (Sing n -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
s) Text
"Non comparable types are not allowed in Sets"
            ErrorSrcPos
instrPos (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ T -> BadTypeForScope -> TCTypeError
UnsupportedTypeForScope (Sing n -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
s) BadTypeForScope
T.BtNotComparable)

      (sq :: Value
sq@(U.ValueSeq ((NonEmpty $ Value) -> [Element (NonEmpty $ Value)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Value)]
mels)), s :: SingT tz
s@(STSet Sing n
vt)) -> Sing n
-> Value
-> Sing ('TSet n)
-> (Comparable n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing n
vt Value
sq Sing ('TSet n)
SingT tz
s ((Comparable n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
        ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT TypeCheckInstrEnv TypeCheck ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos

        [Value n]
els <- ([Value], Sing n) -> TypeCheckInstr [Value n]
forall (t :: T). ([Value], Sing t) -> TypeCheckInstr [Value t]
typeCheckValsImpl ([Element (NonEmpty $ Value)]
[Value]
mels, Sing n
vt)
        Set (Value n)
elsS <- Either TCError (Set (Value n))
-> ReaderT TypeCheckInstrEnv TypeCheck (Set (Value n))
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError (Set (Value n))
 -> ReaderT TypeCheckInstrEnv TypeCheck (Set (Value n)))
-> Either TCError (Set (Value n))
-> ReaderT TypeCheckInstrEnv TypeCheck (Set (Value n))
forall a b. (a -> b) -> a -> b
$ [Value n] -> Set (Value n)
forall a. [a] -> Set a
S.fromDistinctAscList ([Value n] -> Set (Value n))
-> Either TCError [Value n] -> Either TCError (Set (Value n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value n -> Value n) -> [Value n] -> Either Text [Value n]
forall b a.
(Ord b, Buildable a) =>
(a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc Value n -> Value n
forall a. a -> a
id [Value n]
els
                  Either Text [Value n]
-> (Text -> TCError) -> Either TCError [Value n]
forall (p :: * -> * -> *) a c b.
Bifunctor p =>
p a c -> (a -> b) -> p b c
`onFirst` \Text
msg -> Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
sq (Sing n -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
vt) Text
msg ErrorSrcPos
instrPos Maybe TCTypeError
forall a. Maybe a
Nothing
        Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
vt ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TSet n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TSet n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TSet n)
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TSet n)))
-> Value' Instr ('TSet n)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TSet n))
forall a b. (a -> b) -> a -> b
$ Set (Value n) -> Value' Instr ('TSet n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
(SingI t1, Comparable t1) =>
Set (Value' instr t1) -> Value' instr ('TSet t1)
VSet Set (Value n)
elsS

      (v :: Value
v@Value
U.ValueNil, s :: SingT tz
s@(STMap Sing n1
st Sing n2
vt)) ->
        Sing n1
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
st ((SingI n1 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
vt ((SingI n2 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n1
-> Value
-> Sing ('TMap n1 n2)
-> (Comparable n1 => TypeCheckInstr (Value ('TMap n1 n2)))
-> TypeCheckInstr (Value ('TMap n1 n2))
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing n1
st Value
v Sing ('TMap n1 n2)
SingT tz
s ((Comparable n1 => TypeCheckInstr (Value ('TMap n1 n2)))
 -> TypeCheckInstr (Value ('TMap n1 n2)))
-> (Comparable n1 => TypeCheckInstr (Value ('TMap n1 n2)))
-> TypeCheckInstr (Value ('TMap n1 n2))
forall a b. (a -> b) -> a -> b
$ Value ('TMap n1 n2) -> TypeCheckInstr (Value ('TMap n1 n2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TMap n1 n2) -> TypeCheckInstr (Value ('TMap n1 n2)))
-> Value ('TMap n1 n2) -> TypeCheckInstr (Value ('TMap n1 n2))
forall a b. (a -> b) -> a -> b
$ Map (Value' Instr n1) (Value' Instr n2) -> Value ('TMap n1 n2)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
T.VMap Map (Value' Instr n1) (Value' Instr n2)
forall k a. Map k a
M.empty

      (sq :: Value
sq@(U.ValueMap ((NonEmpty $ Elt ExpandedOp)
-> [Element (NonEmpty $ Elt ExpandedOp)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Elt ExpandedOp)]
mels)), s :: SingT tz
s@(STMap Sing n1
kt Sing n2
vt)) ->
        Sing n1
-> Value
-> Sing ('TMap n1 n2)
-> (Comparable n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing n1
kt Value
sq Sing ('TMap n1 n2)
SingT tz
s ((Comparable n1 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
          [(Value n1, Value n2)]
keyOrderedElts <- [Elt ExpandedOp]
-> Value
-> Sing n1
-> Sing n2
-> TypeCheckInstr [(Value n1, Value n2)]
forall (kt :: T) (vt :: T).
[Elt ExpandedOp]
-> Value
-> Sing kt
-> Sing vt
-> TypeCheckInstr [(Value kt, Value vt)]
typeCheckMapVal [Element (NonEmpty $ Elt ExpandedOp)]
[Elt ExpandedOp]
mels Value
sq Sing n1
kt Sing n2
vt
          Sing n1
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
kt ((SingI n1 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
vt ((SingI n2 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$
            Value' Instr ('TMap n1 n2)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TMap n1 n2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TMap n1 n2)
 -> ReaderT
      TypeCheckInstrEnv TypeCheck (Value' Instr ('TMap n1 n2)))
-> Value' Instr ('TMap n1 n2)
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr ('TMap n1 n2))
forall a b. (a -> b) -> a -> b
$ Map (Value n1) (Value n2) -> Value' Instr ('TMap n1 n2)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap ([(Value n1, Value n2)] -> Map (Value n1) (Value n2)
forall k a. [(k, a)] -> Map k a
M.fromDistinctAscList [(Value n1, Value n2)]
keyOrderedElts)

      (v :: Value
v@Value
U.ValueNil, s :: SingT tz
s@(STBigMap Sing n1
st1 Sing n2
st2)) ->
        Sing n1
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
st1 ((SingI n1 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
st2 ((SingI n2 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n1
-> Value
-> Sing ('TBigMap n1 n2)
-> (Comparable n1 => TypeCheckInstr (Value ('TBigMap n1 n2)))
-> TypeCheckInstr (Value ('TBigMap n1 n2))
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing n1
st1 Value
v Sing ('TBigMap n1 n2)
SingT tz
s ((Comparable n1 => TypeCheckInstr (Value ('TBigMap n1 n2)))
 -> TypeCheckInstr (Value ('TBigMap n1 n2)))
-> (Comparable n1 => TypeCheckInstr (Value ('TBigMap n1 n2)))
-> TypeCheckInstr (Value ('TBigMap n1 n2))
forall a b. (a -> b) -> a -> b
$ Sing n2
-> Value
-> Sing ('TBigMap n1 n2)
-> (HasNoBigMap n2 => TypeCheckInstr (Value ('TBigMap n1 n2)))
-> TypeCheckInstr (Value ('TBigMap n1 n2))
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (HasNoBigMap a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withBigMapAbsence Sing n2
st2 Value
v Sing ('TBigMap n1 n2)
SingT tz
s ((HasNoBigMap n2 => TypeCheckInstr (Value ('TBigMap n1 n2)))
 -> TypeCheckInstr (Value ('TBigMap n1 n2)))
-> (HasNoBigMap n2 => TypeCheckInstr (Value ('TBigMap n1 n2)))
-> TypeCheckInstr (Value ('TBigMap n1 n2))
forall a b. (a -> b) -> a -> b
$
          Value ('TBigMap n1 n2) -> TypeCheckInstr (Value ('TBigMap n1 n2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TBigMap n1 n2) -> TypeCheckInstr (Value ('TBigMap n1 n2)))
-> Value ('TBigMap n1 n2)
-> TypeCheckInstr (Value ('TBigMap n1 n2))
forall a b. (a -> b) -> a -> b
$ Maybe Natural
-> Map (Value' Instr n1) (Value' Instr n2)
-> Value ('TBigMap n1 n2)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI v, Comparable k, HasNoBigMap v) =>
Maybe Natural
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap Maybe Natural
forall a. Maybe a
Nothing Map (Value' Instr n1) (Value' Instr n2)
forall k a. Map k a
M.empty

      (sq :: Value
sq@(U.ValueMap ((NonEmpty $ Elt ExpandedOp)
-> [Element (NonEmpty $ Elt ExpandedOp)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Elt ExpandedOp)]
mels)), s :: SingT tz
s@(STBigMap Sing n1
kt Sing n2
vt)) ->
        Sing n1
-> Value
-> Sing ('TBigMap n1 n2)
-> (Comparable n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing n1
kt Value
sq Sing ('TBigMap n1 n2)
SingT tz
s ((Comparable n1 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> Value
-> Sing ('TBigMap n1 n2)
-> (HasNoBigMap n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (HasNoBigMap a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withBigMapAbsence Sing n2
vt Value
sq Sing ('TBigMap n1 n2)
SingT tz
s ((HasNoBigMap n2 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (HasNoBigMap n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
          [(Value n1, Value n2)]
keyOrderedElts <- [Elt ExpandedOp]
-> Value
-> Sing n1
-> Sing n2
-> TypeCheckInstr [(Value n1, Value n2)]
forall (kt :: T) (vt :: T).
[Elt ExpandedOp]
-> Value
-> Sing kt
-> Sing vt
-> TypeCheckInstr [(Value kt, Value vt)]
typeCheckMapVal [Element (NonEmpty $ Elt ExpandedOp)]
[Elt ExpandedOp]
mels Value
sq Sing n1
kt Sing n2
vt
          Sing n1
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
kt ((SingI n1 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
vt ((SingI n2 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$
            Value' Instr ('TBigMap n1 n2)
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TBigMap n1 n2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TBigMap n1 n2)
 -> ReaderT
      TypeCheckInstrEnv TypeCheck (Value' Instr ('TBigMap n1 n2)))
-> Value' Instr ('TBigMap n1 n2)
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TBigMap n1 n2))
forall a b. (a -> b) -> a -> b
$ Maybe Natural
-> Map (Value n1) (Value n2) -> Value' Instr ('TBigMap n1 n2)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI v, Comparable k, HasNoBigMap v) =>
Maybe Natural
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap Maybe Natural
forall a. Maybe a
Nothing ([(Value n1, Value n2)] -> Map (Value n1) (Value n2)
forall k a. [(k, a)] -> Map k a
M.fromDistinctAscList [(Value n1, Value n2)]
keyOrderedElts)

      -- `{ {} }` can be typechecked either as `VLam` or `VList`.
      (U.ValueLambda NonEmpty ExpandedOp
s, STList Sing n
l) ->
        case NonEmpty ExpandedOp -> Maybe Value
emptyLambdaAsList NonEmpty ExpandedOp
s of
          Just Value
xs -> (Value, Sing tz) -> TypeCheckInstr (Value tz)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
xs, Sing tz
sng)
          Maybe Value
Nothing -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
uvalue (Sing n -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
l) Text
"" Maybe TCTypeError
forall a. Maybe a
Nothing

      (U.ValueSeq NonEmpty $ Value
s, STLambda Sing n1
_ Sing n2
_) -> case (NonEmpty $ Value) -> Maybe Value
emptyListAsLambda NonEmpty $ Value
s of
        Just Value
xs -> (Value, Sing tz) -> TypeCheckInstr (Value tz)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
xs, Sing tz
sng)
        Maybe Value
Nothing -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
uvalue (Sing ('TLambda n1 n2) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing tz
Sing ('TLambda n1 n2)
sng) Text
"" Maybe TCTypeError
forall a. Maybe a
Nothing

      (Value
v, STLambda (Sing n1
var :: Sing it) (Sing n2
b :: Sing ot)) -> Sing n1
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
var ((SingI n1 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n1 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
b ((SingI n2 => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n2 => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
        [ExpandedOp]
mp <- case Value
v of
          Value
U.ValueNil       -> [ExpandedOp] -> ReaderT TypeCheckInstrEnv TypeCheck [ExpandedOp]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
          U.ValueLambda NonEmpty ExpandedOp
mp -> [ExpandedOp] -> ReaderT TypeCheckInstrEnv TypeCheck [ExpandedOp]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ExpandedOp] -> ReaderT TypeCheckInstrEnv TypeCheck [ExpandedOp])
-> [ExpandedOp] -> ReaderT TypeCheckInstrEnv TypeCheck [ExpandedOp]
forall a b. (a -> b) -> a -> b
$ NonEmpty ExpandedOp -> [Element (NonEmpty ExpandedOp)]
forall t. Container t => t -> [Element t]
toList NonEmpty ExpandedOp
mp
          Value
_ -> Value
-> T
-> Text
-> Maybe TCTypeError
-> ReaderT TypeCheckInstrEnv TypeCheck [ExpandedOp]
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @ty) Text
"unexpected value" Maybe TCTypeError
forall a. Maybe a
Nothing
        HST '[n1]
_ :/ SomeInstrOut '[n1]
instr <-
          forall (t :: T) a.
SingI t =>
Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP @it Value
uvalue ((WellTyped n1 => TypeCheckInstr (SomeInstr '[n1]))
 -> TypeCheckInstr (SomeInstr '[n1]))
-> (WellTyped n1 => TypeCheckInstr (SomeInstr '[n1]))
-> TypeCheckInstr (SomeInstr '[n1])
forall a b. (a -> b) -> a -> b
$ TypeCheckInstrNoExcept (TypeCheckedSeq '[n1])
-> TypeCheckInstr (SomeInstr '[n1])
forall (inp :: [T]).
TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstr (SomeInstr inp)
throwingTCError (TypeCheckInstrNoExcept (TypeCheckedSeq '[n1])
 -> TypeCheckInstr (SomeInstr '[n1]))
-> TypeCheckInstrNoExcept (TypeCheckedSeq '[n1])
-> TypeCheckInstr (SomeInstr '[n1])
forall a b. (a -> b) -> a -> b
$
            TcInstrHandler
-> [ExpandedOp]
-> HST '[n1]
-> TypeCheckInstrNoExcept (TypeCheckedSeq '[n1])
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl
              -- lambdas can contain operations forbidden inside views, hence
              -- we invent a "not in view" constraint here.
              ((IsNotInView =>
 ExpandedInstr
 -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> ExpandedInstr
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall r. (IsNotInView => r) -> r
giveNotInView ((IsNotInView =>
  ExpandedInstr
  -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
 -> ExpandedInstr
 -> HST inp
 -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> (IsNotInView =>
    ExpandedInstr
    -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> ExpandedInstr
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a b. (a -> b) -> a -> b
$ (TypeCheckInstrEnv -> TypeCheckInstrEnv)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (ASetter
  TypeCheckInstrEnv
  TypeCheckInstrEnv
  (Maybe (Dict IsNotInView))
  (Maybe (Dict IsNotInView))
-> Maybe (Dict IsNotInView)
-> TypeCheckInstrEnv
-> TypeCheckInstrEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter
  TypeCheckInstrEnv
  TypeCheckInstrEnv
  (Maybe (Dict IsNotInView))
  (Maybe (Dict IsNotInView))
Lens' TypeCheckInstrEnv (Maybe (Dict IsNotInView))
tcieNotInView (Maybe (Dict IsNotInView)
 -> TypeCheckInstrEnv -> TypeCheckInstrEnv)
-> Maybe (Dict IsNotInView)
-> TypeCheckInstrEnv
-> TypeCheckInstrEnv
forall a b. (a -> b) -> a -> b
$ Dict IsNotInView -> Maybe (Dict IsNotInView)
forall a. a -> Maybe a
Just Dict IsNotInView
forall (a :: Constraint). a => Dict a
Dict) (TypeCheckInstrNoExcept (TypeCheckedSeq inp)
 -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> (ExpandedInstr
    -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp))
-> ExpandedInstr
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
forall a b c. SuperComposition a b c => a -> b -> c
... ExpandedInstr
-> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
TcInstrHandler
tcDo)
              [ExpandedOp]
mp
              ((forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @it, Dict (WellTyped n1)
forall (a :: Constraint). a => Dict a
Dict) (SingT n1, Dict (WellTyped n1)) -> HST '[] -> HST '[n1]
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST '[]
SNil)
        case SomeInstrOut '[n1]
instr of
          Instr '[n1] out
lam ::: (HST out
lo :: HST lo) -> forall (t :: T) a.
SingI t =>
Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP @ot Value
uvalue ((WellTyped n2 =>
  ReaderT
    TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2)))
 -> ReaderT
      TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2)))
-> (WellTyped n2 =>
    ReaderT
      TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2)))
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2))
forall a b. (a -> b) -> a -> b
$ do
            case forall (t :: T) (st :: [T]).
(SingI st, WellTyped t) =>
HST st -> Either TCTypeError (st :~: '[t])
eqHST1 @ot HST out
lo of
              Right out :~: '[n2]
Refl -> do
                Value' Instr ('TLambda n1 n2)
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TLambda n1 n2)
 -> ReaderT
      TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2)))
-> Value' Instr ('TLambda n1 n2)
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2))
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[n1] '[n2])
-> Value' Instr ('TLambda n1 n2)
forall (t :: T) (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(t ~ 'TLambda inp out, SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
(IsNotInView => RemFail instr '[inp] '[out]) -> Value' instr t
T.mkVLam (Instr '[n1] out -> RemFail Instr '[n1] out
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
T.RfNormal Instr '[n1] out
lam)
              Left TCTypeError
m ->
                Value
-> T
-> Text
-> Maybe TCTypeError
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2))
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @ty)
                        Text
"wrong output type of lambda's value:" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
m)
          AnyOutInstr forall (out :: [T]). Instr '[n1] out
lam ->
            Value' Instr ('TLambda n1 n2)
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TLambda n1 n2)
 -> ReaderT
      TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2)))
-> Value' Instr ('TLambda n1 n2)
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TLambda n1 n2))
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[n1] '[n2])
-> Value' Instr ('TLambda n1 n2)
forall (t :: T) (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(t ~ 'TLambda inp out, SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
(IsNotInView => RemFail instr '[inp] '[out]) -> Value' instr t
T.mkVLam ((forall (out :: [T]). Instr '[n1] out) -> RemFail Instr '[n1] '[n2]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
T.RfAlwaysFails forall (out :: [T]). Instr '[n1] out
lam)

      (v :: Value
v@(U.ValueBytes (U.InternalByteString ByteString
bs)), SingT tz
STChest) ->
        case ByteString -> Either Text Chest
chestFromBytes ByteString
bs of
          Right Chest
res -> Value' Instr 'TChest
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChest)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChest
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChest))
-> Value' Instr 'TChest
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChest)
forall a b. (a -> b) -> a -> b
$ Chest -> Value' Instr 'TChest
forall (instr :: [T] -> [T] -> *). Chest -> Value' instr 'TChest
VChest Chest
res
          Left Text
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v T
T.TChest Text
err Maybe TCTypeError
forall a. Maybe a
Nothing

      (v :: Value
v@(U.ValueBytes (U.InternalByteString ByteString
bs)), SingT tz
STChestKey) ->
        case ByteString -> Either Text ChestKey
chestKeyFromBytes ByteString
bs of
          Right ChestKey
res -> Value' Instr 'TChestKey
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChestKey)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChestKey
 -> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChestKey))
-> Value' Instr 'TChestKey
-> ReaderT TypeCheckInstrEnv TypeCheck (Value' Instr 'TChestKey)
forall a b. (a -> b) -> a -> b
$ ChestKey -> Value' Instr 'TChestKey
forall (instr :: [T] -> [T] -> *).
ChestKey -> Value' instr 'TChestKey
VChestKey ChestKey
res
          Left Text
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v T
T.TChestKey Text
err Maybe TCTypeError
forall a. Maybe a
Nothing

      (Value
v, t :: SingT tz
t@(STSaplingState Sing n
_)) -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing ('TSaplingState n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing ('TSaplingState n)
SingT tz
t)
        Text
"sapling_state is not supported" Maybe TCTypeError
forall a. Maybe a
Nothing

      (Value
v, t :: SingT tz
t@(STSaplingTransaction Sing n
_)) -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing ('TSaplingTransaction n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing ('TSaplingTransaction n)
SingT tz
t)
        Text
"sapling_transaction is not supported" Maybe TCTypeError
forall a. Maybe a
Nothing

      (Value
v, SingT tz
t) -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing tz -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing tz
SingT tz
t) Text
"unknown value" Maybe TCTypeError
forall a. Maybe a
Nothing

    seqToRightCombedPair :: (NonEmpty $ U.Value) -> U.Value
    seqToRightCombedPair :: (NonEmpty $ Value) -> Value
seqToRightCombedPair (Value
x :| [Value
y]) = Value -> Value -> Value
forall op. Value' op -> Value' op -> Value' op
U.ValuePair Value
x Value
y
    seqToRightCombedPair (Value
x :| [Value]
xs) = Value -> Value -> Value
forall op. Value' op -> Value' op -> Value' op
U.ValuePair Value
x (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$ (NonEmpty $ Value) -> Value
seqToRightCombedPair ([Value] -> NonEmpty $ Value
forall a. [a] -> NonEmpty a
NE.fromList [Value]
xs)

    -- Converts a lambda containing only empty 'SeqEx's (possibly nested)
    -- to a list of empty lists.
    emptyLambdaAsList :: NonEmpty U.ExpandedOp -> Maybe U.Value
    emptyLambdaAsList :: NonEmpty ExpandedOp -> Maybe Value
emptyLambdaAsList NonEmpty ExpandedOp
ops =
      let
        opToMaybeList :: U.ExpandedOp -> Maybe U.Value
        opToMaybeList :: ExpandedOp -> Maybe Value
opToMaybeList = \case
          U.SeqEx []      -> Value -> Maybe Value
forall a. a -> Maybe a
Just Value
forall op. Value' op
U.ValueNil
          U.SeqEx [ExpandedOp]
xs      -> (NonEmpty $ Value) -> Value
forall op. (NonEmpty $ Value' op) -> Value' op
U.ValueSeq ((NonEmpty $ Value) -> Value)
-> ([Value] -> NonEmpty $ Value) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> NonEmpty $ Value
forall a. [a] -> NonEmpty a
NE.fromList ([Value] -> Value) -> Maybe [Value] -> Maybe Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExpandedOp -> Maybe Value) -> [ExpandedOp] -> Maybe [Value]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ExpandedOp -> Maybe Value
opToMaybeList [ExpandedOp]
xs
          U.PrimEx {}     -> Maybe Value
forall a. Maybe a
Nothing
          U.WithSrcEx ErrorSrcPos
_ ExpandedOp
i -> ExpandedOp -> Maybe Value
opToMaybeList ExpandedOp
i
      in
        (NonEmpty $ Value) -> Value
forall op. (NonEmpty $ Value' op) -> Value' op
U.ValueSeq ((NonEmpty $ Value) -> Value)
-> Maybe (NonEmpty $ Value) -> Maybe Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExpandedOp -> Maybe Value)
-> NonEmpty ExpandedOp -> Maybe (NonEmpty $ Value)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ExpandedOp -> Maybe Value
opToMaybeList NonEmpty ExpandedOp
ops

    -- Converts a list containing only empty lists (possibly nested)
    -- to a lambda of empty 'SeqEx's.
    emptyListAsLambda :: NonEmpty U.Value -> Maybe U.Value
    emptyListAsLambda :: (NonEmpty $ Value) -> Maybe Value
emptyListAsLambda NonEmpty $ Value
ops =
      let
        listToMaybeOp :: U.Value -> Maybe U.ExpandedOp
        listToMaybeOp :: Value -> Maybe ExpandedOp
listToMaybeOp = \case
          Value
U.ValueNil      -> ExpandedOp -> Maybe ExpandedOp
forall a. a -> Maybe a
Just (ExpandedOp -> Maybe ExpandedOp) -> ExpandedOp -> Maybe ExpandedOp
forall a b. (a -> b) -> a -> b
$ [ExpandedOp] -> ExpandedOp
U.SeqEx []
          U.ValueSeq NonEmpty $ Value
xs   -> [ExpandedOp] -> ExpandedOp
U.SeqEx ([ExpandedOp] -> ExpandedOp)
-> (NonEmpty ExpandedOp -> [ExpandedOp])
-> NonEmpty ExpandedOp
-> ExpandedOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty ExpandedOp -> [ExpandedOp]
forall t. Container t => t -> [Element t]
toList (NonEmpty ExpandedOp -> ExpandedOp)
-> Maybe (NonEmpty ExpandedOp) -> Maybe ExpandedOp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Maybe ExpandedOp)
-> (NonEmpty $ Value) -> Maybe (NonEmpty ExpandedOp)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Value -> Maybe ExpandedOp
listToMaybeOp NonEmpty $ Value
xs
          Value
_               -> Maybe ExpandedOp
forall a. Maybe a
Nothing
      in
        NonEmpty ExpandedOp -> Value
forall op. NonEmpty op -> Value' op
U.ValueLambda (NonEmpty ExpandedOp -> Value)
-> Maybe (NonEmpty ExpandedOp) -> Maybe Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Maybe ExpandedOp)
-> (NonEmpty $ Value) -> Maybe (NonEmpty ExpandedOp)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Value -> Maybe ExpandedOp
listToMaybeOp NonEmpty $ Value
ops

    withWTP
      :: forall t a. SingI t
      => U.Value
      -> (T.WellTyped t => TypeCheckInstr a)
      -> TypeCheckInstr a
    withWTP :: forall (t :: T) a.
SingI t =>
Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP Value
uvalue WellTyped t => TypeCheckInstr a
fn = case forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
T.getWTP @t of
      Right Dict (WellTyped t)
Dict -> TypeCheckInstr a
WellTyped t => TypeCheckInstr a
fn
      Left NotWellTyped
err -> Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
uvalue (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @ty) (NotWellTyped -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty NotWellTyped
err) Maybe TCTypeError
forall a. Maybe a
Nothing

    typeCheckValsImpl
      :: ([U.Value], Sing t)
      -> TypeCheckInstr [T.Value t]
    typeCheckValsImpl :: forall (t :: T). ([Value], Sing t) -> TypeCheckInstr [Value t]
typeCheckValsImpl ([Value]
mvs, Sing t
sng) =
      ([Value t] -> [Value t])
-> ReaderT TypeCheckInstrEnv TypeCheck [Value t]
-> ReaderT TypeCheckInstrEnv TypeCheck [Value t]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Value t] -> [Value t]
forall a. [a] -> [a]
reverse (ReaderT TypeCheckInstrEnv TypeCheck [Value t]
 -> ReaderT TypeCheckInstrEnv TypeCheck [Value t])
-> ReaderT TypeCheckInstrEnv TypeCheck [Value t]
-> ReaderT TypeCheckInstrEnv TypeCheck [Value t]
forall a b. (a -> b) -> a -> b
$ ([Value t]
 -> Value -> ReaderT TypeCheckInstrEnv TypeCheck [Value t])
-> [Value t]
-> [Value]
-> ReaderT TypeCheckInstrEnv TypeCheck [Value t]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\[Value t]
res Value
mv -> (Value t -> [Value t] -> [Value t]
forall a. a -> [a] -> [a]
: [Value t]
res) (Value t -> [Value t])
-> ReaderT TypeCheckInstrEnv TypeCheck (Value t)
-> ReaderT TypeCheckInstrEnv TypeCheck [Value t]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Value, Sing t) -> ReaderT TypeCheckInstrEnv TypeCheck (Value t)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
mv, Sing t
sng))) [] [Value]
mvs

    -- Typechecks given list of @Elt@s and ensures that its keys are in ascending order.
    --
    -- It return list of pairs (key, value) with keys in ascending order
    -- so it is safe to call @fromDistinctAscList@ on returned list
    typeCheckMapVal
      :: [U.Elt U.ExpandedOp]
      -> U.Value
      -> Sing kt
      -> Sing vt
      -> TypeCheckInstr [(T.Value kt, T.Value vt)]
    typeCheckMapVal :: forall (kt :: T) (vt :: T).
[Elt ExpandedOp]
-> Value
-> Sing kt
-> Sing vt
-> TypeCheckInstr [(Value kt, Value vt)]
typeCheckMapVal [Elt ExpandedOp]
mels Value
sq Sing kt
kt Sing vt
vt = Sing kt
-> Value
-> Sing kt
-> (Comparable kt => TypeCheckInstr [(Value kt, Value vt)])
-> TypeCheckInstr [(Value kt, Value vt)]
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing kt
kt Value
sq Sing kt
kt ((Comparable kt => TypeCheckInstr [(Value kt, Value vt)])
 -> TypeCheckInstr [(Value kt, Value vt)])
-> (Comparable kt => TypeCheckInstr [(Value kt, Value vt)])
-> TypeCheckInstr [(Value kt, Value vt)]
forall a b. (a -> b) -> a -> b
$ do
      ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT TypeCheckInstrEnv TypeCheck ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
      [Value kt]
ks <- ([Value], Sing kt) -> TypeCheckInstr [Value kt]
forall (t :: T). ([Value], Sing t) -> TypeCheckInstr [Value t]
typeCheckValsImpl ((Elt ExpandedOp -> Value) -> [Elt ExpandedOp] -> [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (\(U.Elt Value
k Value
_) -> Value
k) [Elt ExpandedOp]
mels, Sing kt
kt)
      [Value vt]
vals <- ([Value], Sing vt) -> TypeCheckInstr [Value vt]
forall (t :: T). ([Value], Sing t) -> TypeCheckInstr [Value t]
typeCheckValsImpl ((Elt ExpandedOp -> Value) -> [Elt ExpandedOp] -> [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (\(U.Elt Value
_ Value
v) -> Value
v) [Elt ExpandedOp]
mels, Sing vt
vt)
      [Value kt]
ksS <- Either TCError [Value kt] -> TypeCheckInstr [Value kt]
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError [Value kt] -> TypeCheckInstr [Value kt])
-> Either TCError [Value kt] -> TypeCheckInstr [Value kt]
forall a b. (a -> b) -> a -> b
$ (Value kt -> Value kt) -> [Value kt] -> Either Text [Value kt]
forall b a.
(Ord b, Buildable a) =>
(a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc Value kt -> Value kt
forall a. a -> a
id [Value kt]
ks
            Either Text [Value kt]
-> (Text -> TCError) -> Either TCError [Value kt]
forall (p :: * -> * -> *) a c b.
Bifunctor p =>
p a c -> (a -> b) -> p b c
`onFirst` \Text
msg -> Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
sq (Sing kt -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing kt
kt) Text
msg ErrorSrcPos
instrPos Maybe TCTypeError
forall a. Maybe a
Nothing
      pure $ [Value kt] -> [Value vt] -> [(Value kt, Value vt)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Value kt]
ksS [Value vt]
vals

    typecheckContractValue
      :: forall cp tz. (tz ~ 'T.TContract cp)
      => U.Value -> EpAddress -> Sing cp -> TypeCheckInstr (T.Value tz)
    typecheckContractValue :: forall (cp :: T) (tz :: T).
(tz ~ 'TContract cp) =>
Value -> EpAddress -> Sing cp -> TypeCheckInstr (Value tz)
typecheckContractValue Value
cv (EpAddress Address
addr EpName
epName) Sing cp
pc = do

      ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT TypeCheckInstrEnv TypeCheck ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
      let ensureTypeMatches :: forall t'. SingI t' => TypeCheckInstr (cp :~: t')
          ensureTypeMatches :: forall (t' :: T). SingI t' => TypeCheckInstr (cp :~: t')
ensureTypeMatches = forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither @_ @TypeCheckInstr (Either TCError (cp :~: t') -> TypeCheckInstr (cp :~: t'))
-> Either TCError (cp :~: t') -> TypeCheckInstr (cp :~: t')
forall a b. (a -> b) -> a -> b
$
            (TCTypeError -> TCError)
-> Either TCTypeError (cp :~: t') -> Either TCError (cp :~: t')
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
cv (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @ty) Text
"wrong contract parameter" ErrorSrcPos
instrPos (Maybe TCTypeError -> TCError)
-> (TCTypeError -> Maybe TCTypeError) -> TCTypeError -> TCError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just) (Either TCTypeError (cp :~: t') -> Either TCError (cp :~: t'))
-> Either TCTypeError (cp :~: t') -> Either TCError (cp :~: t')
forall a b. (a -> b) -> a -> b
$
              (Sing cp
-> (SingI cp => Either TCTypeError (cp :~: t'))
-> Either TCTypeError (cp :~: t')
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing cp
pc ((SingI cp => Either TCTypeError (cp :~: t'))
 -> Either TCTypeError (cp :~: t'))
-> (SingI cp => Either TCTypeError (cp :~: t'))
-> Either TCTypeError (cp :~: t')
forall a b. (a -> b) -> a -> b
$ forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @cp @t')
      let unsupportedType :: T.BadTypeForScope -> TCError
          unsupportedType :: BadTypeForScope -> TCError
unsupportedType BadTypeForScope
reason = Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
cv (Sing cp -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing cp
pc)
            Text
"Unsupported type in type argument of 'contract' type" ErrorSrcPos
instrPos (Maybe TCTypeError -> TCError) -> Maybe TCTypeError -> TCError
forall a b. (a -> b) -> a -> b
$
              TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ T -> BadTypeForScope -> TCTypeError
UnsupportedTypeForScope (Sing cp -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing cp
pc) BadTypeForScope
reason
      case Address
addr of
        KeyAddress Hash 'HashKindPublicKey
_ -> do
          cp :~: 'TUnit
Refl <- forall (t' :: T). SingI t' => TypeCheckInstr (cp :~: t')
ensureTypeMatches @'T.TUnit
          Value' Instr ('TContract 'TUnit)
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TContract 'TUnit))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TContract 'TUnit)
 -> ReaderT
      TypeCheckInstrEnv TypeCheck (Value' Instr ('TContract 'TUnit)))
-> Value' Instr ('TContract 'TUnit)
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TContract 'TUnit))
forall a b. (a -> b) -> a -> b
$ Address
-> SomeEntrypointCallT 'TUnit -> Value' Instr ('TContract 'TUnit)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, HasNoOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract Address
addr SomeEntrypointCallT 'TUnit
forall (t :: T).
(ParameterScope t, ForbidOr t) =>
SomeEntrypointCallT t
T.sepcPrimitive
        ContractAddress ContractHash
ca -> case Maybe TcOriginatedContracts
mOriginatedContracts of
          Maybe TcOriginatedContracts
Nothing -> Either TCError (Value tz) -> TypeCheckInstr (Value tz)
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError (Value tz) -> TypeCheckInstr (Value tz))
-> (TCError -> Either TCError (Value tz))
-> TCError
-> TypeCheckInstr (Value tz)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCError -> Either TCError (Value tz)
forall a b. a -> Either a b
Left (TCError -> TypeCheckInstr (Value tz))
-> TCError -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ BadTypeForScope -> TCError
unsupportedType BadTypeForScope
T.BtHasContract
          Just TcOriginatedContracts
originatedContracts -> case ContractHash -> TcOriginatedContracts -> Maybe SomeParamType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ContractHash
ca TcOriginatedContracts
originatedContracts of
            Just (SomeParamType ParamNotes t
paramNotes) ->
              case EpName -> ParamNotes t -> Maybe (MkEntrypointCallRes t)
forall (param :: T).
ParameterScope param =>
EpName -> ParamNotes param -> Maybe (MkEntrypointCallRes param)
T.mkEntrypointCall EpName
epName ParamNotes t
paramNotes of
                Maybe (MkEntrypointCallRes t)
Nothing ->
                  TCError -> TypeCheckInstr (Value tz)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TypeCheckInstr (Value tz))
-> TCError -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$
                  Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
cv (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @ty) Text
"unknown entrypoint" ErrorSrcPos
instrPos (Maybe TCTypeError -> TCError)
-> (TCTypeError -> Maybe TCTypeError) -> TCTypeError -> TCError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> TCError) -> TCTypeError -> TCError
forall a b. (a -> b) -> a -> b
$
                  EpName -> TCTypeError
EntrypointNotFound EpName
epName
                Just (T.MkEntrypointCallRes (Notes arg
_ :: Notes t') EntrypointCallT t arg
epc) -> do
                  cp :~: arg
Refl <- forall (t' :: T). SingI t' => TypeCheckInstr (cp :~: t')
ensureTypeMatches @t'
                  Value' Instr ('TContract arg)
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TContract arg))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TContract arg)
 -> ReaderT
      TypeCheckInstrEnv TypeCheck (Value' Instr ('TContract arg)))
-> Value' Instr ('TContract arg)
-> ReaderT
     TypeCheckInstrEnv TypeCheck (Value' Instr ('TContract arg))
forall a b. (a -> b) -> a -> b
$ Address -> SomeEntrypointCallT arg -> Value' Instr ('TContract arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, HasNoOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract Address
addr (EntrypointCallT t arg -> SomeEntrypointCallT arg
forall (arg :: T) (param :: T).
ParameterScope param =>
EntrypointCallT param arg -> SomeEntrypointCallT arg
T.SomeEpc EntrypointCallT t arg
epc)
            Maybe SomeParamType
Nothing ->
              TCError -> TypeCheckInstr (Value tz)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TypeCheckInstr (Value tz))
-> TCError -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
cv (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @ty) Text
"Contract literal unknown"
                ErrorSrcPos
instrPos (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ Address -> TCTypeError
UnknownContract Address
addr)
        TransactionRollupAddress TxRollupHash
_ ->
          TCError -> TypeCheckInstr (Value tz)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TypeCheckInstr (Value tz))
-> TCError -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
cv (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @ty) Text
"txr1 address passed as contract"
                ErrorSrcPos
instrPos (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ Address -> TCTypeError
UnknownContract Address
addr)

withComparable
  :: forall a (t :: T.T) ty. Sing a
  -> U.Value
  -> Sing t
  -> (T.Comparable a => TypeCheckInstr ty)
  -> TypeCheckInstr ty
withComparable :: forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing a
s Value
uv Sing t
t Comparable a => TypeCheckInstr ty
act = case Sing a -> Maybe (Dict (Comparable a))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
T.getComparableProofS Sing a
s of
  Just Dict (Comparable a)
Dict -> TypeCheckInstr ty
Comparable a => TypeCheckInstr ty
act
  Maybe (Dict (Comparable a))
Nothing -> do
    ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT TypeCheckInstrEnv TypeCheck ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
    Either TCError ty -> TypeCheckInstr ty
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError ty -> TypeCheckInstr ty)
-> (TCError -> Either TCError ty) -> TCError -> TypeCheckInstr ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCError -> Either TCError ty
forall a b. a -> Either a b
Left (TCError -> TypeCheckInstr ty) -> TCError -> TypeCheckInstr ty
forall a b. (a -> b) -> a -> b
$
      Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
uv (Sing t -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
t) Text
"Require a comparable type here" ErrorSrcPos
instrPos Maybe TCTypeError
forall a. Maybe a
Nothing

withBigMapAbsence
  :: forall a (t :: T.T) ty. Sing a
  -> U.Value
  -> Sing t
  -> (T.HasNoBigMap a => TypeCheckInstr ty)
  -> TypeCheckInstr ty
withBigMapAbsence :: forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (HasNoBigMap a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withBigMapAbsence Sing a
s Value
uv Sing t
t HasNoBigMap a => TypeCheckInstr ty
act = case Sing a -> Maybe (Dict $ HasNoBigMap a)
forall (t :: T). Sing t -> Maybe (Dict $ HasNoBigMap t)
T.bigMapAbsense Sing a
s of
  Just Dict $ HasNoBigMap a
Dict -> TypeCheckInstr ty
HasNoBigMap a => TypeCheckInstr ty
act
  Maybe (Dict $ HasNoBigMap a)
Nothing -> do
    ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT TypeCheckInstrEnv TypeCheck ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos
    Either TCError ty -> TypeCheckInstr ty
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError ty -> TypeCheckInstr ty)
-> (TCError -> Either TCError ty) -> TCError -> TypeCheckInstr ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCError -> Either TCError ty
forall a b. a -> Either a b
Left (TCError -> TypeCheckInstr ty) -> TCError -> TypeCheckInstr ty
forall a b. (a -> b) -> a -> b
$
      Value -> T -> Text -> ErrorSrcPos -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
uv (Sing t -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing t
t) Text
"Require a type which doesn't contain `big_map` here"
        ErrorSrcPos
instrPos Maybe TCTypeError
forall a. Maybe a
Nothing