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

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

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

import Morley.Michelson.Text
import Morley.Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))
import Morley.Michelson.TypeCheck.Helpers
import Morley.Michelson.TypeCheck.TypeCheck
import Morley.Michelson.TypeCheck.Types
import Morley.Michelson.Typed
  (EpAddress(..), Notes(..), SingT(..), SomeVBigMap(..), Value'(..), castM)
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Typed.Contract (giveNotInView)
import Morley.Michelson.Untyped qualified as U
import Morley.Tezos.Address
import Morley.Tezos.Core
import Morley.Tezos.Crypto
import Morley.Tezos.Crypto.BLS12381 qualified as BLS
import Morley.Tezos.Crypto.Timelock (chestFromBytes, chestKeyFromBytes)
import Morley.Util.Type (onFirst)

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

-- | Function @typeCheckValImpl@ converts a single Michelson value
-- given in representation from @Morley.Michelson.Type@ module to representation
-- in strictly typed GADT.
--
-- @typeCheckValImpl@ is polymorphic in the expected type of value.
--
-- Type checking algorithm pattern-matches on parse value representation,
-- expected type @t@ and constructs @Val t@ value.
--
-- If there was no match on a given pair of value and expected type,
-- that is interpreted as input of wrong type and type check finishes with
-- error.
--
-- @typeCheckValImpl@ also has a 'Maybe TcOriginatedContracts' argument that
-- should contain the originated contracts when typechecking a parameter and
-- 'Nothing' otherwise.
typeCheckValImpl
  :: forall ty.
     SingI ty
  => Maybe TcOriginatedContracts
  -> TcInstrHandler
  -> U.Value
  -> TypeCheckInstr (T.Value ty)
typeCheckValImpl :: forall (ty :: T).
SingI ty =>
Maybe TcOriginatedContracts
-> TcInstrHandler -> Value -> TypeCheckInstr (Value ty)
typeCheckValImpl Maybe TcOriginatedContracts
mOriginatedContracts TcInstrHandler
tcDo Value
uv = (Value, Sing ty) -> TypeCheckInstr (Value ty)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
uv, forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @ty)
  where
    doTypeCheckVal :: forall tz. (U.Value, Sing tz) -> TypeCheckInstr (T.Value tz)
    doTypeCheckVal :: forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
uvalue, Sing tz
sng) = do
      TypeCheckMode
typeCheckMode <- (TypeCheckEnv -> TypeCheckMode)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     TypeCheckMode
forall (m :: * -> *) r a (n :: Nat).
MultiReader n r m =>
(r -> a) -> m a
asks' TypeCheckEnv -> TypeCheckMode
tcMode
      case (Value
uvalue, Sing tz
SingT tz
sng) of
        (U.ValueInt Integer
i, SingT tz
STInt) -> Value' Instr 'TInt
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TInt)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TInt
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TInt))
-> Value' Instr 'TInt
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TInt)
forall a b. (a -> b) -> a -> b
$ Integer -> Value' Instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
T.VInt Integer
i
        (v :: Value
v@(U.ValueInt Integer
i), t :: SingT tz
t@SingT tz
STNat)
          | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 -> Value' Instr 'TNat
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TNat)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TNat
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TNat))
-> Value' Instr 'TNat
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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' Instr 'TNat)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TNat -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TNat
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
NegativeNat)
        (v :: Value
v@(U.ValueInt Integer
i), t :: SingT tz
t@SingT tz
STMutez) -> case Integer -> Either Text Mutez
forall i. Integral i => i -> Either Text Mutez
mkMutez Integer
i of
          Right Mutez
m -> Value' Instr 'TMutez
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TMutez)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TMutez
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TMutez))
-> Value' Instr 'TMutez
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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' Instr 'TMutez)
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)

        -- If `tcBigMaps` is a `Just`, then we simulate the behavior of the RPC
        -- @/run_code@ endpoint.
        -- If a value contains a natural number where a big_map is expected,
        -- we assume that number represents a big_map ID and replace it with
        -- the corresponding big_map value (if it exists and has the expected key/value types).
        (U.ValueInt Integer
bigMapId, STBigMap {}) | TypeCheckValue (Value, T)
_ (Just BigMapFinder
bigMapFinder) <- TypeCheckMode
typeCheckMode -> do
          let bigMapMaybe :: Maybe SomeVBigMap
bigMapMaybe = BigMapFinder
bigMapFinder BigMapFinder -> Maybe Natural -> Maybe SomeVBigMap
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
fromIntegralMaybe @Integer @Natural Integer
bigMapId
          case Maybe SomeVBigMap
bigMapMaybe of
            Just (SomeVBigMap (bigMap :: Value ('TBigMap k v)
bigMap@VBigMap{} :: T.Value actualT)) ->
              Sing ('TBigMap n1 n2)
-> (SingI ('TBigMap n1 n2) =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing tz
Sing ('TBigMap n1 n2)
sng ((SingI ('TBigMap n1 n2) =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value tz))
-> (SingI ('TBigMap n1 n2) =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ forall (a :: T) (b :: T) (t :: T -> *) (m :: * -> *).
(SingI a, SingI b, Monad m) =>
t a -> (forall x. MismatchError T -> m x) -> m (t b)
castM @actualT @tz Value ('TBigMap k v)
bigMap ((forall x.
  MismatchError T
  -> ReaderT
       TypeCheckInstrEnv
       (ReaderT
          TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
       x)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value tz))
-> (forall x.
    MismatchError T
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT
            TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
         x)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$
                Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr x
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
uvalue (Sing ('TBigMap n1 n2) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing tz
Sing ('TBigMap n1 n2)
sng) Text
"" (Maybe TCTypeError
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      x)
-> (MismatchError T -> Maybe TCTypeError)
-> MismatchError T
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> (MismatchError T -> TCTypeError)
-> MismatchError T
-> Maybe TCTypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> MismatchError T -> TCTypeError
UnexpectedBigMapType Integer
bigMapId
            Maybe SomeVBigMap
Nothing ->
              Value
-> T
-> Text
-> Maybe TCTypeError
-> TypeCheckInstr (Value ('TBigMap n1 n2))
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
uvalue (Sing ('TBigMap n1 n2) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing tz
Sing ('TBigMap n1 n2)
sng) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (Integer -> TCTypeError
InvalidBigMapId Integer
bigMapId))
        (U.ValueString MText
s, SingT tz
STString) -> Value' Instr 'TString
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TString
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TString))
-> Value' Instr 'TString
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TString)
forall a b. (a -> b) -> a -> b
$ MText -> Value' Instr 'TString
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString MText
s
        (v :: Value
v@(U.ValueString MText
s), t :: SingT tz
t@SingT tz
STAddress) -> case Text -> Either ParseEpAddressError EpAddress
T.parseEpAddress (MText -> Text
unMText MText
s) of
          Right EpAddress
addr -> Value' Instr 'TAddress
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TAddress)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TAddress
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TAddress))
-> Value' Instr 'TAddress
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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' Instr 'TAddress)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TAddress -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TAddress
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ ParseEpAddressError -> TCTypeError
InvalidAddress ParseEpAddressError
err)
        (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STAddress) -> case ByteString -> Either ParseEpAddressError EpAddress
T.parseEpAddressRaw (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
          Right EpAddress
addr -> Value' Instr 'TAddress
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TAddress)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TAddress
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TAddress))
-> Value' Instr 'TAddress
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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' Instr 'TAddress)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TAddress -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TAddress
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ ParseEpAddressError -> TCTypeError
InvalidAddress ParseEpAddressError
err)
        (v :: Value
v@(U.ValueString MText
s), t :: SingT tz
t@SingT tz
STKeyHash) -> case Text -> Either CryptoParseError (Hash 'HashKindPublicKey)
forall (kind :: HashKind).
AllHashTags kind =>
Text -> Either CryptoParseError (Hash kind)
parseHash (MText -> Text
unMText MText
s)  of
          Right Hash 'HashKindPublicKey
kHash -> Value' Instr 'TKeyHash
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TKeyHash)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKeyHash
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TKeyHash))
-> Value' Instr 'TKeyHash
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TKeyHash)
forall a b. (a -> b) -> a -> b
$ Hash 'HashKindPublicKey -> Value' Instr 'TKeyHash
forall (instr :: [T] -> [T] -> *).
Hash 'HashKindPublicKey -> Value' instr 'TKeyHash
VKeyHash Hash 'HashKindPublicKey
kHash
          Left CryptoParseError
err -> Value
-> T
-> Text
-> Maybe TCTypeError
-> TypeCheckInstr (Value' Instr 'TKeyHash)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TKeyHash -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TKeyHash
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ CryptoParseError -> TCTypeError
InvalidKeyHash CryptoParseError
err)
        (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STKeyHash) ->
          case ByteString -> Either CryptoParseError (Hash 'HashKindPublicKey)
parseKeyHashRaw (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
            Right Hash 'HashKindPublicKey
kHash -> Value' Instr 'TKeyHash
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TKeyHash)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKeyHash
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TKeyHash))
-> Value' Instr 'TKeyHash
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TKeyHash)
forall a b. (a -> b) -> a -> b
$ Hash 'HashKindPublicKey -> Value' Instr 'TKeyHash
forall (instr :: [T] -> [T] -> *).
Hash 'HashKindPublicKey -> Value' instr 'TKeyHash
VKeyHash Hash 'HashKindPublicKey
kHash
            Left CryptoParseError
err -> Value
-> T
-> Text
-> Maybe TCTypeError
-> TypeCheckInstr (Value' Instr 'TKeyHash)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TKeyHash -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TKeyHash
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ CryptoParseError -> TCTypeError
InvalidKeyHash CryptoParseError
err)
        (v :: Value
v@(U.ValueString MText
s), t :: SingT tz
t@SingT tz
STTxRollupL2Address) -> case Text -> Either CryptoParseError (Hash 'HashKindL2PublicKey)
forall (kind :: HashKind).
AllHashTags kind =>
Text -> Either CryptoParseError (Hash kind)
parseHash (MText -> Text
unMText MText
s)  of
          Right Hash 'HashKindL2PublicKey
kHash -> Value' Instr 'TTxRollupL2Address
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TTxRollupL2Address)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTxRollupL2Address
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TTxRollupL2Address))
-> Value' Instr 'TTxRollupL2Address
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TTxRollupL2Address)
forall a b. (a -> b) -> a -> b
$ TxRollupL2Address -> Value' Instr 'TTxRollupL2Address
forall (instr :: [T] -> [T] -> *).
TxRollupL2Address -> Value' instr 'TTxRollupL2Address
VTxRollupL2Address (TxRollupL2Address -> Value' Instr 'TTxRollupL2Address)
-> TxRollupL2Address -> Value' Instr 'TTxRollupL2Address
forall a b. (a -> b) -> a -> b
$ Hash 'HashKindL2PublicKey -> TxRollupL2Address
TxRollupL2Address Hash 'HashKindL2PublicKey
kHash
          Left CryptoParseError
err -> Value
-> T
-> Text
-> Maybe TCTypeError
-> TypeCheckInstr (Value' Instr 'TTxRollupL2Address)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TTxRollupL2Address -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TTxRollupL2Address
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ CryptoParseError -> TCTypeError
InvalidKeyHash CryptoParseError
err)
        (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STTxRollupL2Address) ->
          case ByteString -> Either CryptoParseError (Hash 'HashKindL2PublicKey)
parseKeyHashL2Raw (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
            Right Hash 'HashKindL2PublicKey
kHash -> Value' Instr 'TTxRollupL2Address
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TTxRollupL2Address)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTxRollupL2Address
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TTxRollupL2Address))
-> Value' Instr 'TTxRollupL2Address
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TTxRollupL2Address)
forall a b. (a -> b) -> a -> b
$ TxRollupL2Address -> Value' Instr 'TTxRollupL2Address
forall (instr :: [T] -> [T] -> *).
TxRollupL2Address -> Value' instr 'TTxRollupL2Address
VTxRollupL2Address (TxRollupL2Address -> Value' Instr 'TTxRollupL2Address)
-> TxRollupL2Address -> Value' Instr 'TTxRollupL2Address
forall a b. (a -> b) -> a -> b
$ Hash 'HashKindL2PublicKey -> TxRollupL2Address
TxRollupL2Address Hash 'HashKindL2PublicKey
kHash
            Left CryptoParseError
err -> Value
-> T
-> Text
-> Maybe TCTypeError
-> TypeCheckInstr (Value' Instr 'TTxRollupL2Address)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TTxRollupL2Address -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TTxRollupL2Address
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ CryptoParseError -> TCTypeError
InvalidKeyHash CryptoParseError
err)
        (U.ValueInt Integer
i, SingT tz
STBls12381Fr) ->
          Value' Instr 'TBls12381Fr
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBls12381Fr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381Fr
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TBls12381Fr))
-> Value' Instr 'TBls12381Fr
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBls12381Fr)
forall a b. (a -> b) -> a -> b
$ Bls12381Fr -> Value' Instr 'TBls12381Fr
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr (forall a b. (Integral a, Num b) => a -> b
fromIntegralOverflowing @Integer @Bls12381Fr Integer
i)
        (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STBls12381Fr) ->
          case ByteString -> Either DeserializationError Bls12381Fr
forall a.
CurveObject a =>
ByteString -> Either DeserializationError a
BLS.fromMichelsonBytes (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
            Right Bls12381Fr
val -> Value' Instr 'TBls12381Fr
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBls12381Fr)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381Fr
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TBls12381Fr))
-> Value' Instr 'TBls12381Fr
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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' Instr 'TBls12381Fr)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TBls12381Fr -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TBls12381Fr
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ DeserializationError -> TCTypeError
InvalidBls12381Object DeserializationError
err)
        (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STBls12381G1) ->
          case ByteString -> Either DeserializationError Bls12381G1
forall a.
CurveObject a =>
ByteString -> Either DeserializationError a
BLS.fromMichelsonBytes (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
            Right Bls12381G1
val -> Value' Instr 'TBls12381G1
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBls12381G1)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381G1
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TBls12381G1))
-> Value' Instr 'TBls12381G1
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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' Instr 'TBls12381G1)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TBls12381G1 -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TBls12381G1
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ DeserializationError -> TCTypeError
InvalidBls12381Object DeserializationError
err)
        (v :: Value
v@(U.ValueBytes InternalByteString
b), t :: SingT tz
t@SingT tz
STBls12381G2) ->
          case ByteString -> Either DeserializationError Bls12381G2
forall a.
CurveObject a =>
ByteString -> Either DeserializationError a
BLS.fromMichelsonBytes (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
            Right Bls12381G2
val -> Value' Instr 'TBls12381G2
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBls12381G2)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBls12381G2
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TBls12381G2))
-> Value' Instr 'TBls12381G2
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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' Instr 'TBls12381G2)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TBls12381G2 -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TBls12381G2
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ DeserializationError -> TCTypeError
InvalidBls12381Object DeserializationError
err)
        (v :: Value
v@(U.ValueString MText
s), t :: SingT tz
t@SingT tz
STTimestamp) -> case Text -> Maybe Timestamp
parseTimestamp (Text -> Maybe Timestamp) -> Text -> Maybe Timestamp
forall a b. (a -> b) -> a -> b
$ MText -> Text
unMText MText
s of
          Just Timestamp
tstamp -> Value' Instr 'TTimestamp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TTimestamp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTimestamp
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TTimestamp))
-> Value' Instr 'TTimestamp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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' Instr 'TTimestamp)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TTimestamp -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing 'TTimestamp
SingT tz
t) Text
"" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
InvalidTimestamp)
        (U.ValueInt Integer
i, SingT tz
STTimestamp) -> Value' Instr 'TTimestamp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TTimestamp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTimestamp
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TTimestamp))
-> Value' Instr 'TTimestamp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TTimestamp)
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' Instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp (Integer -> Timestamp
timestampFromSeconds Integer
i)
        (U.ValueBytes (U.InternalByteString ByteString
s), SingT tz
STBytes) -> Value' Instr 'TBytes
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBytes)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBytes
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TBytes))
-> Value' Instr 'TBytes
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBytes)
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes ByteString
s
        (Value
U.ValueTrue, SingT tz
STBool) -> Value' Instr 'TBool
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBool)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBool
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TBool))
-> Value' Instr 'TBool
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBool)
forall a b. (a -> b) -> a -> b
$ Bool -> Value' Instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool Bool
True
        (Value
U.ValueFalse, SingT tz
STBool) -> Value' Instr 'TBool
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBool)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBool
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TBool))
-> Value' Instr 'TBool
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TBool)
forall a b. (a -> b) -> a -> b
$ Bool -> Value' Instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool Bool
False

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

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

        (U.ValueString (Text -> Either ParseChainIdError ChainId
parseChainId (Text -> Either ParseChainIdError ChainId)
-> (MText -> Text) -> MText -> Either ParseChainIdError ChainId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MText -> Text
unMText -> Right ChainId
ci), SingT tz
STChainId) ->
          Value' Instr 'TChainId
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TChainId)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChainId
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TChainId))
-> Value' Instr 'TChainId
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TChainId)
forall a b. (a -> b) -> a -> b
$ ChainId -> Value' Instr 'TChainId
forall (instr :: [T] -> [T] -> *).
ChainId -> Value' instr 'TChainId
VChainId ChainId
ci
        (U.ValueBytes (ByteString -> Either ParseChainIdError ChainId
mkChainId (ByteString -> Either ParseChainIdError ChainId)
-> (InternalByteString -> ByteString)
-> InternalByteString
-> Either ParseChainIdError ChainId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InternalByteString -> ByteString
U.unInternalByteString -> Right ChainId
ci), SingT tz
STChainId) ->
          Value' Instr 'TChainId
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TChainId)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChainId
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TChainId))
-> Value' Instr 'TChainId
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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 ('TContract n))
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 ('TContract n))
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)) -> (TypeCheckOptions -> Bool)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     Bool
forall (m :: * -> *) r a (n :: Nat).
MultiReader n r m =>
(r -> a) -> m a
asks' TypeCheckOptions -> Bool
tcStrict ReaderT
  TypeCheckInstrEnv
  (ReaderT
     TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
  Bool
-> (Bool
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT
            TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
         (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value tz)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          -- Note [Tickets forging]
          -- Normally, ticket values cannot be constructed manually (i.e. forged)
          -- by design, and the only valid way to make a ticket is calling
          -- @TICKET@ instruction.
          --
          -- However @tezos-client run@ adds an exception, it allows passing a
          -- manually constructed ticket value as parameter or initial storage.
          Bool
True ->
            Value
-> T
-> Text
-> Maybe TCTypeError
-> TypeCheckInstr (Value ('TTicket n))
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 ('TTicket n)))
-> TypeCheckInstr (Value ('TTicket n))
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 ('TTicket n)))
 -> TypeCheckInstr (Value ('TTicket n)))
-> (Comparable n => TypeCheckInstr (Value ('TTicket n)))
-> TypeCheckInstr (Value ('TTicket n))
forall a b. (a -> b) -> a -> b
$ do
              Value' Instr 'TAddress
addrValue <- (Value, Sing 'TAddress) -> TypeCheckInstr (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) -> TypeCheckInstr (Value' Instr 'TNat)
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value
amV, Sing 'TNat
SingT 'TNat
STNat)
              case (Value' Instr 'TAddress
addrValue, Value' Instr 'TNat
amountValue) of
                (VAddress (EpAddress' Address
addr EpName
ep), VNat Natural
am) -> do
                  Bool
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     ()
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (EpName -> Bool
U.isDefEpName EpName
ep) (ReaderT
   TypeCheckInstrEnv
   (ReaderT
      TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
   ()
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      ())
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     ()
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     ()
forall a b. (a -> b) -> a -> b
$
                    Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr ()
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
cv (Sing ('TTicket n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing tz
Sing ('TTicket n)
sng)
                      Text
"it is pointless to provide an address with entrypoint as a \
                      \ticketer, we do not support that"
                      Maybe TCTypeError
forall a. Maybe a
Nothing
                  -- ↑ Tezos allows passing addresses with entrypoint, but it is
                  -- not possible to sanely work with them after that anyway,
                  -- since @TICKET@ instruction (the only valid way of constructing
                  -- tickets in real run) uses @SELF_ADDRESS@ result as ticketer.
                  pure $ Address -> Value n -> Natural -> Value ('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 ('TTicket n))
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
cv (Sing ('TTicket n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing tz
Sing ('TTicket n)
sng)
                Text
"ticket type expects a value of type `(pair address <data> nat)`"
                Maybe TCTypeError
forall a. Maybe a
Nothing

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

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

        -- If ValueSeq contains at least 2 elements, it can be type checked as a
        -- right combed pair.
        (U.ValueSeq vals :: NonEmpty $ Value
vals@(Value
_ :| (Value
_ : [Value]
_)), STPair Sing n1
_ Sing n2
_) ->
          (Value, Sing ('TPair n1 n2))
-> TypeCheckInstr (Value ('TPair n1 n2))
forall (tz :: T). (Value, Sing tz) -> TypeCheckInstr (Value tz)
doTypeCheckVal ((NonEmpty $ Value) -> Value
seqToRightCombedPair NonEmpty $ Value
vals, Sing tz
Sing ('TPair n1 n2)
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 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
l ((SingI n =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value tz))
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TList n)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr ('TList n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TList n)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr ('TList n)))
-> Value' Instr ('TList n)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr ('TList n))
forall a b. (a -> b) -> a -> b
$ [Value n] -> Value' Instr ('TList n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList [Value n]
els

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

        (sq :: Value
sq@(U.ValueSeq ((NonEmpty $ Value) -> [Element (NonEmpty $ Value)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Value)]
mels)), s :: SingT tz
s@(STSet Sing n
vt)) -> Sing n
-> Value
-> Sing ('TSet n)
-> (Comparable n => TypeCheckInstr (Value ('TSet n)))
-> TypeCheckInstr (Value ('TSet n))
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 ('TSet n)))
 -> TypeCheckInstr (Value ('TSet n)))
-> (Comparable n => TypeCheckInstr (Value ('TSet n)))
-> TypeCheckInstr (Value ('TSet n))
forall a b. (a -> b) -> a -> b
$ do
          ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     ErrorSrcPos
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
Lens' TypeCheckInstrEnv ErrorSrcPos
tcieErrorPos

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

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

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

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

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

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

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

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

        (v :: Value
v@(U.ValueBytes (U.InternalByteString ByteString
bs)), SingT tz
STChest) ->
          case ByteString -> Either Text Chest
chestFromBytes ByteString
bs of
            Right Chest
res -> Value' Instr 'TChest
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TChest)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChest
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TChest))
-> Value' Instr 'TChest
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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' Instr 'TChest)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v T
T.TChest Text
err Maybe TCTypeError
forall a. Maybe a
Nothing

        (v :: Value
v@(U.ValueBytes (U.InternalByteString ByteString
bs)), SingT tz
STChestKey) ->
          case ByteString -> Either Text ChestKey
chestKeyFromBytes ByteString
bs of
            Right ChestKey
res -> Value' Instr 'TChestKey
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (Value' Instr 'TChestKey)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChestKey
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
      (Value' Instr 'TChestKey))
-> Value' Instr 'TChestKey
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        TypeCheckEnv (ReaderT TypeCheckOptions (ExceptT TCError Identity)))
     (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' Instr 'TChestKey)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v T
T.TChestKey Text
err Maybe TCTypeError
forall a. Maybe a
Nothing

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

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

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

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

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

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

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

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

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

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

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

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

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