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

-- TODO [#549]: remove this pragma
{-# OPTIONS_GHC -Wno-deprecations #-}

-- | This module contains a type family for converting a type to its RPC representation,
-- and TemplateHaskell functions for deriving RPC representations for custom types.
module Morley.Client.RPC.AsRPC
  ( AsRPC
  , deriveRPC
  , deriveRPCWithStrategy
  , deriveManyRPC
  , deriveManyRPCWithStrategy
  -- * Conversions
  , valueAsRPC
  , notesAsRPC
  -- * Entailments
  , rpcSingIEvi
  , rpcHasNoOpEvi
  , rpcHasNoBigMapEvi
  , rpcHasNoNestedBigMapsEvi
  , rpcHasNoContractEvi
  , rpcStorageScopeEvi
  ) where

import Prelude hiding (Type)

import Control.Lens.Plated (universe)
import Data.Constraint (Dict(..), (***), (:-)(Sub), (\\))
import qualified Data.List as List ((\\))
import Data.Singletons (Sing, withSingI)
import qualified GHC.Generics as G
import Language.Haskell.TH
  (Con(InfixC, NormalC, RecC), Cxt, Dec(DataD, NewtypeD, TySynD, TySynInstD),
  DerivStrategy(AnyclassStrategy), Info(TyConI), Kind, Loc(loc_module), Name, Q, TyLit(StrTyLit),
  TySynEqn(..), TyVarBndr, Type(..), cxt, location, mkName, nameBase, reify, reifyInstances,
  standaloneDerivWithStrategyD)
import Language.Haskell.TH.ReifyMany (reifyManyTyCons)
import Language.Haskell.TH.ReifyMany.Internal (decConcreteNames)

import Lorentz hiding (TAddress, TSignature, drop, not)
import qualified Lorentz as L
import Lorentz.Extensible (Extensible)
import Morley.Michelson.Typed
  (ContractPresence(ContractAbsent), HasNoBigMap, HasNoContract, HasNoNestedBigMaps, HasNoOp,
  Notes(..), OpPresence(..), SingI(sing), SingT(..), StorageScope, T(..), Value'(..),
  checkContractTypePresence, checkOpPresence)
import Morley.Util.Named hiding (Name(..))
import Morley.Util.TH (isTypeAlias, lookupTypeNameOrFail)

{-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-}

----------------------------------------------------------------------------
-- AsRPC
----------------------------------------------------------------------------

-- | A type-level function that maps a type to its Tezos RPC representation.
--
-- For example, when we retrieve a contract's storage using the Tezos RPC, all its 'BigMap's will be replaced
-- by 'BigMapId's.
--
-- So if a contract has a storage of type @T@, when we call the Tezos RPC
-- to retrieve it, we must deserialize the micheline expression to the type @AsRPC T@.
--
-- > AsRPC (BigMap Integer MText) ~ BigMapId Integer MText
-- > AsRPC [BigMap Integer MText] ~ [BigMapId Integer MText]
-- > AsRPC (MText, (Address, BigMap Integer MText)) ~ (MText, (Address, BigMapId Integer MText))
--
-- The following law holds IFF a type @t@ has an IsoValue instance:
--
-- > ToT (AsRPC t) ~ AsRPC (ToT t)
--
type family AsRPC (a :: k) :: k

-- Value
type instance AsRPC (Value' instr t) = Value' instr (AsRPC t)
type instance AsRPC 'TKey = 'TKey
type instance AsRPC 'TUnit = 'TUnit
type instance AsRPC 'TSignature = 'TSignature
type instance AsRPC 'TChainId = 'TChainId
type instance AsRPC ('TOption t) = 'TOption (AsRPC t)
type instance AsRPC ('TList t) = 'TList (AsRPC t)
type instance AsRPC ('TSet t) = 'TSet t
type instance AsRPC 'TOperation = 'TOperation
type instance AsRPC ('TContract t) = 'TContract t
type instance AsRPC ('TTicket t) = 'TTicket t
type instance AsRPC ('TPair t1 t2) = 'TPair (AsRPC t1) (AsRPC t2)
type instance AsRPC ('TOr t1 t2) = 'TOr (AsRPC t1) (AsRPC t2)
type instance AsRPC ('TLambda t1 t2) = 'TLambda t1 t2
type instance AsRPC ('TMap k v) = 'TMap k (AsRPC v)
type instance AsRPC ('TBigMap _ _) = 'TNat
type instance AsRPC 'TInt = 'TInt
type instance AsRPC 'TNat = 'TNat
type instance AsRPC 'TString = 'TString
type instance AsRPC 'TBytes = 'TBytes
type instance AsRPC 'TMutez = 'TMutez
type instance AsRPC 'TBool = 'TBool
type instance AsRPC 'TKeyHash = 'TKeyHash
type instance AsRPC 'TTimestamp = 'TTimestamp
type instance AsRPC 'TAddress = 'TAddress
type instance AsRPC 'TNever = 'TNever
type instance AsRPC 'TBls12381Fr = 'TBls12381Fr
type instance AsRPC 'TBls12381G1 = 'TBls12381G1
type instance AsRPC 'TBls12381G2 = 'TBls12381G2
type instance AsRPC 'TChest = 'TChest
type instance AsRPC 'TChestKey = 'TChestKey

-- Morley types

-- Note: We don't recursively apply @AsRPC@ to @k@ or @v@ because
-- bigmaps cannot contain nested bigmaps.
-- If this constraint is ever lifted, we'll have to change this instance
-- to @BigMapId k (AsRPC v)@
type instance AsRPC (BigMap k v) = BigMapId k v
type instance AsRPC Integer = Integer
type instance AsRPC Natural = Natural
type instance AsRPC MText = MText
type instance AsRPC Bool = Bool
type instance AsRPC ByteString = ByteString
type instance AsRPC Mutez = Mutez
type instance AsRPC KeyHash = KeyHash
type instance AsRPC Timestamp = Timestamp
type instance AsRPC Address = Address
type instance AsRPC EpAddress = EpAddress
type instance AsRPC (L.TAddress p vd) = L.TAddress p vd
type instance AsRPC (FutureContract p) = FutureContract p
type instance AsRPC PublicKey = PublicKey
type instance AsRPC Signature = Signature
type instance AsRPC ChainId = ChainId
type instance AsRPC Never = Never
type instance AsRPC Bls12381Fr = Bls12381Fr
type instance AsRPC Bls12381G1 = Bls12381G1
type instance AsRPC Bls12381G2 = Bls12381G2
type instance AsRPC () = ()
type instance AsRPC [a] = [AsRPC a]
type instance AsRPC (Maybe a) = Maybe (AsRPC a)
type instance AsRPC (Either l r) = Either (AsRPC l) (AsRPC r)
type instance AsRPC (a, b) = (AsRPC a, AsRPC b)
type instance AsRPC (Set a) = Set a
type instance AsRPC (Map k v) = Map k (AsRPC v)
type instance AsRPC Operation = Operation
type instance AsRPC (Identity a) = Identity (AsRPC a)
type instance AsRPC (NamedF Identity a name) = NamedF Identity (AsRPC a) name
type instance AsRPC (NamedF Maybe a name) = NamedF Maybe (AsRPC a) name
type instance AsRPC (a, b, c) = (AsRPC a, AsRPC b, AsRPC c)
type instance AsRPC (a, b, c, d) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d)
type instance AsRPC (a, b, c, d, e) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e)
type instance AsRPC (a, b, c, d, e, f) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e, AsRPC f)
type instance AsRPC (a, b, c, d, e, f, g) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e, AsRPC f, AsRPC g)
type instance AsRPC (ContractRef arg) = ContractRef arg
type instance AsRPC Chest = Chest
type instance AsRPC ChestKey = ChestKey

-- Lorentz types
type instance AsRPC (Packed a) = Packed a
type instance AsRPC (L.TSignature a) = L.TSignature a
type instance AsRPC (Hash alg a) = Hash alg a
type instance AsRPC (L.TAddress cp) = L.TAddress cp
type instance AsRPC Empty = Empty
type instance AsRPC (Extensible x) = Extensible x
type instance AsRPC (View_ a r) = View_ a r
type instance AsRPC (Void_ a r) = Void_ a r
type instance AsRPC (UParam entries) = UParam entries
type instance AsRPC (inp :-> out) = inp :-> out
type instance AsRPC (ShouldHaveEntrypoints a) = ShouldHaveEntrypoints a
type instance AsRPC (ParameterWrapper deriv cp) = ParameterWrapper deriv (AsRPC cp)
type instance AsRPC L.OpenChest = L.OpenChest
type instance AsRPC (L.ChestT a) = L.ChestT a
type instance AsRPC (L.OpenChestT a) = L.OpenChestT a

----------------------------------------------------------------------------
-- Derive RPC repr
----------------------------------------------------------------------------

-- | Derive an RPC representation for a type, as well as instances for 'Generic', 'IsoValue' and 'AsRPC'.
--
-- > data ExampleStorage a b = ExampleStorage
-- >   { esField1 :: Integer
-- >   , esField2 :: [BigMap Integer MText]
-- >   , esField3 :: a
-- >   }
-- >   deriving stock Generic
-- >   deriving anyclass IsoValue
-- >
-- > deriveRPC "ExampleStorage"
--
-- Will generate:
--
-- > data ExampleStorageRPC a b = ExampleStorageRPC
-- >   { esField1RPC :: AsRPC Integer
-- >   , esField2RPC :: AsRPC [BigMap Integer MText]
-- >   , esField3RPC :: AsRPC a
-- >   }
-- >
-- > type instance AsRPC (ExampleStorage a b) = ExampleStorageRPC a b
-- > deriving anyclass instance (IsoValue (AsRPC a), IsoValue (AsRPC b)) => IsoValue (ExampleStorageRPC a b)
-- > instance Generic (ExampleStorageRPC a b) where
-- >   ...
deriveRPC :: String -> Q [Dec]
deriveRPC :: String -> Q [Dec]
deriveRPC String
typeStr = String -> GenericStrategy -> Q [Dec]
deriveRPCWithStrategy String
typeStr GenericStrategy
haskellBalanced

-- | Recursively enumerate @data@, @newtype@ and @type@ declarations,
-- and derives an RPC representation for each type that doesn't yet have one.
--
-- You can also pass in a list of types for which you _don't_ want
-- an RPC representation to be derived.
--
-- In this example, 'deriveManyRPC' will generate an RPC
-- representation for @A@ and @B@,
-- but not for @C@ (because we explicitly said we don't want one)
-- or @D@ (because it already has one).
--
-- > data B = B
-- > data C = C
-- > data D = D
-- > deriveRPC "D"
-- >
-- > data A = A B C D
-- > deriveManyRPC "A" ["C"]
deriveManyRPC :: String -> [String] -> Q [Dec]
deriveManyRPC :: String -> [String] -> Q [Dec]
deriveManyRPC String
typeStr [String]
skipTypes =
  String -> [String] -> GenericStrategy -> Q [Dec]
deriveManyRPCWithStrategy String
typeStr [String]
skipTypes GenericStrategy
haskellBalanced

-- | Same as 'deriveManyRPC', but uses a custom strategy for deriving a 'Generic' instance.
deriveManyRPCWithStrategy :: String -> [String] -> GenericStrategy -> Q [Dec]
deriveManyRPCWithStrategy :: String -> [String] -> GenericStrategy -> Q [Dec]
deriveManyRPCWithStrategy String
typeStr [String]
skipTypes GenericStrategy
gs = do
  [Name]
skipTypeNames <- (String -> Q Name) -> [String] -> Q [Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse String -> Q Name
lookupTypeNameOrFail [String]
skipTypes
  Name
typeName <- String -> Q Name
lookupTypeNameOrFail String
typeStr
  Q Bool -> Q () -> Q ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Name -> Q Bool
isTypeAlias Name
typeName) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ String -> Q ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ String
typeStr String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" is a 'type' alias but not 'data' or 'newtype'."
  [Name]
allTypeNames <- Name -> Q [Name]
findWithoutInstance Name
typeName
  [[Dec]] -> [Dec]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name] -> (Name -> Q [Dec]) -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Name]
allTypeNames [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Name]
skipTypeNames) \Name
name -> Name -> GenericStrategy -> Q [Dec]
deriveRPCWithStrategy' Name
name GenericStrategy
gs
  where

    -- | Recursively enumerate @data@, @newtype@ and @type@ declarations,
    -- and returns the names of only @data@ and @newtype@ of those that
    -- don't yet have an 'AsRPC' instance. Type aliases don't need instances
    -- and respectively there is no need to derive 'AsRPC' for them.
    findWithoutInstance :: Name -> Q [Name]
    findWithoutInstance :: Name -> Q [Name]
findWithoutInstance Name
typeName =
      ((Name, Info) -> Name) -> [(Name, Info)] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Info) -> Name
forall a b. (a, b) -> a
fst ([(Name, Info)] -> [Name]) -> Q [(Name, Info)] -> Q [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        ((Name, Dec) -> Q (Bool, [Name])) -> [Name] -> Q [(Name, Info)]
reifyManyTyCons
          (\(Name
name, Dec
dec) ->
            Q Bool -> Q (Bool, [Name]) -> Q (Bool, [Name]) -> Q (Bool, [Name])
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Name -> Q Bool
isTypeAlias Name
name)
              ((Bool, [Name]) -> Q (Bool, [Name])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, Dec -> [Name]
decConcreteNames Dec
dec))
              (Q Bool -> Q (Bool, [Name]) -> Q (Bool, [Name]) -> Q (Bool, [Name])
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Name -> Q Bool
hasRPCInstance Name
name)
                ((Bool, [Name]) -> Q (Bool, [Name])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, []))
                ((Bool, [Name]) -> Q (Bool, [Name])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
True, Dec -> [Name]
decConcreteNames Dec
dec)))
          )
          [Name
typeName]

    hasRPCInstance :: Name -> Q Bool
    hasRPCInstance :: Name -> Q Bool
hasRPCInstance Name
typeName = do
      Name -> Q (Maybe Type)
deriveFullTypeFromName Name
typeName Q (Maybe Type) -> (Maybe Type -> Q Bool) -> Q Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe Type
Nothing ->
          String -> Q Bool
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q Bool) -> String -> Q Bool
forall a b. (a -> b) -> a -> b
$ String
"Found a field with a type that is neither a 'data' nor a 'newtype' nor a 'type': "
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall b a. (Show a, IsString b) => a -> b
show Name
typeName
        Just Type
typ ->
          Bool -> Bool
not (Bool -> Bool) -> ([Dec] -> Bool) -> [Dec] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Dec] -> Bool
forall t. Container t => t -> Bool
null ([Dec] -> Bool) -> Q [Dec] -> Q Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [Type] -> Q [Dec]
reifyInstances ''AsRPC [Type
typ]

    -- | Given a type name, return the corresponding type expression
    -- (applied to any type variables, if necessary).
    --
    -- For example, assuming a data type like @data F a b = ...@ exists in the type environment,
    -- then @deriveFullTypeFromName ''F@ will return the type expression @[t|F a b|]@.
    --
    -- Note that only @data@, @newtype@ and @type@ declarations are supported at the moment.
    deriveFullTypeFromName :: Name -> Q (Maybe Type)
    deriveFullTypeFromName :: Name -> Q (Maybe Type)
deriveFullTypeFromName Name
typeName = do
      Info
typeInfo <- Name -> Q Info
reify Name
typeName
      case Info
typeInfo of
        TyConI (DataD [Type]
_ Name
_ [TyVarBndr]
vars Maybe Type
mKind [Con]
_ [DerivClause]
_) -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Q Type -> Q (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Maybe Type -> [TyVarBndr] -> Q Type
deriveFullType Name
typeName Maybe Type
mKind [TyVarBndr]
vars
        TyConI (NewtypeD [Type]
_ Name
_ [TyVarBndr]
vars Maybe Type
mKind Con
_ [DerivClause]
_) -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Q Type -> Q (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Maybe Type -> [TyVarBndr] -> Q Type
deriveFullType Name
typeName Maybe Type
mKind [TyVarBndr]
vars
        TyConI (TySynD Name
_ [TyVarBndr]
vars Type
_) -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Q Type -> Q (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Maybe Type -> [TyVarBndr] -> Q Type
deriveFullType Name
typeName Maybe Type
forall a. Maybe a
Nothing [TyVarBndr]
vars
        Info
_ -> Maybe Type -> Q (Maybe Type)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Type
forall a. Maybe a
Nothing

-- | Same as 'deriveRPC', but uses a custom strategy for deriving a 'Generic' instance.
deriveRPCWithStrategy :: String -> GenericStrategy -> Q [Dec]
deriveRPCWithStrategy :: String -> GenericStrategy -> Q [Dec]
deriveRPCWithStrategy String
typeStr GenericStrategy
gs = do
  Name
typeName <- String -> Q Name
lookupTypeNameOrFail String
typeStr
  Q Bool -> Q () -> Q ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Name -> Q Bool
isTypeAlias Name
typeName) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ String -> Q ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ String
typeStr String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" is a 'type' alias but not 'data' or 'newtype'."
  Name -> GenericStrategy -> Q [Dec]
deriveRPCWithStrategy' Name
typeName GenericStrategy
gs

deriveRPCWithStrategy' :: Name -> GenericStrategy -> Q [Dec]
deriveRPCWithStrategy' :: Name -> GenericStrategy -> Q [Dec]
deriveRPCWithStrategy' Name
typeName GenericStrategy
gs = do
  (Name
_, [Type]
decCxt, Maybe Type
mKind, [TyVarBndr]
tyVars, [Con]
constructors) <- Name -> Q (Name, [Type], Maybe Type, [TyVarBndr], [Con])
reifyDataType Name
typeName

  -- TODO: use `reifyInstances` to check that 'AsRPC' exists for `fieldType`
  -- Print user-friendly error msg if it doesn't.
  let typeNameRPC :: Name
typeNameRPC = Name -> Name
convertName Name
typeName
  [Con]
constructorsRPC <- (Con -> Q Con) -> [Con] -> Q [Con]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Con -> Q Con
convertConstructor [Con]
constructors
  [Type]
fieldTypesRPC <- [Con] -> Q [Type]
getFieldTypes [Con]
constructorsRPC

  Type
derivedType <- Name -> Maybe Type -> [TyVarBndr] -> Q Type
deriveFullType Name
typeName Maybe Type
mKind [TyVarBndr]
tyVars
  Type
derivedTypeRPC <- Name -> Maybe Type -> [TyVarBndr] -> Q Type
deriveFullType Name
typeNameRPC Maybe Type
mKind [TyVarBndr]
tyVars

  -- Note: we can't use `makeRep0Inline` to derive a `Rep` instance for `derivedTypeRPC`
  -- It internally uses `reify` to lookup info about `derivedTypeRPC`, and because `derivedTypeRPC` hasn't
  -- been spliced *yet*, the lookup fails.
  -- So, instead, we fetch the `Rep` instance for `derivedType`, and
  -- append "RPC" to the type/constructor/field names in its metadata.
  --
  -- If, for some reason, we find out that this approach doesn't work for some edge cases,
  -- we should get rid of it and patch the @generic-deriving@ package to export a version of `makeRep0Inline`
  -- that doesn't use `reify` (it should be easy enough).
  TySynEqn
repInstance <- Name -> Type -> Q TySynEqn
reifyRepInstance Name
typeName Type
derivedType
  String
currentModuleName <- Loc -> String
loc_module (Loc -> String) -> Q Loc -> Q String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Q Loc
location
  let repTypeRPC :: Type
repTypeRPC = String -> TySynEqn -> Type
convertRep String
currentModuleName TySynEqn
repInstance
  Dec
typeDecOfRPC <- Name
-> [Type] -> Name -> [TyVarBndr] -> Maybe Type -> [Con] -> Q Dec
mkTypeDeclaration Name
typeName [Type]
decCxt Name
typeNameRPC [TyVarBndr]
tyVars Maybe Type
mKind [Con]
constructorsRPC

  [[Dec]] -> [Dec]
forall a. Monoid a => [a] -> a
mconcat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Q [Dec]] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
    [ [Dec] -> Q [Dec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Dec] -> Q [Dec]) -> (Dec -> [Dec]) -> Dec -> Q [Dec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dec -> [Dec]
forall x. One x => OneItem x -> x
one (Dec -> Q [Dec]) -> Dec -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ Dec
typeDecOfRPC
    , Type -> Type -> Q [Dec]
mkAsRPCInstance Type
derivedType Type
derivedTypeRPC
    , [Type] -> Type -> Q [Dec]
mkIsoValueInstance [Type]
fieldTypesRPC Type
derivedTypeRPC
    , Maybe Type -> Name -> Type -> [Con] -> GenericStrategy -> Q [Dec]
customGeneric' (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
repTypeRPC) Name
typeNameRPC Type
derivedTypeRPC [Con]
constructorsRPC GenericStrategy
gs
    ]

  where
    -- | Given the field type @FieldType a b@, returns @AsRPC (FieldType a b)@.
    convertFieldType :: Type -> Type
    convertFieldType :: Type -> Type
convertFieldType Type
tp = Name -> Type
ConT ''AsRPC Type -> Type -> Type
`AppT` Type
tp

    convertNameStr :: String -> String
    convertNameStr :: String -> String
convertNameStr String
s = String
s String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"RPC"

    convertName :: Name -> Name
    convertName :: Name -> Name
convertName = String -> Name
mkName (String -> Name) -> (Name -> String) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
convertNameStr (String -> String) -> (Name -> String) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameBase

    -- | Given the constructor
    -- @C { f :: Int }@,
    -- returns the constructor
    -- @CRPC { fRPC :: AsRPC Int }@.
    convertConstructor :: Con -> Q Con
    convertConstructor :: Con -> Q Con
convertConstructor = \case
      RecC Name
conName [VarBangType]
fields -> Con -> Q Con
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Con -> Q Con) -> Con -> Q Con
forall a b. (a -> b) -> a -> b
$
        Name -> [VarBangType] -> Con
RecC
          (Name -> Name
convertName Name
conName)
          ([VarBangType]
fields [VarBangType] -> (VarBangType -> VarBangType) -> [VarBangType]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(Name
fieldName, Bang
fieldBang, Type
fieldType) ->
            (Name -> Name
convertName Name
fieldName, Bang
fieldBang, Type -> Type
convertFieldType Type
fieldType)
          )
      NormalC Name
conName [BangType]
fields -> Con -> Q Con
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Con -> Q Con) -> Con -> Q Con
forall a b. (a -> b) -> a -> b
$
        Name -> [BangType] -> Con
NormalC (Name -> Name
convertName Name
conName) ((Type -> Type) -> BangType -> BangType
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Type -> Type
convertFieldType (BangType -> BangType) -> [BangType] -> [BangType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BangType]
fields)
      InfixC BangType
fieldType1 Name
conName BangType
fieldType2 -> Con -> Q Con
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Con -> Q Con) -> Con -> Q Con
forall a b. (a -> b) -> a -> b
$
        BangType -> Name -> BangType -> Con
InfixC ((Type -> Type) -> BangType -> BangType
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Type -> Type
convertFieldType BangType
fieldType1) (Name -> Name
convertName Name
conName) ((Type -> Type) -> BangType -> BangType
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Type -> Type
convertFieldType BangType
fieldType2)
      Con
constr -> String -> Q Con
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q Con) -> String -> Q Con
forall a b. (a -> b) -> a -> b
$ String
"Unsupported constructor for '" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall b a. (Show a, IsString b) => a -> b
show Name
typeName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"': " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Con -> String
forall b a. (Show a, IsString b) => a -> b
show Con
constr

    -- | Get a list of all the unique types of all the fields of all the given constructors.
    getFieldTypes :: [Con] -> Q [Type]
    getFieldTypes :: [Con] -> Q [Type]
getFieldTypes [Con]
constrs = [Type] -> [Type]
forall a. Ord a => [a] -> [a]
ordNub ([Type] -> [Type]) -> ([[Type]] -> [Type]) -> [[Type]] -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Type]] -> [Type]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ([[Type]] -> [Type]) -> Q [[Type]] -> Q [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Con] -> (Con -> Q [Type]) -> Q [[Type]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Con]
constrs \case
      RecC Name
_ [VarBangType]
fields -> [Type] -> Q [Type]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Type] -> Q [Type]) -> [Type] -> Q [Type]
forall a b. (a -> b) -> a -> b
$ [VarBangType]
fields [VarBangType] -> (VarBangType -> Type) -> [Type]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(Name
_, Bang
_, Type
fieldType) -> Type
fieldType
      NormalC Name
_ [BangType]
fields -> [Type] -> Q [Type]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Type] -> Q [Type]) -> [Type] -> Q [Type]
forall a b. (a -> b) -> a -> b
$ BangType -> Type
forall a b. (a, b) -> b
snd (BangType -> Type) -> [BangType] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BangType]
fields
      InfixC BangType
field1 Name
_ BangType
field2 -> [Type] -> Q [Type]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [BangType -> Type
forall a b. (a, b) -> b
snd BangType
field1, BangType -> Type
forall a b. (a, b) -> b
snd BangType
field2]
      Con
constr -> String -> Q [Type]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q [Type]) -> String -> Q [Type]
forall a b. (a -> b) -> a -> b
$ String
"Unsupported constructor for '" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall b a. (Show a, IsString b) => a -> b
show Name
typeName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"': " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Con -> String
forall b a. (Show a, IsString b) => a -> b
show Con
constr

    mkTypeDeclaration :: Name -> Cxt -> Name -> [TyVarBndr] -> Maybe Kind -> [Con] -> Q Dec
    mkTypeDeclaration :: Name
-> [Type] -> Name -> [TyVarBndr] -> Maybe Type -> [Con] -> Q Dec
mkTypeDeclaration Name
tyName [Type]
decCxt Name
typeNameRPC [TyVarBndr]
tyVars Maybe Type
mKind [Con]
constructorsRPC = do
      Info
typeInfo <- Name -> Q Info
reify Name
tyName
      case Info
typeInfo of
        TyConI DataD {} -> Dec -> Q Dec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ [Type]
-> Name
-> [TyVarBndr]
-> Maybe Type
-> [Con]
-> [DerivClause]
-> Dec
DataD [Type]
decCxt Name
typeNameRPC [TyVarBndr]
tyVars Maybe Type
mKind [Con]
constructorsRPC []
        TyConI NewtypeD {} -> (case [Con]
constructorsRPC of
          [Con
con] -> Dec -> Q Dec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ [Type]
-> Name -> [TyVarBndr] -> Maybe Type -> Con -> [DerivClause] -> Dec
NewtypeD [Type]
decCxt Name
typeNameRPC [TyVarBndr]
tyVars Maybe Type
mKind Con
con []
          [Con]
_ -> String -> Q Dec
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Newtype has only one constructor")
        Info
_ -> String -> Q Dec
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q Dec) -> String -> Q Dec
forall a b. (a -> b) -> a -> b
$ String
"Only newtypes and data types are supported, but '" String -> String -> String
forall a. Semigroup a => a -> a -> a
<>
          Name -> String
forall b a. (Show a, IsString b) => a -> b
show Name
tyName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"' is:\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Info -> String
forall b a. (Show a, IsString b) => a -> b
show Info
typeInfo

    -- | Traverse a 'Rep' type and:
    --
    -- 1. Inspect its metadata and append @RPC@ to the type/constructor/field names.
    -- 2. Convert field types (e.g. @T@ becomes @AsRPC T@).
    -- 3. Replace the Rep's module name with the name of the module of where this Q is being spliced.
    convertRep :: String -> TySynEqn -> Type
    convertRep :: String -> TySynEqn -> Type
convertRep String
currentModuleName (TySynEqn Maybe [TyVarBndr]
_tyVars Type
_lhs Type
rhs) = Type -> Type
go Type
rhs
      where
        go :: Type -> Type
        go :: Type -> Type
go = \case
          -- Rename type name and module name
          PromotedT Name
t `AppT` LitT (StrTyLit String
tyName) `AppT` LitT (StrTyLit String
_moduleName)
            | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== 'G.MetaData
            -> Name -> Type
PromotedT Name
t Type -> Type -> Type
`AppT` TyLit -> Type
LitT (String -> TyLit
StrTyLit (String -> String
convertNameStr String
tyName)) Type -> Type -> Type
`AppT` TyLit -> Type
LitT (String -> TyLit
StrTyLit String
currentModuleName)
          -- Rename constructor names
          PromotedT Name
t `AppT` LitT (StrTyLit String
conName)
            | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== 'G.MetaCons
            -> Name -> Type
PromotedT Name
t Type -> Type -> Type
`AppT` TyLit -> Type
LitT (String -> TyLit
StrTyLit (String -> String
convertNameStr String
conName))
          -- Rename field names
          PromotedT Name
t `AppT` (PromotedT Name
just `AppT` LitT (StrTyLit String
fieldName))
            | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== 'G.MetaSel
            -> Name -> Type
PromotedT Name
t Type -> Type -> Type
`AppT` (Name -> Type
PromotedT Name
just Type -> Type -> Type
`AppT` TyLit -> Type
LitT (String -> TyLit
StrTyLit (String -> String
convertNameStr String
fieldName)))
          -- Replace field type @T@ with @AsRPC T@
          ConT Name
x `AppT` Type
fieldType
            | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''G.Rec0
            -> Name -> Type
ConT Name
x Type -> Type -> Type
`AppT` Type -> Type
convertFieldType Type
fieldType
          Type
x `AppT` Type
y -> Type -> Type
go Type
x Type -> Type -> Type
`AppT` Type -> Type
go Type
y
          Type
x -> Type
x

    -- | Lookup the generic 'Rep' type instance for the given type.
    reifyRepInstance :: Name -> Type -> Q TySynEqn
    reifyRepInstance :: Name -> Type -> Q TySynEqn
reifyRepInstance Name
name Type
tp =
      Name -> [Type] -> Q [Dec]
reifyInstances ''G.Rep [Type
tp] Q [Dec] -> ([Dec] -> Q TySynEqn) -> Q TySynEqn
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        [TySynInstD TySynEqn
repInstance] -> TySynEqn -> Q TySynEqn
forall (f :: * -> *) a. Applicative f => a -> f a
pure TySynEqn
repInstance
        (Dec
_:[Dec]
_) -> String -> Q TySynEqn
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q TySynEqn) -> String -> Q TySynEqn
forall a b. (a -> b) -> a -> b
$ String
"Found multiple instances of 'Generic' for '" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall b a. (Show a, IsString b) => a -> b
show Name
name String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"'."
        [] -> String -> Q TySynEqn
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q TySynEqn) -> String -> Q TySynEqn
forall a b. (a -> b) -> a -> b
$ String
"Type '" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall b a. (Show a, IsString b) => a -> b
show Name
name String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"' must implement 'Generic'."

    -- | Given the type @Foo a b = Foo a@, generate an 'IsoValue' instance like:
    --
    -- > deriving anyclass instance IsoValue (AsRPC a) => IsoValue (FooRPC a b)
    --
    -- Note that if a type variable @t@ is a phantom type variable, then no @IsoValue (AsRPC t)@
    -- constraint is generated for it.
    mkIsoValueInstance :: [Type] -> Type -> Q [Dec]
    mkIsoValueInstance :: [Type] -> Type -> Q [Dec]
mkIsoValueInstance [Type]
fieldTypes Type
tp =
      Dec -> [Dec]
forall x. One x => OneItem x -> x
one (Dec -> [Dec]) -> Q Dec -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DerivStrategy -> Q [Type] -> Q Type -> Q Dec
standaloneDerivWithStrategyD (DerivStrategy -> Maybe DerivStrategy
forall a. a -> Maybe a
Just DerivStrategy
AnyclassStrategy) Q [Type]
constraints [t|IsoValue $(pure tp)|]
      where
        constraints :: Q Cxt
        constraints :: Q [Type]
constraints =
          [Q Type] -> Q [Type]
cxt ([Q Type] -> Q [Type]) -> [Q Type] -> Q [Type]
forall a b. (a -> b) -> a -> b
$ (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter Type -> Bool
hasTyVar [Type]
fieldTypes [Type] -> (Type -> Q Type) -> [Q Type]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Type
fieldType ->
            [t|IsoValue $(pure fieldType)|]

        hasTyVar :: Type -> Bool
        hasTyVar :: Type -> Bool
hasTyVar Type
ty =
          ((Type -> Bool) -> [Type] -> Bool)
-> [Type] -> (Type -> Bool) -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Type -> Bool) -> [Type] -> Bool
forall t. Container t => (Element t -> Bool) -> t -> Bool
any (Type -> [Type]
forall a. Plated a => a -> [a]
universe Type
ty) \case
            VarT Name
_ -> Bool
True
            Type
_ -> Bool
False

    mkAsRPCInstance :: Type -> Type -> Q [Dec]
    mkAsRPCInstance :: Type -> Type -> Q [Dec]
mkAsRPCInstance Type
tp Type
tpRPC =
      [d|
        type instance AsRPC $(pure tp) = $(pure tpRPC)
      |]

----------------------------------------------------------------------------
-- Conversions
----------------------------------------------------------------------------

-- | Replace all big_maps in a value with the respective big_map IDs.
--
-- Throws an error if it finds a big_map without an ID.
valueAsRPC :: HasCallStack => Value t -> Value (AsRPC t)
valueAsRPC :: Value t -> Value (AsRPC t)
valueAsRPC Value t
v =
  case Value t
v of
    VKey {} -> Value t
Value (AsRPC t)
v
    VUnit {} -> Value t
Value (AsRPC t)
v
    VSignature {} -> Value t
Value (AsRPC t)
v
    VChainId {} -> Value t
Value (AsRPC t)
v
    VChest {} -> Value t
Value (AsRPC t)
v
    VChestKey {} -> Value t
Value (AsRPC t)
v
    VOption (Maybe (Value t1)
vMaybe :: Maybe (Value elem)) ->
      (SingI t1 :- SingI (AsRPC t1))
-> (SingI (AsRPC t1) => Value ('TOption (AsRPC t1)))
-> Value ('TOption (AsRPC t1))
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (SingI t1 :- SingI (AsRPC t1)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @elem) ((SingI (AsRPC t1) => Value ('TOption (AsRPC t1)))
 -> Value ('TOption (AsRPC t1)))
-> (SingI (AsRPC t1) => Value ('TOption (AsRPC t1)))
-> Value ('TOption (AsRPC t1))
forall a b. (a -> b) -> a -> b
$
        Maybe (Value' Instr (AsRPC t1)) -> Value ('TOption (AsRPC t1))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value' Instr (AsRPC t1)) -> Value ('TOption (AsRPC t1)))
-> Maybe (Value' Instr (AsRPC t1)) -> Value ('TOption (AsRPC t1))
forall a b. (a -> b) -> a -> b
$ Value t1 -> Value' Instr (AsRPC t1)
forall (t :: T). HasCallStack => Value t -> Value (AsRPC t)
valueAsRPC (Value t1 -> Value' Instr (AsRPC t1))
-> Maybe (Value t1) -> Maybe (Value' Instr (AsRPC t1))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Value t1)
vMaybe
    VList ([Value t1]
vList :: [Value elem]) ->
      (SingI t1 :- SingI (AsRPC t1))
-> (SingI (AsRPC t1) => Value ('TList (AsRPC t1)))
-> Value ('TList (AsRPC t1))
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (SingI t1 :- SingI (AsRPC t1)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @elem) ((SingI (AsRPC t1) => Value ('TList (AsRPC t1)))
 -> Value ('TList (AsRPC t1)))
-> (SingI (AsRPC t1) => Value ('TList (AsRPC t1)))
-> Value ('TList (AsRPC t1))
forall a b. (a -> b) -> a -> b
$
        [Value' Instr (AsRPC t1)] -> Value ('TList (AsRPC t1))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList ([Value' Instr (AsRPC t1)] -> Value ('TList (AsRPC t1)))
-> [Value' Instr (AsRPC t1)] -> Value ('TList (AsRPC t1))
forall a b. (a -> b) -> a -> b
$ Value t1 -> Value' Instr (AsRPC t1)
forall (t :: T). HasCallStack => Value t -> Value (AsRPC t)
valueAsRPC (Value t1 -> Value' Instr (AsRPC t1))
-> [Value t1] -> [Value' Instr (AsRPC t1)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Value t1]
vList
    VSet {} -> Value t
Value (AsRPC t)
v
    VOp {} -> Value t
Value (AsRPC t)
v
    VContract {} -> Value t
Value (AsRPC t)
v
    VTicket {} -> Value t
Value (AsRPC t)
v
    VPair (Value' Instr l
x, Value' Instr r
y) -> (Value' Instr (AsRPC l), Value' Instr (AsRPC r))
-> Value' Instr ('TPair (AsRPC l) (AsRPC r))
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value' Instr l -> Value' Instr (AsRPC l)
forall (t :: T). HasCallStack => Value t -> Value (AsRPC t)
valueAsRPC Value' Instr l
x, Value' Instr r -> Value' Instr (AsRPC r)
forall (t :: T). HasCallStack => Value t -> Value (AsRPC t)
valueAsRPC Value' Instr r
y)
    VOr (Either (Value l) (Value r)
vEither :: Either (Value l) (Value r)) ->
      ((SingI l, SingI r) :- (SingI (AsRPC l), SingI (AsRPC r)))
-> ((SingI (AsRPC l), SingI (AsRPC r)) =>
    Value ('TOr (AsRPC l) (AsRPC r)))
-> Value ('TOr (AsRPC l) (AsRPC r))
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (SingI l :- SingI (AsRPC l)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @l (SingI l :- SingI (AsRPC l))
-> (SingI r :- SingI (AsRPC r))
-> (SingI l, SingI r) :- (SingI (AsRPC l), SingI (AsRPC r))
forall (a :: Constraint) (b :: Constraint) (c :: Constraint)
       (d :: Constraint).
(a :- b) -> (c :- d) -> (a, c) :- (b, d)
*** SingI r :- SingI (AsRPC r)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @r) (((SingI (AsRPC l), SingI (AsRPC r)) =>
  Value ('TOr (AsRPC l) (AsRPC r)))
 -> Value ('TOr (AsRPC l) (AsRPC r)))
-> ((SingI (AsRPC l), SingI (AsRPC r)) =>
    Value ('TOr (AsRPC l) (AsRPC r)))
-> Value ('TOr (AsRPC l) (AsRPC r))
forall a b. (a -> b) -> a -> b
$
        case Either (Value l) (Value r)
vEither of
          Right Value r
r -> Either (Value' Instr (AsRPC l)) (Value' Instr (AsRPC r))
-> Value ('TOr (AsRPC l) (AsRPC r))
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' Instr (AsRPC r)
-> Either (Value' Instr (AsRPC l)) (Value' Instr (AsRPC r))
forall a b. b -> Either a b
Right (Value r -> Value' Instr (AsRPC r)
forall (t :: T). HasCallStack => Value t -> Value (AsRPC t)
valueAsRPC Value r
r))
          Left Value l
l -> Either (Value' Instr (AsRPC l)) (Value' Instr (AsRPC r))
-> Value ('TOr (AsRPC l) (AsRPC r))
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' Instr (AsRPC l)
-> Either (Value' Instr (AsRPC l)) (Value' Instr (AsRPC r))
forall a b. a -> Either a b
Left (Value l -> Value' Instr (AsRPC l)
forall (t :: T). HasCallStack => Value t -> Value (AsRPC t)
valueAsRPC Value l
l))
    VLam {} -> Value t
Value (AsRPC t)
v
    VMap (Map (Value k) (Value v)
vMap :: Map (Value k) (Value v)) ->
      (SingI v :- SingI (AsRPC v))
-> (SingI (AsRPC v) => Value ('TMap k (AsRPC v)))
-> Value ('TMap k (AsRPC v))
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (SingI v :- SingI (AsRPC v)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @v) ((SingI (AsRPC v) => Value ('TMap k (AsRPC v)))
 -> Value ('TMap k (AsRPC v)))
-> (SingI (AsRPC v) => Value ('TMap k (AsRPC v)))
-> Value ('TMap k (AsRPC v))
forall a b. (a -> b) -> a -> b
$
        Map (Value k) (Value' Instr (AsRPC v)) -> Value ('TMap k (AsRPC v))
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 (Map (Value k) (Value' Instr (AsRPC v))
 -> Value ('TMap k (AsRPC v)))
-> Map (Value k) (Value' Instr (AsRPC v))
-> Value ('TMap k (AsRPC v))
forall a b. (a -> b) -> a -> b
$ Value v -> Value' Instr (AsRPC v)
forall (t :: T). HasCallStack => Value t -> Value (AsRPC t)
valueAsRPC (Value v -> Value' Instr (AsRPC v))
-> Map (Value k) (Value v)
-> Map (Value k) (Value' Instr (AsRPC v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Value k) (Value v)
vMap
    VBigMap (Just Natural
bmId) Map (Value' Instr k) (Value' Instr v)
_ -> Natural -> Value' Instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
bmId
    VBigMap Maybe Natural
Nothing Map (Value' Instr k) (Value' Instr v)
_ ->
      Text -> Value' Instr 'TNat
forall a. HasCallStack => Text -> a
error (Text -> Value' Instr 'TNat) -> Text -> Value' Instr 'TNat
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
unlines
        [ Text
"Expected all big_maps to have an ID, but at least one big_map didn't."
        , Text
"This is most likely a bug."
        ]
    VInt {} -> Value t
Value (AsRPC t)
v
    VNat {} -> Value t
Value (AsRPC t)
v
    VString {} -> Value t
Value (AsRPC t)
v
    VBytes {} -> Value t
Value (AsRPC t)
v
    VMutez {} -> Value t
Value (AsRPC t)
v
    VBool {} -> Value t
Value (AsRPC t)
v
    VKeyHash {} -> Value t
Value (AsRPC t)
v
    VTimestamp {} -> Value t
Value (AsRPC t)
v
    VAddress {} -> Value t
Value (AsRPC t)
v
    VBls12381Fr {} -> Value t
Value (AsRPC t)
v
    VBls12381G1 {} -> Value t
Value (AsRPC t)
v
    VBls12381G2 {} -> Value t
Value (AsRPC t)
v

-- | Replace all @big_map@ annotations in a value with @nat@ annotations.
notesAsRPC :: Notes t -> Notes (AsRPC t)
notesAsRPC :: Notes t -> Notes (AsRPC t)
notesAsRPC Notes t
notes =
  case Notes t
notes of
    NTKey {} -> Notes t
Notes (AsRPC t)
notes
    NTUnit {} -> Notes t
Notes (AsRPC t)
notes
    NTSignature {} -> Notes t
Notes (AsRPC t)
notes
    NTChainId {} -> Notes t
Notes (AsRPC t)
notes
    NTChest {} -> Notes t
Notes (AsRPC t)
notes
    NTChestKey {} -> Notes t
Notes (AsRPC t)
notes
    NTOption TypeAnn
typeAnn Notes t1
elemNotes -> TypeAnn -> Notes (AsRPC t1) -> Notes ('TOption (AsRPC t1))
forall (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TOption t1)
NTOption TypeAnn
typeAnn (Notes (AsRPC t1) -> Notes ('TOption (AsRPC t1)))
-> Notes (AsRPC t1) -> Notes ('TOption (AsRPC t1))
forall a b. (a -> b) -> a -> b
$ Notes t1 -> Notes (AsRPC t1)
forall (t :: T). Notes t -> Notes (AsRPC t)
notesAsRPC Notes t1
elemNotes
    NTList TypeAnn
typeAnn Notes t1
elemNotes -> TypeAnn -> Notes (AsRPC t1) -> Notes ('TList (AsRPC t1))
forall (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TList t1)
NTList TypeAnn
typeAnn (Notes (AsRPC t1) -> Notes ('TList (AsRPC t1)))
-> Notes (AsRPC t1) -> Notes ('TList (AsRPC t1))
forall a b. (a -> b) -> a -> b
$ Notes t1 -> Notes (AsRPC t1)
forall (t :: T). Notes t -> Notes (AsRPC t)
notesAsRPC Notes t1
elemNotes
    NTSet {} -> Notes t
Notes (AsRPC t)
notes
    NTOperation {} -> Notes t
Notes (AsRPC t)
notes
    NTContract {} -> Notes t
Notes (AsRPC t)
notes
    NTTicket {} -> Notes t
Notes (AsRPC t)
notes
    NTPair TypeAnn
typeAnn FieldAnn
fieldAnn1 FieldAnn
fieldAnn2 VarAnn
varAnn1 VarAnn
varAnn2 Notes p
notes1 Notes q
notes2 ->
      TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes (AsRPC p)
-> Notes (AsRPC q)
-> Notes ('TPair (AsRPC p) (AsRPC q))
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes q
-> Notes ('TPair p q)
NTPair TypeAnn
typeAnn FieldAnn
fieldAnn1 FieldAnn
fieldAnn2 VarAnn
varAnn1 VarAnn
varAnn2 (Notes p -> Notes (AsRPC p)
forall (t :: T). Notes t -> Notes (AsRPC t)
notesAsRPC Notes p
notes1) (Notes q -> Notes (AsRPC q)
forall (t :: T). Notes t -> Notes (AsRPC t)
notesAsRPC Notes q
notes2)
    NTOr TypeAnn
typeAnn FieldAnn
fieldAnn1 FieldAnn
fieldAnn2 Notes p
notes1 Notes q
notes2 ->
      TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes (AsRPC p)
-> Notes (AsRPC q)
-> Notes ('TOr (AsRPC p) (AsRPC q))
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
NTOr TypeAnn
typeAnn FieldAnn
fieldAnn1 FieldAnn
fieldAnn2 (Notes p -> Notes (AsRPC p)
forall (t :: T). Notes t -> Notes (AsRPC t)
notesAsRPC Notes p
notes1) (Notes q -> Notes (AsRPC q)
forall (t :: T). Notes t -> Notes (AsRPC t)
notesAsRPC Notes q
notes2)
    NTLambda {} -> Notes t
Notes (AsRPC t)
notes
    NTMap TypeAnn
typeAnn Notes k
keyAnns Notes v
valueNotes -> TypeAnn -> Notes k -> Notes (AsRPC v) -> Notes ('TMap k (AsRPC v))
forall (k :: T) (v :: T).
TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v)
NTMap TypeAnn
typeAnn Notes k
keyAnns (Notes v -> Notes (AsRPC v)
forall (t :: T). Notes t -> Notes (AsRPC t)
notesAsRPC Notes v
valueNotes)
    NTBigMap TypeAnn
typeAnn Notes k
_ Notes v
_ -> TypeAnn -> Notes 'TNat
NTNat TypeAnn
typeAnn
    NTInt {} -> Notes t
Notes (AsRPC t)
notes
    NTNat {} -> Notes t
Notes (AsRPC t)
notes
    NTString {} -> Notes t
Notes (AsRPC t)
notes
    NTBytes {} -> Notes t
Notes (AsRPC t)
notes
    NTMutez {} -> Notes t
Notes (AsRPC t)
notes
    NTBool {} -> Notes t
Notes (AsRPC t)
notes
    NTKeyHash {} -> Notes t
Notes (AsRPC t)
notes
    NTTimestamp {} -> Notes t
Notes (AsRPC t)
notes
    NTAddress {} -> Notes t
Notes (AsRPC t)
notes
    NTBls12381Fr {} -> Notes t
Notes (AsRPC t)
notes
    NTBls12381G1 {} -> Notes t
Notes (AsRPC t)
notes
    NTBls12381G2 {} -> Notes t
Notes (AsRPC t)
notes
    NTNever {} -> Notes t
Notes (AsRPC t)
notes

----------------------------------------------------------------------------
-- Entailments
----------------------------------------------------------------------------

-- | A proof that if a singleton exists for @t@,
-- then so it does for @AsRPC t@.
rpcSingIEvi :: forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi :: SingI t :- SingI (AsRPC t)
rpcSingIEvi =
  (SingI t => Dict (SingI (AsRPC t))) -> SingI t :- SingI (AsRPC t)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((SingI t => Dict (SingI (AsRPC t))) -> SingI t :- SingI (AsRPC t))
-> (SingI t => Dict (SingI (AsRPC t)))
-> SingI t :- SingI (AsRPC t)
forall a b. (a -> b) -> a -> b
$
    case SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t of
      Sing t
STKey -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STUnit {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STSignature {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STChainId {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STChest {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STChestKey {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STOption (s :: Sing elem) -> Sing n
-> (SingI n => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
s ((SingI n => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t)))
-> (SingI n => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall a b. (a -> b) -> a -> b
$ SingI (AsRPC n) => Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (SingI (AsRPC n) => Dict (SingI (AsRPC t)))
-> (SingI n :- SingI (AsRPC n)) -> Dict (SingI (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI n :- SingI (AsRPC n)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @elem
      STList (s :: Sing elem) -> Sing n
-> (SingI n => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
s ((SingI n => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t)))
-> (SingI n => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall a b. (a -> b) -> a -> b
$  SingI (AsRPC n) => Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (SingI (AsRPC n) => Dict (SingI (AsRPC t)))
-> (SingI n :- SingI (AsRPC n)) -> Dict (SingI (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI n :- SingI (AsRPC n)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @elem
      STSet (s :: Sing elem) -> Sing n
-> (SingI n => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
s ((SingI n => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t)))
-> (SingI n => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall a b. (a -> b) -> a -> b
$ SingI (AsRPC n) => Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (SingI (AsRPC n) => Dict (SingI (AsRPC t)))
-> (SingI n :- SingI (AsRPC n)) -> Dict (SingI (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI n :- SingI (AsRPC n)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @elem
      STOperation {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STContract {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STTicket {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STPair (sa :: Sing a) (sb :: Sing b) ->
        Sing n1
-> (SingI n1 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
sa ((SingI n1 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t)))
-> (SingI n1 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
sb ((SingI n2 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t)))
-> (SingI n2 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall a b. (a -> b) -> a -> b
$
          SingI (AsRPC n1) => Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (SingI (AsRPC n1) => Dict (SingI (AsRPC t)))
-> (SingI n1 :- SingI (AsRPC n1)) -> Dict (SingI (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI n1 :- SingI (AsRPC n1)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @a (SingI (AsRPC n2) => Dict (SingI (AsRPC t)))
-> (SingI n2 :- SingI (AsRPC n2)) -> Dict (SingI (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI n2 :- SingI (AsRPC n2)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @b
      STOr (sl :: Sing l) (sr :: Sing r) ->
        Sing n1
-> (SingI n1 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
sl ((SingI n1 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t)))
-> (SingI n1 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
sr ((SingI n2 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t)))
-> (SingI n2 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall a b. (a -> b) -> a -> b
$
          SingI (AsRPC n1) => Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (SingI (AsRPC n1) => Dict (SingI (AsRPC t)))
-> (SingI n1 :- SingI (AsRPC n1)) -> Dict (SingI (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI n1 :- SingI (AsRPC n1)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @l (SingI (AsRPC n2) => Dict (SingI (AsRPC t)))
-> (SingI n2 :- SingI (AsRPC n2)) -> Dict (SingI (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI n2 :- SingI (AsRPC n2)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @r
      STLambda {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STMap (sk :: Sing k) (sv :: Sing v) ->
        Sing n1
-> (SingI n1 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
sk ((SingI n1 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t)))
-> (SingI n1 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (SingI n2 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
sv ((SingI n2 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t)))
-> (SingI n2 => Dict (SingI (AsRPC t))) -> Dict (SingI (AsRPC t))
forall a b. (a -> b) -> a -> b
$
          SingI (AsRPC n1) => Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (SingI (AsRPC n1) => Dict (SingI (AsRPC t)))
-> (SingI n1 :- SingI (AsRPC n1)) -> Dict (SingI (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI n1 :- SingI (AsRPC n1)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @k (SingI (AsRPC n2) => Dict (SingI (AsRPC t)))
-> (SingI n2 :- SingI (AsRPC n2)) -> Dict (SingI (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI n2 :- SingI (AsRPC n2)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @v
      STBigMap {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STInt {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STNat {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STString {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STBytes {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STMutez {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STBool {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STKeyHash {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STBls12381Fr {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STBls12381G1 {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STBls12381G2 {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STTimestamp {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STAddress {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
      STNever {} -> Dict (SingI (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict

-- | A proof that if @t@ does not contain any operations, then neither does @AsRPC t@.
rpcHasNoOpEvi :: forall (t :: T). (SingI t, HasNoOp t) => HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi :: HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi = Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
forall (t :: T).
HasNoOp t =>
Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' Sing t
forall k (a :: k). SingI a => Sing a
sing

rpcHasNoOpEvi'
  :: HasNoOp t
  => Sing t
  -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' :: Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' Sing t
sng = (HasNoOp t => Dict (HasNoOp (AsRPC t)))
-> HasNoOp t :- HasNoOp (AsRPC t)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((HasNoOp t => Dict (HasNoOp (AsRPC t)))
 -> HasNoOp t :- HasNoOp (AsRPC t))
-> (HasNoOp t => Dict (HasNoOp (AsRPC t)))
-> HasNoOp t :- HasNoOp (AsRPC t)
forall a b. (a -> b) -> a -> b
$ case Sing t
sng of
  Sing t
STKey -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STUnit {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STSignature {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChainId {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChest {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChestKey {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STOption s -> HasNoOp (AsRPC n) => Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoOp (AsRPC n) => Dict (HasNoOp (AsRPC t)))
-> (HasNoOp n :- HasNoOp (AsRPC n)) -> Dict (HasNoOp (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> HasNoOp n :- HasNoOp (AsRPC n)
forall (t :: T).
HasNoOp t =>
Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' Sing n
s
  STList s -> HasNoOp (AsRPC n) => Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoOp (AsRPC n) => Dict (HasNoOp (AsRPC t)))
-> (HasNoOp n :- HasNoOp (AsRPC n)) -> Dict (HasNoOp (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> HasNoOp n :- HasNoOp (AsRPC n)
forall (t :: T).
HasNoOp t =>
Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' Sing n
s
  STSet s -> HasNoOp (AsRPC n) => Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoOp (AsRPC n) => Dict (HasNoOp (AsRPC t)))
-> (HasNoOp n :- HasNoOp (AsRPC n)) -> Dict (HasNoOp (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> HasNoOp n :- HasNoOp (AsRPC n)
forall (t :: T).
HasNoOp t =>
Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' Sing n
s
  STContract {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STTicket {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STPair sa sb -> case Sing n1 -> OpPresence n1
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n1
sa of
    OpPresence n1
OpAbsent -> HasNoOp (AsRPC n1) => Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoOp (AsRPC n1) => Dict (HasNoOp (AsRPC t)))
-> (HasNoOp n1 :- HasNoOp (AsRPC n1)) -> Dict (HasNoOp (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> HasNoOp n1 :- HasNoOp (AsRPC n1)
forall (t :: T).
HasNoOp t =>
Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' Sing n1
sa (HasNoOp (AsRPC n2) => Dict (HasNoOp (AsRPC t)))
-> (HasNoOp n2 :- HasNoOp (AsRPC n2)) -> Dict (HasNoOp (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> HasNoOp n2 :- HasNoOp (AsRPC n2)
forall (t :: T).
HasNoOp t =>
Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' Sing n2
sb
  STOr sl sr -> case Sing n1 -> OpPresence n1
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n1
sl of
    OpPresence n1
OpAbsent -> HasNoOp (AsRPC n1) => Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoOp (AsRPC n1) => Dict (HasNoOp (AsRPC t)))
-> (HasNoOp n1 :- HasNoOp (AsRPC n1)) -> Dict (HasNoOp (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> HasNoOp n1 :- HasNoOp (AsRPC n1)
forall (t :: T).
HasNoOp t =>
Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' Sing n1
sl (HasNoOp (AsRPC n2) => Dict (HasNoOp (AsRPC t)))
-> (HasNoOp n2 :- HasNoOp (AsRPC n2)) -> Dict (HasNoOp (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> HasNoOp n2 :- HasNoOp (AsRPC n2)
forall (t :: T).
HasNoOp t =>
Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' Sing n2
sr
  STLambda {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STMap _ sv -> case Sing n2 -> OpPresence n2
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing n2
sv of
    OpPresence n2
OpAbsent -> HasNoOp (AsRPC n2) => Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoOp (AsRPC n2) => Dict (HasNoOp (AsRPC t)))
-> (HasNoOp n2 :- HasNoOp (AsRPC n2)) -> Dict (HasNoOp (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> HasNoOp n2 :- HasNoOp (AsRPC n2)
forall (t :: T).
HasNoOp t =>
Sing t -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' Sing n2
sv
  STBigMap {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STInt {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STNat {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STString {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBytes {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STMutez {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBool {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STKeyHash {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381Fr {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381G1 {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381G2 {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STTimestamp {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STAddress {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STNever {} -> Dict (HasNoOp (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict

-- | A proof that @AsRPC (Value t)@ does not contain big_maps.
rpcHasNoBigMapEvi :: forall (t :: T). SingI t => Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi :: Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi = Sing t -> Dict (HasNoBigMap (AsRPC t))
forall (t :: T). Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' (SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t)

rpcHasNoBigMapEvi' :: Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' :: Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' = \case
  Sing t
STKey -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STUnit {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STSignature {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChainId {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChest {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChestKey {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STOption s -> HasNoBigMap (AsRPC n) => Dict (HasNoBigMap ('TOption (AsRPC n)))
forall (a :: Constraint). a => Dict a
Dict (HasNoBigMap (AsRPC n) => Dict (HasNoBigMap ('TOption (AsRPC n))))
-> Dict (HasNoBigMap (AsRPC n))
-> Dict (HasNoBigMap ('TOption (AsRPC n)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (HasNoBigMap (AsRPC n))
forall (t :: T). Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' Sing n
s
  STList s -> HasNoBigMap (AsRPC n) => Dict (HasNoBigMap ('TList (AsRPC n)))
forall (a :: Constraint). a => Dict a
Dict (HasNoBigMap (AsRPC n) => Dict (HasNoBigMap ('TList (AsRPC n))))
-> Dict (HasNoBigMap (AsRPC n))
-> Dict (HasNoBigMap ('TList (AsRPC n)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (HasNoBigMap (AsRPC n))
forall (t :: T). Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' Sing n
s
  STSet s -> HasNoBigMap (AsRPC n) => Dict (HasNoBigMap ('TSet n))
forall (a :: Constraint). a => Dict a
Dict (HasNoBigMap (AsRPC n) => Dict (HasNoBigMap ('TSet n)))
-> Dict (HasNoBigMap (AsRPC n)) -> Dict (HasNoBigMap ('TSet n))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (HasNoBigMap (AsRPC n))
forall (t :: T). Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' Sing n
s
  STOperation {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STContract {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STTicket {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STPair sa sb -> HasNoBigMap (AsRPC n1) =>
Dict (HasNoBigMap ('TPair (AsRPC n1) (AsRPC n2)))
forall (a :: Constraint). a => Dict a
Dict (HasNoBigMap (AsRPC n1) =>
 Dict (HasNoBigMap ('TPair (AsRPC n1) (AsRPC n2))))
-> Dict (HasNoBigMap (AsRPC n1))
-> Dict (HasNoBigMap ('TPair (AsRPC n1) (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (HasNoBigMap (AsRPC n1))
forall (t :: T). Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' Sing n1
sa (HasNoBigMap (AsRPC n2) =>
 Dict (HasNoBigMap ('TPair (AsRPC n1) (AsRPC n2))))
-> Dict (HasNoBigMap (AsRPC n2))
-> Dict (HasNoBigMap ('TPair (AsRPC n1) (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (HasNoBigMap (AsRPC n2))
forall (t :: T). Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' Sing n2
sb
  STOr sl sr -> HasNoBigMap (AsRPC n1) =>
Dict (HasNoBigMap ('TOr (AsRPC n1) (AsRPC n2)))
forall (a :: Constraint). a => Dict a
Dict (HasNoBigMap (AsRPC n1) =>
 Dict (HasNoBigMap ('TOr (AsRPC n1) (AsRPC n2))))
-> Dict (HasNoBigMap (AsRPC n1))
-> Dict (HasNoBigMap ('TOr (AsRPC n1) (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (HasNoBigMap (AsRPC n1))
forall (t :: T). Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' Sing n1
sl (HasNoBigMap (AsRPC n2) =>
 Dict (HasNoBigMap ('TOr (AsRPC n1) (AsRPC n2))))
-> Dict (HasNoBigMap (AsRPC n2))
-> Dict (HasNoBigMap ('TOr (AsRPC n1) (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (HasNoBigMap (AsRPC n2))
forall (t :: T). Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' Sing n2
sr
  STLambda {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STMap sk sv -> HasNoBigMap (AsRPC n1) => Dict (HasNoBigMap ('TMap n1 (AsRPC n2)))
forall (a :: Constraint). a => Dict a
Dict (HasNoBigMap (AsRPC n1) =>
 Dict (HasNoBigMap ('TMap n1 (AsRPC n2))))
-> Dict (HasNoBigMap (AsRPC n1))
-> Dict (HasNoBigMap ('TMap n1 (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (HasNoBigMap (AsRPC n1))
forall (t :: T). Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' Sing n1
sk (HasNoBigMap (AsRPC n2) =>
 Dict (HasNoBigMap ('TMap n1 (AsRPC n2))))
-> Dict (HasNoBigMap (AsRPC n2))
-> Dict (HasNoBigMap ('TMap n1 (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (HasNoBigMap (AsRPC n2))
forall (t :: T). Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' Sing n2
sv
  STBigMap {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STInt {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STNat {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STString {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBytes {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STMutez {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBool {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STKeyHash {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381Fr {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381G1 {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381G2 {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STTimestamp {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STAddress {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STNever {} -> Dict (HasNoBigMap (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict

-- | A proof that @AsRPC (Value t)@ does not contain big_maps.
rpcHasNoNestedBigMapsEvi
  :: forall (t :: T).
     SingI t
  => Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi :: Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi = Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (t :: T). Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' (SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t)

rpcHasNoNestedBigMapsEvi' :: Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' :: Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' = \case
  Sing t
STKey -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STUnit {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STSignature {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChainId {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChest {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChestKey {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STOption s -> HasNoNestedBigMaps (AsRPC n) =>
Dict (HasNoNestedBigMaps ('TOption (AsRPC n)))
forall (a :: Constraint). a => Dict a
Dict (HasNoNestedBigMaps (AsRPC n) =>
 Dict (HasNoNestedBigMaps ('TOption (AsRPC n))))
-> Dict (HasNoNestedBigMaps (AsRPC n))
-> Dict (HasNoNestedBigMaps ('TOption (AsRPC n)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (HasNoNestedBigMaps (AsRPC n))
forall (t :: T). Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' Sing n
s
  STList s -> HasNoNestedBigMaps (AsRPC n) =>
Dict (HasNoNestedBigMaps ('TList (AsRPC n)))
forall (a :: Constraint). a => Dict a
Dict (HasNoNestedBigMaps (AsRPC n) =>
 Dict (HasNoNestedBigMaps ('TList (AsRPC n))))
-> Dict (HasNoNestedBigMaps (AsRPC n))
-> Dict (HasNoNestedBigMaps ('TList (AsRPC n)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (HasNoNestedBigMaps (AsRPC n))
forall (t :: T). Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' Sing n
s
  STSet s -> HasNoNestedBigMaps (AsRPC n) => Dict (HasNoNestedBigMaps ('TSet n))
forall (a :: Constraint). a => Dict a
Dict (HasNoNestedBigMaps (AsRPC n) =>
 Dict (HasNoNestedBigMaps ('TSet n)))
-> Dict (HasNoNestedBigMaps (AsRPC n))
-> Dict (HasNoNestedBigMaps ('TSet n))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (HasNoNestedBigMaps (AsRPC n))
forall (t :: T). Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' Sing n
s
  STOperation {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STContract {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STTicket {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STPair sa sb ->
    HasNoNestedBigMaps (AsRPC n1) =>
Dict (HasNoNestedBigMaps ('TPair (AsRPC n1) (AsRPC n2)))
forall (a :: Constraint). a => Dict a
Dict (HasNoNestedBigMaps (AsRPC n1) =>
 Dict (HasNoNestedBigMaps ('TPair (AsRPC n1) (AsRPC n2))))
-> Dict (HasNoNestedBigMaps (AsRPC n1))
-> Dict (HasNoNestedBigMaps ('TPair (AsRPC n1) (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (HasNoNestedBigMaps (AsRPC n1))
forall (t :: T). Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' Sing n1
sa (HasNoNestedBigMaps (AsRPC n2) =>
 Dict (HasNoNestedBigMaps ('TPair (AsRPC n1) (AsRPC n2))))
-> Dict (HasNoNestedBigMaps (AsRPC n2))
-> Dict (HasNoNestedBigMaps ('TPair (AsRPC n1) (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (HasNoNestedBigMaps (AsRPC n2))
forall (t :: T). Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' Sing n2
sb
  STOr sl sr ->
    HasNoNestedBigMaps (AsRPC n1) =>
Dict (HasNoNestedBigMaps ('TOr (AsRPC n1) (AsRPC n2)))
forall (a :: Constraint). a => Dict a
Dict (HasNoNestedBigMaps (AsRPC n1) =>
 Dict (HasNoNestedBigMaps ('TOr (AsRPC n1) (AsRPC n2))))
-> Dict (HasNoNestedBigMaps (AsRPC n1))
-> Dict (HasNoNestedBigMaps ('TOr (AsRPC n1) (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (HasNoNestedBigMaps (AsRPC n1))
forall (t :: T). Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' Sing n1
sl (HasNoNestedBigMaps (AsRPC n2) =>
 Dict (HasNoNestedBigMaps ('TOr (AsRPC n1) (AsRPC n2))))
-> Dict (HasNoNestedBigMaps (AsRPC n2))
-> Dict (HasNoNestedBigMaps ('TOr (AsRPC n1) (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (HasNoNestedBigMaps (AsRPC n2))
forall (t :: T). Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' Sing n2
sr
  STLambda {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STMap sk sv ->
    HasNoNestedBigMaps (AsRPC n1) =>
Dict (HasNoNestedBigMaps ('TMap n1 (AsRPC n2)))
forall (a :: Constraint). a => Dict a
Dict (HasNoNestedBigMaps (AsRPC n1) =>
 Dict (HasNoNestedBigMaps ('TMap n1 (AsRPC n2))))
-> Dict (HasNoNestedBigMaps (AsRPC n1))
-> Dict (HasNoNestedBigMaps ('TMap n1 (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (HasNoNestedBigMaps (AsRPC n1))
forall (t :: T). Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' Sing n1
sk (HasNoNestedBigMaps (AsRPC n2) =>
 Dict (HasNoNestedBigMaps ('TMap n1 (AsRPC n2))))
-> Dict (HasNoNestedBigMaps (AsRPC n2))
-> Dict (HasNoNestedBigMaps ('TMap n1 (AsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (HasNoNestedBigMaps (AsRPC n2))
forall (t :: T). Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' Sing n2
sv
  STBigMap {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STInt {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STNat {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STString {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBytes {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STMutez {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBool {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STKeyHash {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381Fr {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381G1 {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381G2 {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STTimestamp {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STAddress {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STNever {} -> Dict (HasNoNestedBigMaps (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict

-- | A proof that if @t@ does not contain any contract values, then neither does @AsRPC t@.
rpcHasNoContractEvi
  :: forall (t :: T).
     (SingI t, HasNoContract t)
  => HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi :: HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi = Sing t -> HasNoContract t :- HasNoContract (AsRPC t)
forall (t :: T).
HasNoContract t =>
Sing t -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' Sing t
forall k (a :: k). SingI a => Sing a
sing

rpcHasNoContractEvi'
  :: HasNoContract t
  => Sing t
  -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' :: Sing t -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' Sing t
sng = (HasNoContract t => Dict (HasNoContract (AsRPC t)))
-> HasNoContract t :- HasNoContract (AsRPC t)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((HasNoContract t => Dict (HasNoContract (AsRPC t)))
 -> HasNoContract t :- HasNoContract (AsRPC t))
-> (HasNoContract t => Dict (HasNoContract (AsRPC t)))
-> HasNoContract t :- HasNoContract (AsRPC t)
forall a b. (a -> b) -> a -> b
$ case Sing t
sng of
  Sing t
STKey -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STUnit {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STSignature {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChainId {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChest {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChestKey {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STOption s -> HasNoContract (AsRPC n) => Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoContract (AsRPC n) => Dict (HasNoContract (AsRPC t)))
-> (HasNoContract n :- HasNoContract (AsRPC n))
-> Dict (HasNoContract (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> HasNoContract n :- HasNoContract (AsRPC n)
forall (t :: T).
HasNoContract t =>
Sing t -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' Sing n
s
  STList s -> HasNoContract (AsRPC n) => Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoContract (AsRPC n) => Dict (HasNoContract (AsRPC t)))
-> (HasNoContract n :- HasNoContract (AsRPC n))
-> Dict (HasNoContract (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> HasNoContract n :- HasNoContract (AsRPC n)
forall (t :: T).
HasNoContract t =>
Sing t -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' Sing n
s
  STSet _ -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STOperation {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STTicket {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STPair sa sb -> case Sing n1 -> ContractPresence n1
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n1
sa of
    ContractPresence n1
ContractAbsent ->
      HasNoContract (AsRPC n1) => Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoContract (AsRPC n1) => Dict (HasNoContract (AsRPC t)))
-> (HasNoContract n1 :- HasNoContract (AsRPC n1))
-> Dict (HasNoContract (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> HasNoContract n1 :- HasNoContract (AsRPC n1)
forall (t :: T).
HasNoContract t =>
Sing t -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' Sing n1
sa (HasNoContract (AsRPC n2) => Dict (HasNoContract (AsRPC t)))
-> (HasNoContract n2 :- HasNoContract (AsRPC n2))
-> Dict (HasNoContract (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> HasNoContract n2 :- HasNoContract (AsRPC n2)
forall (t :: T).
HasNoContract t =>
Sing t -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' Sing n2
sb
  STOr sl sr -> case Sing n1 -> ContractPresence n1
forall (ty :: T). Sing ty -> ContractPresence ty
checkContractTypePresence Sing n1
sl of
    ContractPresence n1
ContractAbsent ->
      HasNoContract (AsRPC n1) => Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoContract (AsRPC n1) => Dict (HasNoContract (AsRPC t)))
-> (HasNoContract n1 :- HasNoContract (AsRPC n1))
-> Dict (HasNoContract (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> HasNoContract n1 :- HasNoContract (AsRPC n1)
forall (t :: T).
HasNoContract t =>
Sing t -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' Sing n1
sl (HasNoContract (AsRPC n2) => Dict (HasNoContract (AsRPC t)))
-> (HasNoContract n2 :- HasNoContract (AsRPC n2))
-> Dict (HasNoContract (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> HasNoContract n2 :- HasNoContract (AsRPC n2)
forall (t :: T).
HasNoContract t =>
Sing t -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' Sing n2
sr
  STLambda {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STMap _ sv -> HasNoContract (AsRPC n2) => Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict (HasNoContract (AsRPC n2) => Dict (HasNoContract (AsRPC t)))
-> (HasNoContract n2 :- HasNoContract (AsRPC n2))
-> Dict (HasNoContract (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> HasNoContract n2 :- HasNoContract (AsRPC n2)
forall (t :: T).
HasNoContract t =>
Sing t -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' Sing n2
sv
  STBigMap {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STInt {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STNat {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STString {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBytes {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STMutez {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBool {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STKeyHash {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381Fr {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381G1 {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381G2 {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STTimestamp {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STAddress {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STNever {} -> Dict (HasNoContract (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict

-- | A proof that if @t@ is a valid storage type, then so is @AsRPC t@.
rpcStorageScopeEvi :: forall (t :: T). StorageScope t :- StorageScope (AsRPC t)
rpcStorageScopeEvi :: StorageScope t :- StorageScope (AsRPC t)
rpcStorageScopeEvi =
  (StorageScope t => Dict (StorageScope (AsRPC t)))
-> StorageScope t :- StorageScope (AsRPC t)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((StorageScope t => Dict (StorageScope (AsRPC t)))
 -> StorageScope t :- StorageScope (AsRPC t))
-> (StorageScope t => Dict (StorageScope (AsRPC t)))
-> StorageScope t :- StorageScope (AsRPC t)
forall a b. (a -> b) -> a -> b
$ SingI (AsRPC t) => Dict (StorageScope (AsRPC t))
forall (a :: Constraint). a => Dict a
Dict
    (SingI (AsRPC t) => Dict (StorageScope (AsRPC t)))
-> (SingI t :- SingI (AsRPC t)) -> Dict (StorageScope (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI t :- SingI (AsRPC t)
forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi @t
    (HasNoOp (AsRPC t) => Dict (StorageScope (AsRPC t)))
-> (HasNoOp t :- HasNoOp (AsRPC t))
-> Dict (StorageScope (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, HasNoOp t) => HasNoOp t :- HasNoOp (AsRPC t)
forall (t :: T).
(SingI t, HasNoOp t) =>
HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi @t
    (HasNoNestedBigMaps (AsRPC t) => Dict (StorageScope (AsRPC t)))
-> Dict (HasNoNestedBigMaps (AsRPC t))
-> Dict (StorageScope (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingI t => Dict (HasNoNestedBigMaps (AsRPC t))
forall (t :: T). SingI t => Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi @t
    (HasNoContract (AsRPC t) => Dict (StorageScope (AsRPC t)))
-> (HasNoContract t :- HasNoContract (AsRPC t))
-> Dict (StorageScope (AsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (SingI t, HasNoContract t) =>
HasNoContract t :- HasNoContract (AsRPC t)
forall (t :: T).
(SingI t, HasNoContract t) =>
HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi @t