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

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

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

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

tcFailedOnValue :: U.Value -> T.T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue :: Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue v :: Value
v t :: T
t msg :: Text
msg err :: 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 mOriginatedContracts :: Maybe TcOriginatedContracts
mOriginatedContracts tcDo :: 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 uvalue :: Value
uvalue = case (Value
uvalue, SingI tz => Sing tz
forall k (a :: k). SingI a => Sing a
sing @tz) of
      (U.ValueInt i :: Integer
i, STInt) -> Value' Instr 'TInt -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TInt -> TypeCheckInstr (Value tz))
-> Value' Instr 'TInt -> TypeCheckInstr (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
v@(U.ValueInt i :: Integer
i), t :: SingT tz
t@SingT tz
STNat)
        | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 -> Value' Instr 'TNat -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TNat -> TypeCheckInstr (Value tz))
-> Value' Instr 'TNat -> TypeCheckInstr (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. Num a => Integer -> a
fromInteger Integer
i)
        | Bool
otherwise -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TNat -> T
forall (a :: T). Sing a -> T
fromSingT Sing 'TNat
SingT tz
t) "" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
NegativeNat)
      (v :: Value
v@(U.ValueInt i :: 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 mtz :: Mutez
mtz -> Value' Instr 'TMutez -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TMutez -> TypeCheckInstr (Value tz))
-> Value' Instr 'TMutez -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Mutez -> Value' Instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
mtz
        Nothing -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TMutez -> T
forall (a :: T). Sing a -> T
fromSingT Sing 'TMutez
SingT tz
t) "" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
InvalidTimestamp)
      (U.ValueString s :: MText
s, STString) -> Value' Instr 'TString -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TString -> TypeCheckInstr (Value tz))
-> Value' Instr 'TString -> TypeCheckInstr (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
v@(U.ValueString s :: MText
s), t :: SingT tz
t@SingT tz
STAddress) -> case Text -> Either ParseEpAddressError EpAddress
T.parseEpAddress (MText -> Text
unMText MText
s) of
        Right addr :: EpAddress
addr -> Value' Instr 'TAddress -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TAddress -> TypeCheckInstr (Value tz))
-> Value' Instr 'TAddress -> TypeCheckInstr (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 err :: ParseEpAddressError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TAddress -> T
forall (a :: T). Sing a -> T
fromSingT Sing 'TAddress
SingT tz
t) "" (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 b :: InternalByteString
b), t :: SingT tz
t@SingT tz
STAddress) -> case ByteString -> Either ParseEpAddressError EpAddress
T.parseEpAddressRaw (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
        Right addr :: EpAddress
addr -> Value' Instr 'TAddress -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TAddress -> TypeCheckInstr (Value tz))
-> Value' Instr 'TAddress -> TypeCheckInstr (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 err :: ParseEpAddressError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TAddress -> T
forall (a :: T). Sing a -> T
fromSingT Sing 'TAddress
SingT tz
t) "" (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 s :: MText
s), t :: SingT tz
t@SingT tz
STKeyHash) -> case Text -> Either CryptoParseError KeyHash
parseKeyHash (MText -> Text
unMText MText
s)  of
        Right kHash :: KeyHash
kHash -> Value' Instr 'TKeyHash -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKeyHash -> TypeCheckInstr (Value tz))
-> Value' Instr 'TKeyHash -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ KeyHash -> Value' Instr 'TKeyHash
forall (instr :: [T] -> [T] -> *).
KeyHash -> Value' instr 'TKeyHash
VKeyHash KeyHash
kHash
        Left err :: CryptoParseError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TKeyHash -> T
forall (a :: T). Sing a -> T
fromSingT Sing 'TKeyHash
SingT tz
t) "" (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 b :: InternalByteString
b), t :: SingT tz
t@SingT tz
STKeyHash) ->
        case ByteString -> Either CryptoParseError KeyHash
parseKeyHashRaw (InternalByteString -> ByteString
U.unInternalByteString InternalByteString
b) of
          Right kHash :: KeyHash
kHash -> Value' Instr 'TKeyHash -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKeyHash -> TypeCheckInstr (Value tz))
-> Value' Instr 'TKeyHash -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ KeyHash -> Value' Instr 'TKeyHash
forall (instr :: [T] -> [T] -> *).
KeyHash -> Value' instr 'TKeyHash
VKeyHash KeyHash
kHash
          Left err :: CryptoParseError
err -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TKeyHash -> T
forall (a :: T). Sing a -> T
fromSingT Sing 'TKeyHash
SingT tz
t) "" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ CryptoParseError -> TCTypeError
InvalidKeyHash CryptoParseError
err)
      (v :: Value
v@(U.ValueString s :: 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 tstamp :: Timestamp
tstamp -> Value' Instr 'TTimestamp -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTimestamp -> TypeCheckInstr (Value tz))
-> Value' Instr 'TTimestamp -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Timestamp -> Value' Instr 'TTimestamp
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp Timestamp
tstamp
        Nothing -> Value
-> T -> Text -> Maybe TCTypeError -> TypeCheckInstr (Value tz)
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
v (Sing 'TTimestamp -> T
forall (a :: T). Sing a -> T
fromSingT Sing 'TTimestamp
SingT tz
t) "" (TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just TCTypeError
InvalidTimestamp)
      (U.ValueInt i :: Integer
i, STTimestamp) -> Value' Instr 'TTimestamp -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TTimestamp -> TypeCheckInstr (Value tz))
-> Value' Instr 'TTimestamp -> TypeCheckInstr (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 s :: ByteString
s), STBytes) -> Value' Instr 'TBytes -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBytes -> TypeCheckInstr (Value tz))
-> Value' Instr 'TBytes -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes ByteString
s
      (U.ValueTrue, STBool) -> Value' Instr 'TBool -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBool -> TypeCheckInstr (Value tz))
-> Value' Instr 'TBool -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Bool -> Value' Instr 'TBool
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool Bool
True
      (U.ValueFalse, STBool) -> Value' Instr 'TBool -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TBool -> TypeCheckInstr (Value tz))
-> Value' Instr 'TBool -> TypeCheckInstr (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 s :: PublicKey
s), STKey) ->
        Value' Instr 'TKey -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKey -> TypeCheckInstr (Value tz))
-> Value' Instr 'TKey -> TypeCheckInstr (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 s :: PublicKey
s), STKey) ->
        Value' Instr 'TKey -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TKey -> TypeCheckInstr (Value tz))
-> Value' Instr 'TKey -> TypeCheckInstr (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 s :: Signature
s), STSignature) ->
        Value' Instr 'TSignature -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TSignature -> TypeCheckInstr (Value tz))
-> Value' Instr 'TSignature -> TypeCheckInstr (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 s :: Signature
s), STSignature) ->
        Value' Instr 'TSignature -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TSignature -> TypeCheckInstr (Value tz))
-> Value' Instr 'TSignature -> TypeCheckInstr (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 ci :: ChainId
ci), STChainId) ->
        Value' Instr 'TChainId -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChainId -> TypeCheckInstr (Value tz))
-> Value' Instr 'TChainId -> TypeCheckInstr (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 -> 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 ci :: ChainId
ci), STChainId) ->
        Value' Instr 'TChainId -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr 'TChainId -> TypeCheckInstr (Value tz))
-> Value' Instr 'TChainId -> TypeCheckInstr (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
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 addr :: EpAddress
addr))
        , STContract pc :: Sing a
pc) -> Value -> EpAddress -> Sing a -> TypeCheckInstr (Value tz)
forall (cp :: T) (tz :: T).
(Typeable cp, SingI cp, tz ~ 'TContract cp) =>
Value -> EpAddress -> Sing cp -> TypeCheckInstr (Value tz)
typecheckContractValue Value
cv EpAddress
addr Sing a
pc
      (cv :: Value
cv@(U.ValueBytes (ByteString -> Either ParseEpAddressError EpAddress
T.parseEpAddressRaw (ByteString -> Either ParseEpAddressError EpAddress)
-> (InternalByteString -> ByteString)
-> InternalByteString
-> Either ParseEpAddressError EpAddress
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InternalByteString -> ByteString
U.unInternalByteString -> Right addr :: EpAddress
addr))
        , STContract pc :: Sing a
pc) -> Value -> EpAddress -> Sing a -> TypeCheckInstr (Value tz)
forall (cp :: T) (tz :: T).
(Typeable cp, SingI cp, tz ~ 'TContract cp) =>
Value -> EpAddress -> Sing cp -> TypeCheckInstr (Value tz)
typecheckContractValue Value
cv EpAddress
addr Sing a
pc

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

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

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

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

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

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

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

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

      (v :: Value
v@Value
U.ValueNil, s :: SingT tz
s@(STBigMap (st :: Sing st) _)) ->
        Sing a
-> Value
-> Sing ('TBigMap a b)
-> (Comparable a => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall (a :: T) (t :: T) ty.
Sing a
-> Value
-> Sing t
-> (Comparable a => TypeCheckInstr ty)
-> TypeCheckInstr ty
withComparable Sing a
st Value
v Sing ('TBigMap a b)
SingT tz
s ((Comparable a => TypeCheckInstr (Value tz))
 -> TypeCheckInstr (Value tz))
-> (Comparable a => TypeCheckInstr (Value tz))
-> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Value' Instr ('TBigMap a b) -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TBigMap a b) -> TypeCheckInstr (Value tz))
-> Value' Instr ('TBigMap a b) -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Map (Value' Instr a) (Value' Instr b)
-> Value' Instr ('TBigMap a b)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
T.VBigMap Map (Value' Instr a) (Value' Instr b)
forall k a. Map k a
M.empty

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

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

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

    withWTP
      :: forall t a. SingI t
      => U.Value
      -> (T.WellTyped t => TypeCheckInstr a)
      -> TypeCheckInstr a
    withWTP :: Value -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTP uvalue :: Value
uvalue fn :: 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 -> TypeCheckInstr a
WellTyped t => TypeCheckInstr a
fn
      Left (NotWellTyped t :: T
t) -> Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
forall a.
Value -> T -> Text -> Maybe TCTypeError -> TypeCheckInstr a
tcFailedOnValue Value
uvalue (Sing ty -> T
forall (a :: T). Sing a -> T
fromSingT (Sing ty -> T) -> Sing ty -> T
forall a b. (a -> b) -> a -> b
$ SingI ty => Sing ty
forall k (a :: k). SingI a => Sing a
sing @ty)
                  ("Value is not well typed: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> T -> Text
forall b a. (Show a, IsString b) => a -> b
show T
t) Maybe TCTypeError
forall a. Maybe a
Nothing

    typeCheckValsImpl
      :: forall t . (SingI t)
      => [U.Value]
      -> TypeCheckInstr [T.Value t]
    typeCheckValsImpl :: [Value] -> TypeCheckInstr [Value t]
typeCheckValsImpl mvs :: [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 (\res :: [Value t]
res mv :: Value
mv -> (Value t -> [Value t] -> [Value t]
forall a. a -> [a] -> [a]
: [Value t]
res) (Value t -> [Value t])
-> ReaderT InstrCallStack TypeCheck (Value t)
-> TypeCheckInstr [Value t]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> ReaderT InstrCallStack TypeCheck (Value t)
forall (tz :: T). SingI tz => Value -> TypeCheckInstr (Value tz)
doTypeCheckVal @t Value
mv) [] [Value]
mvs

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

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

      InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
      let ensureTypeMatches :: forall t'. KnownT t' => TypeCheckInstr (cp :~: t')
          ensureTypeMatches :: TypeCheckInstr (cp :~: t')
ensureTypeMatches = forall a.
MonadError TCError TypeCheckInstr =>
Either TCError a -> TypeCheckInstr a
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither @_ @TypeCheckInstr (Either TCError (cp :~: t') -> TypeCheckInstr (cp :~: t'))
-> Either TCError (cp :~: t') -> TypeCheckInstr (cp :~: t')
forall a b. (a -> b) -> a -> b
$
            (TCTypeError -> TCError)
-> Either TCTypeError (cp :~: t') -> Either TCError (cp :~: t')
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Value
-> T -> Text -> InstrCallStack -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
cv ((SingKind T, SingI ty) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @ty) "wrong contract parameter" InstrCallStack
instrPos (Maybe TCTypeError -> TCError)
-> (TCTypeError -> Maybe TCTypeError) -> TCTypeError -> TCError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just) (Either TCTypeError (cp :~: t') -> Either TCError (cp :~: t'))
-> Either TCTypeError (cp :~: t') -> Either TCError (cp :~: t')
forall a b. (a -> b) -> a -> b
$
              Each '[KnownT] '[cp, t'] => Either TCTypeError (cp :~: t')
forall (a :: T) (b :: T).
Each '[KnownT] '[a, b] =>
Either TCTypeError (a :~: b)
eqType @cp @t'
      let unsupportedType :: T.BadTypeForScope -> TCError
          unsupportedType :: BadTypeForScope -> TCError
unsupportedType reason :: BadTypeForScope
reason = Value
-> T -> Text -> InstrCallStack -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
cv (Sing cp -> T
forall (a :: T). Sing a -> T
fromSingT Sing cp
pc)
            "Unsupported type in type argument of 'contract' type" InstrCallStack
instrPos (Maybe TCTypeError -> TCError) -> Maybe TCTypeError -> TCError
forall a b. (a -> b) -> a -> b
$
              TCTypeError -> Maybe TCTypeError
forall a. a -> Maybe a
Just (TCTypeError -> Maybe TCTypeError)
-> TCTypeError -> Maybe TCTypeError
forall a b. (a -> b) -> a -> b
$ T -> BadTypeForScope -> TCTypeError
UnsupportedTypeForScope (Sing cp -> T
forall (a :: T). Sing a -> T
fromSingT Sing cp
pc) BadTypeForScope
reason
      case Address
addr of
        KeyAddress _ -> do
          cp :~: 'TUnit
Refl <- KnownT 'TUnit => TypeCheckInstr (cp :~: 'TUnit)
forall (t' :: T). KnownT t' => TypeCheckInstr (cp :~: t')
ensureTypeMatches @'T.TUnit
          Value' Instr ('TContract 'TUnit) -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TContract 'TUnit) -> TypeCheckInstr (Value tz))
-> Value' Instr ('TContract 'TUnit) -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Address
-> SomeEntrypointCallT 'TUnit -> Value' Instr ('TContract 'TUnit)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract Address
addr SomeEntrypointCallT 'TUnit
forall (t :: T).
(ParameterScope t, ForbidOr t) =>
SomeEntrypointCallT t
T.sepcPrimitive
        ContractAddress ca :: ContractHash
ca -> case Maybe TcOriginatedContracts
mOriginatedContracts of
          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 originatedContracts :: 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 :: 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
                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) "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') epc :: EntrypointCallT t arg
epc) -> do
                  cp :~: arg
Refl <- KnownT arg => TypeCheckInstr (cp :~: arg)
forall (t' :: T). KnownT t' => TypeCheckInstr (cp :~: t')
ensureTypeMatches @t'
                  Value' Instr ('TContract arg) -> TypeCheckInstr (Value tz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value' Instr ('TContract arg) -> TypeCheckInstr (Value tz))
-> Value' Instr ('TContract arg) -> TypeCheckInstr (Value tz)
forall a b. (a -> b) -> a -> b
$ Address -> SomeEntrypointCallT arg -> Value' Instr ('TContract arg)
forall (arg :: T) (instr :: [T] -> [T] -> *).
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract Address
addr (EntrypointCallT t arg -> SomeEntrypointCallT arg
forall (arg :: T) (param :: T).
ParameterScope param =>
EntrypointCallT param arg -> SomeEntrypointCallT arg
T.SomeEpc EntrypointCallT t arg
epc)
            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) "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 s :: Sing a
s uv :: Value
uv t :: Sing t
t act :: 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 -> TypeCheckInstr ty
Comparable a => TypeCheckInstr ty
act
  Nothing -> do
    InstrCallStack
instrPos <- ReaderT InstrCallStack TypeCheck InstrCallStack
forall r (m :: * -> *). MonadReader r m => m r
ask
    Either TCError ty -> TypeCheckInstr ty
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either TCError ty -> TypeCheckInstr ty)
-> (TCError -> Either TCError ty) -> TCError -> TypeCheckInstr ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCError -> Either TCError ty
forall a b. a -> Either a b
Left (TCError -> TypeCheckInstr ty) -> TCError -> TypeCheckInstr ty
forall a b. (a -> b) -> a -> b
$
      Value
-> T -> Text -> InstrCallStack -> Maybe TCTypeError -> TCError
TCFailedOnValue Value
uv (Sing t -> T
forall (a :: T). Sing a -> T
fromSingT Sing t
t) "Require a comparable type here" InstrCallStack
instrPos Maybe TCTypeError
forall a. Maybe a
Nothing