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

-- | 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.AsRPC
  ( TAsRPC
  , HasRPCRepr(..)
  , deriveRPCWithOptions
  , DeriveRPCOptions(..)
  , deriveRPC
  -- * Conversions
  , valueAsRPC
  , replaceBigMapIds
  , notesAsRPC
  -- * Entailments
  , rpcSingIEvi
  , rpcHasNoOpEvi
  , rpcHasNoBigMapEvi
  , rpcHasNoNestedBigMapsEvi
  , rpcHasNoContractEvi
  , rpcStorageScopeEvi
  ) where

import Prelude hiding (Type)
import Prelude qualified

import Control.Lens.Plated (universe)
import Data.Constraint ((\\))
import Data.Default (Default(..))
import Data.Generics (everything, everywhere, mkQ, mkT)
import Data.List qualified as List ((\\))
import Data.Map qualified as Map
import Data.Singletons (Sing, withSingI)
import Data.Text qualified as T
import Data.Type.Equality ((:~:)(Refl))
import GHC.Generics qualified as G
import Language.Haskell.TH
  (Con(InfixC, NormalC, RecC), Cxt, Dec(DataD, NewtypeD, TySynD, TySynInstD), Info(TyConI), Kind,
  Loc(loc_module), Name, Q, TyLit(StrTyLit), TySynEqn(..), TyVarBndr(..), Type(..), conT, cxt,
  instanceD, location, lookupTypeName, mkName, nameBase, normalB, ppr, reify, reifyInstances, valD,
  varE, varP)
import Language.Haskell.TH qualified as TH
import Language.Haskell.TH.ReifyMany (reifyManyTyCons)
import Language.Haskell.TH.ReifyMany.Internal (decConcreteNames, unAppsT, unSigT)

import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed
import Morley.Tezos.Address (Address)
import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
import Morley.Tezos.Crypto
import Morley.Util.CustomGeneric
  (GenericStrategy, customGeneric', deriveFullType, haskellBalanced,
  mangleGenericStrategyConstructors, mangleGenericStrategyFields, reifyDataType)
import Morley.Util.Interpolate (itu)
import Morley.Util.Named hiding (Name)
import Morley.Util.StubbedProof (stubProof)
import Morley.Util.TH (isTypeAlias, lookupTypeNameOrFail)

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

{- $setup
>>> import Morley.Michelson.Typed
>>> import Morley.Michelson.Text (MText)
>>> import Data.Default (def)
>>> :{
-- mock definitions for doctests, mirroring those in Lorentz.
data FollowEntrypointFlag = FollowEntrypoint | NotFollowEntrypoint
class HasAnnotation a where
  getAnnotation :: FollowEntrypointFlag -> Notes (ToT a)
  annOptions :: ()
:}
-}


----------------------------------------------------------------------------
-- TAsRPC
----------------------------------------------------------------------------

{- | A type-level function that maps a Michelson type to its Tezos RPC representation.

For example, when we retrieve a contract's storage using the Tezos RPC,
all its @big_map@s will be replaced by @nat@, representing a big_map ID.

>>> :k! TAsRPC ('TBigMap 'TInt 'TString)
...
= 'TNat

>>> :k! TAsRPC ('TList ('TBigMap 'TInt 'TString))
...
= 'TList 'TNat

>>> :k! TAsRPC ('TPair 'TString ('TPair 'TAddress ('TBigMap 'TInt 'TString)))
...
= 'TPair 'TString ('TPair 'TAddress 'TNat)


NB: As far as we are aware, details of RPC representation of Michelson
types are not documented. We know empirically that @big_map@s are
represented as their ids, and are the only type with an explicitly
different representation.

Whether @TAsRPC@ needs to propagate into type parameters then depends on
whether a value can hold big_map values.

* Values of type @option a@, @list a@, @pair a b@, and @or a b@ can
  contain big_map values, so their RPC representations are @option (TAsRPC a)@,
  @list (TAsRPC a)@, @pair (TAsRPC a) (TAsRPC b)@ and @or (TAsRPC a) (TAsRPC b)@.
* The keys of a @map k v@ cannot be big_maps, but the values can, so its
  RPC representation is @map k (TAsRPC v)@.
* Values of type @set a@ cannot contain big_maps, so its RPC
  representation is just @set a@.
* Values of type @contract a@ cannot contain big_maps either, because
  it's just a wrapper for an address and an entrypoint name, so its RPC
  representation is just @contract a@. The same reasoning applies to
  @ticket a@ and @lambda a b@.

-}
type TAsRPC :: T -> T
type family TAsRPC t where
  TAsRPC 'TKey = 'TKey
  TAsRPC 'TUnit = 'TUnit
  TAsRPC 'TSignature = 'TSignature
  TAsRPC 'TChainId = 'TChainId
  TAsRPC ('TOption t) = 'TOption (TAsRPC t)
  TAsRPC ('TList t) = 'TList (TAsRPC t)
  TAsRPC ('TSet t) = 'TSet t
  TAsRPC 'TOperation = 'TOperation
  TAsRPC ('TContract t) = 'TContract t
  TAsRPC ('TTicket t) = 'TTicket t
  TAsRPC ('TPair t1 t2) = 'TPair (TAsRPC t1) (TAsRPC t2)
  TAsRPC ('TOr t1 t2) = 'TOr (TAsRPC t1) (TAsRPC t2)
  TAsRPC ('TLambda t1 t2) = 'TLambda t1 t2
  TAsRPC ('TMap k v) = 'TMap k (TAsRPC v)
  TAsRPC ('TBigMap _ _) = 'TNat
  TAsRPC 'TInt = 'TInt
  TAsRPC 'TNat = 'TNat
  TAsRPC 'TString = 'TString
  TAsRPC 'TBytes = 'TBytes
  TAsRPC 'TMutez = 'TMutez
  TAsRPC 'TBool = 'TBool
  TAsRPC 'TKeyHash = 'TKeyHash
  TAsRPC 'TTimestamp = 'TTimestamp
  TAsRPC 'TAddress = 'TAddress
  TAsRPC 'TNever = 'TNever
  TAsRPC 'TBls12381Fr = 'TBls12381Fr
  TAsRPC 'TBls12381G1 = 'TBls12381G1
  TAsRPC 'TBls12381G2 = 'TBls12381G2
  TAsRPC 'TChest = 'TChest
  TAsRPC 'TChestKey = 'TChestKey
  TAsRPC ('TSaplingState n) = ('TSaplingState n)
  TAsRPC ('TSaplingTransaction n) = ('TSaplingTransaction n)

----------------------------------------------------------------------------
-- 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 must hold:

> TAsRPC (ToT t) ~ ToT (AsRPC t)

In other words, `ToT` and `AsRPC`/`TAsRPC` must be commutative.

@
   Storage ----------(applying ToT)-------------> ToT Storage
      |                                                |
      |                                                |
      |                                                |
(applying AsRPC)                                (applying TAsRPC)
      |                                                |
      |                                                |
      |                                                |
      |                                                V
      |                                        TAsRPC (ToT Storage)
      V                                                ~
AsRPC Storage ------(applying ToT)-----------> ToT (AsRPC Storage)
@


This law ensures that we can go from some type @Storage@ to @AsRPC Storage@ by
composing @fromVal . valueAsRPC . toVal@.

@
   Storage ------------(toVal)--------------> Value (ToT Storage)
      |                                                |
      |                                                |
      |                                                |
(fromVal . valueAsRPC . toVal)                    (valueAsRPC)
      |                                                |
      |                                                |
      |                                                |
      |                                                V
      |                                   Value (TAsRPC (ToT Storage))
      V                                                ~
AsRPC Storage <--------(fromVal)--------- Value (ToT (AsRPC Storage))
@

-}
class (TAsRPC (ToT t) ~ ToT (AsRPC t)) => HasRPCRepr (t :: Prelude.Type) where
  type AsRPC t :: Prelude.Type

-- 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)@
instance HasRPCRepr (BigMap k v) where type AsRPC (BigMap k v) = BigMapId k v
instance HasRPCRepr (Value t) where type AsRPC (Value t) = Value (TAsRPC t)
instance HasRPCRepr Integer where type AsRPC Integer = Integer
instance HasRPCRepr Natural where type AsRPC Natural = Natural
instance HasRPCRepr MText where type AsRPC MText = MText
instance HasRPCRepr Bool where type AsRPC Bool = Bool
instance HasRPCRepr ByteString where type AsRPC ByteString = ByteString
instance HasRPCRepr Mutez where type AsRPC Mutez = Mutez
instance HasRPCRepr KeyHash where type AsRPC KeyHash = KeyHash
instance HasRPCRepr Timestamp where type AsRPC Timestamp = Timestamp
instance HasRPCRepr Address where type AsRPC Address = Address
instance HasRPCRepr EpAddress where type AsRPC EpAddress = EpAddress
instance HasRPCRepr PublicKey where type AsRPC PublicKey = PublicKey
instance HasRPCRepr Signature where type AsRPC Signature = Signature
instance HasRPCRepr ChainId where type AsRPC ChainId = ChainId
instance HasRPCRepr Bls12381Fr where type AsRPC Bls12381Fr = Bls12381Fr
instance HasRPCRepr Bls12381G1 where type AsRPC Bls12381G1 = Bls12381G1
instance HasRPCRepr Bls12381G2 where type AsRPC Bls12381G2 = Bls12381G2
instance HasRPCRepr () where type AsRPC () = ()
instance HasRPCRepr a => HasRPCRepr [a] where
  type AsRPC [a] = [AsRPC a]
instance HasRPCRepr a => HasRPCRepr (Maybe a) where
  type AsRPC (Maybe a) = Maybe (AsRPC a)
instance (HasRPCRepr l, HasRPCRepr r) => HasRPCRepr (Either l r) where
  type AsRPC (Either l r) = Either (AsRPC l) (AsRPC r)
instance (HasRPCRepr a, HasRPCRepr b) => HasRPCRepr (a, b) where
  type AsRPC (a, b) = (AsRPC a, AsRPC b)
instance HasRPCRepr (Set a) where
  type AsRPC (Set a) = Set a
instance HasRPCRepr v => HasRPCRepr (Map k v) where
  type AsRPC (Map k v) = Map k (AsRPC v)
instance HasRPCRepr Operation where
  type AsRPC Operation = Operation
instance HasRPCRepr a => HasRPCRepr (Identity a) where
  type AsRPC (Identity a) = Identity (AsRPC a)
instance HasRPCRepr a => HasRPCRepr (NamedF Identity a name) where
  type AsRPC (NamedF Identity a name) = NamedF Identity (AsRPC a) name
instance HasRPCRepr a => HasRPCRepr (NamedF Maybe a name) where
  type AsRPC (NamedF Maybe a name) = NamedF Maybe (AsRPC a) name
instance Each '[HasRPCRepr] '[a, b, c] => HasRPCRepr (a, b, c) where
  type AsRPC (a, b, c) = (AsRPC a, AsRPC b, AsRPC c)
instance Each '[HasRPCRepr] '[a, b, c, d] => HasRPCRepr (a, b, c, d) where
  type AsRPC (a, b, c, d) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d)
instance Each '[HasRPCRepr] '[a, b, c, d, e] => HasRPCRepr (a, b, c, d, e) where
  type AsRPC (a, b, c, d, e) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e)
instance Each '[HasRPCRepr] '[a, b, c, d, e, f] => HasRPCRepr (a, b, c, d, e, f) where
  type AsRPC (a, b, c, d, e, f) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e, AsRPC f)
instance Each '[HasRPCRepr] '[a, b, c, d, e, f, g] => HasRPCRepr (a, b, c, d, e, f, g) where
  type AsRPC (a, b, c, d, e, f, g) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e, AsRPC f, AsRPC g)
instance HasRPCRepr (ContractRef arg) where
  type AsRPC (ContractRef arg) = ContractRef arg
instance HasRPCRepr Chest where
  type AsRPC Chest = Chest
instance HasRPCRepr ChestKey where
  type AsRPC ChestKey = ChestKey

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

-- | 'deriveRPCWithOptions' using default 'DeriveRPCOptions'.
deriveRPC :: String -> Q [Dec]
deriveRPC :: String -> Q [Dec]
deriveRPC String
typeStr = String -> DeriveRPCOptions -> Q [Dec]
deriveRPCWithOptions String
typeStr DeriveRPCOptions
forall a. Default a => a
def

-- | Options for 'deriveRPCWithOptions'.
data DeriveRPCOptions = DeriveRPCOptions
  { DeriveRPCOptions -> Bool
droRecursive :: Bool
    -- ^ Recursively enumerate @data@, @newtype@ and @type@ declarations, and
    -- derives an RPC representation for each type that doesn't yet have one.
    -- @True@ by default.
  , DeriveRPCOptions -> [String]
droRecursiveSkipTypes :: [String]
    -- ^ List of types for which you _don't_ want an RPC representation to be
    -- derived. This is ignored if @droRecursive@ is @False@.
  , DeriveRPCOptions -> Bool
droHasAnnotation :: Bool
    -- ^ Derive @HasAnnotation@. The class and its methods must be in scope,
    -- otherwise a compilation error is raised. @True@ by default.
  , DeriveRPCOptions -> GenericStrategy
droStrategy :: GenericStrategy
    -- ^ Custom Generic deriving strategy. 'haskellBalanced' by default.
  }

instance Default DeriveRPCOptions where
  def :: DeriveRPCOptions
def = DeriveRPCOptions
    { droRecursive :: Bool
droRecursive = Bool
True
    , droRecursiveSkipTypes :: [String]
droRecursiveSkipTypes = []
    , droHasAnnotation :: Bool
droHasAnnotation = Bool
True
    , droStrategy :: GenericStrategy
droStrategy = GenericStrategy
haskellBalanced
    }

{- | Derive an RPC representation for a type, as well as instances for
'Generic', 'IsoValue', 'HasRPCRepr' and optionally @HasAnnotation@.

>>> :{
data ExampleStorage a b = ExampleStorage
  { esField1 :: Integer
  , esField2 :: [BigMap Integer MText]
  , esField3 :: a
  }
  deriving stock Generic
  deriving anyclass IsoValue
--
deriveRPC "ExampleStorage"
:}

Will generate:

>>> :i ExampleStorageRPC
...
data ExampleStorageRPC a b
  = ExampleStorageRPC {esField1RPC :: !(AsRPC Integer),
                       esField2RPC :: !(AsRPC [BigMap Integer MText]),
                       esField3RPC :: !(AsRPC a)}
...
instance forall a k (b :: k).
         IsoValue (AsRPC a) =>
         IsoValue (ExampleStorageRPC a b)
...
instance forall a k (b :: k). Generic (ExampleStorageRPC a b)
...

>>> :i HasRPCRepr
...
instance forall a k (b :: k).
         HasRPCRepr a =>
         HasRPCRepr (ExampleStorage a b)
...

>>> :i AsRPC
...
type instance forall k a (b :: k). AsRPC (ExampleStorage a b)
  = ExampleStorageRPC a b
...


When 'droHasAnnotation' is @True@ (the default), it will also generate a
@HasAnnotation@ (from @Lorentz@) instance like:

>>> :i HasAnnotation
...
instance forall a k (b :: k).
         With '[HasAnnotation, HasRPCRepr] (ExampleStorage a b) =>
         HasAnnotation (ExampleStorageRPC a b)
...

Note that if the type doesn't contain type variables or only contains phantom
type variables, 'HasRPCRepr' constraint is omitted, as it would be redundant.

@HasAnnotation@ and its methods must be in scope.

Void types will generate a type synonym instead, e.g.

>>> :{
data MyVoidType
  deriving stock Generic
  deriving anyclass IsoValue
--
deriveRPC "MyVoidType"
:}

will produce

>>> :i AsRPC
...
type instance AsRPC MyVoidType = MyVoidTypeRPC
...

>>> :i MyVoidTypeRPC
...
type MyVoidTypeRPC = MyVoidType
...

When 'droRecursive' is @True@, recursively enumerate @data@, @newtype@ and
@type@ declarations, and derive an RPC representation for each type that doesn't
yet have one. This will however silently skip over void types that do not have
an 'IsoValue' instance, which is usually what you want, but be mindful of this.

You can also pass in a list of types for which you _don't_ want an RPC
representation to be derived in 'droRecursiveSkipTypes'. You may need this if
you're using non-void types that don't have an 'IsoValue' instance as phantom
types somewhere. The algorithm isn't smart enough to figure out those don't need
RPC representation and will try to derive it anyway.

>>> :{
data B = B deriving (Generic, IsoValue)
data C = C deriving (Generic, IsoValue)
data D = D deriving (Generic, IsoValue)
data E a = E deriving (Generic, IsoValue)
--
instance HasRPCRepr D where type AsRPC D = ()
--
data A = A B (E C) D deriving (Generic, IsoValue)
deriveRPCWithOptions "A" def{droRecursive=True, droRecursiveSkipTypes=["C"]}
:}

In this example, this will generate an RPC representation for @A@ and @B@,

>>> :i ARPC
...
data ARPC = ...
...
>>> :i BRPC
...
data BRPC = ...
...

but not for @C@ (because we explicitly said we don't want one) or @D@ (because
it already has one).

>>> :i CRPC
...
... Not in scope: ...
...
>>> :i DRPC
...
... Not in scope: ...
...

When using with @droRecursive = False@, if some types do not have 'HasRPCRepr',
'IsoValue' or 'Generic' instances, but need to, an error will be raised:

>>> :{
data B = B deriving (Generic, IsoValue)
data A = A B deriving (Generic, IsoValue)
--
deriveRPCWithOptions "A" def{droRecursive = False}
:}
...
... error:
... Type ... must implement 'HasRPCRepr'.

>>> :{
data B = B deriving (Generic, IsoValue)
data A = A B deriving (Generic, IsoValue)
--
deriveRPCWithOptions "B" def{droRecursive = False}
deriveRPCWithOptions "A" def{droRecursive = False}
:}

>>> :i AsRPC
...
type instance AsRPC A = ARPC ...
type instance AsRPC B = BRPC ...
...

This check isn't very smart, so it might miss some corner cases.
-}
deriveRPCWithOptions :: String -> DeriveRPCOptions -> Q [Dec]
deriveRPCWithOptions :: String -> DeriveRPCOptions -> Q [Dec]
deriveRPCWithOptions String
typeStr opts :: DeriveRPCOptions
opts@DeriveRPCOptions{Bool
droRecursive :: DeriveRPCOptions -> Bool
droRecursive :: Bool
droRecursive}
  | Bool
droRecursive = String -> DeriveRPCOptions -> Q [Dec]
deriveManyRPCWithStrategy' String
typeStr DeriveRPCOptions
opts
  | Bool
otherwise = 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 a. String -> Q a
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 -> Bool -> DeriveRPCOptions -> Q [Dec]
deriveRPCWithStrategy' Name
typeName Bool
False DeriveRPCOptions
opts

deriveManyRPCWithStrategy' :: String -> DeriveRPCOptions -> Q [Dec]
deriveManyRPCWithStrategy' :: String -> DeriveRPCOptions -> Q [Dec]
deriveManyRPCWithStrategy' String
typeStr opts :: DeriveRPCOptions
opts@DeriveRPCOptions{[String]
droRecursiveSkipTypes :: DeriveRPCOptions -> [String]
droRecursiveSkipTypes :: [String]
droRecursiveSkipTypes} = 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse String -> Q Name
lookupTypeNameOrFail [String]
droRecursiveSkipTypes
  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 a. String -> Q a
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 -> Bool -> DeriveRPCOptions -> Q [Dec]
deriveRPCWithStrategy' Name
name (Name
name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
typeName) DeriveRPCOptions
opts
  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 a b. (a -> b) -> [a] -> [b]
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)])
-> [Name] -> ((Name, Dec) -> Q (Bool, [Name])) -> Q [(Name, Info)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Name, Dec) -> Q (Bool, [Name])) -> [Name] -> Q [(Name, Info)]
reifyManyTyCons [Name
typeName] \(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
hasRPCInstance Name
name)
          do (Bool, [Name]) -> Q (Bool, [Name])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
False, []) -- exclude, don't recurse further
          do (, Dec -> [Name]
decConcreteNames Dec
dec) (Bool -> (Bool, [Name]))
-> (Bool -> Bool) -> Bool -> (Bool, [Name])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
forall a. Boolean a => a -> a
not (Bool -> (Bool, [Name])) -> Q Bool -> Q (Bool, [Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Q Bool
isTypeAlias Name
name
            -- exclude type aliases, recurse further

    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 a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe Type
Nothing ->
          String -> Q Bool
forall a. String -> Q a
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. (PrettyShow a, Show a, IsString b) => a -> b
show Name
typeName
        Just Type
typ ->
          Bool -> Bool
forall a. Boolean a => a -> a
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
forall flag. Name -> Maybe Type -> [TyVarBndr flag] -> 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
forall flag. Name -> Maybe Type -> [TyVarBndr flag] -> 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
forall flag. Name -> Maybe Type -> [TyVarBndr flag] -> Q Type
deriveFullType Name
typeName Maybe Type
forall a. Maybe a
Nothing [TyVarBndr ()]
vars
        Info
_ -> Maybe Type -> Q (Maybe Type)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Type
forall a. Maybe a
Nothing

-- skipVoids is set to True when doing deriveManyRPC recursively, i.e. for types
-- not explicitly requested by the caller.
deriveRPCWithStrategy' :: Name -> Bool -> DeriveRPCOptions -> Q [Dec]
deriveRPCWithStrategy' :: Name -> Bool -> DeriveRPCOptions -> Q [Dec]
deriveRPCWithStrategy' Name
typeName Bool
skipVoids DeriveRPCOptions{Bool
[String]
GenericStrategy
droRecursive :: DeriveRPCOptions -> Bool
droRecursiveSkipTypes :: DeriveRPCOptions -> [String]
droHasAnnotation :: DeriveRPCOptions -> Bool
droStrategy :: DeriveRPCOptions -> GenericStrategy
droRecursive :: Bool
droRecursiveSkipTypes :: [String]
droHasAnnotation :: Bool
droStrategy :: GenericStrategy
..} = do
  (Name
_, [Type]
decCxt, Maybe Type
mKind, [TyVarBndr ()]
tyVars, [Con]
constructors) <- Name -> Q (Name, [Type], Maybe Type, [TyVarBndr ()], [Con])
reifyDataType Name
typeName

  Type
derivedType <- Name -> Maybe Type -> [TyVarBndr ()] -> Q Type
forall flag. Name -> Maybe Type -> [TyVarBndr flag] -> Q Type
deriveFullType Name
typeName Maybe Type
mKind [TyVarBndr ()]
tyVars
  let typeNameRPC :: Name
typeNameRPC = Name -> Name
convertName Name
typeName
  Type
derivedTypeRPC <- Name -> Maybe Type -> [TyVarBndr ()] -> Q Type
forall flag. Name -> Maybe Type -> [TyVarBndr flag] -> Q Type
deriveFullType Name
typeNameRPC Maybe Type
mKind [TyVarBndr ()]
tyVars

  if [Con] -> Bool
forall t. Container t => t -> Bool
null [Con]
constructors
  then Q Bool -> Q [Dec] -> Q [Dec] -> Q [Dec]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Bool
skipVoids Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&&) (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 ''IsoValue [Type
derivedType])
    -- if a void type doesn't have an IsoValue instance, it's likely used as a
    -- typelevel tag. Skip it. Otherwise, derive a trivial 'HasRPCRepr'
    -- instance.
    do [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    do [Q Dec] -> Q [Dec]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
        [ [Type] -> Type -> Type -> Q Dec
mkAsRPCInstance [] Type
derivedType Type
derivedTypeRPC
        , Dec -> Q Dec
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ Name -> [TyVarBndr ()] -> Type -> Dec
TySynD Name
typeNameRPC [] (Type -> Dec) -> Type -> Dec
forall a b. (a -> b) -> a -> b
$ Name -> Type
ConT Name
typeName
        ]
  else do
    [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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Con -> Q Con
convertConstructor [Con]
constructors
    [Type]
fieldTypes <- [Con] -> Q [Type]
getFieldTypes [Con]
constructors
    [Type] -> (Element [Type] -> Q ()) -> Q ()
forall t (m :: * -> *) b.
(Container t, Monad m) =>
t -> (Element t -> m b) -> m ()
forM_ [Type]
fieldTypes Type -> Q ()
Element [Type] -> Q ()
checkInstanceForFieldTy
    [Type]
fieldTypesRPC <- [Con] -> Q [Type]
getFieldTypes [Con]
constructorsRPC

    -- 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 -> [TyVarBndr ()] -> Type
forall a. String -> TySynEqn -> [TyVarBndr a] -> Type
convertRep String
currentModuleName TySynEqn
repInstance [TyVarBndr ()]
tyVars
    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

    -- Slightly modify the deriving strategy so that the field/constructor
    -- reordering function from original strategy acts on input field names in
    -- RPC type after stripping RPC suffix. Fix for #811
    let
      gs' :: GenericStrategy
gs' = (Text -> Text) -> GenericStrategy -> GenericStrategy
mangleGenericStrategyFields Text -> Text
dropRPCSuffix (GenericStrategy -> GenericStrategy)
-> GenericStrategy -> GenericStrategy
forall a b. (a -> b) -> a -> b
$
              (Text -> Text) -> GenericStrategy -> GenericStrategy
mangleGenericStrategyConstructors Text -> Text
dropRPCSuffix GenericStrategy
droStrategy

    [[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)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
      [ [Dec] -> Q [Dec]
forall a. a -> Q a
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]
OneItem [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
      , Dec -> [Dec]
OneItem [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
<$> [Type] -> Type -> Type -> Q Dec
mkAsRPCInstance [Type]
fieldTypes 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'
      , [Type] -> Type -> Type -> Q [Dec]
annotationInstance [Type]
fieldTypes Type
derivedType Type
derivedTypeRPC
      ]

  where
    checkInstanceForFieldTy :: Type -> Q ()
checkInstanceForFieldTy Type
fieldTy =
      Name -> [Type] -> Q [Dec]
reifyInstances ''HasRPCRepr [Type
fieldTy] Q [Dec] -> ([Dec] -> Q ()) -> Q ()
forall a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        [] | Bool
droRecursive -> Q ()
forall (f :: * -> *). Applicative f => f ()
pass
           | Bool
otherwise
           -> String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ String
"Type '" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Doc -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr Type
fieldTy) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"' must implement 'HasRPCRepr'."
        [TH.InstanceD Maybe Overlap
_ [Type]
cs (ConT Name
n' `AppT` Type
ty) [Dec]
_] | Name
n' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''HasRPCRepr -> do
          let tyMap :: Map Type Type
tyMap = [(Type, Type)] -> Map Type Type
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Type, Type)] -> Map Type Type)
-> [(Type, Type)] -> Map Type Type
forall a b. (a -> b) -> a -> b
$ ((Type, Type) -> Bool) -> [(Type, Type)] -> [(Type, Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Type, Type) -> Bool
forall {b}. (Type, b) -> Bool
isVarMapping ([(Type, Type)] -> [(Type, Type)])
-> [(Type, Type)] -> [(Type, Type)]
forall a b. (a -> b) -> a -> b
$
                [Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Type -> Type
unSigT (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> [Type]
unAppsT Type
ty) (Type -> Type
unSigT (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> [Type]
unAppsT Type
fieldTy)
              isVarMapping :: (Type, b) -> Bool
isVarMapping = \case
                (VarT{}, b
_) -> Bool
True
                (Type, b)
_ -> Bool
False
              instantiatedConstraints :: [Type]
instantiatedConstraints =
                (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map ((forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((Type -> Type) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT Type -> Type
substVar)) ([Type] -> [Type]) -> ([Type] -> [Type]) -> [Type] -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Element [Type] -> [Type]) -> [Type] -> [Type]
forall c b. Container c => (Element c -> [b]) -> c -> [b]
concatMap Type -> [Type]
Element [Type] -> [Type]
getHasRPCReprTys ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$
                  (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((Type -> Type) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT Type -> Type
unSigT) [Type]
cs
              getHasRPCReprTys :: Type -> [Type]
getHasRPCReprTys = \case
                ConT Name
n `AppT` Type
x | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''HasRPCRepr -> [Type
x]
                ConT Name
n `AppT` (Type
PromotedConsT `AppT` ConT Name
n2 `AppT` Type
PromotedNilT) `AppT` Type
xs
                  | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Each, Name
n2 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''HasRPCRepr -> ((Type -> Maybe (Type, Type)) -> Type -> [Type])
-> Type -> (Type -> Maybe (Type, Type)) -> [Type]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Type -> Maybe (Type, Type)) -> Type -> [Type]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr Type
xs \case
                      Type
PromotedNilT -> Maybe (Type, Type)
forall a. Maybe a
Nothing
                      Type
PromotedConsT `AppT` Type
x `AppT` Type
xs' -> (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (Type
x, Type
xs')
                      Type
_ -> Maybe (Type, Type)
forall a. Maybe a
Nothing
                Type
_ -> [] -- we could error here and above, but for safety we don't
              substVar :: Type -> Type
substVar = \case
                v :: Type
v@VarT{} | Just Type
s <- Type -> Map Type Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Type
v Map Type Type
tyMap -> Type
s
                Type
x -> Type
x
          [Type] -> (Element [Type] -> Q ()) -> Q ()
forall t (m :: * -> *) b.
(Container t, Monad m) =>
t -> (Element t -> m b) -> m ()
forM_ [Type]
instantiatedConstraints Type -> Q ()
Element [Type] -> Q ()
checkInstanceForFieldTy
        [Dec
d] -> String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ String
"Unexpected instance for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Doc -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr Type
fieldTy) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
": " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Doc -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Dec -> Doc
forall a. Ppr a => a -> Doc
ppr Dec
d)
        -- most likely fieldTy is a tyvar, if not, GHC will complain about
        -- duplicate instances anyway
        (Dec
_:Dec
_:[Dec]
_) -> Q ()
forall (f :: * -> *). Applicative f => f ()
pass

    -- 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"

    dropRPCSuffix :: Text -> Text
    dropRPCSuffix :: Text -> Text
dropRPCSuffix = Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe (Text -> Text
forall a. HasCallStack => Text -> a
error Text
"Unexpected field/constructor without RPC suffix") (Maybe Text -> Text) -> (Text -> Maybe Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> Maybe Text
T.stripSuffix Text
"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 a. a -> Q a
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 a. a -> Q a
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 b c a. (b -> c) -> (a, b) -> (a, c)
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 a. a -> Q a
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 b c a. (b -> c) -> (a, b) -> (a, c)
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 b c a. (b -> c) -> (a, b) -> (a, c)
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 a. String -> Q a
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. (PrettyShow 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
<> Doc -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Con -> Doc
forall a. Ppr a => a -> Doc
ppr 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 a. a -> Q a
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 a. a -> Q a
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 a. a -> Q a
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 a. String -> Q a
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. (PrettyShow 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
<> Doc -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Con -> Doc
forall a. Ppr a => a -> Doc
ppr 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 a. a -> Q a
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 a. a -> Q a
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 a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Newtype has only one constructor")
        Info
_ -> String -> Q Dec
forall a. String -> Q a
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. (PrettyShow 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
<> Doc -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Info -> Doc
forall a. Ppr a => a -> Doc
ppr 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 -> [TyVarBndr a] -> Type
    convertRep :: forall a. String -> TySynEqn -> [TyVarBndr a] -> Type
convertRep String
currentModuleName (TySynEqn Maybe [TyVarBndr ()]
_tyVars Type
lhs Type
rhs) [TyVarBndr a]
tvs = Type -> Type
go Type
rhs
      where
        varMap :: Map Name Name
varMap = [(Name, Name)] -> Map Name Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, Name)] -> Map Name Name)
-> [(Name, Name)] -> Map Name Name
forall a b. (a -> b) -> a -> b
$ [Name] -> [Name] -> [(Name, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
lhsTvs ([Name] -> [(Name, Name)]) -> [Name] -> [(Name, Name)]
forall a b. (a -> b) -> a -> b
$ [TyVarBndr a]
tvs [TyVarBndr a] -> (TyVarBndr a -> Name) -> [Name]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
          PlainTV Name
vName a
_ -> Name
vName
          KindedTV Name
vName a
_ Type
_ -> Name
vName
        lhsTvs :: [Name]
lhsTvs = ([Name] -> [Name] -> [Name]) -> GenericQ [Name] -> GenericQ [Name]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
(<>) ([Name]
forall a. Monoid a => a
mempty [Name] -> (Type -> [Name]) -> a -> [Name]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` ([Name] -> (Name -> [Name]) -> Maybe Name -> [Name]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Name]
forall a. Monoid a => a
mempty Name -> [Name]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Name -> [Name]) -> (Type -> Maybe Name) -> Type -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe Name
varTName)) Type
lhs
        varTName :: Type -> Maybe Name
varTName = \case
          VarT Name
v -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
v
          Type
_ -> Maybe Name
forall a. Maybe a
Nothing
        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 -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
replaceVars Type
fieldType)
          Type
x `AppT` Type
y -> Type -> Type
go Type
x Type -> Type -> Type
`AppT` Type -> Type
go Type
y
          Type
x -> Type -> Type
replaceVars Type
x
        replaceVars :: Type -> Type
replaceVars = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((Type -> Type) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT Type -> Type
doReplace)
        doReplace :: Type -> Type
doReplace = \case
          VarT Name
v -> Name -> Type
VarT (Name -> Type) -> Name -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Maybe Name -> Name
forall a. a -> Maybe a -> a
fromMaybe Name
v (Maybe Name -> Name) -> Maybe Name -> Name
forall a b. (a -> b) -> a -> b
$ Name -> Map Name Name -> Maybe Name
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
v Map Name Name
varMap
          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 a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        [TySynInstD TySynEqn
repInstance] -> TySynEqn -> Q TySynEqn
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TySynEqn
repInstance
        (Dec
_:[Dec]
_) -> String -> Q TySynEqn
forall a. String -> Q a
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. (PrettyShow 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 a. String -> Q a
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. (PrettyShow 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 (Bar a)@, generate an 'IsoValue' instance like:
    --
    -- > instance IsoValue (AsRPC (Bar 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]
OneItem [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
<$> Q [Type] -> Q Type -> [Q Dec] -> Q Dec
forall (m :: * -> *).
Quote m =>
m [Type] -> m Type -> [m Dec] -> m Dec
instanceD Q [Type]
constraints [t|IsoValue $(Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
tp)|] []
      where
        constraints :: Q Cxt
        constraints :: Q [Type]
constraints =
          [Q Type] -> Q [Type]
forall (m :: * -> *). Quote m => [m Type] -> m [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 $(Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
fieldType)|]

    -- Given the type @Foo a b = Foo (Bar a)@, generate an 'HasRPCRepr' instance like:
    --
    -- > instance HasRPCRepr (Bar a) => HasRPCRepr (Foo a b) where
    -- >   type AsRPC (Foo a b) = FooRPC a b
    --
    -- Note that if a type variable @t@ is a phantom type variable, then no @HasRPCRepr@
    -- constraint is generated for it.
    mkAsRPCInstance :: [Type] -> Type -> Type -> Q Dec
    mkAsRPCInstance :: [Type] -> Type -> Type -> Q Dec
mkAsRPCInstance [Type]
fieldTypes Type
tp Type
tpRPC = do
      [Dec]
typeInstance <- [d|type instance AsRPC $(Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
tp) = $(Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
tpRPC)|]
      Q [Type] -> Q Type -> [Q Dec] -> Q Dec
forall (m :: * -> *).
Quote m =>
m [Type] -> m Type -> [m Dec] -> m Dec
instanceD Q [Type]
constraints [t|HasRPCRepr $(Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
tp)|]
        (Dec -> Q Dec
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> [Dec] -> [Q Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dec]
typeInstance)
      where
        constraints :: Q Cxt
        constraints :: Q [Type]
constraints =
          [Q Type] -> Q [Type]
forall (m :: * -> *). Quote m => [m Type] -> m [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|HasRPCRepr $(Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
fieldType)|]

    -- When @HasAnnotation@ and its methods are in scope, given the type @ty@
    -- where @AsRPC ty = tyRPC@, generate a @HasAnnotation@ instance like:
    --
    -- > instance With [HasAnnotation, HasRPCRepr] ty => HasAnnotation tyRPC where
    -- >   getAnnotation = notesAsRPC . getAnnotation @ty
    -- >   annOptions = annOptions @ty
    --
    -- Note that if @ty@ doesn't contain type variables or only contains phantom
    -- type variables, 'HasRPCRepr' constraint is omitted, as it would be
    -- redundant.
    --
    -- Will fail if @HasAnnotation@ or its methods are not in scope.
    annotationInstance :: [Type] -> Type -> Type -> Q [Dec]
    annotationInstance :: [Type] -> Type -> Type -> Q [Dec]
annotationInstance [Type]
_ Type
_ Type
_ | Bool -> Bool
forall a. Boolean a => a -> a
not Bool
droHasAnnotation = [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    annotationInstance [Type]
fields (Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure -> Q Type
ty) (Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure -> Q Type
tyRPC) = Dec -> [Dec]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> [Dec]) -> Q Dec -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      let noHasAnnError :: Text -> Q b
          noHasAnnError :: forall b. Text -> Q b
noHasAnnError Text
reason =
            -- NB: weird indentation is due to how GHC formats multiline TH
            -- errors (it doesn't)
            String -> Q b
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail [itu|
              #{reason}
                  Did you mean to derive 'HasAnnotation' instances? If not, use:
                      deriveRPCWithOptions "#{tyBase}" def{droHasAnnotation=False}
              |]
            where tyBase :: String
tyBase = Name -> String
nameBase Name
typeName
      Name
hasAnnNm <- Q Name -> (Name -> Q Name) -> Maybe Name -> Q Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Text -> Q Name
forall b. Text -> Q b
noHasAnnError Text
"'HasAnnotation' is not in scope.") Name -> Q Name
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Name -> Q Name) -> Q (Maybe Name) -> Q Name
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        String -> Q (Maybe Name)
lookupTypeName String
"HasAnnotation"
      [Name]
methodNames <- Name -> Q Info
reify Name
hasAnnNm Q Info -> (Info -> Q [Name]) -> Q [Name]
forall a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        TH.ClassI (TH.ClassD [Type]
_ Name
_ [TyVarBndr ()]
_ [FunDep]
_ [Dec]
decs) [Dec]
_ ->
          [Name] -> Q [Name]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Name] -> Q [Name]) -> [Name] -> Q [Name]
forall a b. (a -> b) -> a -> b
$ ((Dec -> Maybe Name) -> [Dec] -> [Name])
-> [Dec] -> (Dec -> Maybe Name) -> [Name]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Dec -> Maybe Name) -> [Dec] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [Dec]
decs \case
            TH.SigD Name
name Type
_ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name
            Dec
_ -> Maybe Name
forall a. Maybe a
Nothing
        Info
x -> Text -> Q [Name]
forall b. Text -> Q b
noHasAnnError (Text -> Q [Name]) -> Text -> Q [Name]
forall a b. (a -> b) -> a -> b
$
          Text
"Expected 'HasAnnotation' to be a class, but instead found " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Doc -> Text
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Info -> Doc
forall a. Ppr a => a -> Doc
ppr Info
x)
      Name
getAnnNm <- (Element [Name] -> Bool) -> [Name] -> Maybe (Element [Name])
forall t.
Container t =>
(Element t -> Bool) -> t -> Maybe (Element t)
find (\Element [Name]
nm -> Name -> String
nameBase Name
Element [Name]
nm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"getAnnotation") [Name]
methodNames Maybe Name -> (Maybe Name -> Q Name) -> Q Name
forall a b. a -> (a -> b) -> b
&
        Q Name -> (Name -> Q Name) -> Maybe Name -> Q Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Text -> Q Name
forall b. Text -> Q b
noHasAnnError Text
"Did not find 'getAnnotation' method on 'HasAnnotation'") Name -> Q Name
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      Name
annOptNm <- (Element [Name] -> Bool) -> [Name] -> Maybe (Element [Name])
forall t.
Container t =>
(Element t -> Bool) -> t -> Maybe (Element t)
find (\Element [Name]
nm -> Name -> String
nameBase Name
Element [Name]
nm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"annOptions") [Name]
methodNames Maybe Name -> (Maybe Name -> Q Name) -> Q Name
forall a b. a -> (a -> b) -> b
&
        Q Name -> (Name -> Q Name) -> Maybe Name -> Q Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Text -> Q Name
forall b. Text -> Q b
noHasAnnError Text
"Did not find 'annOptions' method on 'HasAnnotation'") Name -> Q Name
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      let hasAnn :: Q Type
hasAnn = Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
conT Name
hasAnnNm
          constraints :: [Q Type]
constraints
            | (Element [Type] -> Bool) -> [Type] -> Bool
forall c b.
(Container c, BooleanMonoid b) =>
(Element c -> b) -> c -> b
any Type -> Bool
Element [Type] -> Bool
hasTyVar [Type]
fields = [[t| With '[$Q Type
hasAnn, HasRPCRepr] $Q Type
ty |]]
            | Bool
otherwise = [[t| $Q Type
hasAnn $Q Type
ty |]]
      Q [Type] -> Q Type -> [Q Dec] -> Q Dec
forall (m :: * -> *).
Quote m =>
m [Type] -> m Type -> [m Dec] -> m Dec
instanceD ([Q Type] -> Q [Type]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Q Type]
constraints) [t|$Q Type
hasAnn $Q Type
tyRPC|]
          [ Q Pat -> Q Body -> [Q Dec] -> Q Dec
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Dec
valD (Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
varP Name
getAnnNm) (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
normalB [|notesAsRPC . $(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
varE Name
getAnnNm) @($Q Type
ty)|]) []
          , Q Pat -> Q Body -> [Q Dec] -> Q Dec
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Dec
valD (Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
varP Name
annOptNm) (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
normalB [|$(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
varE Name
annOptNm) @($Q Type
ty)|]) []
          ]

    -- Checks if the given type has any type variables.
    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
(Element [Type] -> Bool) -> [Type] -> Bool
forall c b.
(Container c, BooleanMonoid b) =>
(Element c -> b) -> c -> b
any (Type -> [Type]
forall a. Plated a => a -> [a]
universe Type
ty) \case
        VarT Name
_ -> Bool
True
        Type
_ -> Bool
False

----------------------------------------------------------------------------
-- 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 (TAsRPC t)
valueAsRPC :: forall (t :: T). HasCallStack => Value t -> Value (TAsRPC t)
valueAsRPC Value t
v = case Value t
v of
  VKey {} -> Value t
Value (TAsRPC t)
v
  VUnit {} -> Value t
Value (TAsRPC t)
v
  VSignature {} -> Value t
Value (TAsRPC t)
v
  VChainId {} -> Value t
Value (TAsRPC t)
v
  VChest {} -> Value t
Value (TAsRPC t)
v
  VChestKey {} -> Value t
Value (TAsRPC t)
v
  VOption (Maybe (Value t1)
vMaybe :: Maybe (Value elem)) ->
    Maybe (Value' Instr (TAsRPC t1))
-> Value' Instr ('TOption (TAsRPC t1))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Value t1 -> Value' Instr (TAsRPC t1)
forall (t :: T). HasCallStack => Value t -> Value (TAsRPC t)
valueAsRPC (Value t1 -> Value' Instr (TAsRPC t1))
-> Maybe (Value t1) -> Maybe (Value' Instr (TAsRPC t1))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Value t1)
vMaybe) (SingI (TAsRPC t1) => Value' Instr ('TOption (TAsRPC t1)))
-> Dict (SingI (TAsRPC t1)) -> Value' Instr ('TOption (TAsRPC t1))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T). SingI t => Dict (SingI (TAsRPC t))
rpcSingIEvi @elem
  VList ([Value t1]
vList :: [Value elem]) ->
    [Value' Instr (TAsRPC t1)] -> Value' Instr ('TList (TAsRPC t1))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList (Value t1 -> Value' Instr (TAsRPC t1)
forall (t :: T). HasCallStack => Value t -> Value (TAsRPC t)
valueAsRPC (Value t1 -> Value' Instr (TAsRPC t1))
-> [Value t1] -> [Value' Instr (TAsRPC t1)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Value t1]
vList) (SingI (TAsRPC t1) => Value' Instr ('TList (TAsRPC t1)))
-> Dict (SingI (TAsRPC t1)) -> Value' Instr ('TList (TAsRPC t1))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T). SingI t => Dict (SingI (TAsRPC t))
rpcSingIEvi @elem
  VSet {} -> Value t
Value (TAsRPC t)
v
  VOp {} -> Value t
Value (TAsRPC t)
v
  VContract {} -> Value t
Value (TAsRPC t)
v
  VTicket {} -> Value t
Value (TAsRPC t)
v
  VPair (Value' Instr l
x, Value' Instr r
y) -> (Value' Instr (TAsRPC l), Value' Instr (TAsRPC r))
-> Value' Instr ('TPair (TAsRPC l) (TAsRPC 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 (TAsRPC l)
forall (t :: T). HasCallStack => Value t -> Value (TAsRPC t)
valueAsRPC Value' Instr l
x, Value' Instr r -> Value' Instr (TAsRPC r)
forall (t :: T). HasCallStack => Value t -> Value (TAsRPC t)
valueAsRPC Value' Instr r
y)
  VOr (Either (Value l) (Value r)
vEither :: Either (Value l) (Value r)) ->
    Either (Value' Instr (TAsRPC l)) (Value' Instr (TAsRPC r))
-> Value ('TOr (TAsRPC l) (TAsRPC 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 l -> Value' Instr (TAsRPC l))
-> (Value r -> Value' Instr (TAsRPC r))
-> Either (Value l) (Value r)
-> Either (Value' Instr (TAsRPC l)) (Value' Instr (TAsRPC r))
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Value l -> Value' Instr (TAsRPC l)
forall (t :: T). HasCallStack => Value t -> Value (TAsRPC t)
valueAsRPC Value r -> Value' Instr (TAsRPC r)
forall (t :: T). HasCallStack => Value t -> Value (TAsRPC t)
valueAsRPC Either (Value l) (Value r)
vEither) (SingI (TAsRPC l) => Value ('TOr (TAsRPC l) (TAsRPC r)))
-> Dict (SingI (TAsRPC l)) -> Value ('TOr (TAsRPC l) (TAsRPC r))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T). SingI t => Dict (SingI (TAsRPC t))
rpcSingIEvi @l (SingI (TAsRPC r) => Value ('TOr (TAsRPC l) (TAsRPC r)))
-> Dict (SingI (TAsRPC r)) -> Value ('TOr (TAsRPC l) (TAsRPC r))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T). SingI t => Dict (SingI (TAsRPC t))
rpcSingIEvi @r
  VLam {} -> Value t
Value (TAsRPC t)
v
  VMap (Map (Value k) (Value v)
vMap :: Map (Value k) (Value v)) ->
    Map (Value k) (Value' Instr (TAsRPC v))
-> Value' Instr ('TMap k (TAsRPC v))
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap (Value v -> Value' Instr (TAsRPC v)
forall (t :: T). HasCallStack => Value t -> Value (TAsRPC t)
valueAsRPC (Value v -> Value' Instr (TAsRPC v))
-> Map (Value k) (Value v)
-> Map (Value k) (Value' Instr (TAsRPC v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Value k) (Value v)
vMap) (SingI (TAsRPC v) => Value' Instr ('TMap k (TAsRPC v)))
-> Dict (SingI (TAsRPC v)) -> Value' Instr ('TMap k (TAsRPC v))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T). SingI t => Dict (SingI (TAsRPC t))
rpcSingIEvi @v
  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 (TAsRPC t)
forall a. HasCallStack => Text -> a
error (Text -> Value (TAsRPC t)) -> Text -> Value (TAsRPC t)
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 (TAsRPC t)
v
  VNat {} -> Value t
Value (TAsRPC t)
v
  VString {} -> Value t
Value (TAsRPC t)
v
  VBytes {} -> Value t
Value (TAsRPC t)
v
  VMutez {} -> Value t
Value (TAsRPC t)
v
  VBool {} -> Value t
Value (TAsRPC t)
v
  VKeyHash {} -> Value t
Value (TAsRPC t)
v
  VTimestamp {} -> Value t
Value (TAsRPC t)
v
  VAddress {} -> Value t
Value (TAsRPC t)
v
  VBls12381Fr {} -> Value t
Value (TAsRPC t)
v
  VBls12381G1 {} -> Value t
Value (TAsRPC t)
v
  VBls12381G2 {} -> Value t
Value (TAsRPC t)
v

-- | Replaces all bigmap IDs with their corresponding bigmap values.
-- This is the inverse of `valueAsRPC`.
replaceBigMapIds
  :: forall t m. Monad m
  => (forall k v. (SingI k, SingI v) => Natural -> m (Value ('TBigMap k v)))
  -- ^ A function for looking up a bigmap using its ID.
  -> Sing t -> Value (TAsRPC t) -> m (Value t)
replaceBigMapIds :: forall (t :: T) (m :: * -> *).
Monad m =>
(forall (k :: T) (v :: T).
 (SingI k, SingI v) =>
 Natural -> m (Value ('TBigMap k v)))
-> Sing t -> Value (TAsRPC t) -> m (Value t)
replaceBigMapIds forall (k :: T) (v :: T).
(SingI k, SingI v) =>
Natural -> m (Value ('TBigMap k v))
findBigMapById = Sing t -> Value (TAsRPC t) -> m (Value t)
forall (t1 :: T). Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
go
  where
    go :: forall t1. Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
    go :: forall (t1 :: T). Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
go Sing t1
s !Value (TAsRPC t1)
v = case (Sing t1
SingT t1
s, Value (TAsRPC t1)
v) of
      (STKey {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STUnit {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STSignature {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STChainId {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STChest {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STChestKey {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STOption Sing n
sMaybe, VOption Maybe (Value' Instr t1)
vMaybe) ->
        Sing n -> (SingI n => m (Value t1)) -> m (Value t1)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sMaybe ((SingI n => m (Value t1)) -> m (Value t1))
-> (SingI n => m (Value t1)) -> m (Value t1)
forall a b. (a -> b) -> a -> b
$
          Maybe (Value' Instr n) -> Value t1
Maybe (Value' Instr n) -> Value' Instr ('TOption n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value' Instr n) -> Value t1)
-> m (Maybe (Value' Instr n)) -> m (Value t1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value' Instr t1 -> m (Value' Instr n))
-> Maybe (Value' Instr t1) -> m (Maybe (Value' Instr n))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (Sing n -> Value (TAsRPC n) -> m (Value' Instr n)
forall (t1 :: T). Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
go Sing n
sMaybe) Maybe (Value' Instr t1)
vMaybe
      (STList Sing n
sList, VList [Value' Instr t1]
vList) ->
        Sing n -> (SingI n => m (Value t1)) -> m (Value t1)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sList ((SingI n => m (Value t1)) -> m (Value t1))
-> (SingI n => m (Value t1)) -> m (Value t1)
forall a b. (a -> b) -> a -> b
$
          [Value' Instr n] -> Value t1
[Value' Instr n] -> Value' Instr ('TList n)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList ([Value' Instr n] -> Value t1)
-> m [Value' Instr n] -> m (Value t1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value' Instr t1 -> m (Value' Instr n))
-> [Value' Instr t1] -> m [Value' Instr n]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Sing n -> Value (TAsRPC n) -> m (Value' Instr n)
forall (t1 :: T). Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
go Sing n
sList) [Value' Instr t1]
vList
      (STSet {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STOperation {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STContract {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STTicket {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STPair Sing n1
sa Sing n2
sb, VPair (Value' Instr l
a, Value' Instr r
b)) -> do
        Value n1
a' <- Sing n1 -> Value (TAsRPC n1) -> m (Value n1)
forall (t1 :: T). Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
go Sing n1
sa Value' Instr l
Value (TAsRPC n1)
a
        Value n2
b' <- Sing n2 -> Value (TAsRPC n2) -> m (Value n2)
forall (t1 :: T). Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
go Sing n2
sb Value' Instr r
Value (TAsRPC n2)
b
        pure $ (Value n1, Value n2) -> Value' Instr ('TPair n1 n2)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value n1
a', Value n2
b')
      (STOr Sing n1
sl Sing n2
sr, VOr Either (Value' Instr l) (Value' Instr r)
vEither) -> Sing n1 -> (SingI n1 => m (Value t1)) -> m (Value t1)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
sl ((SingI n1 => m (Value t1)) -> m (Value t1))
-> (SingI n1 => m (Value t1)) -> m (Value t1)
forall a b. (a -> b) -> a -> b
$ Sing n2 -> (SingI n2 => m (Value t1)) -> m (Value t1)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
sr ((SingI n2 => m (Value t1)) -> m (Value t1))
-> (SingI n2 => m (Value t1)) -> m (Value t1)
forall a b. (a -> b) -> a -> b
$
        case Either (Value' Instr l) (Value' Instr r)
vEither of
          Right Value' Instr r
r -> Either (Value' Instr n1) (Value' Instr n2) -> Value t1
Either (Value' Instr n1) (Value' Instr n2)
-> Value' Instr ('TOr n1 n2)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Either (Value' Instr n1) (Value' Instr n2) -> Value t1)
-> (Value' Instr n2 -> Either (Value' Instr n1) (Value' Instr n2))
-> Value' Instr n2
-> Value t1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr n2 -> Either (Value' Instr n1) (Value' Instr n2)
forall a b. b -> Either a b
Right (Value' Instr n2 -> Value t1)
-> m (Value' Instr n2) -> m (Value t1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing n2 -> Value (TAsRPC n2) -> m (Value' Instr n2)
forall (t1 :: T). Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
go Sing n2
sr Value' Instr r
Value (TAsRPC n2)
r
          Left Value' Instr l
l -> Either (Value' Instr n1) (Value' Instr n2) -> Value t1
Either (Value' Instr n1) (Value' Instr n2)
-> Value' Instr ('TOr n1 n2)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Either (Value' Instr n1) (Value' Instr n2) -> Value t1)
-> (Value' Instr n1 -> Either (Value' Instr n1) (Value' Instr n2))
-> Value' Instr n1
-> Value t1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr n1 -> Either (Value' Instr n1) (Value' Instr n2)
forall a b. a -> Either a b
Left (Value' Instr n1 -> Value t1)
-> m (Value' Instr n1) -> m (Value t1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing n1 -> Value (TAsRPC n1) -> m (Value' Instr n1)
forall (t1 :: T). Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
go Sing n1
sl Value' Instr l
Value (TAsRPC n1)
l
      (STLambda {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STMap Sing n1
_ Sing n2
sv, VMap Map (Value' Instr k) (Value' Instr v)
vList) ->
        Sing n2 -> (SingI n2 => m (Value t1)) -> m (Value t1)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
sv ((SingI n2 => m (Value t1)) -> m (Value t1))
-> (SingI n2 => m (Value t1)) -> m (Value t1)
forall a b. (a -> b) -> a -> b
$
          Map (Value' Instr k) (Value' Instr n2) -> Value t1
Map (Value' Instr k) (Value' Instr n2) -> Value' Instr ('TMap k n2)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap (Map (Value' Instr k) (Value' Instr n2) -> Value t1)
-> m (Map (Value' Instr k) (Value' Instr n2)) -> m (Value t1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value' Instr v -> m (Value' Instr n2))
-> Map (Value' Instr k) (Value' Instr v)
-> m (Map (Value' Instr k) (Value' Instr n2))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map (Value' Instr k) a -> f (Map (Value' Instr k) b)
traverse (Sing n2 -> Value (TAsRPC n2) -> m (Value' Instr n2)
forall (t1 :: T). Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
go Sing n2
sv) Map (Value' Instr k) (Value' Instr v)
vList
      (STBigMap Sing n1
sk Sing n2
sv, VNat Natural
bigMapId) -> Sing n1 -> (SingI n1 => m (Value t1)) -> m (Value t1)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
sk ((SingI n1 => m (Value t1)) -> m (Value t1))
-> (SingI n1 => m (Value t1)) -> m (Value t1)
forall a b. (a -> b) -> a -> b
$ Sing n2 -> (SingI n2 => m (Value t1)) -> m (Value t1)
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n2
sv ((SingI n2 => m (Value t1)) -> m (Value t1))
-> (SingI n2 => m (Value t1)) -> m (Value t1)
forall a b. (a -> b) -> a -> b
$ Natural -> m (Value ('TBigMap n1 n2))
forall (k :: T) (v :: T).
(SingI k, SingI v) =>
Natural -> m (Value ('TBigMap k v))
findBigMapById Natural
bigMapId
      (STInt {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STNat {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STString {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STBytes {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STMutez {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STBool {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STKeyHash {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STTimestamp {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STAddress {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STBls12381Fr {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STBls12381G1 {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v
      (STBls12381G2 {}, Value (TAsRPC t1)
_) -> Value t1 -> m (Value t1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value t1
Value (TAsRPC t1)
v

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

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

-- | A proof that if a singleton exists for @t@,
-- then so it does for @TAsRPC t@.
rpcSingIEvi :: forall t. SingI t => Dict (SingI (TAsRPC t))
rpcSingIEvi :: forall (t :: T). SingI t => Dict (SingI (TAsRPC t))
rpcSingIEvi = Sing (TAsRPC t)
-> (SingI (TAsRPC t) => Dict (SingI (TAsRPC t)))
-> Dict (SingI (TAsRPC t))
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI (Sing t -> Sing (TAsRPC t)
forall (t :: T). Sing t -> Sing (TAsRPC t)
rpcSing (Sing t -> Sing (TAsRPC t)) -> Sing t -> Sing (TAsRPC t)
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t) Dict (SingI (TAsRPC t))
SingI (TAsRPC t) => Dict (SingI (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict

rpcSing :: Sing t -> Sing (TAsRPC t)
rpcSing :: forall (t :: T). Sing t -> Sing (TAsRPC t)
rpcSing Sing t
st = case Sing t
st of
  Sing t
SingT t
STKey -> Sing t
Sing (TAsRPC t)
st
  STUnit {} -> Sing t
Sing (TAsRPC t)
st
  STSignature {} -> Sing t
Sing (TAsRPC t)
st
  STChainId {} -> Sing t
Sing (TAsRPC t)
st
  STChest {} -> Sing t
Sing (TAsRPC t)
st
  STChestKey {} -> Sing t
Sing (TAsRPC t)
st
  STOption Sing n
s -> Sing (TAsRPC n) -> SingT ('TOption (TAsRPC n))
forall (n :: T). Sing n -> SingT ('TOption n)
STOption (Sing (TAsRPC n) -> SingT ('TOption (TAsRPC n)))
-> Sing (TAsRPC n) -> SingT ('TOption (TAsRPC n))
forall a b. (a -> b) -> a -> b
$ Sing n -> Sing (TAsRPC n)
forall (t :: T). Sing t -> Sing (TAsRPC t)
rpcSing Sing n
s
  STList Sing n
s ->  Sing (TAsRPC n) -> SingT ('TList (TAsRPC n))
forall (n :: T). Sing n -> SingT ('TList n)
STList (Sing (TAsRPC n) -> SingT ('TList (TAsRPC n)))
-> Sing (TAsRPC n) -> SingT ('TList (TAsRPC n))
forall a b. (a -> b) -> a -> b
$ Sing n -> Sing (TAsRPC n)
forall (t :: T). Sing t -> Sing (TAsRPC t)
rpcSing Sing n
s
  STSet{} -> Sing t
Sing (TAsRPC t)
st
  STOperation {} -> Sing t
Sing (TAsRPC t)
st
  STContract {} -> Sing t
Sing (TAsRPC t)
st
  STTicket {} -> Sing t
Sing (TAsRPC t)
st
  STPair Sing n1
sa Sing n2
sb -> Sing (TAsRPC n1)
-> Sing (TAsRPC n2) -> SingT ('TPair (TAsRPC n1) (TAsRPC n2))
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TPair n1 n2)
STPair (Sing n1 -> Sing (TAsRPC n1)
forall (t :: T). Sing t -> Sing (TAsRPC t)
rpcSing Sing n1
sa) (Sing n2 -> Sing (TAsRPC n2)
forall (t :: T). Sing t -> Sing (TAsRPC t)
rpcSing Sing n2
sb)
  STOr Sing n1
sl Sing n2
sr -> Sing (TAsRPC n1)
-> Sing (TAsRPC n2) -> SingT ('TOr (TAsRPC n1) (TAsRPC n2))
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TOr n1 n2)
STOr (Sing n1 -> Sing (TAsRPC n1)
forall (t :: T). Sing t -> Sing (TAsRPC t)
rpcSing Sing n1
sl) (Sing n2 -> Sing (TAsRPC n2)
forall (t :: T). Sing t -> Sing (TAsRPC t)
rpcSing Sing n2
sr)
  STLambda {} -> Sing t
Sing (TAsRPC t)
st
  STMap Sing n1
sk Sing n2
sv -> Sing n1 -> Sing (TAsRPC n2) -> SingT ('TMap n1 (TAsRPC n2))
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TMap n1 n2)
STMap Sing n1
sk (Sing n2 -> Sing (TAsRPC n2)
forall (t :: T). Sing t -> Sing (TAsRPC t)
rpcSing Sing n2
sv)
  STBigMap {} -> Sing (TAsRPC t)
SingT 'TNat
STNat
  STInt {} -> Sing t
Sing (TAsRPC t)
st
  STNat {} -> Sing t
Sing (TAsRPC t)
st
  STString {} -> Sing t
Sing (TAsRPC t)
st
  STBytes {} -> Sing t
Sing (TAsRPC t)
st
  STMutez {} -> Sing t
Sing (TAsRPC t)
st
  STBool {} -> Sing t
Sing (TAsRPC t)
st
  STKeyHash {} -> Sing t
Sing (TAsRPC t)
st
  STBls12381Fr {} -> Sing t
Sing (TAsRPC t)
st
  STBls12381G1 {} -> Sing t
Sing (TAsRPC t)
st
  STBls12381G2 {} -> Sing t
Sing (TAsRPC t)
st
  STTimestamp {} -> Sing t
Sing (TAsRPC t)
st
  STAddress {} -> Sing t
Sing (TAsRPC t)
st
  STNever {} -> Sing t
Sing (TAsRPC t)
st
  STSaplingState Sing n
_ -> Sing t
Sing (TAsRPC t)
st
  STSaplingTransaction Sing n
_ -> Sing t
Sing (TAsRPC t)
st

-- | A proof that if @t@ is well-typed, then @TAsRPC t@ is also well-typed.
rpcWellTypedEvi :: forall t. WellTyped t => Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi :: forall (t :: T). WellTyped t => Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi = Sing t -> Dict (WellTyped (TAsRPC t))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' (Sing t -> Dict (WellTyped (TAsRPC t)))
-> Sing t -> Dict (WellTyped (TAsRPC t))
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t

rpcWellTypedEvi' :: WellTyped t => Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' :: forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing t
sng = case Sing t
sng of
  Sing t
SingT t
STKey -> Dict (WellTyped 'TKey)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STUnit {} -> Dict (WellTyped 'TUnit)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STSignature {} -> Dict (WellTyped 'TSignature)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChainId {} -> Dict (WellTyped 'TChainId)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STOption Sing n
s -> Dict (WellTyped ('TOption (TAsRPC n)))
WellTyped (TAsRPC n) => Dict (WellTyped ('TOption (TAsRPC n)))
forall (a :: Constraint). a => Dict a
Dict (WellTyped (TAsRPC n) => Dict (WellTyped ('TOption (TAsRPC n))))
-> Dict (WellTyped (TAsRPC n))
-> Dict (WellTyped ('TOption (TAsRPC n)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (WellTyped (TAsRPC n))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n
s
  STList Sing n
s -> Dict (WellTyped ('TList (TAsRPC n)))
WellTyped (TAsRPC n) => Dict (WellTyped ('TList (TAsRPC n)))
forall (a :: Constraint). a => Dict a
Dict (WellTyped (TAsRPC n) => Dict (WellTyped ('TList (TAsRPC n))))
-> Dict (WellTyped (TAsRPC n))
-> Dict (WellTyped ('TList (TAsRPC n)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (WellTyped (TAsRPC n))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n
s
  STSet Sing n
s -> Dict (WellTyped ('TSet n))
WellTyped (TAsRPC n) => Dict (WellTyped ('TSet n))
forall (a :: Constraint). a => Dict a
Dict (WellTyped (TAsRPC n) => Dict (WellTyped ('TSet n)))
-> Dict (WellTyped (TAsRPC n)) -> Dict (WellTyped ('TSet n))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (WellTyped (TAsRPC n))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n
s
  STOperation {} -> Dict (WellTyped 'TOperation)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STContract Sing n
s -> Dict (WellTyped ('TContract n))
WellTyped (TAsRPC n) => Dict (WellTyped ('TContract n))
forall (a :: Constraint). a => Dict a
Dict (WellTyped (TAsRPC n) => Dict (WellTyped ('TContract n)))
-> Dict (WellTyped (TAsRPC n)) -> Dict (WellTyped ('TContract n))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (WellTyped (TAsRPC n))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n
s
  STTicket Sing n
s -> Dict (WellTyped ('TTicket n))
WellTyped (TAsRPC n) => Dict (WellTyped ('TTicket n))
forall (a :: Constraint). a => Dict a
Dict (WellTyped (TAsRPC n) => Dict (WellTyped ('TTicket n)))
-> Dict (WellTyped (TAsRPC n)) -> Dict (WellTyped ('TTicket n))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> Dict (WellTyped (TAsRPC n))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n
s
  STPair Sing n1
sa Sing n2
sb -> Dict (WellTyped ('TPair (TAsRPC n1) (TAsRPC n2)))
WellTyped (TAsRPC n1) =>
Dict (WellTyped ('TPair (TAsRPC n1) (TAsRPC n2)))
forall (a :: Constraint). a => Dict a
Dict (WellTyped (TAsRPC n1) =>
 Dict (WellTyped ('TPair (TAsRPC n1) (TAsRPC n2))))
-> Dict (WellTyped (TAsRPC n1))
-> Dict (WellTyped ('TPair (TAsRPC n1) (TAsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (WellTyped (TAsRPC n1))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n1
sa (WellTyped (TAsRPC n2) =>
 Dict (WellTyped ('TPair (TAsRPC n1) (TAsRPC n2))))
-> Dict (WellTyped (TAsRPC n2))
-> Dict (WellTyped ('TPair (TAsRPC n1) (TAsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (WellTyped (TAsRPC n2))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n2
sb
  STOr Sing n1
sl Sing n2
sr -> Dict (WellTyped ('TOr (TAsRPC n1) (TAsRPC n2)))
WellTyped (TAsRPC n1) =>
Dict (WellTyped ('TOr (TAsRPC n1) (TAsRPC n2)))
forall (a :: Constraint). a => Dict a
Dict (WellTyped (TAsRPC n1) =>
 Dict (WellTyped ('TOr (TAsRPC n1) (TAsRPC n2))))
-> Dict (WellTyped (TAsRPC n1))
-> Dict (WellTyped ('TOr (TAsRPC n1) (TAsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (WellTyped (TAsRPC n1))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n1
sl (WellTyped (TAsRPC n2) =>
 Dict (WellTyped ('TOr (TAsRPC n1) (TAsRPC n2))))
-> Dict (WellTyped (TAsRPC n2))
-> Dict (WellTyped ('TOr (TAsRPC n1) (TAsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (WellTyped (TAsRPC n2))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n2
sr
  STLambda Sing n1
sa Sing n2
sb -> Dict (WellTyped ('TLambda n1 n2))
WellTyped (TAsRPC n1) => Dict (WellTyped ('TLambda n1 n2))
forall (a :: Constraint). a => Dict a
Dict (WellTyped (TAsRPC n1) => Dict (WellTyped ('TLambda n1 n2)))
-> Dict (WellTyped (TAsRPC n1))
-> Dict (WellTyped ('TLambda n1 n2))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (WellTyped (TAsRPC n1))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n1
sa (WellTyped (TAsRPC n2) => Dict (WellTyped ('TLambda n1 n2)))
-> Dict (WellTyped (TAsRPC n2))
-> Dict (WellTyped ('TLambda n1 n2))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (WellTyped (TAsRPC n2))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n2
sb
  STMap Sing n1
sk Sing n2
sv -> Dict (WellTyped ('TMap n1 (TAsRPC n2)))
WellTyped (TAsRPC n1) => Dict (WellTyped ('TMap n1 (TAsRPC n2)))
forall (a :: Constraint). a => Dict a
Dict (WellTyped (TAsRPC n1) => Dict (WellTyped ('TMap n1 (TAsRPC n2))))
-> Dict (WellTyped (TAsRPC n1))
-> Dict (WellTyped ('TMap n1 (TAsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (WellTyped (TAsRPC n1))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n1
sk (WellTyped (TAsRPC n2) => Dict (WellTyped ('TMap n1 (TAsRPC n2))))
-> Dict (WellTyped (TAsRPC n2))
-> Dict (WellTyped ('TMap n1 (TAsRPC n2)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (WellTyped (TAsRPC n2))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n2
sv
  STBigMap Sing n1
sk Sing n2
sv -> Dict (WellTyped 'TNat)
WellTyped (TAsRPC n1) => Dict (WellTyped 'TNat)
forall (a :: Constraint). a => Dict a
Dict (WellTyped (TAsRPC n1) => Dict (WellTyped 'TNat))
-> Dict (WellTyped (TAsRPC n1)) -> Dict (WellTyped 'TNat)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> Dict (WellTyped (TAsRPC n1))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n1
sk (WellTyped (TAsRPC n2) => Dict (WellTyped 'TNat))
-> Dict (WellTyped (TAsRPC n2)) -> Dict (WellTyped 'TNat)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> Dict (WellTyped (TAsRPC n2))
forall (t :: T).
WellTyped t =>
Sing t -> Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi' Sing n2
sv
  STInt {} -> Dict (WellTyped 'TInt)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STNat {} -> Dict (WellTyped 'TNat)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STString {} -> Dict (WellTyped 'TString)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBytes {} -> Dict (WellTyped 'TBytes)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STMutez {} -> Dict (WellTyped 'TMutez)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBool {} -> Dict (WellTyped 'TBool)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STKeyHash {} -> Dict (WellTyped 'TKeyHash)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381Fr {} -> Dict (WellTyped 'TBls12381Fr)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381G1 {} -> Dict (WellTyped 'TBls12381G1)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STBls12381G2 {} -> Dict (WellTyped 'TBls12381G2)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STTimestamp {} -> Dict (WellTyped 'TTimestamp)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STAddress {} -> Dict (WellTyped 'TAddress)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChest {} -> Dict (WellTyped 'TChest)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STChestKey {} -> Dict (WellTyped 'TChestKey)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STNever {} -> Dict (WellTyped 'TNever)
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STSaplingState Sing n
_ -> Dict (WellTyped ('TSaplingState n))
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  STSaplingTransaction Sing n
_ -> Dict (WellTyped ('TSaplingTransaction n))
Dict (WellTyped (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict

-- | A proof that if @t@ does not contain any operations, then neither does @TAsRPC t@.
rpcHasNoOpEvi :: forall (t :: T). (SingI t, ForbidOp t) => Dict (ForbidOp (TAsRPC t))
rpcHasNoOpEvi :: forall (t :: T).
(SingI t, ForbidOp t) =>
Dict (ForbidOp (TAsRPC t))
rpcHasNoOpEvi = Dict (ForbidOp (TAsRPC t))
(ContainsT 'PSOp (TAsRPC t) ~ 'False) => Dict (ForbidOp (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict ((ContainsT 'PSOp (TAsRPC t) ~ 'False) =>
 Dict (ForbidOp (TAsRPC t)))
-> (ContainsT 'PSOp (TAsRPC t) :~: 'False)
-> Dict (ForbidOp (TAsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T) (p :: TPredicateSym).
(SingI t, ContainsT p t ~ 'False) =>
Sing p -> ContainsT p (TAsRPC t) :~: 'False
rpcHasNoTEvi @t Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp

-- | A proof that @AsRPC (Value t)@ does not contain big_maps.
rpcHasNoBigMapEvi :: forall (t :: T). (SingI t, ForbidBigMap t) => Dict (ForbidBigMap (TAsRPC t))
rpcHasNoBigMapEvi :: forall (t :: T).
(SingI t, ForbidBigMap t) =>
Dict (ForbidBigMap (TAsRPC t))
rpcHasNoBigMapEvi = Dict (ForbidBigMap (TAsRPC t))
(ContainsT 'PSBigMap (TAsRPC t) ~ 'False) =>
Dict (ForbidBigMap (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict ((ContainsT 'PSBigMap (TAsRPC t) ~ 'False) =>
 Dict (ForbidBigMap (TAsRPC t)))
-> (ContainsT 'PSBigMap (TAsRPC t) :~: 'False)
-> Dict (ForbidBigMap (TAsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T) (p :: TPredicateSym).
(SingI t, ContainsT p t ~ 'False) =>
Sing p -> ContainsT p (TAsRPC t) :~: 'False
rpcHasNoTEvi @t Sing 'PSBigMap
SingTPredicateSym 'PSBigMap
SPSBigMap

-- | A proof that @AsRPC (Value t)@ does not contain nested big_maps.
rpcHasNoNestedBigMapsEvi
  :: forall (t :: T). (SingI t, ForbidNestedBigMaps t) => Dict (ForbidNestedBigMaps (TAsRPC t))
rpcHasNoNestedBigMapsEvi :: forall (t :: T).
(SingI t, ForbidNestedBigMaps t) =>
Dict (ForbidNestedBigMaps (TAsRPC t))
rpcHasNoNestedBigMapsEvi = Dict (ForbidNestedBigMaps (TAsRPC t))
(ContainsT 'PSNestedBigMaps (TAsRPC t) ~ 'False) =>
Dict (ForbidNestedBigMaps (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict ((ContainsT 'PSNestedBigMaps (TAsRPC t) ~ 'False) =>
 Dict (ForbidNestedBigMaps (TAsRPC t)))
-> (ContainsT 'PSNestedBigMaps (TAsRPC t) :~: 'False)
-> Dict (ForbidNestedBigMaps (TAsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T) (p :: TPredicateSym).
(SingI t, ContainsT p t ~ 'False) =>
Sing p -> ContainsT p (TAsRPC t) :~: 'False
rpcHasNoTEvi @t Sing 'PSNestedBigMaps
SingTPredicateSym 'PSNestedBigMaps
SPSNestedBigMaps

-- | A proof that @AsRPC (Value t)@ does not contain some type defined by a predicate.
rpcHasNoTEvi
  :: forall (t :: T) p.
     (SingI t, ContainsT p t ~ 'False)
  => Sing p -> (ContainsT p (TAsRPC t) :~: 'False)
rpcHasNoTEvi :: forall (t :: T) (p :: TPredicateSym).
(SingI t, ContainsT p t ~ 'False) =>
Sing p -> ContainsT p (TAsRPC t) :~: 'False
rpcHasNoTEvi Sing p
sp = Sing p -> Sing t -> ContainsT p (TAsRPC t) :~: 'False
forall (t :: T) (p :: TPredicateSym).
(ContainsT p t ~ 'False) =>
Sing p -> Sing t -> ContainsT p (TAsRPC t) :~: 'False
rpcHasNoTEvi' Sing p
sp (forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t)

rpcHasNoTEvi'
  :: forall t p. (ContainsT p t ~ 'False)
  => Sing p -> Sing t -> ContainsT p (TAsRPC t) :~: 'False
rpcHasNoTEvi' :: forall (t :: T) (p :: TPredicateSym).
(ContainsT p t ~ 'False) =>
Sing p -> Sing t -> ContainsT p (TAsRPC t) :~: 'False
rpcHasNoTEvi' Sing p
ps Sing t
ts = (Stubbed => ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case Sing t
ts of
  Sing t
SingT t
STKey -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STUnit {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STSignature {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STChainId {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STChest {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STChestKey {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STOption Sing n
s -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT p (TAsRPC n) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT p (TAsRPC n) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT p (TAsRPC n) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> ContainsT p (TAsRPC n) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n
s
  STList Sing n
s -> case Sing p
ps of
    Sing p
SingTPredicateSym p
SPSOp -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSOp (TAsRPC n) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSOp (TAsRPC n) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSOp (TAsRPC n) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> ContainsT p (TAsRPC n) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n
s
    Sing p
SingTPredicateSym p
SPSContract -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSContract (TAsRPC n) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSContract (TAsRPC n) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSContract (TAsRPC n) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> ContainsT p (TAsRPC n) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n
s
    Sing p
SingTPredicateSym p
SPSTicket -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSTicket (TAsRPC n) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSTicket (TAsRPC n) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSTicket (TAsRPC n) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> ContainsT p (TAsRPC n) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n
s
    Sing p
SingTPredicateSym p
SPSBigMap -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSBigMap (TAsRPC n) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSBigMap (TAsRPC n) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSBigMap (TAsRPC n) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> ContainsT p (TAsRPC n) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n
s
    Sing p
SingTPredicateSym p
SPSNestedBigMaps -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSNestedBigMaps (TAsRPC n) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSNestedBigMaps (TAsRPC n) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSNestedBigMaps (TAsRPC n) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> ContainsT p (TAsRPC n) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n
s
    Sing p
SingTPredicateSym p
SPSSaplingState -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSSaplingState (TAsRPC n) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSSaplingState (TAsRPC n) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSSaplingState (TAsRPC n) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n -> ContainsT p (TAsRPC n) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n
s
  STSet Sing n
_ -> case Sing p
ps of
    Sing p
SingTPredicateSym p
SPSOp -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSContract -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSTicket -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSBigMap -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSNestedBigMaps -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSSaplingState -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STOperation {} -> case Sing p
ps of
    Sing p
SingTPredicateSym p
SPSContract -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSTicket -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSBigMap -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSNestedBigMaps -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSSaplingState -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STContract {} -> case Sing p
ps of
    Sing p
SingTPredicateSym p
SPSOp -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSTicket -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSBigMap -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSNestedBigMaps -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSSaplingState -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STTicket Sing n
_ -> case Sing p
ps of
    Sing p
SingTPredicateSym p
SPSOp -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSContract -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSBigMap -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSNestedBigMaps -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSSaplingState -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STPair Sing n1
sa Sing n2
sb -> Sing p
-> Sing n1
-> Sing n2
-> ((ForbidT p n1, ForbidT p n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing p
ps Sing n1
sa Sing n2
sb (((ForbidT p n1, ForbidT p n2) =>
  ContainsT p (TAsRPC t) :~: 'False)
 -> ContainsT p (TAsRPC t) :~: 'False)
-> ((ForbidT p n1, ForbidT p n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall a b. (a -> b) -> a -> b
$ ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT p (TAsRPC n1) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT p (TAsRPC n1) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT p (TAsRPC n1) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> ContainsT p (TAsRPC n1) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n1
sa ((ContainsT p (TAsRPC n2) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT p (TAsRPC n2) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT p (TAsRPC n2) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n2
sb
  STOr Sing n1
sl Sing n2
sr -> Sing p
-> Sing n1
-> Sing n2
-> ((ForbidT p n1, ForbidT p n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing p
ps Sing n1
sl Sing n2
sr (((ForbidT p n1, ForbidT p n2) =>
  ContainsT p (TAsRPC t) :~: 'False)
 -> ContainsT p (TAsRPC t) :~: 'False)
-> ((ForbidT p n1, ForbidT p n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall a b. (a -> b) -> a -> b
$ ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT p (TAsRPC n1) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT p (TAsRPC n1) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT p (TAsRPC n1) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n1 -> ContainsT p (TAsRPC n1) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n1
sl ((ContainsT p (TAsRPC n2) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT p (TAsRPC n2) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT p (TAsRPC n2) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n2
sr
  STLambda {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STMap Sing n1
sk Sing n2
sv -> case Sing p
ps of
    Sing p
SingTPredicateSym p
SPSOp -> Sing 'PSOp
-> Sing n1
-> Sing n2
-> ((ForbidT 'PSOp n1, ForbidT 'PSOp n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing p
Sing 'PSOp
ps Sing n1
sk Sing n2
sv (((ForbidT 'PSOp n1, ForbidT 'PSOp n2) =>
  ContainsT p (TAsRPC t) :~: 'False)
 -> ContainsT p (TAsRPC t) :~: 'False)
-> ((ForbidT 'PSOp n1, ForbidT 'PSOp n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall a b. (a -> b) -> a -> b
$ ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSOp (TAsRPC n2) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSOp (TAsRPC n2) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSOp (TAsRPC n2) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT p (TAsRPC n2) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n2
sv
    Sing p
SingTPredicateSym p
SPSContract -> Sing 'PSContract
-> Sing n1
-> Sing n2
-> ((ForbidT 'PSContract n1, ForbidT 'PSContract n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing p
Sing 'PSContract
ps Sing n1
sk Sing n2
sv (((ForbidT 'PSContract n1, ForbidT 'PSContract n2) =>
  ContainsT p (TAsRPC t) :~: 'False)
 -> ContainsT p (TAsRPC t) :~: 'False)
-> ((ForbidT 'PSContract n1, ForbidT 'PSContract n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall a b. (a -> b) -> a -> b
$ ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSContract (TAsRPC n2) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSContract (TAsRPC n2) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSContract (TAsRPC n2) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT p (TAsRPC n2) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n2
sv
    Sing p
SingTPredicateSym p
SPSTicket -> Sing 'PSTicket
-> Sing n1
-> Sing n2
-> ((ForbidT 'PSTicket n1, ForbidT 'PSTicket n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing p
Sing 'PSTicket
ps Sing n1
sk Sing n2
sv (((ForbidT 'PSTicket n1, ForbidT 'PSTicket n2) =>
  ContainsT p (TAsRPC t) :~: 'False)
 -> ContainsT p (TAsRPC t) :~: 'False)
-> ((ForbidT 'PSTicket n1, ForbidT 'PSTicket n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall a b. (a -> b) -> a -> b
$ ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSTicket (TAsRPC n2) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSTicket (TAsRPC n2) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSTicket (TAsRPC n2) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT p (TAsRPC n2) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n2
sv
    Sing p
SingTPredicateSym p
SPSBigMap -> Sing 'PSBigMap
-> Sing n1
-> Sing n2
-> ((ForbidT 'PSBigMap n1, ForbidT 'PSBigMap n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing p
Sing 'PSBigMap
ps Sing n1
sk Sing n2
sv (((ForbidT 'PSBigMap n1, ForbidT 'PSBigMap n2) =>
  ContainsT p (TAsRPC t) :~: 'False)
 -> ContainsT p (TAsRPC t) :~: 'False)
-> ((ForbidT 'PSBigMap n1, ForbidT 'PSBigMap n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall a b. (a -> b) -> a -> b
$ ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSBigMap (TAsRPC n2) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSBigMap (TAsRPC n2) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSBigMap (TAsRPC n2) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT p (TAsRPC n2) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n2
sv
    Sing p
SingTPredicateSym p
SPSNestedBigMaps -> Sing 'PSNestedBigMaps
-> Sing n1
-> Sing n2
-> ((ForbidT 'PSNestedBigMaps n1, ForbidT 'PSNestedBigMaps n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing p
Sing 'PSNestedBigMaps
ps Sing n1
sk Sing n2
sv (((ForbidT 'PSNestedBigMaps n1, ForbidT 'PSNestedBigMaps n2) =>
  ContainsT p (TAsRPC t) :~: 'False)
 -> ContainsT p (TAsRPC t) :~: 'False)
-> ((ForbidT 'PSNestedBigMaps n1, ForbidT 'PSNestedBigMaps n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall a b. (a -> b) -> a -> b
$ ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSNestedBigMaps (TAsRPC n2) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSNestedBigMaps (TAsRPC n2) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSNestedBigMaps (TAsRPC n2) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT p (TAsRPC n2) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n2
sv
    Sing p
SingTPredicateSym p
SPSSaplingState -> Sing 'PSSaplingState
-> Sing n1
-> Sing n2
-> ((ForbidT 'PSSaplingState n1, ForbidT 'PSSaplingState n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing p
Sing 'PSSaplingState
ps Sing n1
sk Sing n2
sv (((ForbidT 'PSSaplingState n1, ForbidT 'PSSaplingState n2) =>
  ContainsT p (TAsRPC t) :~: 'False)
 -> ContainsT p (TAsRPC t) :~: 'False)
-> ((ForbidT 'PSSaplingState n1, ForbidT 'PSSaplingState n2) =>
    ContainsT p (TAsRPC t) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall a b. (a -> b) -> a -> b
$ ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
(ContainsT 'PSSaplingState (TAsRPC n2) ~ 'False) =>
ContainsT p (TAsRPC t) :~: 'False
forall {k} (a :: k). a :~: a
Refl ((ContainsT 'PSSaplingState (TAsRPC n2) ~ 'False) =>
 ContainsT p (TAsRPC t) :~: 'False)
-> (ContainsT 'PSSaplingState (TAsRPC n2) :~: 'False)
-> ContainsT p (TAsRPC t) :~: 'False
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing n2 -> ContainsT p (TAsRPC n2) :~: 'False
forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go Sing n2
sv
  STBigMap {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STInt {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STNat {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STString {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STBytes {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STMutez {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STBool {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STKeyHash {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STBls12381Fr {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STBls12381G1 {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STBls12381G2 {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STTimestamp {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STAddress {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STNever {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STSaplingState {} -> case Sing p
ps of
    Sing p
SingTPredicateSym p
SPSOp -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSTicket -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSContract -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSBigMap -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
    Sing p
SingTPredicateSym p
SPSNestedBigMaps -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  STSaplingTransaction {} -> ContainsT p (TAsRPC t) :~: 'False
ContainsT p (TAsRPC t) :~: ContainsT p (TAsRPC t)
forall {k} (a :: k). a :~: a
Refl
  where
    go :: (ContainsT p t' ~ 'False) => Sing t' -> ContainsT p (TAsRPC t') :~: 'False
    go :: forall (t' :: T).
(ContainsT p t' ~ 'False) =>
Sing t' -> ContainsT p (TAsRPC t') :~: 'False
go = Sing p -> Sing t' -> ContainsT p (TAsRPC t') :~: 'False
forall (t :: T) (p :: TPredicateSym).
(ContainsT p t ~ 'False) =>
Sing p -> Sing t -> ContainsT p (TAsRPC t) :~: 'False
rpcHasNoTEvi' Sing p
ps

-- | A proof that if @t@ does not contain any contract values, then neither does @TAsRPC t@.
rpcHasNoContractEvi
  :: forall (t :: T). (SingI t, ForbidContract t) => Dict (ForbidContract (TAsRPC t))
rpcHasNoContractEvi :: forall (t :: T).
(SingI t, ForbidContract t) =>
Dict (ForbidContract (TAsRPC t))
rpcHasNoContractEvi = Dict (ForbidContract (TAsRPC t))
(ContainsT 'PSContract (TAsRPC t) ~ 'False) =>
Dict (ForbidContract (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict ((ContainsT 'PSContract (TAsRPC t) ~ 'False) =>
 Dict (ForbidContract (TAsRPC t)))
-> (ContainsT 'PSContract (TAsRPC t) :~: 'False)
-> Dict (ForbidContract (TAsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T) (p :: TPredicateSym).
(SingI t, ContainsT p t ~ 'False) =>
Sing p -> ContainsT p (TAsRPC t) :~: 'False
rpcHasNoTEvi @t Sing 'PSContract
SingTPredicateSym 'PSContract
SPSContract

-- | A proof that if @t@ is a valid storage type, then so is @TAsRPC t@.
rpcStorageScopeEvi :: forall (t :: T). StorageScope t => Dict (StorageScope (TAsRPC t))
rpcStorageScopeEvi :: forall (t :: T). StorageScope t => Dict (StorageScope (TAsRPC t))
rpcStorageScopeEvi = Dict (StorageScope (TAsRPC t))
SingI (TAsRPC t) => Dict (StorageScope (TAsRPC t))
forall (a :: Constraint). a => Dict a
Dict
  (SingI (TAsRPC t) => Dict (StorageScope (TAsRPC t)))
-> Dict (SingI (TAsRPC t)) -> Dict (StorageScope (TAsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T). SingI t => Dict (SingI (TAsRPC t))
rpcSingIEvi @t
  (ForbidT 'PSOp (TAsRPC t) => Dict (StorageScope (TAsRPC t)))
-> Dict (ForbidT 'PSOp (TAsRPC t))
-> Dict (StorageScope (TAsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T).
(SingI t, ForbidOp t) =>
Dict (ForbidOp (TAsRPC t))
rpcHasNoOpEvi @t
  (ForbidT 'PSNestedBigMaps (TAsRPC t) =>
 Dict (StorageScope (TAsRPC t)))
-> Dict (ForbidT 'PSNestedBigMaps (TAsRPC t))
-> Dict (StorageScope (TAsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T).
(SingI t, ForbidNestedBigMaps t) =>
Dict (ForbidNestedBigMaps (TAsRPC t))
rpcHasNoNestedBigMapsEvi @t
  (ForbidT 'PSContract (TAsRPC t) => Dict (StorageScope (TAsRPC t)))
-> Dict (ForbidT 'PSContract (TAsRPC t))
-> Dict (StorageScope (TAsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T).
(SingI t, ForbidContract t) =>
Dict (ForbidContract (TAsRPC t))
rpcHasNoContractEvi @t
  (WellTyped (TAsRPC t) => Dict (StorageScope (TAsRPC t)))
-> Dict (WellTyped (TAsRPC t)) -> Dict (StorageScope (TAsRPC t))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (t :: T). WellTyped t => Dict (WellTyped (TAsRPC t))
rpcWellTypedEvi @t