module Morley.Michelson.TypeCheck.Value
( typeCheckValImpl
, tcFailedOnValue
) where
import Control.Monad.Except (liftEither, throwError)
import Data.Constraint (Dict(..))
import Data.Default (def)
import qualified Data.List.NonEmpty as NE
import qualified Data.Map as M
import qualified Data.Set 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(..),
throwingTCError)
import Morley.Michelson.TypeCheck.Types
import Morley.Michelson.Typed (EpAddress(..), Notes(..), SingT(..), Value'(..), starNotes)
import qualified Morley.Michelson.Typed as T
import qualified Morley.Michelson.Untyped as U
import Morley.Tezos.Address (Address(..))
import Morley.Tezos.Core
import Morley.Tezos.Crypto
import qualified Morley.Tezos.Crypto.BLS12381 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 :: Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v T
t Text
msg Maybe TCTypeError
err = do
InstrCallStack
loc <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
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 -> InstrCallStack -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
v T
t Text
msg InstrCallStack
loc Maybe TCTypeError
err
typeCheckValImpl
:: forall ty.
SingI ty
=> Maybe TcOriginatedContracts
-> TcInstrHandler
-> U.Value
-> TypeCheckInstr (T.Value ty)
typeCheckValImpl :: 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, SingI ty => Sing ty
forall k (a :: k). SingI a => Sing a
sing @ty)
where
doTypeCheckVal :: forall tz. (U.Value, Sing tz) -> TypeCheckInstr (T.Value tz)
doTypeCheckVal :: (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 InstrCallStack TypeCheck (Value' Instr 'TInt)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TInt
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TInt))
-> Value' Instr 'TInt
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TNat)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TNat
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TNat))
-> Value' Instr 'TNat
-> ReaderT InstrCallStack 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, Bits i) => i -> Either Text Mutez
mkMutez Integer
i of
Right Mutez
m -> Value' Instr 'TMutez
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TMutez)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TMutez
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TMutez))
-> Value' Instr 'TMutez
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TString
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TString))
-> Value' Instr 'TString
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TAddress)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TAddress
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TAddress))
-> Value' Instr 'TAddress
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TAddress)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TAddress
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TAddress))
-> Value' Instr 'TAddress
-> ReaderT InstrCallStack 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 KeyHash
parseKeyHash (MText -> Text
unMText MText
s) of
Right KeyHash
kHash -> Value' Instr 'TKeyHash
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TKeyHash)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKeyHash
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TKeyHash))
-> Value' Instr 'TKeyHash
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TKeyHash)
forall a b. (a -> b) -> a -> b
$ KeyHash -> Value' Instr 'TKeyHash
forall (instr :: [T] -> [T] -> *).
KeyHash -> Value' instr 'TKeyHash
VKeyHash KeyHash
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 KeyHash
parseKeyHashRaw (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
Right KeyHash
kHash -> Value' Instr 'TKeyHash
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TKeyHash)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKeyHash
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TKeyHash))
-> Value' Instr 'TKeyHash
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TKeyHash)
forall a b. (a -> b) -> a -> b
$ KeyHash -> Value' Instr 'TKeyHash
forall (instr :: [T] -> [T] -> *).
KeyHash -> Value' instr 'TKeyHash
VKeyHash KeyHash
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)
(U.ValueInt Integer
i, SingT tz
STBls12381Fr) ->
Value' Instr 'TBls12381Fr
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TBls12381Fr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381Fr
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TBls12381Fr))
-> Value' Instr 'TBls12381Fr
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' Instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (Integer -> Bls12381Fr
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 InstrCallStack TypeCheck (Value' Instr 'TBls12381Fr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381Fr
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TBls12381Fr))
-> Value' Instr 'TBls12381Fr
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TBls12381G1)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381G1
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TBls12381G1))
-> Value' Instr 'TBls12381G1
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TBls12381G2)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381G2
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TBls12381G2))
-> Value' Instr 'TBls12381G2
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TTimestamp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTimestamp
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TTimestamp))
-> Value' Instr 'TTimestamp
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TTimestamp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTimestamp
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TTimestamp))
-> Value' Instr 'TTimestamp
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TBytes)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBytes
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TBytes))
-> Value' Instr 'TBytes
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TBool)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBool
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TBool))
-> Value' Instr 'TBool
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TBool)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBool
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TBool))
-> Value' Instr 'TBool
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TKey)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKey
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TKey))
-> Value' Instr 'TKey
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TKey)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKey
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TKey))
-> Value' Instr 'TKey
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TSignature)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TSignature
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TSignature))
-> Value' Instr 'TSignature
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TSignature)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TSignature
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TSignature))
-> Value' Instr 'TSignature
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TChainId)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChainId
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TChainId))
-> Value' Instr 'TChainId
-> ReaderT InstrCallStack 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 -> Maybe ChainId
mkChainId (ByteString -> Maybe ChainId)
-> (InternalByteString -> ByteString)
-> InternalByteString
-> Maybe ChainId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InternalByteString -> ByteString
U.unInternalByteString -> Just ChainId
ci), SingT tz
STChainId) ->
Value' Instr 'TChainId
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TChainId)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChainId
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TChainId))
-> Value' Instr 'TChainId
-> ReaderT InstrCallStack 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 InstrCallStack 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 InstrCallStack TypeCheck Bool
-> (Bool -> TypeCheckInstr (Value tz)) -> TypeCheckInstr (Value tz)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
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 InstrCallStack 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 InstrCallStack 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 InstrCallStack TypeCheck ()
-> ReaderT InstrCallStack TypeCheck ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (EpName -> Bool
U.isDefEpName EpName
ep) (ReaderT InstrCallStack TypeCheck ()
-> ReaderT InstrCallStack TypeCheck ())
-> ReaderT InstrCallStack TypeCheck ()
-> ReaderT InstrCallStack TypeCheck ()
forall a b. (a -> b) -> a -> b
$
Value
-> T
-> Text
-> Maybe TCTypeError
-> ReaderT InstrCallStack 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
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 InstrCallStack TypeCheck (Value' Instr 'TUnit)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TUnit
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TUnit))
-> Value' Instr 'TUnit
-> ReaderT InstrCallStack 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 n
lt Sing n
rt) -> do
Value n
l <- (Value, Sing n) -> TypeCheckInstr (Value n)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
ml, Sing n
lt)
Value n
r <- (Value, Sing n) -> TypeCheckInstr (Value n)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
mr, Sing n
rt)
pure $ (Value n, Value n) -> Value' Instr ('TPair n n)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value n
l, Value n
r)
(U.ValueLeft Value
ml, STOr Sing n
lt Sing n
rt) -> do
Value n
l <- (Value, Sing n) -> TypeCheckInstr (Value n)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
ml, Sing n
lt)
Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
lt ((SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
rt ((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 ('TOr n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOr n n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TOr n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOr n n)))
-> Value' Instr ('TOr n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOr n n))
forall a b. (a -> b) -> a -> b
$ Either (Value n) (Value' Instr n) -> Value' Instr ('TOr n n)
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 n -> Either (Value n) (Value' Instr n)
forall a b. a -> Either a b
Left Value n
l)
(U.ValueRight Value
mr, STOr Sing n
lt Sing n
rt) -> do
Value n
r <- (Value, Sing n) -> TypeCheckInstr (Value n)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
mr, Sing n
rt)
Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
lt ((SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
rt ((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 ('TOr n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOr n n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TOr n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOr n n)))
-> Value' Instr ('TOr n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOr n n))
forall a b. (a -> b) -> a -> b
$ Either (Value' Instr n) (Value n) -> Value' Instr ('TOr n n)
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 n -> Either (Value' Instr n) (Value n)
forall a b. b -> Either a b
Right Value n
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 InstrCallStack TypeCheck (Value' Instr ('TOption n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TOption n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOption n)))
-> Value' Instr ('TOption n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOption n))
forall a b. (a -> b) -> a -> b
$ Maybe (Value n) -> Value' Instr ('TOption n)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
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 InstrCallStack TypeCheck (Value' Instr ('TOption n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TOption n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOption n)))
-> Value' Instr ('TOption n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOption n))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' Instr n) -> Value' Instr ('TOption n)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
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 InstrCallStack TypeCheck (Value' Instr ('TList n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TList n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TList n)))
-> Value' Instr ('TList n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TList n))
forall a b. (a -> b) -> a -> b
$ [Value' Instr n] -> Value' Instr ('TList n)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
[Value' instr t] -> Value' instr ('TList t)
T.VList []
(U.ValueSeq vals :: NonEmpty $ Value
vals@(Value
_ :| (Value
_ : [Value]
_)), STPair Sing n
_ Sing n
_) ->
(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 InstrCallStack TypeCheck (Value' Instr ('TList n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TList n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TList n)))
-> Value' Instr ('TList n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TList n))
forall a b. (a -> b) -> a -> b
$ [Value n] -> Value' Instr ('TList n)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value n]
els
(Value
U.ValueNil, STSet Sing n
s) -> do
InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
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 InstrCallStack TypeCheck (Value' Instr ('TSet n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Value' Instr n) -> Value' Instr ('TSet n)
forall (t :: T) (instr :: [T] -> [T] -> *).
(SingI t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
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 -> InstrCallStack -> 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"
InstrCallStack
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
InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
[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 InstrCallStack TypeCheck (Set (Value n))
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError (Set (Value n))
-> ReaderT InstrCallStack TypeCheck (Set (Value n)))
-> Either TCError (Set (Value n))
-> ReaderT InstrCallStack 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, Show 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 -> InstrCallStack -> 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 InstrCallStack
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 InstrCallStack TypeCheck (Value' Instr ('TSet n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TSet n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TSet n)))
-> Value' Instr ('TSet n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TSet n))
forall a b. (a -> b) -> a -> b
$ Set (Value n) -> Value' Instr ('TSet n)
forall (t :: T) (instr :: [T] -> [T] -> *).
(SingI t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
VSet Set (Value n)
elsS
(v :: Value
v@Value
U.ValueNil, s :: SingT tz
s@(STMap Sing n
st Sing n
vt)) ->
Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
st ((SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ 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
$ Sing n
-> Value
-> Sing ('TMap n n)
-> (Comparable n => TypeCheckInstr (Value ('TMap n n)))
-> TypeCheckInstr (Value ('TMap n n))
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing n
st Value
v Sing ('TMap n n)
SingT tz
s ((Comparable n => TypeCheckInstr (Value ('TMap n n)))
-> TypeCheckInstr (Value ('TMap n n)))
-> (Comparable n => TypeCheckInstr (Value ('TMap n n)))
-> TypeCheckInstr (Value ('TMap n n))
forall a b. (a -> b) -> a -> b
$ Value ('TMap n n) -> TypeCheckInstr (Value ('TMap n n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TMap n n) -> TypeCheckInstr (Value ('TMap n n)))
-> Value ('TMap n n) -> TypeCheckInstr (Value ('TMap n n))
forall a b. (a -> b) -> a -> b
$ Map (Value' Instr n) (Value' Instr n) -> Value ('TMap n n)
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 n) (Value' Instr n)
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 n
kt Sing n
vt)) ->
Sing n
-> Value
-> Sing ('TMap n 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
kt Value
sq Sing ('TMap n 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 n, Value n)]
keyOrderedElts <- [Elt ExpandedOp]
-> Value -> Sing n -> Sing n -> TypeCheckInstr [(Value n, Value n)]
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 n
kt Sing n
vt
Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
kt ((SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ 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 ('TMap n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TMap n n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TMap n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TMap n n)))
-> Value' Instr ('TMap n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TMap n n))
forall a b. (a -> b) -> a -> b
$ Map (Value n) (Value n) -> Value' Instr ('TMap n n)
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 n, Value n)] -> Map (Value n) (Value n)
forall k a. [(k, a)] -> Map k a
M.fromDistinctAscList [(Value n, Value n)]
keyOrderedElts)
(v :: Value
v@Value
U.ValueNil, s :: SingT tz
s@(STBigMap Sing n
st1 Sing n
st2)) ->
Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
st1 ((SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
st2 ((SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n
-> Value
-> Sing ('TBigMap n n)
-> (Comparable n => TypeCheckInstr (Value ('TBigMap n n)))
-> TypeCheckInstr (Value ('TBigMap n n))
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing n
st1 Value
v Sing ('TBigMap n n)
SingT tz
s ((Comparable n => TypeCheckInstr (Value ('TBigMap n n)))
-> TypeCheckInstr (Value ('TBigMap n n)))
-> (Comparable n => TypeCheckInstr (Value ('TBigMap n n)))
-> TypeCheckInstr (Value ('TBigMap n n))
forall a b. (a -> b) -> a -> b
$ Sing n
-> Value
-> Sing ('TBigMap n n)
-> (HasNoBigMap n => TypeCheckInstr (Value ('TBigMap n n)))
-> TypeCheckInstr (Value ('TBigMap n n))
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (HasNoBigMap a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withBigMapAbsence Sing n
st2 Value
v Sing ('TBigMap n n)
SingT tz
s ((HasNoBigMap n => TypeCheckInstr (Value ('TBigMap n n)))
-> TypeCheckInstr (Value ('TBigMap n n)))
-> (HasNoBigMap n => TypeCheckInstr (Value ('TBigMap n n)))
-> TypeCheckInstr (Value ('TBigMap n n))
forall a b. (a -> b) -> a -> b
$
Value ('TBigMap n n) -> TypeCheckInstr (Value ('TBigMap n n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TBigMap n n) -> TypeCheckInstr (Value ('TBigMap n n)))
-> Value ('TBigMap n n) -> TypeCheckInstr (Value ('TBigMap n n))
forall a b. (a -> b) -> a -> b
$ Maybe Natural
-> Map (Value' Instr n) (Value' Instr n) -> Value ('TBigMap n n)
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 n) (Value' Instr n)
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 n
kt Sing n
vt)) ->
Sing n
-> Value
-> Sing ('TBigMap n 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
kt Value
sq Sing ('TBigMap n 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
$ Sing n
-> Value
-> Sing ('TBigMap n n)
-> (HasNoBigMap n => 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 n
vt Value
sq Sing ('TBigMap n n)
SingT tz
s ((HasNoBigMap n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz))
-> (HasNoBigMap n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
[(Value n, Value n)]
keyOrderedElts <- [Elt ExpandedOp]
-> Value -> Sing n -> Sing n -> TypeCheckInstr [(Value n, Value n)]
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 n
kt Sing n
vt
Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
kt ((SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ 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 ('TBigMap n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TBigMap n n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TBigMap n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TBigMap n n)))
-> Value' Instr ('TBigMap n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TBigMap n n))
forall a b. (a -> b) -> a -> b
$ Maybe Natural
-> Map (Value n) (Value n) -> Value' Instr ('TBigMap n n)
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 n, Value n)] -> Map (Value n) (Value n)
forall k a. [(k, a)] -> Map k a
M.fromDistinctAscList [(Value n, Value n)]
keyOrderedElts)
(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 n
_ Sing n
_) -> 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 n n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing tz
Sing ('TLambda n n)
sng) Text
"" Maybe TCTypeError
forall a. Maybe a
Nothing
(Value
v, STLambda (var :: Sing it) (b :: Sing ot)) -> Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
var ((SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
b ((SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz))
-> (SingI n => 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 InstrCallStack TypeCheck [ExpandedOp]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
U.ValueLambda NonEmpty ExpandedOp
mp -> [ExpandedOp] -> ReaderT InstrCallStack TypeCheck [ExpandedOp]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ExpandedOp] -> ReaderT InstrCallStack TypeCheck [ExpandedOp])
-> [ExpandedOp] -> ReaderT InstrCallStack 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 InstrCallStack TypeCheck [ExpandedOp]
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v ((SingKind T, SingI ty) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @ty) Text
"unexpected value" Maybe TCTypeError
forall a. Maybe a
Nothing
HST '[n]
_ :/ SomeInstrOut '[n]
instr <-
Value
-> (WellTyped n => TypeCheckInstr (SomeInstr '[n]))
-> TypeCheckInstr (SomeInstr '[n])
forall (t :: T) a.
SingI t =>
Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP @it Value
uvalue ((WellTyped n => TypeCheckInstr (SomeInstr '[n]))
-> TypeCheckInstr (SomeInstr '[n]))
-> (WellTyped n => TypeCheckInstr (SomeInstr '[n]))
-> TypeCheckInstr (SomeInstr '[n])
forall a b. (a -> b) -> a -> b
$ TypeCheckInstrNoExcept (TypeCheckedSeq '[n])
-> TypeCheckInstr (SomeInstr '[n])
forall (inp :: [T]).
TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstr (SomeInstr inp)
throwingTCError (TypeCheckInstrNoExcept (TypeCheckedSeq '[n])
-> TypeCheckInstr (SomeInstr '[n]))
-> TypeCheckInstrNoExcept (TypeCheckedSeq '[n])
-> TypeCheckInstr (SomeInstr '[n])
forall a b. (a -> b) -> a -> b
$
TcInstrHandler
-> [ExpandedOp]
-> HST '[n]
-> TypeCheckInstrNoExcept (TypeCheckedSeq '[n])
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcDo [ExpandedOp]
mp ((SingI n => Notes n
forall (t :: T). SingI t => Notes t
starNotes @it, Dict (WellTyped n)
forall (a :: Constraint). a => Dict a
Dict, Annotation VarTag
forall a. Default a => a
def) (Notes n, Dict (WellTyped n), Annotation VarTag)
-> HST '[] -> HST '[n]
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), Annotation VarTag)
-> HST xs -> HST (x : xs)
::& HST '[]
SNil)
case SomeInstrOut '[n]
instr of
Instr '[n] out
lam ::: (HST out
lo :: HST lo) -> Value
-> (WellTyped n =>
ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall (t :: T) a.
SingI t =>
Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP @ot Value
uvalue ((WellTyped n =>
ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> (WellTyped n =>
ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall a b. (a -> b) -> a -> b
$ do
case HST out -> Either TCTypeError (out :~: '[n])
forall (t :: T) (st :: [T]).
(SingI st, WellTyped t) =>
HST st -> Either TCTypeError (st :~: '[t])
eqHST1 @ot HST out
lo of
Right out :~: '[n]
Refl -> do
Value' Instr ('TLambda n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TLambda n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> Value' Instr ('TLambda n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[n] '[n] -> Value' Instr ('TLambda n n)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(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)) =>
RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
VLam (Instr '[n] out -> RemFail Instr '[n] out
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
T.RfNormal Instr '[n] out
lam)
Left TCTypeError
m ->
Value
-> T
-> Text
-> Maybe TCTypeError
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v ((SingKind T, SingI ty) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
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 '[n] out
lam ->
Value' Instr ('TLambda n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TLambda n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> Value' Instr ('TLambda n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[n] '[n] -> Value' Instr ('TLambda n n)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(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)) =>
RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
VLam ((forall (out :: [T]). Instr '[n] out) -> RemFail Instr '[n] '[n]
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 '[n] 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 InstrCallStack TypeCheck (Value' Instr 'TChest)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChest
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TChest))
-> Value' Instr 'TChest
-> ReaderT InstrCallStack 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 InstrCallStack TypeCheck (Value' Instr 'TChestKey)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChestKey
-> ReaderT InstrCallStack TypeCheck (Value' Instr 'TChestKey))
-> Value' Instr 'TChestKey
-> ReaderT InstrCallStack 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, 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)
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 InstrCallStack
_ 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
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 :: Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP Value
uvalue WellTyped t => TypeCheckInstr a
fn = case SingI t => Either NotWellTyped (Dict (WellTyped t))
forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
getWTP @t of
Right Dict (WellTyped t)
Dict -> TypeCheckInstr a
WellTyped t => TypeCheckInstr a
fn
Left (NotWellTyped T
t BadTypeForScope
cause) -> Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
uvalue ((SingKind T, SingI ty) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @ty)
(Text
"Value is not well typed: '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> T -> Text
forall b a. (Show a, IsString b) => a -> b
show T
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"' because it " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> BadTypeForScope -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty BadTypeForScope
cause) Maybe TCTypeError
forall a. Maybe a
Nothing
typeCheckValsImpl
:: ([U.Value], Sing t)
-> TypeCheckInstr [T.Value t]
typeCheckValsImpl :: ([Value], Sing t) -> TypeCheckInstr [Value t]
typeCheckValsImpl ([Value]
mvs, Sing t
sng) =
([Value t] -> [Value t])
-> TypeCheckInstr [Value t] -> TypeCheckInstr [Value t]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Value t] -> [Value t]
forall a. [a] -> [a]
reverse (TypeCheckInstr [Value t] -> TypeCheckInstr [Value t])
-> TypeCheckInstr [Value t] -> TypeCheckInstr [Value t]
forall a b. (a -> b) -> a -> b
$ ([Value t] -> Value -> TypeCheckInstr [Value t])
-> [Value t] -> [Value] -> TypeCheckInstr [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 InstrCallStack TypeCheck (Value t)
-> TypeCheckInstr [Value t]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Value, Sing t) -> ReaderT InstrCallStack TypeCheck (Value t)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
mv, Sing t
sng))) [] [Value]
mvs
typeCheckMapVal
:: [U.Elt U.ExpandedOp]
-> U.Value
-> Sing kt
-> Sing vt
-> TypeCheckInstr [(T.Value kt, T.Value vt)]
typeCheckMapVal :: [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
InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
[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, Show 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 -> InstrCallStack -> 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 InstrCallStack
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 :: Value -> EpAddress -> Sing cp -> TypeCheckInstr (Value tz)
typecheckContractValue Value
cv (EpAddress Address
addr EpName
epName) Sing cp
pc = do
InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
let ensureTypeMatches :: forall t'. SingI t' => TypeCheckInstr (cp :~: t')
ensureTypeMatches :: TypeCheckInstr (cp :~: t')
ensureTypeMatches = forall a.
MonadError TCError TypeCheckInstr =>
Either TCError a -> TypeCheckInstr a
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 -> InstrCallStack -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
cv ((SingKind T, SingI ty) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @ty) Text
"wrong contract parameter" InstrCallStack
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
$ Each '[SingI] '[cp, t'] => Either TCTypeError (cp :~: t')
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 -> InstrCallStack -> 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" InstrCallStack
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 KeyHash
_ -> do
cp :~: 'TUnit
Refl <- SingI 'TUnit => TypeCheckInstr (cp :~: 'TUnit)
forall (t' :: T). SingI t' => TypeCheckInstr (cp :~: t')
ensureTypeMatches @'T.TUnit
Value' Instr ('TContract 'TUnit)
-> ReaderT
InstrCallStack TypeCheck (Value' Instr ('TContract 'TUnit))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TContract 'TUnit)
-> ReaderT
InstrCallStack TypeCheck (Value' Instr ('TContract 'TUnit)))
-> Value' Instr ('TContract 'TUnit)
-> ReaderT
InstrCallStack 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 (_ :: Sing cp') 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 -> InstrCallStack -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
cv ((SingKind T, SingI ty) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @ty) Text
"unknown entrypoint" InstrCallStack
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 <- SingI arg => TypeCheckInstr (cp :~: arg)
forall (t' :: T). SingI t' => TypeCheckInstr (cp :~: t')
ensureTypeMatches @t'
Value' Instr ('TContract arg)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TContract arg))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TContract arg)
-> ReaderT
InstrCallStack TypeCheck (Value' Instr ('TContract arg)))
-> Value' Instr ('TContract arg)
-> ReaderT InstrCallStack 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 -> InstrCallStack -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
cv ((SingKind T, SingI ty) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @ty) Text
"Contract literal unknown"
InstrCallStack
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 :: 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
InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
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 -> InstrCallStack -> 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" InstrCallStack
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 :: 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
InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
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 -> InstrCallStack -> 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"
InstrCallStack
instrPos Maybe TCTypeError
forall a. Maybe a
Nothing