-- 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' [] op -> T.T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue :: forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v T
t Text
msg Maybe TcTypeError
err = do
  ErrorSrcPos
loc <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall a.
TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      a)
-> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall a b. (a -> b) -> a -> b
$ Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
forall op.
Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
TcFailedOnValue Value' [] op
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 op.
     (SingI ty, IsInstrOp op)
  => Maybe TcOriginatedContracts
  -> TcInstrBase op
  -> U.Value' [] op
  -> TypeCheckInstr op (T.Value ty)
typeCheckValImpl :: forall (ty :: T) op.
(SingI ty, IsInstrOp op) =>
Maybe TcOriginatedContracts
-> TcInstrBase op -> Value' [] op -> TypeCheckInstr op (Value ty)
typeCheckValImpl Maybe TcOriginatedContracts
mOriginatedContracts TcInstrBase op
tcDo Value' [] op
uv = (Value' [] op, Sing ty)
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     (Value' Instr ty)
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
uv, forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @ty)
  where
    doTypeCheckVal :: forall tz. (U.Value' [] op, Sing tz) -> TypeCheckInstr op (T.Value tz)
    doTypeCheckVal :: forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
uvalue, Sing tz
sng) = do
      TypeCheckMode op
typeCheckMode <- (TypeCheckEnv op -> TypeCheckMode op)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (TypeCheckMode op)
forall (m :: * -> *) r a (n :: Peano).
MultiReader n r m =>
(r -> a) -> m a
asks' (forall op. TypeCheckEnv op -> TypeCheckMode op
tcMode @op)
      case (Value' [] op
uvalue, Sing tz
SingT tz
sng) of
        (U.ValueInt Integer
i, SingT tz
STInt) -> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TNat)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v (Sing 'TNat -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing Sing 'TNat
SingT tz
t) Text
"" (TcTypeError -> Maybe TcTypeError
forall a. a -> Maybe a
Just TcTypeError
NegativeNat)
        (v :: Value' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TMutez)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v (Sing 'TMutez -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op, T)
_ (Just BigMapFinder
bigMapFinder) <- TypeCheckMode op
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 op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI ('TBigMap n1 n2) =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 op)
          (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
       x)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (forall {x}.
    MismatchError T
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT
            (TypeCheckEnv op)
            (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
         x)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$
                Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op x
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
uvalue (Sing ('TBigMap n1 n2) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing Sing tz
Sing ('TBigMap n1 n2)
sng) Text
"" (Maybe TcTypeError
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      x)
-> (MismatchError T -> Maybe TcTypeError)
-> MismatchError T
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value ('TBigMap n1 n2))
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
uvalue (Sing ('TBigMap n1 n2) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ MText -> Value' Instr 'TString
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString MText
s
        (v :: Value' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TAddress)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v (Sing 'TAddress -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TAddress)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v (Sing 'TAddress -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TKeyHash)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v (Sing 'TKeyHash -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TKeyHash)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v (Sing 'TKeyHash -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing Sing 'TKeyHash
SingT tz
t) Text
"" (TcTypeError -> Maybe TcTypeError
forall a. a -> Maybe a
Just (TcTypeError -> Maybe TcTypeError)
-> TcTypeError -> Maybe TcTypeError
forall a b. (a -> b) -> a -> b
$ CryptoParseError -> TcTypeError
InvalidKeyHash CryptoParseError
err)
        (U.ValueInt Integer
i, SingT tz
STBls12381Fr) ->
          Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TBls12381Fr)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v (Sing 'TBls12381Fr -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TBls12381G1)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v (Sing 'TBls12381G1 -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TBls12381G2)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v (Sing 'TBls12381G2 -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TTimestamp)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v (Sing 'TTimestamp -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes ByteString
s
        (Value' [] op
U.ValueTrue, SingT tz
STBool) -> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Bool -> Value' Instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool Bool
True
        (Value' [] op
U.ValueFalse, SingT tz
STBool) -> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ ChainId -> Value' Instr 'TChainId
forall (instr :: [T] -> [T] -> *).
ChainId -> Value' instr 'TChainId
VChainId ChainId
ci

        (cv :: Value' [] op
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' [] op
-> EpAddress -> Sing n -> TypeCheckInstr op (Value ('TContract n))
forall (cp :: T) (tz :: T).
(tz ~ 'TContract cp) =>
Value' [] op
-> EpAddress -> Sing cp -> TypeCheckInstr op (Value tz)
typecheckContractValue Value' [] op
cv EpAddress
addr Sing n
pc
        (cv :: Value' [] op
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' [] op
-> EpAddress -> Sing n -> TypeCheckInstr op (Value ('TContract n))
forall (cp :: T) (tz :: T).
(tz ~ 'TContract cp) =>
Value' [] op
-> EpAddress -> Sing cp -> TypeCheckInstr op (Value tz)
typecheckContractValue Value' [] op
cv EpAddress
addr Sing n
pc

        (Value' [] op
cv, s :: SingT tz
s@(STTicket Sing n
vt)) -> (TypeCheckOptions -> Bool)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     Bool
forall (m :: * -> *) r a (n :: Peano).
MultiReader n r m =>
(r -> a) -> m a
asks' TypeCheckOptions -> Bool
tcStrict ReaderT
  TypeCheckInstrEnv
  (ReaderT
     (TypeCheckEnv op)
     (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
  Bool
-> (Bool
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT
            (TypeCheckEnv op)
            (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
         (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b.
ReaderT
  TypeCheckInstrEnv
  (ReaderT
     (TypeCheckEnv op)
     (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
  a
-> (a
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT
            (TypeCheckEnv op)
            (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
         b)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     b
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 @octez-client run@ adds an exception, it allows passing a
          -- manually constructed ticket value as parameter or initial storage.
          --
          -- Since protocol lima zero amount tickets are no longer allowed
          -- event in "lax" mode, so we forbid them here is well. (see !1270)
          Bool
True ->
            Value' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value ('TTicket n))
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
cv (Sing ('TTicket n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op
cv of
            U.ValuePair Value' [] op
addrV (U.ValuePair Value' [] op
datV Value' [] op
amV) -> Sing n
-> Value' [] op
-> Sing ('TTicket n)
-> (Comparable n => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (Comparable a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withComparable Sing n
vt Value' [] op
cv Sing ('TTicket n)
SingT tz
s ((Comparable n => TypeCheckInstr op (Value tz))
 -> TypeCheckInstr op (Value tz))
-> (Comparable n => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall a b. (a -> b) -> a -> b
$ do
              Value' Instr 'TAddress
addrValue <- (Value' [] op, Sing 'TAddress)
-> TypeCheckInstr op (Value' Instr 'TAddress)
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
addrV, Sing 'TAddress
SingT 'TAddress
STAddress)
              Value n
dat <- (Value' [] op, Sing n) -> TypeCheckInstr op (Value n)
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
datV, Sing n
vt)
              Value' Instr 'TNat
amountValue <- (Value' [] op, Sing 'TNat)
-> TypeCheckInstr op (Value' Instr 'TNat)
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
amV, Sing 'TNat
SingT 'TNat
STNat)
              case (Value' Instr 'TAddress
addrValue, Value' Instr 'TNat
amountValue) of
                (Value' Instr 'TAddress
_, VNat Natural
0) ->
                  Value' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value ('TTicket n))
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
cv (Sing ('TTicket n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing Sing tz
Sing ('TTicket n)
sng) Text
"ticket amount of 0 is not allowed"
                  Maybe TcTypeError
forall a. Maybe a
Nothing
                (VAddress (EpAddress' Address
addr EpName
ep), VNat Natural
am) -> do
                  Bool
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (EpName -> Bool
U.isDefEpName EpName
ep) (ReaderT
   TypeCheckInstrEnv
   (ReaderT
      (TypeCheckEnv op)
      (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
   ()
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      ())
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
forall a b. (a -> b) -> a -> b
$
                    Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op ()
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
cv (Sing ('TTicket n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op
_ ->
              Value' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value ('TTicket n))
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
cv (Sing ('TTicket n) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op
U.ValueUnit, SingT tz
STUnit) -> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Value tz
Value' Instr 'TUnit
forall (instr :: [T] -> [T] -> *). Value' instr 'TUnit
VUnit
        (U.ValuePair Value' [] op
ml Value' [] op
mr, STPair Sing n1
lt Sing n2
rt) -> do
          Value' Instr n1
l <- (Value' [] op, Sing n1) -> TypeCheckInstr op (Value' Instr n1)
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
ml, Sing n1
lt)
          Value' Instr n2
r <- (Value' [] op, Sing n2) -> TypeCheckInstr op (Value' Instr n2)
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
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' [] op
ml, STOr Sing n1
lt Sing n2
rt) -> do
          Value n1
l <- (Value' [] op, Sing n1) -> TypeCheckInstr op (Value n1)
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
ml, Sing n1
lt)
          Sing n1
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
lt ((SingI n1 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
rt ((SingI n2 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
mr, STOr Sing n1
lt Sing n2
rt) -> do
          Value n2
r <- (Value' [] op, Sing n2) -> TypeCheckInstr op (Value n2)
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
mr, Sing n2
rt)
          Sing n1
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
lt ((SingI n1 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
rt ((SingI n2 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
mv, STOption Sing n
op) -> do
          Value n
v <- (Value' [] op, Sing n) -> TypeCheckInstr op (Value n)
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
mv, Sing n
op)
          Sing n
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
op ((SingI n =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
U.ValueNone, STOption Sing n
op) -> do
          Sing n
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
op ((SingI n =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
U.ValueNil, STList Sing n
l) -> Sing n
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
l ((SingI n =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$
          Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
vals@(Value' [] op
_ :| (Value' [] op
_ : [Value' [] op]
_)), STPair Sing n1
_ Sing n2
_) ->
          (Value' [] op, Sing ('TPair n1 n2))
-> TypeCheckInstr op (Value ('TPair n1 n2))
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal ((NonEmpty $ Value' [] op) -> Value' [] op
seqToRightCombedPair NonEmpty $ Value' [] op
vals, Sing tz
Sing ('TPair n1 n2)
sng)

        (U.ValueSeq ((NonEmpty $ Value' [] op) -> [Element (NonEmpty $ Value' [] op)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Value' [] op)]
mels), STList Sing n
l) -> do
          [Value n]
els <- ([Value' [] op], Sing n) -> TypeCheckInstr op [Value n]
forall (t :: T).
([Value' [] op], Sing t) -> TypeCheckInstr op [Value t]
typeCheckValsImpl ([Element (NonEmpty $ Value' [] op)]
[Value' [] op]
mels, Sing n
l)
          Sing n
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
l ((SingI n =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
U.ValueNil, STSet Sing n
s) -> do
          ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 (t :: T). Sing t -> Maybe (Dict (Comparable t))
T.comparabilityPresence Sing n
s of
            Just Dict (Comparable n)
Dict -> Sing n
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
s ((SingI n =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Value' Instr n) -> Value' Instr ('TSet n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
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' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
forall op.
Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
TcFailedOnValue Value' [] op
uvalue (Sing n -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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
forall (a :: T). Sing a -> Demote T
fromSing Sing n
s) BadTypeForScope
T.BtNotComparable)

        (sq :: Value' [] op
sq@(U.ValueSeq ((NonEmpty $ Value' [] op) -> [Element (NonEmpty $ Value' [] op)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Value' [] op)]
mels)), s :: SingT tz
s@(STSet Sing n
vt)) -> Sing n
-> Value' [] op
-> Sing ('TSet n)
-> (Comparable n => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (Comparable a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withComparable Sing n
vt Value' [] op
sq Sing ('TSet n)
SingT tz
s ((Comparable n => TypeCheckInstr op (Value tz))
 -> TypeCheckInstr op (Value tz))
-> (Comparable n => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall a b. (a -> b) -> a -> b
$ do
          ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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' [] op], Sing n) -> TypeCheckInstr op [Value n]
forall (t :: T).
([Value' [] op], Sing t) -> TypeCheckInstr op [Value t]
typeCheckValsImpl ([Element (NonEmpty $ Value' [] op)]
[Value' [] op]
mels, Sing n
vt)
          Set (Value n)
elsS <- Either (TcError' op) (Set (Value n))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Set (Value n))
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either (TcError' op) (Set (Value n))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Set (Value n)))
-> Either (TcError' op) (Set (Value n))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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' op) [Value n]
-> Either (TcError' op) (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' op) -> Either (TcError' op) [Value n]
forall (p :: * -> * -> *) a c b.
Bifunctor p =>
p a c -> (a -> b) -> p b c
`onFirst` \Text
msg -> Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
forall op.
Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
TcFailedOnValue Value' [] op
sq (Sing n -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing Sing n
vt) Text
msg ErrorSrcPos
instrPos Maybe TcTypeError
forall a. Maybe a
Nothing
          Sing n
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TSet n)))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value ('TSet n)))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TSet n)))
-> (SingI n =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TSet n)))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TSet n))
forall a b. (a -> b) -> a -> b
$ Value ('TSet n)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TSet n))
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TSet n)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TSet n)))
-> Value ('TSet n)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TSet n))
forall a b. (a -> b) -> a -> b
$ Set (Value n) -> Value ('TSet n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
Comparable t1 =>
Set (Value' instr t1) -> Value' instr ('TSet t1)
VSet Set (Value n)
elsS

        (v :: Value' [] op
v@Value' [] op
U.ValueNil, s :: SingT tz
s@(STMap Sing n1
st Sing n2
vt)) ->
          Sing n1
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
st ((SingI n1 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
vt ((SingI n2 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n1
-> Value' [] op
-> Sing ('TMap n1 n2)
-> (Comparable n1 => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (Comparable a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withComparable Sing n1
st Value' [] op
v Sing ('TMap n1 n2)
SingT tz
s ((Comparable n1 => TypeCheckInstr op (Value tz))
 -> TypeCheckInstr op (Value tz))
-> (Comparable n1 => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall a b. (a -> b) -> a -> b
$ Value tz -> TypeCheckInstr op (Value tz)
forall a.
a
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz -> TypeCheckInstr op (Value tz))
-> Value tz -> TypeCheckInstr op (Value tz)
forall a b. (a -> b) -> a -> b
$ Map (Value' Instr n1) (Value' Instr n2)
-> Value' Instr ('TMap n1 n2)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(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' [] op
sq@(U.ValueMap ((NonEmpty $ Elt [] op) -> [Element (NonEmpty $ Elt [] op)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Elt [] op)]
mels)), s :: SingT tz
s@(STMap Sing n1
kt Sing n2
vt)) ->
          Sing n1
-> Value' [] op
-> Sing ('TMap n1 n2)
-> (Comparable n1 => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (Comparable a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withComparable Sing n1
kt Value' [] op
sq Sing ('TMap n1 n2)
SingT tz
s ((Comparable n1 => TypeCheckInstr op (Value tz))
 -> TypeCheckInstr op (Value tz))
-> (Comparable n1 => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall a b. (a -> b) -> a -> b
$ do
            [(Value n1, Value n2)]
keyOrderedElts <- [Elt [] op]
-> Value' [] op
-> Sing n1
-> Sing n2
-> TypeCheckInstr op [(Value n1, Value n2)]
forall (kt :: T) (vt :: T).
[Elt [] op]
-> Value' [] op
-> Sing kt
-> Sing vt
-> TypeCheckInstr op [(Value kt, Value vt)]
typeCheckMapVal [Element (NonEmpty $ Elt [] op)]
[Elt [] op]
mels Value' [] op
sq Sing n1
kt Sing n2
vt
            Sing n1
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TMap n1 n2)))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value ('TMap n1 n2)))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TMap n1 n2)))
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TMap n1 n2)))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TMap n1 n2))
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TMap n1 n2)))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value ('TMap n1 n2)))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TMap n1 n2)))
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TMap n1 n2)))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TMap n1 n2))
forall a b. (a -> b) -> a -> b
$
              Value ('TMap n1 n2)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TMap n1 n2))
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TMap n1 n2)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TMap n1 n2)))
-> Value ('TMap n1 n2)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 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' [] op
v@Value' [] op
U.ValueNil, s :: SingT tz
s@(STBigMap Sing n1
st1 Sing n2
st2)) ->
          Sing n1
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
st1 ((SingI n1 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
st2 ((SingI n2 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n1
-> Value' [] op
-> Sing ('TBigMap n1 n2)
-> (Comparable n1 => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (Comparable a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withComparable Sing n1
st1 Value' [] op
v Sing ('TBigMap n1 n2)
SingT tz
s ((Comparable n1 => TypeCheckInstr op (Value tz))
 -> TypeCheckInstr op (Value tz))
-> (Comparable n1 => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> Value' [] op
-> Sing ('TBigMap n1 n2)
-> (ForbidBigMap n2 => TypeCheckInstr op (Value ('TBigMap n1 n2)))
-> TypeCheckInstr op (Value ('TBigMap n1 n2))
forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (ForbidBigMap a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withBigMapAbsence Sing n2
st2 Value' [] op
v Sing ('TBigMap n1 n2)
SingT tz
s ((ForbidBigMap n2 => TypeCheckInstr op (Value ('TBigMap n1 n2)))
 -> TypeCheckInstr op (Value ('TBigMap n1 n2)))
-> (ForbidBigMap n2 => TypeCheckInstr op (Value ('TBigMap n1 n2)))
-> TypeCheckInstr op (Value ('TBigMap n1 n2))
forall a b. (a -> b) -> a -> b
$
            Value ('TBigMap n1 n2)
-> TypeCheckInstr op (Value ('TBigMap n1 n2))
forall a.
a
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TBigMap n1 n2)
 -> TypeCheckInstr op (Value ('TBigMap n1 n2)))
-> Value ('TBigMap n1 n2)
-> TypeCheckInstr op (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 v, Comparable k, ForbidBigMap 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' [] op
sq@(U.ValueMap ((NonEmpty $ Elt [] op) -> [Element (NonEmpty $ Elt [] op)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Elt [] op)]
mels)), s :: SingT tz
s@(STBigMap Sing n1
kt Sing n2
vt)) ->
          Sing n1
-> Value' [] op
-> Sing ('TBigMap n1 n2)
-> (Comparable n1 => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (Comparable a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withComparable Sing n1
kt Value' [] op
sq Sing ('TBigMap n1 n2)
SingT tz
s ((Comparable n1 => TypeCheckInstr op (Value tz))
 -> TypeCheckInstr op (Value tz))
-> (Comparable n1 => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> Value' [] op
-> Sing ('TBigMap n1 n2)
-> (ForbidBigMap n2 => TypeCheckInstr op (Value ('TBigMap n1 n2)))
-> TypeCheckInstr op (Value ('TBigMap n1 n2))
forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (ForbidBigMap a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withBigMapAbsence Sing n2
vt Value' [] op
sq Sing ('TBigMap n1 n2)
SingT tz
s ((ForbidBigMap n2 => TypeCheckInstr op (Value ('TBigMap n1 n2)))
 -> TypeCheckInstr op (Value ('TBigMap n1 n2)))
-> (ForbidBigMap n2 => TypeCheckInstr op (Value ('TBigMap n1 n2)))
-> TypeCheckInstr op (Value ('TBigMap n1 n2))
forall a b. (a -> b) -> a -> b
$ do
            [(Value n1, Value n2)]
keyOrderedElts <- [Elt [] op]
-> Value' [] op
-> Sing n1
-> Sing n2
-> TypeCheckInstr op [(Value n1, Value n2)]
forall (kt :: T) (vt :: T).
[Elt [] op]
-> Value' [] op
-> Sing kt
-> Sing vt
-> TypeCheckInstr op [(Value kt, Value vt)]
typeCheckMapVal [Element (NonEmpty $ Elt [] op)]
[Elt [] op]
mels Value' [] op
sq Sing n1
kt Sing n2
vt
            Sing n1
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TBigMap n1 n2)))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value ('TBigMap n1 n2)))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TBigMap n1 n2)))
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TBigMap n1 n2)))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TBigMap n1 n2))
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TBigMap n1 n2)))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value ('TBigMap n1 n2)))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TBigMap n1 n2)))
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TBigMap n1 n2)))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TBigMap n1 n2))
forall a b. (a -> b) -> a -> b
$
              Value ('TBigMap n1 n2)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TBigMap n1 n2))
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TBigMap n1 n2)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TBigMap n1 n2)))
-> Value ('TBigMap n1 n2)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 v, Comparable k, ForbidBigMap 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 [op]
s, STList Sing n
l) ->
          case (op -> Maybe (Value' [] op)) -> [op] -> Maybe [Value' [] op]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse op -> Maybe (Value' [] op)
forall op. IsInstrOp op => op -> Maybe (Value' [] op)
tryOpToVal [op]
s of
            Just [Value' [] op]
xs -> (Value' [] op, Sing ('TList n))
-> TypeCheckInstr op (Value ('TList n))
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
-> ((NonEmpty $ Value' [] op) -> Value' [] op)
-> Maybe (NonEmpty $ Value' [] op)
-> Value' [] op
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Value' [] op
forall {k} (f :: k -> *) (op :: k). Value' f op
U.ValueNil (NonEmpty $ Value' [] op) -> Value' [] op
forall {k} (f :: k -> *) (op :: k).
(NonEmpty $ Value' f op) -> Value' f op
U.ValueSeq (Maybe (NonEmpty $ Value' [] op) -> Value' [] op)
-> Maybe (NonEmpty $ Value' [] op) -> Value' [] op
forall a b. (a -> b) -> a -> b
$ [Value' [] op] -> Maybe (NonEmpty $ Value' [] op)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [Value' [] op]
xs, Sing tz
Sing ('TList n)
sng)
            Maybe [Value' [] op]
Nothing -> Value' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value ('TList n))
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
uvalue (Sing n -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing Sing n
l) Text
"" Maybe TcTypeError
forall a. Maybe a
Nothing

        (U.ValueSeq NonEmpty $ Value' [] op
s, STLambda Sing n1
_ Sing n2
_) -> case (Value' [] op -> Maybe op)
-> (NonEmpty $ Value' [] op) -> Maybe (NonEmpty op)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse Value' [] op -> Maybe op
forall op. IsInstrOp op => Value' [] op -> Maybe op
tryValToOp NonEmpty $ Value' [] op
s of
          Just NonEmpty op
xs -> (Value' [] op, Sing ('TLambda n1 n2))
-> TypeCheckInstr op (Value ('TLambda n1 n2))
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal ([op] -> Value' [] op
forall {k} (f :: k -> *) (op :: k). f op -> Value' f op
U.ValueLambda ([op] -> Value' [] op) -> [op] -> Value' [] op
forall a b. (a -> b) -> a -> b
$ NonEmpty op -> [Element (NonEmpty op)]
forall t. Container t => t -> [Element t]
toList NonEmpty op
xs, Sing tz
Sing ('TLambda n1 n2)
sng)
          Maybe (NonEmpty op)
Nothing -> Value' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value ('TLambda n1 n2))
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
uvalue (Sing ('TLambda n1 n2) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing Sing tz
Sing ('TLambda n1 n2)
sng) Text
"" Maybe TcTypeError
forall a. Maybe a
Nothing

        (U.ValueLamRec [op]
mp, lam :: Sing tz
lam@(STLambda (Sing n1
var :: Sing it) (Sing n2
b :: Sing ot)) :: Sing lam) ->
          Sing n1
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
var ((SingI n1 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
b ((SingI n2 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ do
            HST '[n1, 'TLambda n1 n2]
_ :/ SomeTcInstrOut '[n1, 'TLambda n1 n2]
instr <-
              forall (t :: T) a.
SingI t =>
Value' [] op
-> (WellTyped t => TypeCheckInstr op a) -> TypeCheckInstr op a
withWTP @lam Value' [] op
uvalue ((WellTyped tz =>
  TypeCheckInstr op (SomeTcInstr '[n1, 'TLambda n1 n2]))
 -> TypeCheckInstr op (SomeTcInstr '[n1, 'TLambda n1 n2]))
-> (WellTyped tz =>
    TypeCheckInstr op (SomeTcInstr '[n1, 'TLambda n1 n2]))
-> TypeCheckInstr op (SomeTcInstr '[n1, 'TLambda n1 n2])
forall a b. (a -> b) -> a -> b
$ ReaderT
  TypeCheckInstrEnv
  (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq op '[n1, 'TLambda n1 n2])
-> TypeCheckInstr op (SomeTcInstr '[n1, 'TLambda n1 n2])
forall op (inp :: [T]) (m :: * -> *) (m' :: * -> *).
(MonadMultiReaderT m Identity,
 m' ~ ChangeMultiReaderBase m (Except (TcError' op)),
 MonadError (TcError' op) m') =>
m (TypeCheckedSeq op inp) -> m' (SomeTcInstr inp)
throwingTcError (ReaderT
   TypeCheckInstrEnv
   (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
   (TypeCheckedSeq op '[n1, 'TLambda n1 n2])
 -> TypeCheckInstr op (SomeTcInstr '[n1, 'TLambda n1 n2]))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op '[n1, 'TLambda n1 n2])
-> TypeCheckInstr op (SomeTcInstr '[n1, 'TLambda n1 n2])
forall a b. (a -> b) -> a -> b
$
                TcInstrBase op -> TcInstr op [op]
forall op. IsInstrOp op => TcInstrBase op -> TcInstr op [op]
typeCheckImpl
                  -- lambdas can contain operations forbidden inside views, hence
                  -- we invent a "not in view" constraint here.
                  ((IsNotInView =>
 op -> HST inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> op
-> HST inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall r. (IsNotInView => r) -> r
giveNotInView ((IsNotInView =>
  op -> HST inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
 -> op
 -> HST inp
 -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> (IsNotInView =>
    op -> HST inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> op
-> HST inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall a b. (a -> b) -> a -> b
$ (TypeCheckInstrEnv -> TypeCheckInstrEnv)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp)
forall a.
(TypeCheckInstrEnv -> TypeCheckInstrEnv)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     a
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 op) (ReaderT TypeCheckOptions Identity))
   (TypeCheckedSeq op inp)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq op inp))
-> (op
    -> HST inp
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq op inp))
-> op
-> HST inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp)
forall a b c. SuperComposition a b c => a -> b -> c
... op
-> HST inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp)
op -> HST inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
TcInstrBase op
tcDo)
                  ([op] -> [Element [op]]
forall t. Container t => t -> [Element t]
toList [op]
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 '[ 'TLambda n1 n2] -> HST '[n1, 'TLambda n1 n2]
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& (Sing tz
SingT ('TLambda n1 n2)
lam, Dict (WellTyped ('TLambda n1 n2))
forall (a :: Constraint). a => Dict a
Dict) (SingT ('TLambda n1 n2), Dict (WellTyped ('TLambda n1 n2)))
-> HST '[] -> HST '[ 'TLambda n1 n2]
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(SingT x, Dict (WellTyped x)) -> HST xs -> HST (x : xs)
::& HST '[]
SNil)
            case SomeTcInstrOut '[n1, 'TLambda n1 n2]
instr of
              Instr '[n1, 'TLambda n1 n2] out
code ::: (HST out
lo :: HST lo) -> forall (t :: T) a.
SingI t =>
Value' [] op
-> (WellTyped t => TypeCheckInstr op a) -> TypeCheckInstr op a
withWTP @ot Value' [] op
uvalue ((WellTyped n2 => TypeCheckInstr op (Value tz))
 -> TypeCheckInstr op (Value tz))
-> (WellTyped n2 => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
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 tz -> TypeCheckInstr op (Value tz)
forall a.
a
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz -> TypeCheckInstr op (Value tz))
-> Value tz -> TypeCheckInstr op (Value tz)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[n1, 'TLambda n1 n2] '[n2])
-> Value' Instr ('TLambda n1 n2)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
(IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out])
-> Value' instr ('TLambda inp out)
T.mkVLamRec (Instr '[n1, 'TLambda n1 n2] '[n2]
-> RemFail Instr '[n1, 'TLambda n1 n2] '[n2]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
T.RfNormal Instr '[n1, 'TLambda n1 n2] out
Instr '[n1, 'TLambda n1 n2] '[n2]
code)
                  Left TcTypeError
m ->
                    Value' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr ('TLambda n1 n2))
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
uvalue (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, 'TLambda n1 n2] out
code ->
                Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[n1, 'TLambda n1 n2] '[n2])
-> Value' Instr ('TLambda n1 n2)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
(IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out])
-> Value' instr ('TLambda inp out)
T.mkVLamRec ((forall (out :: [T]). Instr '[n1, 'TLambda n1 n2] out)
-> RemFail Instr '[n1, 'TLambda n1 n2] '[n2]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
T.RfAlwaysFails Instr '[n1, 'TLambda n1 n2] o'
forall (out :: [T]). Instr '[n1, 'TLambda n1 n2] out
code)

        (Value' [] op
v, STLambda (Sing n1
var :: Sing it) (Sing n2
b :: Sing ot)) -> Sing n1
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
var ((SingI n1 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n1 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
b ((SingI n2 =>
  ReaderT
    TypeCheckInstrEnv
    (ReaderT
       (TypeCheckEnv op)
       (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
    (Value tz))
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> (SingI n2 =>
    ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ do
          [op]
mp <- case Value' [] op
v of
            Value' [] op
U.ValueNil       -> [op]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     [op]
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
            U.ValueLambda [op]
mp -> [op]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     [op]
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([op]
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      [op])
-> [op]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     [op]
forall a b. (a -> b) -> a -> b
$ [op] -> [Element [op]]
forall t. Container t => t -> [Element t]
toList [op]
mp
            Value' [] op
_ -> Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op [op]
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
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]
_ :/ SomeTcInstrOut '[n1]
instr <-
            forall (t :: T) a.
SingI t =>
Value' [] op
-> (WellTyped t => TypeCheckInstr op a) -> TypeCheckInstr op a
withWTP @it Value' [] op
uvalue ((WellTyped n1 => TypeCheckInstr op (SomeTcInstr '[n1]))
 -> TypeCheckInstr op (SomeTcInstr '[n1]))
-> (WellTyped n1 => TypeCheckInstr op (SomeTcInstr '[n1]))
-> TypeCheckInstr op (SomeTcInstr '[n1])
forall a b. (a -> b) -> a -> b
$ ReaderT
  TypeCheckInstrEnv
  (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
  (TypeCheckedSeq op '[n1])
-> TypeCheckInstr op (SomeTcInstr '[n1])
forall op (inp :: [T]) (m :: * -> *) (m' :: * -> *).
(MonadMultiReaderT m Identity,
 m' ~ ChangeMultiReaderBase m (Except (TcError' op)),
 MonadError (TcError' op) m') =>
m (TypeCheckedSeq op inp) -> m' (SomeTcInstr inp)
throwingTcError (ReaderT
   TypeCheckInstrEnv
   (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
   (TypeCheckedSeq op '[n1])
 -> TypeCheckInstr op (SomeTcInstr '[n1]))
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op '[n1])
-> TypeCheckInstr op (SomeTcInstr '[n1])
forall a b. (a -> b) -> a -> b
$
              TcInstrBase op -> TcInstr op [op]
forall op. IsInstrOp op => TcInstrBase op -> TcInstr op [op]
typeCheckImpl
                -- lambdas can contain operations forbidden inside views, hence
                -- we invent a "not in view" constraint here.
                ((IsNotInView =>
 op -> HST inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> op
-> HST inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall r. (IsNotInView => r) -> r
giveNotInView ((IsNotInView =>
  op -> HST inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
 -> op
 -> HST inp
 -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> (IsNotInView =>
    op -> HST inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
-> op
-> HST inp
-> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
forall a b. (a -> b) -> a -> b
$ (TypeCheckInstrEnv -> TypeCheckInstrEnv)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp)
forall a.
(TypeCheckInstrEnv -> TypeCheckInstrEnv)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     a
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 op) (ReaderT TypeCheckOptions Identity))
   (TypeCheckedSeq op inp)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
      (TypeCheckedSeq op inp))
-> (op
    -> HST inp
    -> ReaderT
         TypeCheckInstrEnv
         (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
         (TypeCheckedSeq op inp))
-> op
-> HST inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp)
forall a b c. SuperComposition a b c => a -> b -> c
... op
-> HST inp
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT (TypeCheckEnv op) (ReaderT TypeCheckOptions Identity))
     (TypeCheckedSeq op inp)
op -> HST inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
TcInstrBase op
tcDo)
                [op]
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 SomeTcInstrOut '[n1]
instr of
            Instr '[n1] out
lam ::: (HST out
lo :: HST lo) -> forall (t :: T) a.
SingI t =>
Value' [] op
-> (WellTyped t => TypeCheckInstr op a) -> TypeCheckInstr op a
withWTP @ot Value' [] op
uvalue ((WellTyped n2 => TypeCheckInstr op (Value tz))
 -> TypeCheckInstr op (Value tz))
-> (WellTyped n2 => TypeCheckInstr op (Value tz))
-> TypeCheckInstr op (Value tz)
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 tz -> TypeCheckInstr op (Value tz)
forall a.
a
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz -> TypeCheckInstr op (Value tz))
-> Value tz -> TypeCheckInstr op (Value tz)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[n1] '[n2])
-> Value' Instr ('TLambda n1 n2)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
(IsNotInView => RemFail instr '[inp] '[out])
-> Value' instr ('TLambda inp out)
T.mkVLam (Instr '[n1] '[n2] -> RemFail Instr '[n1] '[n2]
forall {k} (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
T.RfNormal Instr '[n1] out
Instr '[n1] '[n2]
lam)
                Left TcTypeError
m ->
                  Value' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr ('TLambda n1 n2))
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
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 tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[n1] '[n2])
-> Value' Instr ('TLambda n1 n2)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
(IsNotInView => RemFail instr '[inp] '[out])
-> Value' instr ('TLambda inp out)
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 Instr '[n1] o'
forall (out :: [T]). Instr '[n1] out
lam)

        (v :: Value' [] op
v@(U.ValueBytes (U.InternalByteString ByteString
bs)), SingT tz
STChest) -> do
          Bool
isStrict <- (TypeCheckOptions -> Bool)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     Bool
forall (m :: * -> *) r a (n :: Peano).
MultiReader n r m =>
(r -> a) -> m a
asks' TypeCheckOptions -> Bool
tcStrict
          Bool
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isStrict (ReaderT
   TypeCheckInstrEnv
   (ReaderT
      (TypeCheckEnv op)
      (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
   ()
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      ())
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
forall a b. (a -> b) -> a -> b
$ Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op ()
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v T
T.TChest Text
"chest type temporarily deprecated" Maybe TcTypeError
forall a. Maybe a
Nothing
          case ByteString -> Either Text Chest
chestFromBytes ByteString
bs of
            Right Chest
res -> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TChest)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v T
T.TChest Text
err Maybe TcTypeError
forall a. Maybe a
Nothing

        (v :: Value' [] op
v@(U.ValueBytes (U.InternalByteString ByteString
bs)), SingT tz
STChestKey) -> do
          Bool
isStrict <- (TypeCheckOptions -> Bool)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     Bool
forall (m :: * -> *) r a (n :: Peano).
MultiReader n r m =>
(r -> a) -> m a
asks' TypeCheckOptions -> Bool
tcStrict
          Bool
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isStrict (ReaderT
   TypeCheckInstrEnv
   (ReaderT
      (TypeCheckEnv op)
      (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
   ()
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      ())
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ()
forall a b. (a -> b) -> a -> b
$
            Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op ()
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v T
T.TChestKey Text
"chest_key type temporarily deprecated" Maybe TcTypeError
forall a. Maybe a
Nothing
          case ByteString -> Either Text ChestKey
chestKeyFromBytes ByteString
bs of
            Right ChestKey
res -> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value tz
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value tz))
-> Value tz
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value tz)
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' [] op
-> T
-> Text
-> Maybe TcTypeError
-> TypeCheckInstr op (Value' Instr 'TChestKey)
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
v T
T.TChestKey Text
err Maybe TcTypeError
forall a. Maybe a
Nothing

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

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

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

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

    withWTP
      :: forall t a. SingI t
      => U.Value' [] op
      -> (T.WellTyped t => TypeCheckInstr op a)
      -> TypeCheckInstr op a
    withWTP :: forall (t :: T) a.
SingI t =>
Value' [] op
-> (WellTyped t => TypeCheckInstr op a) -> TypeCheckInstr op a
withWTP Value' [] op
uvalue WellTyped t => TypeCheckInstr op a
fn = case forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
T.getWTP @t of
      Right Dict (WellTyped t)
Dict -> TypeCheckInstr op a
WellTyped t => TypeCheckInstr op a
fn
      Left NotWellTyped
err -> Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
forall op a.
Value' [] op
-> T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a
tcFailedOnValue Value' [] op
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, FromDoc b) => a -> b
pretty NotWellTyped
err) Maybe TcTypeError
forall a. Maybe a
Nothing

    typeCheckValsImpl
      :: ([U.Value' [] op], Sing t)
      -> TypeCheckInstr op [T.Value t]
    typeCheckValsImpl :: forall (t :: T).
([Value' [] op], Sing t) -> TypeCheckInstr op [Value t]
typeCheckValsImpl ([Value' [] op]
mvs, Sing t
sng) =
      ([Value t] -> [Value t])
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     [Value t]
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     [Value t]
forall a b.
(a -> b)
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     a
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Value t] -> [Value t]
forall a. [a] -> [a]
reverse (MultiReaderT
   '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
   (ExceptT (TcError' op) Identity)
   [Value t]
 -> MultiReaderT
      '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
      (ExceptT (TcError' op) Identity)
      [Value t])
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     [Value t]
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     [Value t]
forall a b. (a -> b) -> a -> b
$ ([Value t]
 -> Value' [] op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      [Value t])
-> [Value t]
-> [Value' [] op]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     [Value t]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\[Value t]
res Value' [] op
mv -> (Value t -> [Value t] -> [Value t]
forall a. a -> [a] -> [a]
: [Value t]
res) (Value t -> [Value t])
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value t)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     [Value t]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Value' [] op, Sing t) -> TypeCheckInstr op (Value t)
forall (tz :: T).
(Value' [] op, Sing tz) -> TypeCheckInstr op (Value tz)
doTypeCheckVal (Value' [] op
mv, Sing t
sng))) [] [Value' [] op]
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 [] op]
      -> U.Value' [] op
      -> Sing kt
      -> Sing vt
      -> TypeCheckInstr op [(T.Value kt, T.Value vt)]
    typeCheckMapVal :: forall (kt :: T) (vt :: T).
[Elt [] op]
-> Value' [] op
-> Sing kt
-> Sing vt
-> TypeCheckInstr op [(Value kt, Value vt)]
typeCheckMapVal [Elt [] op]
mels Value' [] op
sq Sing kt
kt Sing vt
vt = Sing kt
-> Value' [] op
-> Sing kt
-> (Comparable kt =>
    MultiReaderT
      '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
      (ExceptT (TcError' op) Identity)
      [(Value' Instr kt, Value' Instr vt)])
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) Identity)
     [(Value' Instr kt, Value' Instr vt)]
forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (Comparable a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withComparable Sing kt
kt Value' [] op
sq Sing kt
kt ((Comparable kt =>
  MultiReaderT
    '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
    (ExceptT (TcError' op) Identity)
    [(Value' Instr kt, Value' Instr vt)])
 -> MultiReaderT
      '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
      (ExceptT (TcError' op) Identity)
      [(Value' Instr kt, Value' Instr vt)])
-> (Comparable kt =>
    MultiReaderT
      '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
      (ExceptT (TcError' op) Identity)
      [(Value' Instr kt, Value' Instr vt)])
-> MultiReaderT
     '[TypeCheckInstrEnv, TypeCheckEnv op, TypeCheckOptions]
     (ExceptT (TcError' op) 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 op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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' [] op], Sing kt) -> TypeCheckInstr op [Value' Instr kt]
forall (t :: T).
([Value' [] op], Sing t) -> TypeCheckInstr op [Value t]
typeCheckValsImpl ((Elt [] op -> Value' [] op) -> [Elt [] op] -> [Value' [] op]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (\(U.Elt Value' [] op
k Value' [] op
_) -> Value' [] op
k) [Elt [] op]
mels, Sing kt
kt)
      [Value' Instr vt]
vals <- ([Value' [] op], Sing vt) -> TypeCheckInstr op [Value' Instr vt]
forall (t :: T).
([Value' [] op], Sing t) -> TypeCheckInstr op [Value t]
typeCheckValsImpl ((Elt [] op -> Value' [] op) -> [Elt [] op] -> [Value' [] op]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (\(U.Elt Value' [] op
_ Value' [] op
v) -> Value' [] op
v) [Elt [] op]
mels, Sing vt
vt)
      [Value' Instr kt]
ksS <- Either (TcError' op) [Value' Instr kt]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     [Value' Instr kt]
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either (TcError' op) [Value' Instr kt]
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      [Value' Instr kt])
-> Either (TcError' op) [Value' Instr kt]
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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' op) -> Either (TcError' op) [Value' Instr kt]
forall (p :: * -> * -> *) a c b.
Bifunctor p =>
p a c -> (a -> b) -> p b c
`onFirst` \Text
msg -> Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
forall op.
Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
TcFailedOnValue Value' [] op
sq (Sing kt -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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' [] op -> EpAddress -> Sing cp -> TypeCheckInstr op (T.Value tz)
    typecheckContractValue :: forall (cp :: T) (tz :: T).
(tz ~ 'TContract cp) =>
Value' [] op
-> EpAddress -> Sing cp -> TypeCheckInstr op (Value tz)
typecheckContractValue Value' [] op
cv (EpAddress KindedAddress kind
addr EpName
epName) Sing cp
pc = do

      ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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 unsupportedType :: TcTypeError -> TcError' op
unsupportedType =
            Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
forall op.
Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
TcFailedOnValue Value' [] op
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' op)
-> (TcTypeError -> Maybe TcTypeError) -> TcTypeError -> TcError' op
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcTypeError -> Maybe TcTypeError
forall a. a -> Maybe a
Just
          checkParameterScope :: TypeCheckInstr op (Dict (T.ParameterScope cp))
          checkParameterScope :: TypeCheckInstr op (Dict (ParameterScope cp))
checkParameterScope = Either (TcError' op) (Dict (ParameterScope cp))
-> TypeCheckInstr op (Dict (ParameterScope cp))
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither
            (Either (TcError' op) (Dict (ParameterScope cp))
 -> TypeCheckInstr op (Dict (ParameterScope cp)))
-> Either (TcError' op) (Dict (ParameterScope cp))
-> TypeCheckInstr op (Dict (ParameterScope cp))
forall a b. (a -> b) -> a -> b
$ (BadTypeForScope -> TcError' op)
-> Either BadTypeForScope (Dict (ParameterScope cp))
-> Either (TcError' op) (Dict (ParameterScope cp))
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (TcTypeError -> TcError' op
unsupportedType (TcTypeError -> TcError' op)
-> (BadTypeForScope -> TcTypeError)
-> BadTypeForScope
-> TcError' op
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> BadTypeForScope -> TcTypeError
UnsupportedTypeForScope (Sing cp -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing Sing cp
pc))
            (Either BadTypeForScope (Dict (ParameterScope cp))
 -> Either (TcError' op) (Dict (ParameterScope cp)))
-> Either BadTypeForScope (Dict (ParameterScope cp))
-> Either (TcError' op) (Dict (ParameterScope cp))
forall a b. (a -> b) -> a -> b
$ Sing cp
-> (SingI cp => Either BadTypeForScope (Dict (ParameterScope cp)))
-> Either BadTypeForScope (Dict (ParameterScope cp))
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing cp
pc ((SingI cp => Either BadTypeForScope (Dict (ParameterScope cp)))
 -> Either BadTypeForScope (Dict (ParameterScope cp)))
-> (SingI cp => Either BadTypeForScope (Dict (ParameterScope cp)))
-> Either BadTypeForScope (Dict (ParameterScope cp))
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
T.checkScope @(T.ParameterScope cp)
      case KindedAddress kind
addr of
        ImplicitAddress Hash 'HashKindPublicKey
_ -> case Sing cp
pc of
          Sing cp
SingT cp
STUnit -> Value ('TContract cp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TContract cp)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TContract cp)))
-> Value ('TContract cp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a b. (a -> b) -> a -> b
$ Address
-> SomeEntrypointCallT 'TUnit -> Value' Instr ('TContract 'TUnit)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, ForbidOp 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
          STTicket Sing n
_ -> do
            Dict (ParameterScope ('TTicket n))
Dict <- ReaderT
  TypeCheckInstrEnv
  (ReaderT
     (TypeCheckEnv op)
     (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
  (Dict (ParameterScope ('TTicket n)))
TypeCheckInstr op (Dict (ParameterScope cp))
checkParameterScope
            Value ('TContract cp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TContract cp)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TContract cp)))
-> Value ('TContract cp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a b. (a -> b) -> a -> b
$ Address
-> SomeEntrypointCallT ('TTicket n)
-> Value' Instr ('TContract ('TTicket n))
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, ForbidOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract (KindedAddress kind -> Address
forall (kind :: AddressKind). KindedAddress kind -> Address
MkAddress KindedAddress kind
addr) SomeEntrypointCallT ('TTicket n)
forall (t :: T).
(ParameterScope t, ForbidOr t) =>
SomeEntrypointCallT t
T.sepcPrimitive
          Sing cp
_ -> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a.
TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TContract cp)))
-> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a b. (a -> b) -> a -> b
$ TcTypeError -> TcError' op
unsupportedType (TcTypeError -> TcError' op) -> TcTypeError -> TcError' op
forall a b. (a -> b) -> a -> b
$ NonEmpty (NonEmpty Text) -> TcTypeError
UnexpectedType (OneItem (NonEmpty Text) -> NonEmpty Text
forall x. One x => OneItem x -> x
one Text
OneItem (NonEmpty Text)
"unit" NonEmpty Text -> [NonEmpty Text] -> NonEmpty (NonEmpty Text)
forall a. a -> [a] -> NonEmpty a
:| [OneItem (NonEmpty Text) -> NonEmpty Text
forall x. One x => OneItem x -> x
one Text
OneItem (NonEmpty Text)
"ticket 'a"])
        ContractAddress ContractHash
ca -> case Maybe TcOriginatedContracts
mOriginatedContracts of
          Maybe TcOriginatedContracts
Nothing -> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a.
TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TContract cp)))
-> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a b. (a -> b) -> a -> b
$ Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
forall op.
Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
TcFailedOnValue Value' [] op
cv (Sing ('TContract cp) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing (Sing ('TContract cp) -> Demote T)
-> Sing ('TContract cp) -> Demote T
forall a b. (a -> b) -> a -> b
$ Sing cp -> SingT ('TContract cp)
forall (n :: T). Sing n -> SingT ('TContract n)
STContract Sing cp
pc)
            Text
"'contract' type can not be used in this context" ErrorSrcPos
instrPos (Maybe TcTypeError -> TcError' op)
-> Maybe TcTypeError -> TcError' op
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 ('TContract cp) -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing (Sing ('TContract cp) -> Demote T)
-> Sing ('TContract cp) -> Demote T
forall a b. (a -> b) -> a -> b
$ Sing cp -> SingT ('TContract cp)
forall (n :: T). Sing n -> SingT ('TContract n)
STContract Sing cp
pc) 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' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a.
TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TContract cp)))
-> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a b. (a -> b) -> a -> b
$
                  Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
forall op.
Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
TcFailedOnValue Value' [] op
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' op)
-> (TcTypeError -> Maybe TcTypeError) -> TcTypeError -> TcError' op
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcTypeError -> Maybe TcTypeError
forall a. a -> Maybe a
Just (TcTypeError -> TcError' op) -> TcTypeError -> TcError' op
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 <- Either (TcError' op) (cp :~: arg)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (cp :~: arg)
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either (TcError' op) (cp :~: arg)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (cp :~: arg))
-> Either (TcError' op) (cp :~: arg)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (cp :~: arg)
forall a b. (a -> b) -> a -> b
$ (TcTypeError -> TcError' op)
-> Either TcTypeError (cp :~: arg)
-> Either (TcError' op) (cp :~: arg)
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TcTypeError -> TcError' op
unsupportedType (Either TcTypeError (cp :~: arg)
 -> Either (TcError' op) (cp :~: arg))
-> Either TcTypeError (cp :~: arg)
-> Either (TcError' op) (cp :~: arg)
forall a b. (a -> b) -> a -> b
$ Sing cp
-> (SingI cp => Either TcTypeError (cp :~: arg))
-> Either TcTypeError (cp :~: arg)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing cp
pc ((SingI cp => Either TcTypeError (cp :~: arg))
 -> Either TcTypeError (cp :~: arg))
-> (SingI cp => Either TcTypeError (cp :~: arg))
-> Either TcTypeError (cp :~: arg)
forall a b. (a -> b) -> a -> b
$ forall (a :: T) (b :: T).
Each '[SingI] '[a, b] =>
Either TcTypeError (a :~: b)
eqType @cp @t'
                  Value ('TContract cp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TContract cp)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TContract cp)))
-> Value ('TContract cp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a b. (a -> b) -> a -> b
$ Address -> SomeEntrypointCallT arg -> Value' Instr ('TContract arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, ForbidOp 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' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a.
TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TcError' op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TContract cp)))
-> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a b. (a -> b) -> a -> b
$ Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
forall op.
Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
TcFailedOnValue Value' [] op
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)
        SmartRollupAddress SmartRollupHash
_ -> do
          -- TODO [#932]: Check that argument type matches
          Dict (ParameterScope cp)
Dict <- ReaderT
  TypeCheckInstrEnv
  (ReaderT
     (TypeCheckEnv op)
     (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
  (Dict (ParameterScope cp))
TypeCheckInstr op (Dict (ParameterScope cp))
checkParameterScope
          Value ('TContract cp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a.
a
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value ('TContract cp)
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      (Value ('TContract cp)))
-> Value ('TContract cp)
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     (Value ('TContract cp))
forall a b. (a -> b) -> a -> b
$ Address -> SomeEntrypointCallT cp -> Value ('TContract cp)
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, ForbidOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract (KindedAddress kind -> Address
forall (kind :: AddressKind). KindedAddress kind -> Address
MkAddress KindedAddress kind
addr) (SomeEntrypointCallT cp -> Value ('TContract cp))
-> SomeEntrypointCallT cp -> Value ('TContract cp)
forall a b. (a -> b) -> a -> b
$ EntrypointCallT cp cp -> SomeEntrypointCallT cp
forall (arg :: T) (param :: T).
ParameterScope param =>
EntrypointCallT param arg -> SomeEntrypointCallT arg
T.SomeEpc EntrypointCallT cp cp
forall (param :: T).
ParameterScope param =>
EntrypointCallT param param
T.unsafeEpcCallRoot

withComparable
  :: forall a (t :: T.T) ty op. Sing a
  -> U.Value' [] op
  -> Sing t
  -> (T.Comparable a => TypeCheckInstr op ty)
  -> TypeCheckInstr op ty
withComparable :: forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (Comparable a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withComparable Sing a
s Value' [] op
uv Sing t
t Comparable a => TypeCheckInstr op ty
act = case Sing a -> Maybe (Dict (Comparable a))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
T.comparabilityPresence Sing a
s of
  Just Dict (Comparable a)
Dict -> TypeCheckInstr op ty
Comparable a => TypeCheckInstr op ty
act
  Maybe (Dict (Comparable a))
Nothing -> do
    ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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' op) ty
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ty
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either (TcError' op) ty
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      ty)
-> (TcError' op -> Either (TcError' op) ty)
-> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcError' op -> Either (TcError' op) ty
forall a b. a -> Either a b
Left (TcError' op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      ty)
-> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ty
forall a b. (a -> b) -> a -> b
$
      Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
forall op.
Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
TcFailedOnValue Value' [] op
uv (Sing t -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
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 op. Sing a
  -> U.Value' [] op
  -> Sing t
  -> (T.ForbidBigMap a => TypeCheckInstr op ty)
  -> TypeCheckInstr op ty
withBigMapAbsence :: forall (a :: T) (t :: T) ty op.
Sing a
-> Value' [] op
-> Sing t
-> (ForbidBigMap a => TypeCheckInstr op ty)
-> TypeCheckInstr op ty
withBigMapAbsence Sing a
s Value' [] op
uv Sing t
t ForbidBigMap a => TypeCheckInstr op ty
act = case Sing 'PSBigMap
-> Sing a -> Maybe (ContainsT 'PSBigMap a :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
T.tAbsence Sing 'PSBigMap
SingTPredicateSym 'PSBigMap
T.SPSBigMap Sing a
s of
  Just ContainsT 'PSBigMap a :~: 'False
Refl -> TypeCheckInstr op ty
ForbidBigMap a => TypeCheckInstr op ty
act
  Maybe (ContainsT 'PSBigMap a :~: 'False)
Nothing -> do
    ErrorSrcPos
instrPos <- Getting ErrorSrcPos TypeCheckInstrEnv ErrorSrcPos
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) 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' op) ty
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ty
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either (TcError' op) ty
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      ty)
-> (TcError' op -> Either (TcError' op) ty)
-> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcError' op -> Either (TcError' op) ty
forall a b. a -> Either a b
Left (TcError' op
 -> ReaderT
      TypeCheckInstrEnv
      (ReaderT
         (TypeCheckEnv op)
         (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
      ty)
-> TcError' op
-> ReaderT
     TypeCheckInstrEnv
     (ReaderT
        (TypeCheckEnv op)
        (ReaderT TypeCheckOptions (ExceptT (TcError' op) Identity)))
     ty
forall a b. (a -> b) -> a -> b
$
      Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
forall op.
Value' [] op
-> T -> Text -> ErrorSrcPos -> Maybe TcTypeError -> TcError' op
TcFailedOnValue Value' [] op
uv (Sing t -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing Sing t
t) Text
"Require a type which doesn't contain `big_map` here"
        ErrorSrcPos
instrPos Maybe TcTypeError
forall a. Maybe a
Nothing