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

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Conversions between haskell types/values and Michelson ones.
module Morley.Michelson.Typed.Haskell.Value
  ( -- * Value conversions
    IsoValue (..)
  , isoValue
  , KnownIsoT
  , GIsoValue (GValueType)
  , ToT'
  , GenericIsoValue
  , WellTypedToT
  , HasNoOpToT

  , Dict(..) -- * Re-exporting to use in tests.

    -- * Missing Haskell analogies to Michelson values
  , EntrypointCall
  , SomeEntrypointCall
  , ContractRef (..)
  , coerceContractRef
  , contractRefToAddr
  , Ticket (..)
  , BigMapId(..)
  , BigMap(..)
  , ToBigMap(..)

    -- * Stack conversion
  , ToTs
  , ToTs'
  , IsoValuesStack (..)
  , totsKnownLemma
  , totsAppendLemma
  ) where
import Control.Lens (At(..), Index, Iso, IxValue, Ixed(..), iso)
import Data.Constraint (Bottom(..), Dict(..))
import Data.Data (Data)
import Data.Default (Default(..))
import Data.Fixed (Fixed(..))
import Data.Foldable (Foldable(foldr))
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Vinyl.Core (Rec(..))
import Fmt (Buildable(..), mapF)
import GHC.Exts as Exts (IsList(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import GHC.Generics qualified as G

import Morley.Michelson.Text
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T
import Morley.Michelson.Typed.Value
import Morley.Tezos.Address
import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
import Morley.Tezos.Crypto
  (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature)
import Morley.Util.Named
import Morley.Util.SizedList.Types
import Morley.Util.Type

----------------------------------------------------------------------------
-- Complex values isomorphism
----------------------------------------------------------------------------

type KnownIsoT a = (IsoValue a, SingI (ToT a))

-- | Isomorphism between Michelson values and plain Haskell types.
--
-- Default implementation of this typeclass converts ADTs to Michelson
-- "pair"s and "or"s.
class (WellTypedToT a) => IsoValue a where
  -- | Type function that converts a regular Haskell type into a @T@ type.
  type ToT a :: T
  type ToT a = GValueType (G.Rep a)

  -- | Converts a Haskell structure into @Value@ representation.
  toVal :: a -> Value (ToT a)
  default toVal
    :: (Generic a, GIsoValue (G.Rep a), ToT a ~ GValueType (G.Rep a))
    => a -> Value (ToT a)
  toVal = Rep a Any -> Value' Instr (GValueType (Rep a))
forall (x :: * -> *) p. GIsoValue x => x p -> Value (GValueType x)
gToValue (Rep a Any -> Value' Instr (GValueType (Rep a)))
-> (a -> Rep a Any) -> a -> Value' Instr (GValueType (Rep a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall a x. Generic a => a -> Rep a x
G.from

  -- | Converts a @Value@ into Haskell type.
  fromVal :: Value (ToT a) -> a
  default fromVal
    :: (Generic a, GIsoValue (G.Rep a), ToT a ~ GValueType (G.Rep a))
    => Value (ToT a) -> a
  fromVal = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
G.to (Rep a Any -> a)
-> (Value' Instr (GValueType (Rep a)) -> Rep a Any)
-> Value' Instr (GValueType (Rep a))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr (GValueType (Rep a)) -> Rep a Any
forall (x :: * -> *) p. GIsoValue x => Value (GValueType x) -> x p
gFromValue

-- | Overloaded version of 'ToT' to work on Haskell and @T@ types.
type ToT' :: forall k. k -> T
type family ToT' t where
  ToT' (t :: T) = t
  ToT' (t :: Type) = ToT t

-- | An optic witnessing the isomorphism between a michelson type and a haskell type.
isoValue :: (IsoValue a, IsoValue b) => Iso (Value (ToT a)) (Value (ToT b)) a b
isoValue :: forall a b.
(IsoValue a, IsoValue b) =>
Iso (Value (ToT a)) (Value (ToT b)) a b
isoValue = (Value' Instr (ToT a) -> a)
-> (b -> Value' Instr (ToT b))
-> Iso (Value' Instr (ToT a)) (Value' Instr (ToT b)) a b
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso Value' Instr (ToT a) -> a
forall a. IsoValue a => Value (ToT a) -> a
fromVal b -> Value' Instr (ToT b)
forall a. IsoValue a => a -> Value (ToT a)
toVal

-- Instances
----------------------------------------------------------------------------

instance WellTyped t => IsoValue (Value t) where
  type ToT (Value t) = t
  toVal :: Value t -> Value (ToT (Value t))
toVal = Value t -> Value (ToT (Value t))
forall a. a -> a
id
  fromVal :: Value (ToT (Value t)) -> Value t
fromVal = Value (ToT (Value t)) -> Value t
forall a. a -> a
id

instance IsoValue Integer where
  type ToT Integer = 'TInt
  toVal :: Integer -> Value (ToT Integer)
toVal = Integer -> Value (ToT Integer)
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt
  fromVal :: Value (ToT Integer) -> Integer
fromVal (VInt Integer
x) = Integer
x

instance IsoValue Natural where
  type ToT Natural = 'TNat
  toVal :: Natural -> Value (ToT Natural)
toVal = Natural -> Value (ToT Natural)
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat
  fromVal :: Value (ToT Natural) -> Natural
fromVal (VNat Natural
x) = Natural
x

instance IsoValue MText where
  type ToT MText = 'TString
  toVal :: MText -> Value (ToT MText)
toVal = MText -> Value (ToT MText)
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString
  fromVal :: Value (ToT MText) -> MText
fromVal (VString MText
x) = MText
x

instance (Bottom, DoNotUseTextError) => IsoValue Text where
  type ToT Text = ToT MText
  toVal :: Text -> Value (ToT Text)
toVal = Text -> Value (ToT Text)
forall a. Bottom => a
no
  fromVal :: Value (ToT Text) -> Text
fromVal = forall a. Bottom => a
Value (ToT Text) -> Text
no

instance IsoValue Bool where
  type ToT Bool = 'TBool
  toVal :: Bool -> Value (ToT Bool)
toVal = Bool -> Value (ToT Bool)
forall (instr :: [T] -> [T] -> *). Bool -> Value' instr 'TBool
VBool
  fromVal :: Value (ToT Bool) -> Bool
fromVal (VBool Bool
x) = Bool
x

instance IsoValue ByteString where
  type ToT ByteString = 'TBytes
  toVal :: ByteString -> Value (ToT ByteString)
toVal = ByteString -> Value (ToT ByteString)
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes
  fromVal :: Value (ToT ByteString) -> ByteString
fromVal (VBytes ByteString
x) = ByteString
x

instance IsoValue Mutez where
  type ToT Mutez = 'TMutez
  toVal :: Mutez -> Value (ToT Mutez)
toVal = Mutez -> Value (ToT Mutez)
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez
  fromVal :: Value (ToT Mutez) -> Mutez
fromVal (VMutez Mutez
x) = Mutez
x

instance IsoValue KeyHash where
  type ToT KeyHash = 'TKeyHash
  toVal :: KeyHash -> Value (ToT KeyHash)
toVal = KeyHash -> Value (ToT KeyHash)
forall (instr :: [T] -> [T] -> *).
KeyHash -> Value' instr 'TKeyHash
VKeyHash
  fromVal :: Value (ToT KeyHash) -> KeyHash
fromVal (VKeyHash KeyHash
x) = KeyHash
x

instance IsoValue Bls12381Fr where
  type ToT Bls12381Fr = 'TBls12381Fr
  toVal :: Bls12381Fr -> Value (ToT Bls12381Fr)
toVal = Bls12381Fr -> Value (ToT Bls12381Fr)
forall (instr :: [T] -> [T] -> *).
Bls12381Fr -> Value' instr 'TBls12381Fr
VBls12381Fr
  fromVal :: Value (ToT Bls12381Fr) -> Bls12381Fr
fromVal (VBls12381Fr Bls12381Fr
x) = Bls12381Fr
x

instance IsoValue Bls12381G1 where
  type ToT Bls12381G1 = 'TBls12381G1
  toVal :: Bls12381G1 -> Value (ToT Bls12381G1)
toVal = Bls12381G1 -> Value (ToT Bls12381G1)
forall (instr :: [T] -> [T] -> *).
Bls12381G1 -> Value' instr 'TBls12381G1
VBls12381G1
  fromVal :: Value (ToT Bls12381G1) -> Bls12381G1
fromVal (VBls12381G1 Bls12381G1
x) = Bls12381G1
x

instance IsoValue Bls12381G2 where
  type ToT Bls12381G2 = 'TBls12381G2
  toVal :: Bls12381G2 -> Value (ToT Bls12381G2)
toVal = Bls12381G2 -> Value (ToT Bls12381G2)
forall (instr :: [T] -> [T] -> *).
Bls12381G2 -> Value' instr 'TBls12381G2
VBls12381G2
  fromVal :: Value (ToT Bls12381G2) -> Bls12381G2
fromVal (VBls12381G2 Bls12381G2
x) = Bls12381G2
x

instance IsoValue Timestamp where
  type ToT Timestamp = 'TTimestamp
  toVal :: Timestamp -> Value (ToT Timestamp)
toVal = Timestamp -> Value (ToT Timestamp)
forall (instr :: [T] -> [T] -> *).
Timestamp -> Value' instr 'TTimestamp
VTimestamp
  fromVal :: Value (ToT Timestamp) -> Timestamp
fromVal (VTimestamp Timestamp
x) = Timestamp
x

instance IsoValue Address where
  type ToT Address = 'TAddress
  toVal :: Address -> Value (ToT Address)
toVal Address
addr = EpAddress -> Value' Instr 'TAddress
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value' Instr 'TAddress)
-> EpAddress -> Value' Instr 'TAddress
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress' Address
addr EpName
DefEpName
  fromVal :: Value (ToT Address) -> Address
fromVal (VAddress EpAddress
x) = EpAddress -> Address
eaAddress EpAddress
x

instance IsoValue EpAddress where
  type ToT EpAddress = 'TAddress
  toVal :: EpAddress -> Value (ToT EpAddress)
toVal = EpAddress -> Value (ToT EpAddress)
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress
  fromVal :: Value (ToT EpAddress) -> EpAddress
fromVal (VAddress EpAddress
x) = EpAddress
x

instance IsoValue PublicKey where
  type ToT PublicKey = 'TKey
  toVal :: PublicKey -> Value (ToT PublicKey)
toVal = PublicKey -> Value (ToT PublicKey)
forall (instr :: [T] -> [T] -> *). PublicKey -> Value' instr 'TKey
VKey
  fromVal :: Value (ToT PublicKey) -> PublicKey
fromVal (VKey PublicKey
x) = PublicKey
x

instance IsoValue Signature where
  type ToT Signature = 'TSignature
  toVal :: Signature -> Value (ToT Signature)
toVal = Signature -> Value (ToT Signature)
forall (instr :: [T] -> [T] -> *).
Signature -> Value' instr 'TSignature
VSignature
  fromVal :: Value (ToT Signature) -> Signature
fromVal (VSignature Signature
x) = Signature
x

instance IsoValue ChainId where
  type ToT ChainId = 'TChainId
  toVal :: ChainId -> Value (ToT ChainId)
toVal = ChainId -> Value (ToT ChainId)
forall (instr :: [T] -> [T] -> *).
ChainId -> Value' instr 'TChainId
VChainId
  fromVal :: Value (ToT ChainId) -> ChainId
fromVal (VChainId ChainId
x) = ChainId
x

instance IsoValue (Fixed p) where
  type ToT (Fixed p) = 'TInt
  toVal :: Fixed p -> Value (ToT (Fixed p))
toVal (MkFixed Integer
x) = Integer -> Value' Instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt Integer
x
  fromVal :: Value (ToT (Fixed p)) -> Fixed p
fromVal (VInt Integer
x) = Integer -> Fixed p
forall k (a :: k). Integer -> Fixed a
MkFixed Integer
x

instance IsoValue ()

instance IsoValue a => IsoValue [a] where
  type ToT [a] = 'TList (ToT a)
  toVal :: [a] -> Value (ToT [a])
toVal = [Value' Instr (ToT a)] -> Value' Instr ('TList (ToT a))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList ([Value' Instr (ToT a)] -> Value' Instr ('TList (ToT a)))
-> ([a] -> [Value' Instr (ToT a)])
-> [a]
-> Value' Instr ('TList (ToT a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Value' Instr (ToT a)) -> [a] -> [Value' Instr (ToT a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map a -> Value' Instr (ToT a)
forall a. IsoValue a => a -> Value (ToT a)
toVal
  fromVal :: Value (ToT [a]) -> [a]
fromVal (VList [Value' Instr t1]
x) = (Value' Instr t1 -> a) -> [Value' Instr t1] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map Value' Instr t1 -> a
forall a. IsoValue a => Value (ToT a) -> a
fromVal [Value' Instr t1]
x

instance IsoValue a => IsoValue (Maybe a) where
  type ToT (Maybe a) = 'TOption (ToT a)
  toVal :: Maybe a -> Value (ToT (Maybe a))
toVal = Maybe (Value' Instr (ToT a)) -> Value' Instr ('TOption (ToT a))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
Maybe (Value' instr t1) -> Value' instr ('TOption t1)
VOption (Maybe (Value' Instr (ToT a)) -> Value' Instr ('TOption (ToT a)))
-> (Maybe a -> Maybe (Value' Instr (ToT a)))
-> Maybe a
-> Value' Instr ('TOption (ToT a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Value' Instr (ToT a))
-> Maybe a -> Maybe (Value' Instr (ToT a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Value' Instr (ToT a)
forall a. IsoValue a => a -> Value (ToT a)
toVal
  fromVal :: Value (ToT (Maybe a)) -> Maybe a
fromVal (VOption Maybe (Value' Instr t1)
x) = (Value' Instr t1 -> a) -> Maybe (Value' Instr t1) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value' Instr t1 -> a
forall a. IsoValue a => Value (ToT a) -> a
fromVal Maybe (Value' Instr t1)
x

instance IsoValue Void

instance (IsoValue l, IsoValue r) => IsoValue (Either l r)

instance (IsoValue a, IsoValue b) => IsoValue (a, b)

instance (Comparable (ToT c), Ord c, IsoValue c) => IsoValue (Set c) where
  type ToT (Set c) = 'TSet (ToT c)
  toVal :: Set c -> Value (ToT (Set c))
toVal = Set (Value' Instr (ToT c)) -> Value' Instr ('TSet (ToT c))
forall (t1 :: T) (instr :: [T] -> [T] -> *).
(SingI t1, Comparable t1) =>
Set (Value' instr t1) -> Value' instr ('TSet t1)
VSet (Set (Value' Instr (ToT c)) -> Value' Instr ('TSet (ToT c)))
-> (Set c -> Set (Value' Instr (ToT c)))
-> Set c
-> Value' Instr ('TSet (ToT c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> Value' Instr (ToT c)) -> Set c -> Set (Value' Instr (ToT c))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map c -> Value' Instr (ToT c)
forall a. IsoValue a => a -> Value (ToT a)
toVal
  fromVal :: Value (ToT (Set c)) -> Set c
fromVal (VSet Set (Value' Instr t1)
x) = (Value' Instr t1 -> c) -> Set (Value' Instr t1) -> Set c
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Value' Instr t1 -> c
forall a. IsoValue a => Value (ToT a) -> a
fromVal Set (Value' Instr t1)
x

instance (Comparable (ToT k), Ord k, IsoValue k, IsoValue v) => IsoValue (Map k v) where
  type ToT (Map k v) = 'TMap (ToT k) (ToT v)
  toVal :: Map k v -> Value (ToT (Map k v))
toVal = Map (Value' Instr (ToT k)) (Value' Instr (ToT v))
-> Value' Instr ('TMap (ToT k) (ToT v))
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap (Map (Value' Instr (ToT k)) (Value' Instr (ToT v))
 -> Value' Instr ('TMap (ToT k) (ToT v)))
-> (Map k v -> Map (Value' Instr (ToT k)) (Value' Instr (ToT v)))
-> Map k v
-> Value' Instr ('TMap (ToT k) (ToT v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (k -> Value' Instr (ToT k))
-> Map k (Value' Instr (ToT v))
-> Map (Value' Instr (ToT k)) (Value' Instr (ToT v))
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys k -> Value' Instr (ToT k)
forall a. IsoValue a => a -> Value (ToT a)
toVal (Map k (Value' Instr (ToT v))
 -> Map (Value' Instr (ToT k)) (Value' Instr (ToT v)))
-> (Map k v -> Map k (Value' Instr (ToT v)))
-> Map k v
-> Map (Value' Instr (ToT k)) (Value' Instr (ToT v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v -> Value' Instr (ToT v))
-> Map k v -> Map k (Value' Instr (ToT v))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map v -> Value' Instr (ToT v)
forall a. IsoValue a => a -> Value (ToT a)
toVal
  fromVal :: Value (ToT (Map k v)) -> Map k v
fromVal (VMap Map (Value' Instr k) (Value' Instr v)
x) = (Value' Instr v -> v) -> Map k (Value' Instr v) -> Map k v
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Value' Instr v -> v
forall a. IsoValue a => Value (ToT a) -> a
fromVal (Map k (Value' Instr v) -> Map k v)
-> Map k (Value' Instr v) -> Map k v
forall a b. (a -> b) -> a -> b
$ (Value' Instr k -> k)
-> Map (Value' Instr k) (Value' Instr v) -> Map k (Value' Instr v)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Value' Instr k -> k
forall a. IsoValue a => Value (ToT a) -> a
fromVal Map (Value' Instr k) (Value' Instr v)
x

instance IsoValue Operation where
  type ToT Operation = 'TOperation
  toVal :: Operation -> Value (ToT Operation)
toVal = Operation -> Value (ToT Operation)
forall (instr :: [T] -> [T] -> *).
Operation' instr -> Value' instr 'TOperation
VOp
  fromVal :: Value (ToT Operation) -> Operation
fromVal (VOp Operation
x) = Operation
x

instance IsoValue Chest where
  type ToT Chest = 'TChest
  toVal :: Chest -> Value (ToT Chest)
toVal = Chest -> Value (ToT Chest)
forall (instr :: [T] -> [T] -> *). Chest -> Value' instr 'TChest
VChest
  fromVal :: Value (ToT Chest) -> Chest
fromVal (VChest Chest
x) = Chest
x

instance IsoValue ChestKey where
  type ToT ChestKey = 'TChestKey
  toVal :: ChestKey -> Value (ToT ChestKey)
toVal = ChestKey -> Value (ToT ChestKey)
forall (instr :: [T] -> [T] -> *).
ChestKey -> Value' instr 'TChestKey
VChestKey
  fromVal :: Value (ToT ChestKey) -> ChestKey
fromVal (VChestKey ChestKey
x) = ChestKey
x

instance IsoValue TxRollupL2Address where
  type ToT TxRollupL2Address = 'TTxRollupL2Address
  toVal :: TxRollupL2Address -> Value (ToT TxRollupL2Address)
toVal = TxRollupL2Address -> Value (ToT TxRollupL2Address)
forall (instr :: [T] -> [T] -> *).
TxRollupL2Address -> Value' instr 'TTxRollupL2Address
VTxRollupL2Address
  fromVal :: Value (ToT TxRollupL2Address) -> TxRollupL2Address
fromVal (VTxRollupL2Address TxRollupL2Address
x) = TxRollupL2Address
x

deriving newtype instance IsoValue a => IsoValue (Identity a)
deriving newtype instance IsoValue a => IsoValue (NamedF Identity a name)
deriving newtype instance IsoValue a => IsoValue (NamedF Maybe a name)

instance (IsoValue a, IsoValue b, IsoValue c) => IsoValue (a, b, c)
instance (IsoValue a, IsoValue b, IsoValue c, IsoValue d)
       => IsoValue (a, b, c, d)
instance (IsoValue a, IsoValue b, IsoValue c, IsoValue d, IsoValue e)
       => IsoValue (a, b, c, d, e)
instance (IsoValue a, IsoValue b, IsoValue c, IsoValue d, IsoValue e,
          IsoValue f)
       => IsoValue (a, b, c, d, e, f)
instance (IsoValue a, IsoValue b, IsoValue c, IsoValue d, IsoValue e,
          IsoValue f, IsoValue g)
       => IsoValue (a, b, c, d, e, f, g)

-- Types used specifically for conversion
----------------------------------------------------------------------------

type EntrypointCall param arg = EntrypointCallT (ToT param) (ToT arg)

type SomeEntrypointCall arg = SomeEntrypointCallT (ToT arg)

type WellTypedToT a = (IsoValue a, WellTyped (ToT a))
type HasNoOpToT a = (IsoValue a, HasNoOp (ToT a))
type HasNoBigMapToT a = (IsoValue a, HasNoBigMap (ToT a))

-- | Since @Contract@ name is used to designate contract code, lets call
-- analogy of 'TContract' type as follows.
--
-- Note that type argument always designates an argument of entrypoint.
-- If a contract has explicit default entrypoint (and no root entrypoint),
-- @ContractRef@ referring to it can never have the entire parameter as its
-- type argument.
data ContractRef (arg :: Type) = ContractRef
  { forall arg. ContractRef arg -> Address
crAddress :: Address
  , forall arg. ContractRef arg -> SomeEntrypointCall arg
crEntrypoint :: SomeEntrypointCall arg
  } deriving stock (ContractRef arg -> ContractRef arg -> Bool
(ContractRef arg -> ContractRef arg -> Bool)
-> (ContractRef arg -> ContractRef arg -> Bool)
-> Eq (ContractRef arg)
forall arg. ContractRef arg -> ContractRef arg -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ContractRef arg -> ContractRef arg -> Bool
$c/= :: forall arg. ContractRef arg -> ContractRef arg -> Bool
== :: ContractRef arg -> ContractRef arg -> Bool
$c== :: forall arg. ContractRef arg -> ContractRef arg -> Bool
Eq, Int -> ContractRef arg -> ShowS
[ContractRef arg] -> ShowS
ContractRef arg -> String
(Int -> ContractRef arg -> ShowS)
-> (ContractRef arg -> String)
-> ([ContractRef arg] -> ShowS)
-> Show (ContractRef arg)
forall arg. Int -> ContractRef arg -> ShowS
forall arg. [ContractRef arg] -> ShowS
forall arg. ContractRef arg -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ContractRef arg] -> ShowS
$cshowList :: forall arg. [ContractRef arg] -> ShowS
show :: ContractRef arg -> String
$cshow :: forall arg. ContractRef arg -> String
showsPrec :: Int -> ContractRef arg -> ShowS
$cshowsPrec :: forall arg. Int -> ContractRef arg -> ShowS
Show)

instance (IsoValue (ContractRef arg)) => Buildable (ContractRef arg) where
  build :: ContractRef arg -> Builder
build = Value' Instr ('TContract (ToT arg)) -> Builder
forall (instr :: [T] -> [T] -> *) (arg :: T).
Value' instr ('TContract arg) -> Builder
buildVContract (Value' Instr ('TContract (ToT arg)) -> Builder)
-> (ContractRef arg -> Value' Instr ('TContract (ToT arg)))
-> ContractRef arg
-> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractRef arg -> Value' Instr ('TContract (ToT arg))
forall a. IsoValue a => a -> Value (ToT a)
toVal

instance (HasNoOpToT arg, HasNoNestedBigMaps (ToT arg), WellTypedToT arg)
  => IsoValue (ContractRef arg) where
  type ToT (ContractRef arg) = 'TContract (ToT arg)
  toVal :: ContractRef arg -> Value (ToT (ContractRef arg))
toVal ContractRef{Address
SomeEntrypointCall arg
crEntrypoint :: SomeEntrypointCall arg
crAddress :: Address
crEntrypoint :: forall arg. ContractRef arg -> SomeEntrypointCall arg
crAddress :: forall arg. ContractRef arg -> Address
..} = Address
-> SomeEntrypointCall arg -> Value' Instr ('TContract (ToT arg))
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, HasNoOp arg) =>
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract Address
crAddress SomeEntrypointCall arg
crEntrypoint
  fromVal :: Value (ToT (ContractRef arg)) -> ContractRef arg
fromVal (VContract Address
addr SomeEntrypointCallT arg
epc) = Address -> SomeEntrypointCall arg -> ContractRef arg
forall arg. Address -> SomeEntrypointCall arg -> ContractRef arg
ContractRef Address
addr SomeEntrypointCallT arg
SomeEntrypointCall arg
epc

-- | Replace type argument of 'ContractRef' with isomorphic one.
coerceContractRef :: (ToT a ~ ToT b) => ContractRef a -> ContractRef b
coerceContractRef :: forall a b. (ToT a ~ ToT b) => ContractRef a -> ContractRef b
coerceContractRef ContractRef{Address
SomeEntrypointCall a
crEntrypoint :: SomeEntrypointCall a
crAddress :: Address
crEntrypoint :: forall arg. ContractRef arg -> SomeEntrypointCall arg
crAddress :: forall arg. ContractRef arg -> Address
..} = ContractRef :: forall arg. Address -> SomeEntrypointCall arg -> ContractRef arg
ContractRef{Address
SomeEntrypointCall a
SomeEntrypointCallT (ToT b)
crEntrypoint :: SomeEntrypointCall a
crAddress :: Address
crEntrypoint :: SomeEntrypointCallT (ToT b)
crAddress :: Address
..}

contractRefToAddr :: ContractRef cp -> EpAddress
contractRefToAddr :: forall cp. ContractRef cp -> EpAddress
contractRefToAddr ContractRef{Address
SomeEntrypointCall cp
crEntrypoint :: SomeEntrypointCall cp
crAddress :: Address
crEntrypoint :: forall arg. ContractRef arg -> SomeEntrypointCall arg
crAddress :: forall arg. ContractRef arg -> Address
..} = Address -> EpName -> EpAddress
EpAddress' Address
crAddress (SomeEntrypointCall cp -> EpName
forall (arg :: T). SomeEntrypointCallT arg -> EpName
sepcName SomeEntrypointCall cp
crEntrypoint)

-- | Ticket type.
data Ticket (arg :: Type) = Ticket
  { forall arg. Ticket arg -> Address
tTicketer :: Address
  , forall arg. Ticket arg -> arg
tData :: arg
  , forall arg. Ticket arg -> Natural
tAmount :: Natural
  } deriving stock (Ticket arg -> Ticket arg -> Bool
(Ticket arg -> Ticket arg -> Bool)
-> (Ticket arg -> Ticket arg -> Bool) -> Eq (Ticket arg)
forall arg. Eq arg => Ticket arg -> Ticket arg -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ticket arg -> Ticket arg -> Bool
$c/= :: forall arg. Eq arg => Ticket arg -> Ticket arg -> Bool
== :: Ticket arg -> Ticket arg -> Bool
$c== :: forall arg. Eq arg => Ticket arg -> Ticket arg -> Bool
Eq, Int -> Ticket arg -> ShowS
[Ticket arg] -> ShowS
Ticket arg -> String
(Int -> Ticket arg -> ShowS)
-> (Ticket arg -> String)
-> ([Ticket arg] -> ShowS)
-> Show (Ticket arg)
forall arg. Show arg => Int -> Ticket arg -> ShowS
forall arg. Show arg => [Ticket arg] -> ShowS
forall arg. Show arg => Ticket arg -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ticket arg] -> ShowS
$cshowList :: forall arg. Show arg => [Ticket arg] -> ShowS
show :: Ticket arg -> String
$cshow :: forall arg. Show arg => Ticket arg -> String
showsPrec :: Int -> Ticket arg -> ShowS
$cshowsPrec :: forall arg. Show arg => Int -> Ticket arg -> ShowS
Show)

instance (Comparable (ToT a), IsoValue a) => IsoValue (Ticket a) where
  type ToT (Ticket a) = 'TTicket (ToT a)
  toVal :: Ticket a -> Value (ToT (Ticket a))
toVal Ticket{a
Natural
Address
tAmount :: Natural
tData :: a
tTicketer :: Address
tAmount :: forall arg. Ticket arg -> Natural
tData :: forall arg. Ticket arg -> arg
tTicketer :: forall arg. Ticket arg -> Address
..} = Address
-> Value' Instr (ToT a)
-> Natural
-> Value' Instr ('TTicket (ToT a))
forall (arg :: T) (instr :: [T] -> [T] -> *).
Comparable arg =>
Address
-> Value' instr arg -> Natural -> Value' instr ('TTicket arg)
VTicket Address
tTicketer (a -> Value' Instr (ToT a)
forall a. IsoValue a => a -> Value (ToT a)
toVal a
tData) Natural
tAmount
  fromVal :: Value (ToT (Ticket a)) -> Ticket a
fromVal (VTicket Address
tTicketer Value' Instr arg
dat Natural
tAmount) = Ticket :: forall arg. Address -> arg -> Natural -> Ticket arg
Ticket{ tData :: a
tData = Value' Instr (ToT a) -> a
forall a. IsoValue a => Value (ToT a) -> a
fromVal Value' Instr arg
Value' Instr (ToT a)
dat, Natural
Address
tAmount :: Natural
tTicketer :: Address
tAmount :: Natural
tTicketer :: Address
.. }

-- | Phantom type that represents the ID of a big_map with
-- keys of type @k@ and values of type @v@.
newtype BigMapId k v = BigMapId { forall {k} {k} (k :: k) (v :: k). BigMapId k v -> Natural
unBigMapId :: Natural }
  -- Note: we purposefully do not derive an `Eq` instance.
  -- If we did, it would be possible for a @cleveland@ user to mistakenly
  -- compare two big_map IDs, whilst being under the impression that they were
  -- actually comparing the big_map's contents.
  -- To avoid this confusion, we simply do not create an `Eq` instance.
  -- For context, see: https://gitlab.com/morley-framework/morley/-/merge_requests/833#note_598577341
  deriving stock (Int -> BigMapId k v -> ShowS
[BigMapId k v] -> ShowS
BigMapId k v -> String
(Int -> BigMapId k v -> ShowS)
-> (BigMapId k v -> String)
-> ([BigMapId k v] -> ShowS)
-> Show (BigMapId k v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (k :: k) k (v :: k). Int -> BigMapId k v -> ShowS
forall k (k :: k) k (v :: k). [BigMapId k v] -> ShowS
forall k (k :: k) k (v :: k). BigMapId k v -> String
showList :: [BigMapId k v] -> ShowS
$cshowList :: forall k (k :: k) k (v :: k). [BigMapId k v] -> ShowS
show :: BigMapId k v -> String
$cshow :: forall k (k :: k) k (v :: k). BigMapId k v -> String
showsPrec :: Int -> BigMapId k v -> ShowS
$cshowsPrec :: forall k (k :: k) k (v :: k). Int -> BigMapId k v -> ShowS
Show, Typeable (BigMapId k v)
Typeable (BigMapId k v)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> BigMapId k v -> c (BigMapId k v))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (BigMapId k v))
-> (BigMapId k v -> Constr)
-> (BigMapId k v -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (BigMapId k v)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (BigMapId k v)))
-> ((forall b. Data b => b -> b) -> BigMapId k v -> BigMapId k v)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r)
-> (forall u. (forall d. Data d => d -> u) -> BigMapId k v -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BigMapId k v -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v))
-> Data (BigMapId k v)
BigMapId k v -> DataType
BigMapId k v -> Constr
(forall b. Data b => b -> b) -> BigMapId k v -> BigMapId k v
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BigMapId k v -> u
forall u. (forall d. Data d => d -> u) -> BigMapId k v -> [u]
forall {k} {k :: k} {k} {v :: k}.
(Typeable k, Typeable v, Typeable k, Typeable k) =>
Typeable (BigMapId k v)
forall k (k :: k) k (v :: k).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
BigMapId k v -> DataType
forall k (k :: k) k (v :: k).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
BigMapId k v -> Constr
forall k (k :: k) k (v :: k).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(forall b. Data b => b -> b) -> BigMapId k v -> BigMapId k v
forall k (k :: k) k (v :: k) u.
(Typeable k, Typeable v, Typeable k, Typeable k) =>
Int -> (forall d. Data d => d -> u) -> BigMapId k v -> u
forall k (k :: k) k (v :: k) u.
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(forall d. Data d => d -> u) -> BigMapId k v -> [u]
forall k (k :: k) k (v :: k) r r'.
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r
forall k (k :: k) k (v :: k) r r'.
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r
forall k (k :: k) k (v :: k) (m :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k, Monad m) =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v)
forall k (k :: k) k (v :: k) (m :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v)
forall k (k :: k) k (v :: k) (c :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BigMapId k v)
forall k (k :: k) k (v :: k) (c :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BigMapId k v -> c (BigMapId k v)
forall k (k :: k) k (v :: k) (t :: * -> *) (c :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BigMapId k v))
forall k (k :: k) k (v :: k) (t :: * -> * -> *) (c :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BigMapId k v))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BigMapId k v)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BigMapId k v -> c (BigMapId k v)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BigMapId k v))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BigMapId k v))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v)
$cgmapMo :: forall k (k :: k) k (v :: k) (m :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v)
$cgmapMp :: forall k (k :: k) k (v :: k) (m :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v)
$cgmapM :: forall k (k :: k) k (v :: k) (m :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k, Monad m) =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (BigMapId k v)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BigMapId k v -> u
$cgmapQi :: forall k (k :: k) k (v :: k) u.
(Typeable k, Typeable v, Typeable k, Typeable k) =>
Int -> (forall d. Data d => d -> u) -> BigMapId k v -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> BigMapId k v -> [u]
$cgmapQ :: forall k (k :: k) k (v :: k) u.
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(forall d. Data d => d -> u) -> BigMapId k v -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r
$cgmapQr :: forall k (k :: k) k (v :: k) r r'.
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r
$cgmapQl :: forall k (k :: k) k (v :: k) r r'.
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r
gmapT :: (forall b. Data b => b -> b) -> BigMapId k v -> BigMapId k v
$cgmapT :: forall k (k :: k) k (v :: k).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(forall b. Data b => b -> b) -> BigMapId k v -> BigMapId k v
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BigMapId k v))
$cdataCast2 :: forall k (k :: k) k (v :: k) (t :: * -> * -> *) (c :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BigMapId k v))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BigMapId k v))
$cdataCast1 :: forall k (k :: k) k (v :: k) (t :: * -> *) (c :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BigMapId k v))
dataTypeOf :: BigMapId k v -> DataType
$cdataTypeOf :: forall k (k :: k) k (v :: k).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
BigMapId k v -> DataType
toConstr :: BigMapId k v -> Constr
$ctoConstr :: forall k (k :: k) k (v :: k).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
BigMapId k v -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BigMapId k v)
$cgunfold :: forall k (k :: k) k (v :: k) (c :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BigMapId k v)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BigMapId k v -> c (BigMapId k v)
$cgfoldl :: forall k (k :: k) k (v :: k) (c :: * -> *).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BigMapId k v -> c (BigMapId k v)
Data)
  deriving newtype (WellTypedToT (BigMapId k v)
WellTypedToT (BigMapId k v)
-> (BigMapId k v -> Value (ToT (BigMapId k v)))
-> (Value (ToT (BigMapId k v)) -> BigMapId k v)
-> IsoValue (BigMapId k v)
Value (ToT (BigMapId k v)) -> BigMapId k v
BigMapId k v -> Value (ToT (BigMapId k v))
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
forall {k} {k :: k} {k} {v :: k}. WellTypedToT (BigMapId k v)
forall k (k :: k) k (v :: k).
Value (ToT (BigMapId k v)) -> BigMapId k v
forall k (k :: k) k (v :: k).
BigMapId k v -> Value (ToT (BigMapId k v))
fromVal :: Value (ToT (BigMapId k v)) -> BigMapId k v
$cfromVal :: forall k (k :: k) k (v :: k).
Value (ToT (BigMapId k v)) -> BigMapId k v
toVal :: BigMapId k v -> Value (ToT (BigMapId k v))
$ctoVal :: forall k (k :: k) k (v :: k).
BigMapId k v -> Value (ToT (BigMapId k v))
IsoValue, BigMapId k v -> Builder
(BigMapId k v -> Builder) -> Buildable (BigMapId k v)
forall p. (p -> Builder) -> Buildable p
forall k (k :: k) k (v :: k). BigMapId k v -> Builder
build :: BigMapId k v -> Builder
$cbuild :: forall k (k :: k) k (v :: k). BigMapId k v -> Builder
Buildable, Integer -> BigMapId k v
BigMapId k v -> BigMapId k v
BigMapId k v -> BigMapId k v -> BigMapId k v
(BigMapId k v -> BigMapId k v -> BigMapId k v)
-> (BigMapId k v -> BigMapId k v -> BigMapId k v)
-> (BigMapId k v -> BigMapId k v -> BigMapId k v)
-> (BigMapId k v -> BigMapId k v)
-> (BigMapId k v -> BigMapId k v)
-> (BigMapId k v -> BigMapId k v)
-> (Integer -> BigMapId k v)
-> Num (BigMapId k v)
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
forall k (k :: k) k (v :: k). Integer -> BigMapId k v
forall k (k :: k) k (v :: k). BigMapId k v -> BigMapId k v
forall k (k :: k) k (v :: k).
BigMapId k v -> BigMapId k v -> BigMapId k v
fromInteger :: Integer -> BigMapId k v
$cfromInteger :: forall k (k :: k) k (v :: k). Integer -> BigMapId k v
signum :: BigMapId k v -> BigMapId k v
$csignum :: forall k (k :: k) k (v :: k). BigMapId k v -> BigMapId k v
abs :: BigMapId k v -> BigMapId k v
$cabs :: forall k (k :: k) k (v :: k). BigMapId k v -> BigMapId k v
negate :: BigMapId k v -> BigMapId k v
$cnegate :: forall k (k :: k) k (v :: k). BigMapId k v -> BigMapId k v
* :: BigMapId k v -> BigMapId k v -> BigMapId k v
$c* :: forall k (k :: k) k (v :: k).
BigMapId k v -> BigMapId k v -> BigMapId k v
- :: BigMapId k v -> BigMapId k v -> BigMapId k v
$c- :: forall k (k :: k) k (v :: k).
BigMapId k v -> BigMapId k v -> BigMapId k v
+ :: BigMapId k v -> BigMapId k v -> BigMapId k v
$c+ :: forall k (k :: k) k (v :: k).
BigMapId k v -> BigMapId k v -> BigMapId k v
Num)

data BigMap k v = BigMap
  { forall k v. BigMap k v -> Maybe (BigMapId k v)
bmId :: Maybe (BigMapId k v)
  , forall k v. BigMap k v -> Map k v
bmMap :: Map k v
  }
  deriving stock (Int -> BigMap k v -> ShowS
[BigMap k v] -> ShowS
BigMap k v -> String
(Int -> BigMap k v -> ShowS)
-> (BigMap k v -> String)
-> ([BigMap k v] -> ShowS)
-> Show (BigMap k v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k v. (Show k, Show v) => Int -> BigMap k v -> ShowS
forall k v. (Show k, Show v) => [BigMap k v] -> ShowS
forall k v. (Show k, Show v) => BigMap k v -> String
showList :: [BigMap k v] -> ShowS
$cshowList :: forall k v. (Show k, Show v) => [BigMap k v] -> ShowS
show :: BigMap k v -> String
$cshow :: forall k v. (Show k, Show v) => BigMap k v -> String
showsPrec :: Int -> BigMap k v -> ShowS
$cshowsPrec :: forall k v. (Show k, Show v) => Int -> BigMap k v -> ShowS
Show, (forall x. BigMap k v -> Rep (BigMap k v) x)
-> (forall x. Rep (BigMap k v) x -> BigMap k v)
-> Generic (BigMap k v)
forall x. Rep (BigMap k v) x -> BigMap k v
forall x. BigMap k v -> Rep (BigMap k v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k v x. Rep (BigMap k v) x -> BigMap k v
forall k v x. BigMap k v -> Rep (BigMap k v) x
$cto :: forall k v x. Rep (BigMap k v) x -> BigMap k v
$cfrom :: forall k v x. BigMap k v -> Rep (BigMap k v) x
Generic, Typeable (BigMap k v)
Typeable (BigMap k v)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> BigMap k v -> c (BigMap k v))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (BigMap k v))
-> (BigMap k v -> Constr)
-> (BigMap k v -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (BigMap k v)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (BigMap k v)))
-> ((forall b. Data b => b -> b) -> BigMap k v -> BigMap k v)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BigMap k v -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BigMap k v -> r)
-> (forall u. (forall d. Data d => d -> u) -> BigMap k v -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BigMap k v -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v))
-> Data (BigMap k v)
BigMap k v -> DataType
BigMap k v -> Constr
(forall b. Data b => b -> b) -> BigMap k v -> BigMap k v
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BigMap k v -> u
forall u. (forall d. Data d => d -> u) -> BigMap k v -> [u]
forall {k} {v}. (Data k, Data v, Ord k) => Typeable (BigMap k v)
forall k v. (Data k, Data v, Ord k) => BigMap k v -> DataType
forall k v. (Data k, Data v, Ord k) => BigMap k v -> Constr
forall k v.
(Data k, Data v, Ord k) =>
(forall b. Data b => b -> b) -> BigMap k v -> BigMap k v
forall k v u.
(Data k, Data v, Ord k) =>
Int -> (forall d. Data d => d -> u) -> BigMap k v -> u
forall k v u.
(Data k, Data v, Ord k) =>
(forall d. Data d => d -> u) -> BigMap k v -> [u]
forall k v r r'.
(Data k, Data v, Ord k) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BigMap k v -> r
forall k v r r'.
(Data k, Data v, Ord k) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BigMap k v -> r
forall k v (m :: * -> *).
(Data k, Data v, Ord k, Monad m) =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v)
forall k v (m :: * -> *).
(Data k, Data v, Ord k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v)
forall k v (c :: * -> *).
(Data k, Data v, Ord k) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BigMap k v)
forall k v (c :: * -> *).
(Data k, Data v, Ord k) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BigMap k v -> c (BigMap k v)
forall k v (t :: * -> *) (c :: * -> *).
(Data k, Data v, Ord k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BigMap k v))
forall k v (t :: * -> * -> *) (c :: * -> *).
(Data k, Data v, Ord k, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BigMap k v))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BigMap k v -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BigMap k v -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BigMap k v)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BigMap k v -> c (BigMap k v)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BigMap k v))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BigMap k v))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v)
$cgmapMo :: forall k v (m :: * -> *).
(Data k, Data v, Ord k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v)
$cgmapMp :: forall k v (m :: * -> *).
(Data k, Data v, Ord k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v)
$cgmapM :: forall k v (m :: * -> *).
(Data k, Data v, Ord k, Monad m) =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (BigMap k v)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BigMap k v -> u
$cgmapQi :: forall k v u.
(Data k, Data v, Ord k) =>
Int -> (forall d. Data d => d -> u) -> BigMap k v -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> BigMap k v -> [u]
$cgmapQ :: forall k v u.
(Data k, Data v, Ord k) =>
(forall d. Data d => d -> u) -> BigMap k v -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BigMap k v -> r
$cgmapQr :: forall k v r r'.
(Data k, Data v, Ord k) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BigMap k v -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BigMap k v -> r
$cgmapQl :: forall k v r r'.
(Data k, Data v, Ord k) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BigMap k v -> r
gmapT :: (forall b. Data b => b -> b) -> BigMap k v -> BigMap k v
$cgmapT :: forall k v.
(Data k, Data v, Ord k) =>
(forall b. Data b => b -> b) -> BigMap k v -> BigMap k v
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BigMap k v))
$cdataCast2 :: forall k v (t :: * -> * -> *) (c :: * -> *).
(Data k, Data v, Ord k, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BigMap k v))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BigMap k v))
$cdataCast1 :: forall k v (t :: * -> *) (c :: * -> *).
(Data k, Data v, Ord k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BigMap k v))
dataTypeOf :: BigMap k v -> DataType
$cdataTypeOf :: forall k v. (Data k, Data v, Ord k) => BigMap k v -> DataType
toConstr :: BigMap k v -> Constr
$ctoConstr :: forall k v. (Data k, Data v, Ord k) => BigMap k v -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BigMap k v)
$cgunfold :: forall k v (c :: * -> *).
(Data k, Data v, Ord k) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BigMap k v)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BigMap k v -> c (BigMap k v)
$cgfoldl :: forall k v (c :: * -> *).
(Data k, Data v, Ord k) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BigMap k v -> c (BigMap k v)
Data)
  deriving anyclass (BigMap k v
BigMap k v -> Default (BigMap k v)
forall a. a -> Default a
forall k v. BigMap k v
def :: BigMap k v
$cdef :: forall k v. BigMap k v
Default, Eq (Element (BigMap k v)) =>
Element (BigMap k v) -> BigMap k v -> Bool
Ord (Element (BigMap k v)) =>
BigMap k v -> Maybe (Element (BigMap k v))
Monoid (Element (BigMap k v)) => BigMap k v -> Element (BigMap k v)
(Element (BigMap k v) ~ Bool) => BigMap k v -> Bool
BigMap k v -> Bool
BigMap k v -> Int
BigMap k v -> [Element (BigMap k v)]
BigMap k v -> Maybe (Element (BigMap k v))
(Element (BigMap k v) -> Bool) -> BigMap k v -> Bool
(Element (BigMap k v) -> Bool)
-> BigMap k v -> Maybe (Element (BigMap k v))
(Element (BigMap k v)
 -> Element (BigMap k v) -> Element (BigMap k v))
-> BigMap k v -> Maybe (Element (BigMap k v))
(BigMap k v -> [Element (BigMap k v)])
-> (BigMap k v -> Bool)
-> (forall b.
    (Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b)
-> (forall b.
    (b -> Element (BigMap k v) -> b) -> b -> BigMap k v -> b)
-> (forall b.
    (b -> Element (BigMap k v) -> b) -> b -> BigMap k v -> b)
-> (BigMap k v -> Int)
-> (Eq (Element (BigMap k v)) =>
    Element (BigMap k v) -> BigMap k v -> Bool)
-> (forall m.
    Monoid m =>
    (Element (BigMap k v) -> m) -> BigMap k v -> m)
-> (Monoid (Element (BigMap k v)) =>
    BigMap k v -> Element (BigMap k v))
-> (forall b.
    (Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b)
-> (Eq (Element (BigMap k v)) =>
    Element (BigMap k v) -> BigMap k v -> Bool)
-> ((Element (BigMap k v) -> Bool) -> BigMap k v -> Bool)
-> ((Element (BigMap k v) -> Bool) -> BigMap k v -> Bool)
-> ((Element (BigMap k v) ~ Bool) => BigMap k v -> Bool)
-> ((Element (BigMap k v) ~ Bool) => BigMap k v -> Bool)
-> ((Element (BigMap k v) -> Bool)
    -> BigMap k v -> Maybe (Element (BigMap k v)))
-> (BigMap k v -> Maybe (Element (BigMap k v)))
-> (Ord (Element (BigMap k v)) =>
    BigMap k v -> Maybe (Element (BigMap k v)))
-> (Ord (Element (BigMap k v)) =>
    BigMap k v -> Maybe (Element (BigMap k v)))
-> ((Element (BigMap k v)
     -> Element (BigMap k v) -> Element (BigMap k v))
    -> BigMap k v -> Maybe (Element (BigMap k v)))
-> ((Element (BigMap k v)
     -> Element (BigMap k v) -> Element (BigMap k v))
    -> BigMap k v -> Maybe (Element (BigMap k v)))
-> Container (BigMap k v)
forall m.
Monoid m =>
(Element (BigMap k v) -> m) -> BigMap k v -> m
forall t.
(t -> [Element t])
-> (t -> Bool)
-> (forall b. (Element t -> b -> b) -> b -> t -> b)
-> (forall b. (b -> Element t -> b) -> b -> t -> b)
-> (forall b. (b -> Element t -> b) -> b -> t -> b)
-> (t -> Int)
-> (Eq (Element t) => Element t -> t -> Bool)
-> (forall m. Monoid m => (Element t -> m) -> t -> m)
-> (Monoid (Element t) => t -> Element t)
-> (forall b. (Element t -> b -> b) -> b -> t -> b)
-> (Eq (Element t) => Element t -> t -> Bool)
-> ((Element t -> Bool) -> t -> Bool)
-> ((Element t -> Bool) -> t -> Bool)
-> ((Element t ~ Bool) => t -> Bool)
-> ((Element t ~ Bool) => t -> Bool)
-> ((Element t -> Bool) -> t -> Maybe (Element t))
-> (t -> Maybe (Element t))
-> (Ord (Element t) => t -> Maybe (Element t))
-> (Ord (Element t) => t -> Maybe (Element t))
-> ((Element t -> Element t -> Element t)
    -> t -> Maybe (Element t))
-> ((Element t -> Element t -> Element t)
    -> t -> Maybe (Element t))
-> Container t
forall b. (b -> Element (BigMap k v) -> b) -> b -> BigMap k v -> b
forall b. (Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b
forall k v.
Eq (Element (BigMap k v)) =>
Element (BigMap k v) -> BigMap k v -> Bool
forall k v.
Ord (Element (BigMap k v)) =>
BigMap k v -> Maybe (Element (BigMap k v))
forall k v.
Monoid (Element (BigMap k v)) =>
BigMap k v -> Element (BigMap k v)
forall k v. (Element (BigMap k v) ~ Bool) => BigMap k v -> Bool
forall k v. BigMap k v -> Bool
forall k v. BigMap k v -> Int
forall k v. BigMap k v -> [Element (BigMap k v)]
forall k v. BigMap k v -> Maybe (Element (BigMap k v))
forall k v. (Element (BigMap k v) -> Bool) -> BigMap k v -> Bool
forall k v.
(Element (BigMap k v) -> Bool)
-> BigMap k v -> Maybe (Element (BigMap k v))
forall k v.
(Element (BigMap k v)
 -> Element (BigMap k v) -> Element (BigMap k v))
-> BigMap k v -> Maybe (Element (BigMap k v))
forall k v m.
Monoid m =>
(Element (BigMap k v) -> m) -> BigMap k v -> m
forall k v b.
(b -> Element (BigMap k v) -> b) -> b -> BigMap k v -> b
forall k v b.
(Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b
safeFoldl1 :: (Element (BigMap k v)
 -> Element (BigMap k v) -> Element (BigMap k v))
-> BigMap k v -> Maybe (Element (BigMap k v))
$csafeFoldl1 :: forall k v.
(Element (BigMap k v)
 -> Element (BigMap k v) -> Element (BigMap k v))
-> BigMap k v -> Maybe (Element (BigMap k v))
safeFoldr1 :: (Element (BigMap k v)
 -> Element (BigMap k v) -> Element (BigMap k v))
-> BigMap k v -> Maybe (Element (BigMap k v))
$csafeFoldr1 :: forall k v.
(Element (BigMap k v)
 -> Element (BigMap k v) -> Element (BigMap k v))
-> BigMap k v -> Maybe (Element (BigMap k v))
safeMinimum :: Ord (Element (BigMap k v)) =>
BigMap k v -> Maybe (Element (BigMap k v))
$csafeMinimum :: forall k v.
Ord (Element (BigMap k v)) =>
BigMap k v -> Maybe (Element (BigMap k v))
safeMaximum :: Ord (Element (BigMap k v)) =>
BigMap k v -> Maybe (Element (BigMap k v))
$csafeMaximum :: forall k v.
Ord (Element (BigMap k v)) =>
BigMap k v -> Maybe (Element (BigMap k v))
safeHead :: BigMap k v -> Maybe (Element (BigMap k v))
$csafeHead :: forall k v. BigMap k v -> Maybe (Element (BigMap k v))
find :: (Element (BigMap k v) -> Bool)
-> BigMap k v -> Maybe (Element (BigMap k v))
$cfind :: forall k v.
(Element (BigMap k v) -> Bool)
-> BigMap k v -> Maybe (Element (BigMap k v))
or :: (Element (BigMap k v) ~ Bool) => BigMap k v -> Bool
$cor :: forall k v. (Element (BigMap k v) ~ Bool) => BigMap k v -> Bool
and :: (Element (BigMap k v) ~ Bool) => BigMap k v -> Bool
$cand :: forall k v. (Element (BigMap k v) ~ Bool) => BigMap k v -> Bool
any :: (Element (BigMap k v) -> Bool) -> BigMap k v -> Bool
$cany :: forall k v. (Element (BigMap k v) -> Bool) -> BigMap k v -> Bool
all :: (Element (BigMap k v) -> Bool) -> BigMap k v -> Bool
$call :: forall k v. (Element (BigMap k v) -> Bool) -> BigMap k v -> Bool
notElem :: Eq (Element (BigMap k v)) =>
Element (BigMap k v) -> BigMap k v -> Bool
$cnotElem :: forall k v.
Eq (Element (BigMap k v)) =>
Element (BigMap k v) -> BigMap k v -> Bool
foldr' :: forall b. (Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b
$cfoldr' :: forall k v b.
(Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b
fold :: Monoid (Element (BigMap k v)) => BigMap k v -> Element (BigMap k v)
$cfold :: forall k v.
Monoid (Element (BigMap k v)) =>
BigMap k v -> Element (BigMap k v)
foldMap :: forall m.
Monoid m =>
(Element (BigMap k v) -> m) -> BigMap k v -> m
$cfoldMap :: forall k v m.
Monoid m =>
(Element (BigMap k v) -> m) -> BigMap k v -> m
elem :: Eq (Element (BigMap k v)) =>
Element (BigMap k v) -> BigMap k v -> Bool
$celem :: forall k v.
Eq (Element (BigMap k v)) =>
Element (BigMap k v) -> BigMap k v -> Bool
length :: BigMap k v -> Int
$clength :: forall k v. BigMap k v -> Int
foldl' :: forall b. (b -> Element (BigMap k v) -> b) -> b -> BigMap k v -> b
$cfoldl' :: forall k v b.
(b -> Element (BigMap k v) -> b) -> b -> BigMap k v -> b
foldl :: forall b. (b -> Element (BigMap k v) -> b) -> b -> BigMap k v -> b
$cfoldl :: forall k v b.
(b -> Element (BigMap k v) -> b) -> b -> BigMap k v -> b
foldr :: forall b. (Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b
$cfoldr :: forall k v b.
(Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b
null :: BigMap k v -> Bool
$cnull :: forall k v. BigMap k v -> Bool
toList :: BigMap k v -> [Element (BigMap k v)]
$ctoList :: forall k v. BigMap k v -> [Element (BigMap k v)]
Container)

type instance Index (BigMap k _) = k
type instance IxValue (BigMap _ v) = v
instance Ord k => Ixed (BigMap k v)
instance Ord k => At (BigMap k v) where
  at :: Index (BigMap k v)
-> Lens' (BigMap k v) (Maybe (IxValue (BigMap k v)))
at Index (BigMap k v)
key Maybe (IxValue (BigMap k v)) -> f (Maybe (IxValue (BigMap k v)))
handler (BigMap Maybe (BigMapId k v)
bmId Map k v
bmMap) = Maybe (BigMapId k v) -> Map k v -> BigMap k v
forall k v. Maybe (BigMapId k v) -> Map k v -> BigMap k v
BigMap Maybe (BigMapId k v)
bmId (Map k v -> BigMap k v) -> f (Map k v) -> f (BigMap k v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index (Map k v) -> Lens' (Map k v) (Maybe (IxValue (Map k v)))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map k v)
Index (BigMap k v)
key Maybe (IxValue (Map k v)) -> f (Maybe (IxValue (Map k v)))
Maybe (IxValue (BigMap k v)) -> f (Maybe (IxValue (BigMap k v)))
handler Map k v
bmMap

class ToBigMap m where
  type ToBigMapKey m
  type ToBigMapValue m
  mkBigMap :: m -> BigMap (ToBigMapKey m) (ToBigMapValue m)

instance Ord k => ToBigMap [(k, v)] where
  type ToBigMapValue [(k, v)] = v
  type ToBigMapKey [(k, v)] = k
  mkBigMap :: [(k, v)] -> BigMap (ToBigMapKey [(k, v)]) (ToBigMapValue [(k, v)])
mkBigMap = [(k, v)] -> BigMap (ToBigMapKey [(k, v)]) (ToBigMapValue [(k, v)])
forall l. IsList l => [Item l] -> l
Exts.fromList

instance ToBigMap (Map k v) where
  type ToBigMapValue (Map k v) = v
  type ToBigMapKey (Map k v) = k
  mkBigMap :: Map k v -> BigMap (ToBigMapKey (Map k v)) (ToBigMapValue (Map k v))
mkBigMap = Maybe (BigMapId k v) -> Map k v -> BigMap k v
forall k v. Maybe (BigMapId k v) -> Map k v -> BigMap k v
BigMap Maybe (BigMapId k v)
forall a. Maybe a
Nothing

instance Ord k => ToBigMap (NonEmpty (k, v)) where
  type ToBigMapValue (NonEmpty (k, v)) = v
  type ToBigMapKey (NonEmpty (k, v)) = k
  mkBigMap :: NonEmpty (k, v)
-> BigMap
     (ToBigMapKey (NonEmpty (k, v))) (ToBigMapValue (NonEmpty (k, v)))
mkBigMap ((k, v)
h :| [(k, v)]
t) = OneItem (BigMap k v) -> BigMap k v
forall x. One x => OneItem x -> x
one (k, v)
OneItem (BigMap k v)
h BigMap k v -> BigMap k v -> BigMap k v
forall a. Semigroup a => a -> a -> a
<> [(k, v)] -> BigMap (ToBigMapKey [(k, v)]) (ToBigMapValue [(k, v)])
forall m.
ToBigMap m =>
m -> BigMap (ToBigMapKey m) (ToBigMapValue m)
mkBigMap [(k, v)]
t

instance Ord k => ToBigMap (SizedList' n (k, v)) where
  type ToBigMapValue (SizedList' n (k, v)) = v
  type ToBigMapKey (SizedList' n (k, v)) = k
  mkBigMap :: SizedList' n (k, v)
-> BigMap
     (ToBigMapKey (SizedList' n (k, v)))
     (ToBigMapValue (SizedList' n (k, v)))
mkBigMap = [(k, v)] -> BigMap k v
forall l. IsList l => [Item l] -> l
Exts.fromList ([(k, v)] -> BigMap k v)
-> (SizedList' n (k, v) -> [(k, v)])
-> SizedList' n (k, v)
-> BigMap k v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizedList' n (k, v) -> [(k, v)]
forall t. Container t => t -> [Element t]
Prelude.toList

instance Ord k => Semigroup (BigMap k v) where
  BigMap Maybe (BigMapId k v)
_ Map k v
m1 <> :: BigMap k v -> BigMap k v -> BigMap k v
<> BigMap Maybe (BigMapId k v)
_ Map k v
m2 = Maybe (BigMapId k v) -> Map k v -> BigMap k v
forall k v. Maybe (BigMapId k v) -> Map k v -> BigMap k v
BigMap Maybe (BigMapId k v)
forall a. Maybe a
Nothing (Map k v
m1 Map k v -> Map k v -> Map k v
forall a. Semigroup a => a -> a -> a
<> Map k v
m2)

instance Foldable (BigMap k) where
  foldr :: forall a b. (a -> b -> b) -> b -> BigMap k a -> b
foldr a -> b -> b
f b
z (BigMap Maybe (BigMapId k a)
_ Map k a
bmMap) = (a -> b -> b) -> b -> Map k a -> b
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr a -> b -> b
f b
z Map k a
bmMap

instance One (BigMap k v) where
  type OneItem (BigMap k v) = OneItem (Map k v)
  one :: OneItem (BigMap k v) -> BigMap k v
one OneItem (BigMap k v)
x = Maybe (BigMapId k v) -> Map k v -> BigMap k v
forall k v. Maybe (BigMapId k v) -> Map k v -> BigMap k v
BigMap Maybe (BigMapId k v)
forall a. Maybe a
Nothing (OneItem (Map k v) -> Map k v
forall x. One x => OneItem x -> x
one OneItem (Map k v)
OneItem (BigMap k v)
x)

instance Ord k => IsList (BigMap k v) where
  type Item (BigMap k v) = Item (Map k v)
  fromList :: [Item (BigMap k v)] -> BigMap k v
fromList [Item (BigMap k v)]
xs = Maybe (BigMapId k v) -> Map k v -> BigMap k v
forall k v. Maybe (BigMapId k v) -> Map k v -> BigMap k v
BigMap Maybe (BigMapId k v)
forall a. Maybe a
Nothing ([Item (Map k v)] -> Map k v
forall l. IsList l => [Item l] -> l
Exts.fromList [Item (Map k v)]
[Item (BigMap k v)]
xs)
  toList :: BigMap k v -> [Item (BigMap k v)]
toList (BigMap Maybe (BigMapId k v)
_ Map k v
xs) = Map k v -> [Item (Map k v)]
forall l. IsList l => l -> [Item l]
Exts.toList Map k v
xs

instance (Ord k, Buildable k, Buildable v) => Buildable (BigMap k v) where
  build :: BigMap k v -> Builder
build = BigMap k v -> Builder
forall t k v.
(IsList t, Item t ~ (k, v), Buildable k, Buildable v) =>
t -> Builder
mapF

instance
  ( Comparable (ToT k) , Ord k, IsoValue k
  , IsoValue v, HasNoBigMapToT v, HasNoOpToT v
  ) => IsoValue (BigMap k v) where
  type ToT (BigMap k v) = 'TBigMap (ToT k) (ToT v)
  toVal :: BigMap k v -> Value (ToT (BigMap k v))
toVal (BigMap Maybe (BigMapId k v)
bmId Map k v
bmMap) =
    Maybe Natural
-> Map (Value' Instr (ToT k)) (Value' Instr (ToT v))
-> Value' Instr ('TBigMap (ToT k) (ToT v))
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(SingI k, SingI v, Comparable k, HasNoBigMap v) =>
Maybe Natural
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap
      (BigMapId k v -> Natural
forall {k} {k} (k :: k) (v :: k). BigMapId k v -> Natural
unBigMapId (BigMapId k v -> Natural) -> Maybe (BigMapId k v) -> Maybe Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (BigMapId k v)
bmId)
      ((k -> Value' Instr (ToT k))
-> Map k (Value' Instr (ToT v))
-> Map (Value' Instr (ToT k)) (Value' Instr (ToT v))
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys k -> Value' Instr (ToT k)
forall a. IsoValue a => a -> Value (ToT a)
toVal (Map k (Value' Instr (ToT v))
 -> Map (Value' Instr (ToT k)) (Value' Instr (ToT v)))
-> Map k (Value' Instr (ToT v))
-> Map (Value' Instr (ToT k)) (Value' Instr (ToT v))
forall a b. (a -> b) -> a -> b
$ (v -> Value' Instr (ToT v))
-> Map k v -> Map k (Value' Instr (ToT v))
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map v -> Value' Instr (ToT v)
forall a. IsoValue a => a -> Value (ToT a)
toVal Map k v
bmMap)
  fromVal :: Value (ToT (BigMap k v)) -> BigMap k v
fromVal (VBigMap Maybe Natural
bmId Map (Value' Instr k) (Value' Instr v)
x) =
    Maybe (BigMapId k v) -> Map k v -> BigMap k v
forall k v. Maybe (BigMapId k v) -> Map k v -> BigMap k v
BigMap
      (Natural -> BigMapId k v
forall {k} {k} (k :: k) (v :: k). Natural -> BigMapId k v
BigMapId (Natural -> BigMapId k v) -> Maybe Natural -> Maybe (BigMapId k v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Natural
bmId)
      ((Value' Instr v -> v) -> Map k (Value' Instr v) -> Map k v
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Value' Instr v -> v
forall a. IsoValue a => Value (ToT a) -> a
fromVal (Map k (Value' Instr v) -> Map k v)
-> Map k (Value' Instr v) -> Map k v
forall a b. (a -> b) -> a -> b
$ (Value' Instr k -> k)
-> Map (Value' Instr k) (Value' Instr v) -> Map k (Value' Instr v)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Value' Instr k -> k
forall a. IsoValue a => Value (ToT a) -> a
fromVal Map (Value' Instr k) (Value' Instr v)
x)

-- Generic magic
----------------------------------------------------------------------------

-- | Implements ADT conversion to Michelson value.
--
-- Thanks to Generic, Michelson representation will
-- be a balanced tree; this reduces average access time in general case.
--
-- A drawback of such approach is that, in theory, in new GHC version
-- generified representation may change; however, chances are small and
-- I (martoon) believe that contract versions will change much faster anyway.
--
-- In case an unbalanced tree is needed, the Generic instance can be derived by
-- using the utilities in the "Morley.Util.Generic" module.
class SingI (GValueType x) =>
      GIsoValue (x :: Type -> Type) where
  type GValueType x :: T
  gToValue :: x p -> Value (GValueType x)
  gFromValue :: Value (GValueType x) -> x p

instance GIsoValue x => GIsoValue (G.M1 t i x) where
  type GValueType (G.M1 t i x) = GValueType x
  gToValue :: forall p. M1 t i x p -> Value (GValueType (M1 t i x))
gToValue = x p -> Value' Instr (GValueType x)
forall (x :: * -> *) p. GIsoValue x => x p -> Value (GValueType x)
gToValue (x p -> Value' Instr (GValueType x))
-> (M1 t i x p -> x p) -> M1 t i x p -> Value' Instr (GValueType x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 t i x p -> x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
  gFromValue :: forall p. Value (GValueType (M1 t i x)) -> M1 t i x p
gFromValue = x p -> M1 t i x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (x p -> M1 t i x p)
-> (Value' Instr (GValueType x) -> x p)
-> Value' Instr (GValueType x)
-> M1 t i x p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr (GValueType x) -> x p
forall (x :: * -> *) p. GIsoValue x => Value (GValueType x) -> x p
gFromValue

instance (GIsoValue x, GIsoValue y) => GIsoValue (x :+: y) where
  type GValueType (x :+: y) = 'TOr (GValueType x) (GValueType y)
  gToValue :: forall p. (:+:) x y p -> Value (GValueType (x :+: y))
gToValue = Either (Value' Instr (GValueType x)) (Value' Instr (GValueType y))
-> Value' Instr ('TOr (GValueType x) (GValueType y))
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 (GValueType x)) (Value' Instr (GValueType y))
 -> Value' Instr ('TOr (GValueType x) (GValueType y)))
-> ((:+:) x y p
    -> Either
         (Value' Instr (GValueType x)) (Value' Instr (GValueType y)))
-> (:+:) x y p
-> Value' Instr ('TOr (GValueType x) (GValueType y))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    L1 x p
x -> Value' Instr (GValueType x)
-> Either
     (Value' Instr (GValueType x)) (Value' Instr (GValueType y))
forall a b. a -> Either a b
Left (x p -> Value' Instr (GValueType x)
forall (x :: * -> *) p. GIsoValue x => x p -> Value (GValueType x)
gToValue x p
x)
    R1 y p
y -> Value' Instr (GValueType y)
-> Either
     (Value' Instr (GValueType x)) (Value' Instr (GValueType y))
forall a b. b -> Either a b
Right (y p -> Value' Instr (GValueType y)
forall (x :: * -> *) p. GIsoValue x => x p -> Value (GValueType x)
gToValue y p
y)
  gFromValue :: forall p. Value (GValueType (x :+: y)) -> (:+:) x y p
gFromValue (VOr Either (Value' Instr l) (Value' Instr r)
e) = case Either (Value' Instr l) (Value' Instr r)
e of
    Left Value' Instr l
vx -> x p -> (:+:) x y p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (Value' Instr (GValueType x) -> x p
forall (x :: * -> *) p. GIsoValue x => Value (GValueType x) -> x p
gFromValue Value' Instr l
Value' Instr (GValueType x)
vx)
    Right Value' Instr r
vy -> y p -> (:+:) x y p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Value' Instr (GValueType y) -> y p
forall (x :: * -> *) p. GIsoValue x => Value (GValueType x) -> x p
gFromValue Value' Instr r
Value' Instr (GValueType y)
vy)

instance (GIsoValue x, GIsoValue y) => GIsoValue (x :*: y) where
  type GValueType (x :*: y) = 'TPair (GValueType x) (GValueType y)
  gToValue :: forall p. (:*:) x y p -> Value (GValueType (x :*: y))
gToValue (x p
x :*: y p
y) = (Value' Instr (GValueType x), Value' Instr (GValueType y))
-> Value' Instr ('TPair (GValueType x) (GValueType y))
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (x p -> Value' Instr (GValueType x)
forall (x :: * -> *) p. GIsoValue x => x p -> Value (GValueType x)
gToValue x p
x, y p -> Value' Instr (GValueType y)
forall (x :: * -> *) p. GIsoValue x => x p -> Value (GValueType x)
gToValue y p
y)
  gFromValue :: forall p. Value (GValueType (x :*: y)) -> (:*:) x y p
gFromValue (VPair (Value' Instr l
vx, Value' Instr r
vy)) = Value' Instr (GValueType x) -> x p
forall (x :: * -> *) p. GIsoValue x => Value (GValueType x) -> x p
gFromValue Value' Instr l
Value' Instr (GValueType x)
vx x p -> y p -> (:*:) x y p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Value' Instr (GValueType y) -> y p
forall (x :: * -> *) p. GIsoValue x => Value (GValueType x) -> x p
gFromValue Value' Instr r
Value' Instr (GValueType y)
vy

instance GIsoValue G.U1 where
  type GValueType G.U1 = 'TUnit
  gToValue :: forall p. U1 p -> Value (GValueType U1)
gToValue U1 p
G.U1 = Value (GValueType U1)
forall (instr :: [T] -> [T] -> *). Value' instr 'TUnit
VUnit
  gFromValue :: forall p. Value (GValueType U1) -> U1 p
gFromValue Value (GValueType U1)
VUnit = U1 p
forall k (p :: k). U1 p
G.U1

instance GIsoValue G.V1 where
  type GValueType G.V1 = 'TNever
  gToValue :: forall p. V1 p -> Value (GValueType V1)
gToValue = V1 p -> Value (GValueType V1)
\case
  gFromValue :: forall p. Value (GValueType V1) -> V1 p
gFromValue = Value (GValueType V1) -> V1 p
\case

instance IsoValue a => GIsoValue (G.Rec0 a) where
  type GValueType (G.Rec0 a) = ToT a
  gToValue :: forall p. Rec0 a p -> Value (GValueType (Rec0 a))
gToValue = a -> Value' Instr (ToT a)
forall a. IsoValue a => a -> Value (ToT a)
toVal (a -> Value' Instr (ToT a))
-> (K1 R a p -> a) -> K1 R a p -> Value' Instr (ToT a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 R a p -> a
forall k i c (p :: k). K1 i c p -> c
G.unK1
  gFromValue :: forall p. Value (GValueType (Rec0 a)) -> Rec0 a p
gFromValue = a -> K1 R a p
forall k i c (p :: k). c -> K1 i c p
G.K1 (a -> K1 R a p)
-> (Value' Instr (ToT a) -> a) -> Value' Instr (ToT a) -> K1 R a p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value' Instr (ToT a) -> a
forall a. IsoValue a => Value (ToT a) -> a
fromVal

-- | Whether Michelson representation of the type is derived via Generics.
type GenericIsoValue t =
  (IsoValue t, Generic t, ToT t ~ GValueType (G.Rep t))

----------------------------------------------------------------------------
-- Stacks conversion
----------------------------------------------------------------------------

-- | Type function to convert a Haskell stack type to @T@-based one.
type family ToTs (ts :: [Type]) :: [T] where
  ToTs '[] = '[]
  ToTs (x ': xs) = ToT x ': ToTs xs

-- | Overloaded version of 'ToTs' to work on Haskell and @T@ stacks.
type ToTs' :: forall k. [k] -> [T]
type family ToTs' t where
  ToTs' (t :: [T]) = t
  ToTs' (a :: [Type]) = ToTs a

-- | Isomorphism between Michelson stack and its Haskell reflection.
class IsoValuesStack (ts :: [Type]) where
  toValStack :: Rec Identity ts -> Rec Value (ToTs ts)
  fromValStack :: Rec Value (ToTs ts) -> Rec Identity ts

instance IsoValuesStack '[] where
  toValStack :: Rec Identity '[] -> Rec Value (ToTs '[])
toValStack Rec Identity '[]
RNil = Rec Value (ToTs '[])
forall {u} (a :: u -> *). Rec a '[]
RNil
  fromValStack :: Rec Value (ToTs '[]) -> Rec Identity '[]
fromValStack Rec Value (ToTs '[])
RNil = Rec Identity '[]
forall {u} (a :: u -> *). Rec a '[]
RNil

instance (IsoValue t, IsoValuesStack st) => IsoValuesStack (t ': st) where
  toValStack :: Rec Identity (t : st) -> Rec Value (ToTs (t : st))
toValStack (Identity r
v :& Rec Identity rs
vs) = Identity r -> Value (ToT (Identity r))
forall a. IsoValue a => a -> Value (ToT a)
toVal Identity r
v Value' Instr (ToT t)
-> Rec Value (ToTs st) -> Rec Value (ToT t : ToTs st)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Identity rs -> Rec Value (ToTs rs)
forall (ts :: [*]).
IsoValuesStack ts =>
Rec Identity ts -> Rec Value (ToTs ts)
toValStack Rec Identity rs
vs
  fromValStack :: Rec Value (ToTs (t : st)) -> Rec Identity (t : st)
fromValStack (Value r
v :& Rec Value rs
vs) = Value (ToT (Identity t)) -> Identity t
forall a. IsoValue a => Value (ToT a) -> a
fromVal Value r
Value (ToT (Identity t))
v Identity t -> Rec Identity st -> Rec Identity (t : st)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec Value (ToTs st) -> Rec Identity st
forall (ts :: [*]).
IsoValuesStack ts =>
Rec Value (ToTs ts) -> Rec Identity ts
fromValStack Rec Value rs
Rec Value (ToTs st)
vs

totsKnownLemma :: forall s. KnownList s :- KnownList (ToTs s)
totsKnownLemma :: forall (s :: [*]). KnownList s :- KnownList (ToTs s)
totsKnownLemma = (KnownList s => Dict (KnownList (ToTs s)))
-> KnownList s :- KnownList (ToTs s)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((KnownList s => Dict (KnownList (ToTs s)))
 -> KnownList s :- KnownList (ToTs s))
-> (KnownList s => Dict (KnownList (ToTs s)))
-> KnownList s :- KnownList (ToTs s)
forall a b. (a -> b) -> a -> b
$ case forall (l :: [*]). KnownList l => KList l
forall {k} (l :: [k]). KnownList l => KList l
klist @s of
  KList s
KNil -> Dict (KnownList (ToTs s))
forall (a :: Constraint). a => Dict a
Dict
  KCons Proxy x
_ (Proxy xs
_ :: Proxy a') ->
    case forall (s :: [*]). KnownList s :- KnownList (ToTs s)
totsKnownLemma @a' of Sub Dict (KnownList (ToTs xs))
KnownList xs => Dict (KnownList (ToTs xs))
Dict -> Dict (KnownList (ToTs s))
forall (a :: Constraint). a => Dict a
Dict

totsAppendLemma
  :: forall a b.
      (KnownList a)
  => Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma :: forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma = case forall (l :: [*]). KnownList l => KList l
forall {k} (l :: [k]). KnownList l => KList l
klist @a of
  KList a
KNil -> Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
forall (a :: Constraint). a => Dict a
Dict
  KCons Proxy x
_ (Proxy xs
_ :: Proxy a') ->
    case forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma @a' @b of Dict (ToTs (xs ++ b) ~ (ToTs xs ++ ToTs b))
Dict -> Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
forall (a :: Constraint). a => Dict a
Dict