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

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

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

import Michelson.Text
import Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))
import Michelson.TypeCheck.Helpers
import Michelson.TypeCheck.TypeCheck
  (SomeParamType(..), TcInstrHandler, TcOriginatedContracts, TypeCheckInstr, TypeCheckOptions(..),
  throwingTCError)
import Michelson.TypeCheck.Types
import Michelson.Typed
  (EpAddress(..), Notes(..), SingT(..), Value'(..), starNotes)
import qualified Michelson.Typed as T
import qualified Michelson.Untyped as U
import Tezos.Address (Address(..))
import Tezos.Core
import Tezos.Crypto
import qualified Tezos.Crypto.BLS12381 as BLS
import Util.Type (onFirst)

tcFailedOnValue :: U.Value -> T.T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue :: Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v T
t Text
msg Maybe TCTypeError
err = do
  InstrCallStack
loc <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
  TCError -> TypeCheckInstr a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCError -> TypeCheckInstr a) -> TCError -> TypeCheckInstr a
forall a b. (a -> b) -> a -> b
$ Value
-> T -> Text -> InstrCallStack -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
v T
t Text
msg InstrCallStack
loc Maybe TCTypeError
err

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

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

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

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

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

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

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

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

      -- If ValueSeq contains at least 2 elements, it can be type checked as a
      -- right combed pair.
      (U.ValueSeq vals :: NonEmpty $ Value
vals@(Value
_ :| (Value
_ : [Value]
_)), STPair Sing n
l Sing n
r) ->
        Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
l ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
r ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value -> TypeCheckInstr (Value ('TPair n n))
forall (tz :: T). SingI tz => Value -> TypeCheckInstr (Value tz)
doTypeCheckVal (Value -> TypeCheckInstr (Value ('TPair n n)))
-> Value -> TypeCheckInstr (Value ('TPair n n))
forall a b. (a -> b) -> a -> b
$ (NonEmpty $ Value) -> Value
seqToRightCombedPair NonEmpty $ Value
vals

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

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

      (sq :: Value
sq@(U.ValueSeq ((NonEmpty $ Value) -> [Element (NonEmpty $ Value)]
forall t. Container t => t -> [Element t]
toList -> [Element (NonEmpty $ Value)]
mels)), s :: SingT tz
s@(STSet (vt :: Sing st))) ->
        Sing n
-> Value
-> Sing ('TSet n)
-> (Comparable n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing n
vt Value
sq Sing ('TSet n)
SingT tz
s ((Comparable n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
vt ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
        InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask

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

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

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

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

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

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

      (U.ValueSeq NonEmpty $ Value
s, ((STLambda (i :: Sing inp) (o :: Sing out))) :: Sing l) ->
        Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
i ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
o ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ case (NonEmpty $ Value) -> Maybe Value
emptyListAsLambda NonEmpty $ Value
s of
          Just Value
xs -> Value -> TypeCheckInstr (Value tz)
forall (tz :: T). SingI tz => Value -> TypeCheckInstr (Value tz)
doTypeCheckVal @l Value
xs
          Maybe Value
Nothing -> Value
-> T
-> Text
-> Maybe TCTypeError
-> TypeCheckInstr (Value ('TLambda n n))
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
uvalue ((SingKind T, SingI tz) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @l) Text
"" Maybe TCTypeError
forall a. Maybe a
Nothing

      (Value
v, STLambda (var :: Sing it) (b :: Sing ot)) -> Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
var ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Sing n
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
b ((SingI n => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (SingI n => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ do
        [ExpandedOp]
mp <- case Value
v of
          Value
U.ValueNil       -> [ExpandedOp] -> ReaderT InstrCallStack TypeCheck [ExpandedOp]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
          U.ValueLambda NonEmpty ExpandedOp
mp -> [ExpandedOp] -> ReaderT InstrCallStack TypeCheck [ExpandedOp]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ExpandedOp] -> ReaderT InstrCallStack TypeCheck [ExpandedOp])
-> [ExpandedOp] -> ReaderT InstrCallStack TypeCheck [ExpandedOp]
forall a b. (a -> b) -> a -> b
$ NonEmpty ExpandedOp -> [Element (NonEmpty ExpandedOp)]
forall t. Container t => t -> [Element t]
toList NonEmpty ExpandedOp
mp
          Value
_ -> Value
-> T
-> Text
-> Maybe TCTypeError
-> ReaderT InstrCallStack TypeCheck [ExpandedOp]
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v ((SingKind T, SingI ty) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @ty) Text
"unexpected value" Maybe TCTypeError
forall a. Maybe a
Nothing
        HST '[n]
_ :/ SomeInstrOut '[n]
instr <-
          Value
-> (WellTyped n => TypeCheckInstr (SomeInstr '[n]))
-> TypeCheckInstr (SomeInstr '[n])
forall (t :: T) a.
SingI t =>
Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP @it Value
uvalue ((WellTyped n => TypeCheckInstr (SomeInstr '[n]))
 -> TypeCheckInstr (SomeInstr '[n]))
-> (WellTyped n => TypeCheckInstr (SomeInstr '[n]))
-> TypeCheckInstr (SomeInstr '[n])
forall a b. (a -> b) -> a -> b
$ TypeCheckInstrNoExcept (TypeCheckedSeq '[n])
-> TypeCheckInstr (SomeInstr '[n])
forall (inp :: [T]).
TypeCheckInstrNoExcept (TypeCheckedSeq inp)
-> TypeCheckInstr (SomeInstr inp)
throwingTCError (TypeCheckInstrNoExcept (TypeCheckedSeq '[n])
 -> TypeCheckInstr (SomeInstr '[n]))
-> TypeCheckInstrNoExcept (TypeCheckedSeq '[n])
-> TypeCheckInstr (SomeInstr '[n])
forall a b. (a -> b) -> a -> b
$
            TcInstrHandler
-> [ExpandedOp]
-> HST '[n]
-> TypeCheckInstrNoExcept (TypeCheckedSeq '[n])
forall (inp :: [T]).
SingI inp =>
TcInstrHandler
-> [ExpandedOp]
-> HST inp
-> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
typeCheckImpl TcInstrHandler
tcDo [ExpandedOp]
mp ((SingI n => Notes n
forall (t :: T). SingI t => Notes t
starNotes @it, Dict (WellTyped n)
forall (a :: Constraint). a => Dict a
Dict, Annotation VarTag
forall a. Default a => a
def) (Notes n, Dict (WellTyped n), Annotation VarTag)
-> HST '[] -> HST '[n]
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), Annotation VarTag)
-> HST xs -> HST (x : xs)
::& HST '[]
SNil)
        case SomeInstrOut '[n]
instr of
          Instr '[n] out
lam ::: (HST out
lo :: HST lo) -> Value
-> (WellTyped n =>
    ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall (t :: T) a.
SingI t =>
Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP @ot Value
uvalue ((WellTyped n =>
  ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
 -> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> (WellTyped n =>
    ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall a b. (a -> b) -> a -> b
$ do
            case HST out -> Either TCTypeError (out :~: '[n])
forall (t :: T) (st :: [T]).
(SingI st, WellTyped t) =>
HST st -> Either TCTypeError (st :~: '[t])
eqHST1 @ot HST out
lo of
              Right out :~: '[n]
Refl -> do
                Value' Instr ('TLambda n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TLambda n n)
 -> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> Value' Instr ('TLambda n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[n] '[n] -> Value' Instr ('TLambda n n)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
VLam (Instr '[n] out -> RemFail Instr '[n] out
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
instr i o -> RemFail instr i o
T.RfNormal Instr '[n] out
lam)
              Left TCTypeError
m ->
                Value
-> T
-> Text
-> Maybe TCTypeError
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v ((SingKind T, SingI ty) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @ty)
                        Text
"wrong output type of lambda's value:" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
m)
          AnyOutInstr forall (out :: [T]). Instr '[n] out
lam ->
            Value' Instr ('TLambda n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TLambda n n)
 -> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n)))
-> Value' Instr ('TLambda n n)
-> ReaderT InstrCallStack TypeCheck (Value' Instr ('TLambda n n))
forall a b. (a -> b) -> a -> b
$ RemFail Instr '[n] '[n] -> Value' Instr ('TLambda n n)
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
RemFail instr '[inp] '[out] -> Value' instr ('TLambda inp out)
VLam ((forall (out :: [T]). Instr '[n] out) -> RemFail Instr '[n] '[n]
forall k (instr :: k -> k -> *) (i :: k) (o :: k).
(forall (o' :: k). instr i o') -> RemFail instr i o
T.RfAlwaysFails forall (out :: [T]). Instr '[n] out
lam)

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

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

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

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

    withWTP
      :: forall t a. SingI t
      => U.Value
      -> (T.WellTyped t => TypeCheckInstr a)
      -> TypeCheckInstr a
    withWTP :: Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP Value
uvalue WellTyped t => TypeCheckInstr a
fn = case SingI t => Either NotWellTyped (Dict (WellTyped t))
forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
getWTP @t of
      Right Dict (WellTyped t)
Dict -> TypeCheckInstr a
WellTyped t => TypeCheckInstr a
fn
      Left (NotWellTyped T
t BadTypeForScope
cause) -> Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
uvalue ((SingKind T, SingI ty) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @ty)
                  (Text
"Value is not well typed: '" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> T -> Text
forall b a. (Show a, IsString b) => a -> b
show T
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"' because it " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> BadTypeForScope -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty BadTypeForScope
cause) Maybe TCTypeError
forall a. Maybe a
Nothing

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

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

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

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

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

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