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

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

import Control.Monad.Except (liftEither, throwError)
import Data.Constraint (Dict(..))
import Data.Default (def)
import qualified Data.Map as M
import qualified Data.Set as S
import Data.Singletons (Sing, SingI(..), demote)
import Data.Typeable ((:~:)(..))
import Prelude hiding (EQ, GT, LT)

import Michelson.Text
import Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))
import Michelson.TypeCheck.Helpers
import Michelson.TypeCheck.TypeCheck
  (SomeParamType(..), TcInstrHandler, TcOriginatedContracts, TypeCheckInstr, throwingTCError)
import Michelson.TypeCheck.Types
import Michelson.Typed
  (EpAddress(..), KnownT, Notes(..), SingT(..), Value'(..), fromSingT, starNotes)
import qualified Michelson.Typed as T
import qualified Michelson.Untyped as U
import Tezos.Address (Address(..))
import Tezos.Core
import Tezos.Crypto
import qualified Tezos.Crypto.BLS12381 as BLS
import 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

-- | Function @typeCheckValImpl@ converts a single Michelson value
-- given in representation from @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 :: Maybe TcOriginatedContracts
-> TcInstrHandler -> Value -> TypeCheckInstr (Value ty)
typeCheckValImpl Maybe TcOriginatedContracts
mOriginatedContracts TcInstrHandler
tcDo = Value -> TypeCheckInstr (Value ty)
forall (tz :: T). SingI tz => Value -> TypeCheckInstr (Value tz)
doTypeCheckVal
  where
    doTypeCheckVal :: forall tz. SingI tz => U.Value -> TypeCheckInstr (T.Value tz)
    doTypeCheckVal :: Value -> TypeCheckInstr (Value tz)
doTypeCheckVal Value
uvalue = case (Value
uvalue, SingI tz => Sing tz
forall k (a :: k). SingI a => Sing a
sing @tz) 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. Num 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 -> T
forall (a :: T). Sing a -> T
fromSingT 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 Word64 -> Maybe Mutez
mkMutez (Word64 -> Maybe Mutez) -> Word64 -> Maybe Mutez
forall a b. (a -> b) -> a -> b
$ Integer -> Word64
forall a. Num a => Integer -> a
fromInteger Integer
i of
        Just 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
        Maybe Mutez
Nothing -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TMutez -> T
forall (a :: T). Sing a -> T
fromSingT Sing 'TMutez
SingT tz
t) Text
"" (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 -> T
forall (a :: T). Sing a -> T
fromSingT 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 -> T
forall (a :: T). Sing a -> T
fromSingT 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 -> T
forall (a :: T). Sing a -> T
fromSingT 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 -> T
forall (a :: T). Sing a -> T
fromSingT 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
fromIntegral 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 -> T
forall (a :: T). Sing a -> T
fromSingT 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 -> T
forall (a :: T). Sing a -> T
fromSingT 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 -> T
forall (a :: T). Sing a -> T
fromSingT 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 -> T
forall (a :: T). Sing a -> T
fromSingT 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 a
pc) -> Value -> EpAddress -> Sing a -> TypeCheckInstr (Value tz)
forall (cp :: T) (tz :: T).
(Typeable cp, SingI cp, tz ~ 'TContract cp) =>
Value -> EpAddress -> Sing cp -> TypeCheckInstr (Value tz)
typecheckContractValue Value
cv EpAddress
addr Sing a
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 a
pc) -> Value -> EpAddress -> Sing a -> TypeCheckInstr (Value tz)
forall (cp :: T) (tz :: T).
(Typeable cp, SingI cp, tz ~ 'TContract cp) =>
Value -> EpAddress -> Sing cp -> TypeCheckInstr (Value tz)
typecheckContractValue Value
cv EpAddress
addr Sing a
pc

      (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 a
_ Sing b
_) -> do
        Value a
l <- Value -> TypeCheckInstr (Value a)
forall (tz :: T). SingI tz => Value -> TypeCheckInstr (Value tz)
doTypeCheckVal Value
ml
        Value b
r <- Value -> TypeCheckInstr (Value b)
forall (tz :: T). SingI tz => Value -> TypeCheckInstr (Value tz)
doTypeCheckVal Value
mr
        pure $ (Value a, Value b) -> Value' Instr ('TPair a b)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value a
l, Value b
r)
      (U.ValueLeft Value
ml, STOr{}) -> do
        Value a
l <- Value -> TypeCheckInstr (Value a)
forall (tz :: T). SingI tz => Value -> TypeCheckInstr (Value tz)
doTypeCheckVal Value
ml
        pure $ Either (Value a) (Value' Instr b) -> Value' Instr ('TOr a b)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(KnownT l, KnownT r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Value a -> Either (Value a) (Value' Instr b)
forall a b. a -> Either a b
Left Value a
l)
      (U.ValueRight Value
mr, STOr{}) -> do
        Value b
r <- Value -> TypeCheckInstr (Value b)
forall (tz :: T). SingI tz => Value -> TypeCheckInstr (Value tz)
doTypeCheckVal Value
mr
        pure $ Either (Value' Instr a) (Value b) -> Value' Instr ('TOr a b)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(KnownT l, KnownT r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Value b -> Either (Value' Instr a) (Value b)
forall a b. b -> Either a b
Right Value b
r)
      (U.ValueSome Value
mv, STOption{}) -> do
        Value a
v <- Value -> TypeCheckInstr (Value a)
forall (tz :: T). SingI tz => Value -> TypeCheckInstr (Value tz)
doTypeCheckVal Value
mv
        pure $ Maybe (Value a) -> Value' Instr ('TOption a)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Value a -> Maybe (Value a)
forall a. a -> Maybe a
Just Value a
v)
      (Value
U.ValueNone, STOption Sing a
_) -> do
        Value' Instr ('TOption a)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOption a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TOption a)
 -> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOption a)))
-> Value' Instr ('TOption a)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TOption a))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' Instr a) -> Value' Instr ('TOption a)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption Maybe (Value' Instr a)
forall a. Maybe a
Nothing

      (Value
U.ValueNil, STList Sing a
_) ->
        Value' Instr ('TList a)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TList a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TList a)
 -> ReaderT InstrCallStack TypeCheck (Value' Instr ('TList a)))
-> Value' Instr ('TList a)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TList a))
forall a b. (a -> b) -> a -> b
$ [Value' Instr a] -> Value' Instr ('TList a)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
T.VList []

      (U.ValueSeq ((NonEmpty $ Value) -> [Element (NonEmpty $ Value)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Value)]
mels), STList Sing a
_) -> do
        [Value a]
els <- [Value] -> TypeCheckInstr [Value a]
forall (t :: T). SingI t => [Value] -> TypeCheckInstr [Value t]
typeCheckValsImpl [Element (NonEmpty $ Value)]
[Value]
mels
        pure $ [Value a] -> Value' Instr ('TList a)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value a]
els

      (Value
U.ValueNil, STSet (s :: Sing st)) -> do
        InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
        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 -> Value' Instr ('TSet a)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TSet a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Value' Instr a) -> Value' Instr ('TSet a)
forall (t :: T) (instr :: [T] -> [T] -> *).
(KnownT t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
T.VSet Set (Value' Instr a)
forall a. Set a
S.empty)
          Maybe (Dict (Comparable a))
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 ((SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @st) 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 ((SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @st) 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 (vt :: Sing st))) -> Sing a
-> Value
-> Sing ('TSet a)
-> (Comparable a => 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 a
vt Value
sq Sing ('TSet a)
SingT tz
s ((Comparable a => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable a => 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 a]
els <- [Value] -> TypeCheckInstr [Value a]
forall (t :: T). SingI t => [Value] -> TypeCheckInstr [Value t]
typeCheckValsImpl [Element (NonEmpty $ Value)]
[Value]
mels
        Set (Value a)
elsS <- Either TCError (Set (Value a))
-> ReaderT InstrCallStack TypeCheck (Set (Value a))
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError (Set (Value a))
 -> ReaderT InstrCallStack TypeCheck (Set (Value a)))
-> Either TCError (Set (Value a))
-> ReaderT InstrCallStack TypeCheck (Set (Value a))
forall a b. (a -> b) -> a -> b
$ [Value a] -> Set (Value a)
forall a. [a] -> Set a
S.fromDistinctAscList ([Value a] -> Set (Value a))
-> Either TCError [Value a] -> Either TCError (Set (Value a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value a -> Value a) -> [Value a] -> Either Text [Value a]
forall b a. (Ord b, Show a) => (a -> b) -> [a] -> Either Text [a]
ensureDistinctAsc Value a -> Value a
forall a. a -> a
id [Value a]
els
                  Either Text [Value a]
-> (Text -> TCError) -> Either TCError [Value a]
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 a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
vt) Text
msg InstrCallStack
instrPos Maybe TCTypeError
forall a. Maybe a
Nothing
        pure $ Set (Value a) -> Value' Instr ('TSet a)
forall (t :: T) (instr :: [T] -> [T] -> *).
(KnownT t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
VSet Set (Value a)
elsS

      (v :: Value
v@Value
U.ValueNil, s :: SingT tz
s@(STMap (st :: Sing st) Sing b
_)) -> Sing a
-> Value
-> Sing ('TMap a b)
-> (Comparable a => 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 a
st Value
v Sing ('TMap a b)
SingT tz
s ((Comparable a => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable a => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TMap a b)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TMap a b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TMap a b)
 -> ReaderT InstrCallStack TypeCheck (Value' Instr ('TMap a b)))
-> Value' Instr ('TMap a b)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TMap a b))
forall a b. (a -> b) -> a -> b
$ Map (Value' Instr a) (Value' Instr b) -> Value' Instr ('TMap a b)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
T.VMap Map (Value' Instr a) (Value' Instr b)
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 (kt :: Sing st) Sing b
_)) -> Sing a
-> Value
-> Sing ('TMap a b)
-> (Comparable a => 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 a
kt Value
sq Sing ('TMap a b)
SingT tz
s ((Comparable a => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable a => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
        [(Value a, Value b)]
keyOrderedElts <- [Elt ExpandedOp]
-> Value -> Sing a -> TypeCheckInstr [(Value a, Value b)]
forall (kt :: T) (vt :: T).
(SingI kt, SingI vt) =>
[Elt ExpandedOp]
-> Value -> Sing kt -> TypeCheckInstr [(Value kt, Value vt)]
typeCheckMapVal [Element (NonEmpty $ Elt ExpandedOp)]
[Elt ExpandedOp]
mels Value
sq Sing a
kt
        pure $ Map (Value a) (Value b) -> Value' Instr ('TMap a b)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap ([(Value a, Value b)] -> Map (Value a) (Value b)
forall k a. [(k, a)] -> Map k a
M.fromDistinctAscList [(Value a, Value b)]
keyOrderedElts)

      (v :: Value
v@Value
U.ValueNil, s :: SingT tz
s@(STBigMap (st :: Sing st) Sing b
_)) ->
        Sing a
-> Value
-> Sing ('TBigMap a b)
-> (Comparable a => 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 a
st Value
v Sing ('TBigMap a b)
SingT tz
s ((Comparable a => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable a => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TBigMap a b)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TBigMap a b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TBigMap a b)
 -> ReaderT InstrCallStack TypeCheck (Value' Instr ('TBigMap a b)))
-> Value' Instr ('TBigMap a b)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TBigMap a b))
forall a b. (a -> b) -> a -> b
$ Map (Value' Instr a) (Value' Instr b)
-> Value' Instr ('TBigMap a b)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
T.VBigMap Map (Value' Instr a) (Value' Instr b)
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 (kt :: Sing st) Sing b
_)) -> Sing a
-> Value
-> Sing ('TBigMap a b)
-> (Comparable a => 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 a
kt Value
sq Sing ('TBigMap a b)
SingT tz
s ((Comparable a => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable a => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
        [(Value a, Value b)]
keyOrderedElts <- [Elt ExpandedOp]
-> Value -> Sing a -> TypeCheckInstr [(Value a, Value b)]
forall (kt :: T) (vt :: T).
(SingI kt, SingI vt) =>
[Elt ExpandedOp]
-> Value -> Sing kt -> TypeCheckInstr [(Value kt, Value vt)]
typeCheckMapVal [Element (NonEmpty $ Elt ExpandedOp)]
[Elt ExpandedOp]
mels Value
sq Sing a
kt
        pure $ Map (Value a) (Value b) -> Value' Instr ('TBigMap a b)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap ([(Value a, Value b)] -> Map (Value a) (Value b)
forall k a. [(k, a)] -> Map k a
M.fromDistinctAscList [(Value a, Value b)]
keyOrderedElts)

      (Value
v, STLambda (_ :: Sing it) (_ :: Sing ot)) -> 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 '[a]
_ :/ SomeInstrOut '[a]
instr <-
          Value
-> (WellTyped a => TypeCheckInstr (SomeInstr '[a]))
-> TypeCheckInstr (SomeInstr '[a])
forall (t :: T) a.
SingI t =>
Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP @it Value
uvalue ((WellTyped a => TypeCheckInstr (SomeInstr '[a]))
 -> TypeCheckInstr (SomeInstr '[a]))
-> (WellTyped a => TypeCheckInstr (SomeInstr '[a]))
-> TypeCheckInstr (SomeInstr '[a])
forall a b. (a -> b) -> a -> b
$ TypeCheckInstrNoExcept (TypeCheckedSeq '[a])
-> TypeCheckInstr (SomeInstr '[a])
forall (inp :: [T]).
TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstr (SomeInstr inp)
throwingTCError (TypeCheckInstrNoExcept (TypeCheckedSeq '[a])
 -> TypeCheckInstr (SomeInstr '[a]))
-> TypeCheckInstrNoExcept (TypeCheckedSeq '[a])
-> TypeCheckInstr (SomeInstr '[a])
forall a b. (a -> b) -> a -> b
$
            TcInstrHandler
-> [ExpandedOp]
-> HST '[a]
-> TypeCheckInstrNoExcept (TypeCheckedSeq '[a])
forall (inp :: [T]).
Typeable inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcDo [ExpandedOp]
mp ((SingI a => Notes a
forall (t :: T). SingI t => Notes t
starNotes @it, Dict (WellTyped a)
forall (a :: Constraint). a => Dict a
Dict, Annotation VarTag
forall a. Default a => a
def) (Notes a, Dict (WellTyped a), Annotation VarTag)
-> HST '[] -> HST '[a]
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), Annotation VarTag)
-> HST xs -> HST (x : xs)
::& HST '[]
SNil)
        case SomeInstrOut '[a]
instr of
          Instr '[a] out
lam ::: (HST out
lo :: HST lo) -> Value
-> (WellTyped b => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall (t :: T) a.
SingI t =>
Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP @ot Value
uvalue ((WellTyped b => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (WellTyped b => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
            case HST out -> Either TCTypeError (out :~: '[b])
forall (t :: T) (st :: [T]).
(Typeable st, WellTyped t) =>
HST st -> Either TCTypeError (st :~: '[t])
eqHST1 @ot HST out
lo of
              Right out :~: '[b]
Refl -> do
                Value' Instr ('TLambda a b)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda a b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TLambda a b)
 -> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda a b)))
-> Value' Instr ('TLambda a b)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda a b))
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[a] '[b] -> Value' Instr ('TLambda a b)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(KnownT inp, KnownT 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 '[a] out -> RemFail Instr '[a] out
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
T.RfNormal Instr '[a] out
lam)
              Left TCTypeError
m ->
                Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
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 '[a] out
lam ->
            Value' Instr ('TLambda a b)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda a b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TLambda a b)
 -> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda a b)))
-> Value' Instr ('TLambda a b)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda a b))
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[a] '[b] -> Value' Instr ('TLambda a b)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(KnownT inp, KnownT 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 '[a] out) -> RemFail Instr '[a] '[b]
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 '[a] out
lam)

      (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 -> T
forall (a :: T). Sing a -> T
fromSingT Sing tz
SingT tz
t) Text
"unknown value" Maybe TCTypeError
forall a. Maybe a
Nothing

    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) -> Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
uvalue (Sing ty -> T
forall (a :: T). Sing a -> T
fromSingT (Sing ty -> T) -> Sing ty -> T
forall a b. (a -> b) -> a -> b
$ SingI ty => Sing ty
forall k (a :: k). SingI a => Sing a
sing @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) Maybe TCTypeError
forall a. Maybe a
Nothing

    typeCheckValsImpl
      :: forall t . (SingI t)
      => [U.Value]
      -> TypeCheckInstr [T.Value t]
    typeCheckValsImpl :: [Value] -> TypeCheckInstr [Value t]
typeCheckValsImpl [Value]
mvs =
      ([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 -> ReaderT InstrCallStack TypeCheck (Value t)
forall (tz :: T). SingI tz => Value -> TypeCheckInstr (Value tz)
doTypeCheckVal @t Value
mv) [] [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
      :: forall kt vt. (SingI kt, SingI vt)
      => [U.Elt U.ExpandedOp]
      -> U.Value
      -> Sing kt
      -> TypeCheckInstr [(T.Value kt, T.Value vt)]
    typeCheckMapVal :: [Elt ExpandedOp]
-> Value -> Sing kt -> TypeCheckInstr [(Value kt, Value vt)]
typeCheckMapVal [Elt ExpandedOp]
mels Value
sq Sing kt
kt = 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] -> TypeCheckInstr [Value kt]
forall (t :: T). SingI t => [Value] -> TypeCheckInstr [Value t]
typeCheckValsImpl @kt ((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)
      [Value vt]
vals <- [Value] -> TypeCheckInstr [Value vt]
forall (t :: T). SingI t => [Value] -> TypeCheckInstr [Value t]
typeCheckValsImpl @vt ((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)
      [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 -> T
forall (a :: T). Sing a -> T
fromSingT 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. (Typeable cp, SingI cp, 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'. KnownT 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
$
              Each '[KnownT] '[cp, t'] => Either TCTypeError (cp :~: t')
forall (a :: T) (b :: T).
Each '[KnownT] '[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 -> T
forall (a :: T). Sing a -> T
fromSingT 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 -> T
forall (a :: T). Sing a -> T
fromSingT Sing cp
pc) BadTypeForScope
reason
      case Address
addr of
        KeyAddress KeyHash
_ -> do
          cp :~: 'TUnit
Refl <- KnownT 'TUnit => TypeCheckInstr (cp :~: 'TUnit)
forall (t' :: T). KnownT 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] -> *).
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 <- KnownT arg => TypeCheckInstr (cp :~: arg)
forall (t' :: T). KnownT 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] -> *).
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 -> T
forall (a :: T). Sing a -> T
fromSingT Sing t
t) Text
"Require a comparable type here" InstrCallStack
instrPos Maybe TCTypeError
forall a. Maybe a
Nothing