-- 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.Generic
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.

Can be derived generically. If the type is missing the 'Generic' instance, a
custom error is generated.

>>> data Foo = Foo
>>> instance IsoValue Foo
...
... GHC.Generics.Rep Foo
... is stuck. Likely
... Generic Foo
... instance is missing or out of scope.
...
>>> data Foo = Foo deriving Generic
>>> instance IsoValue Foo -- ok
-}
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 (GRep a)

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

  -- | Converts a @Value@ into Haskell type.
  fromVal :: Value (ToT a) -> a
  default fromVal
    :: (NiceGeneric a, GIsoValue (GRep a), ToT a ~ GValueType (GRep a))
    => Value (ToT a) -> a
  fromVal = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
G.to (Rep a Any -> a)
-> (Value (GValueType (Rep a)) -> Rep a Any)
-> Value (GValueType (Rep a))
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value (GValueType (Rep a)) -> Rep a Any
forall p. Value (GValueType (Rep a)) -> Rep a p
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 (ToT a) -> a)
-> (b -> Value (ToT b)) -> Iso (Value (ToT a)) (Value (ToT b)) a b
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso Value (ToT a) -> a
forall a. IsoValue a => Value (ToT a) -> a
fromVal b -> Value (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 t
Value t -> Value (ToT (Value t))
forall a. a -> a
id
  fromVal :: Value (ToT (Value t)) -> Value t
fromVal = Value t -> Value t
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' Instr 'TInt
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' Instr 'TNat
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' Instr 'TString
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' Instr 'TString
Text -> Value (ToT Text)
forall a. Bottom => a
forall a. a
no
  fromVal :: Value (ToT Text) -> Text
fromVal = forall a. Bottom => a
Value' Instr 'TString -> Text
Value (ToT Text) -> Text
forall a. a
no

instance IsoValue Bool where
  type ToT Bool = 'TBool
  toVal :: Bool -> Value (ToT Bool)
toVal = Bool -> Value' Instr 'TBool
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' Instr 'TBytes
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' Instr 'TMutez
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' Instr 'TKeyHash
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' Instr 'TBls12381Fr
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' Instr 'TBls12381G1
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' Instr 'TBls12381G2
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' Instr 'TTimestamp
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' Instr 'TAddress
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' Instr 'TKey
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' Instr 'TSignature
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' Instr 'TChainId
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
Value' Instr (ToT a) -> 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 a b. (a -> b) -> Maybe a -> Maybe b
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 a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value' Instr t1 -> a
Value' Instr (ToT a) -> 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] -> *).
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
Value' Instr (ToT c) -> 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 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
Value' Instr (ToT 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
Value' Instr (ToT 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' Instr 'TOperation
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' Instr 'TChest
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' Instr 'TChestKey
ChestKey -> Value (ToT ChestKey)
forall (instr :: [T] -> [T] -> *).
ChestKey -> Value' instr 'TChestKey
VChestKey
  fromVal :: Value (ToT ChestKey) -> ChestKey
fromVal (VChestKey ChestKey
x) = ChestKey
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, ForbidOp (ToT a))
type HasNoBigMapToT a = (IsoValue a, ForbidBigMap (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
$c== :: forall arg. ContractRef arg -> ContractRef arg -> Bool
== :: ContractRef arg -> ContractRef arg -> Bool
$c/= :: forall arg. ContractRef arg -> ContractRef arg -> Bool
/= :: 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
$cshowsPrec :: forall arg. Int -> ContractRef arg -> ShowS
showsPrec :: Int -> ContractRef arg -> ShowS
$cshow :: forall arg. ContractRef arg -> String
show :: ContractRef arg -> String
$cshowList :: forall arg. [ContractRef arg] -> ShowS
showList :: [ContractRef arg] -> ShowS
Show)

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

instance (HasNoOpToT arg, ForbidNestedBigMaps (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
crAddress :: forall arg. ContractRef arg -> Address
crEntrypoint :: forall arg. ContractRef arg -> SomeEntrypointCall arg
crAddress :: Address
crEntrypoint :: SomeEntrypointCall arg
..} = Address
-> SomeEntrypointCall arg -> Value' Instr ('TContract (ToT arg))
forall (arg :: T) (instr :: [T] -> [T] -> *).
(SingI arg, ForbidOp 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
crAddress :: forall arg. ContractRef arg -> Address
crEntrypoint :: forall arg. ContractRef arg -> SomeEntrypointCall arg
crAddress :: Address
crEntrypoint :: SomeEntrypointCall a
..} = ContractRef{Address
SomeEntrypointCall a
SomeEntrypointCall b
crAddress :: Address
crEntrypoint :: SomeEntrypointCall b
crAddress :: Address
crEntrypoint :: SomeEntrypointCall a
..}

contractRefToAddr :: ContractRef cp -> EpAddress
contractRefToAddr :: forall cp. ContractRef cp -> EpAddress
contractRefToAddr ContractRef{Address
SomeEntrypointCall cp
crAddress :: forall arg. ContractRef arg -> Address
crEntrypoint :: forall arg. ContractRef arg -> SomeEntrypointCall arg
crAddress :: Address
crEntrypoint :: SomeEntrypointCall cp
..} = 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
$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
/= :: 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
$cshowsPrec :: forall arg. Show arg => Int -> Ticket arg -> ShowS
showsPrec :: Int -> Ticket arg -> ShowS
$cshow :: forall arg. Show arg => Ticket arg -> String
show :: Ticket arg -> String
$cshowList :: forall arg. Show arg => [Ticket arg] -> ShowS
showList :: [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
tTicketer :: forall arg. Ticket arg -> Address
tData :: forall arg. Ticket arg -> arg
tAmount :: forall arg. Ticket arg -> Natural
tTicketer :: Address
tData :: a
tAmount :: Natural
..} = 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{ 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
tTicketer :: Address
tAmount :: Natural
tTicketer :: Address
tAmount :: Natural
.. }

-- | 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
$cshowsPrec :: forall k (k :: k) k (v :: k). Int -> BigMapId k v -> ShowS
showsPrec :: Int -> BigMapId k v -> ShowS
$cshow :: forall k (k :: k) k (v :: k). BigMapId k v -> String
show :: BigMapId k v -> String
$cshowList :: forall k (k :: k) k (v :: k). [BigMapId k v] -> ShowS
showList :: [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 -> Constr
BigMapId k v -> DataType
(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 -> Constr
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) =>
(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))
$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)
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)
$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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BigMapId k v)
$ctoConstr :: forall k (k :: k) k (v :: k).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
BigMapId k v -> Constr
toConstr :: BigMapId k v -> Constr
$cdataTypeOf :: forall k (k :: k) k (v :: k).
(Typeable k, Typeable v, Typeable k, Typeable k) =>
BigMapId k v -> DataType
dataTypeOf :: BigMapId k v -> DataType
$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))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (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
gmapT :: (forall b. Data b => b -> b) -> BigMapId k v -> BigMapId k v
$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
gmapQl :: 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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BigMapId k v -> r
$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]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BigMapId k v -> u
$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)
gmapM :: forall (m :: * -> *).
Monad 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)
gmapMp :: 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BigMapId k v -> m (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))
$ctoVal :: forall k (k :: k) k (v :: k).
BigMapId k v -> Value (ToT (BigMapId k v))
toVal :: BigMapId k v -> Value (ToT (BigMapId k v))
$cfromVal :: forall k (k :: k) k (v :: k).
Value (ToT (BigMapId k v)) -> BigMapId k v
fromVal :: Value (ToT (BigMapId k v)) -> BigMapId k v
IsoValue, [BigMapId k v] -> Doc
BigMapId k v -> Doc
(BigMapId k v -> Doc)
-> ([BigMapId k v] -> Doc) -> Buildable (BigMapId k v)
forall a. (a -> Doc) -> ([a] -> Doc) -> Buildable a
forall k (k :: k) k (v :: k). [BigMapId k v] -> Doc
forall k (k :: k) k (v :: k). BigMapId k v -> Doc
$cbuild :: forall k (k :: k) k (v :: k). BigMapId k v -> Doc
build :: BigMapId k v -> Doc
$cbuildList :: forall k (k :: k) k (v :: k). [BigMapId k v] -> Doc
buildList :: [BigMapId k v] -> Doc
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
$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
* :: BigMapId k v -> BigMapId k v -> BigMapId k v
$cnegate :: forall k (k :: k) k (v :: k). BigMapId k v -> BigMapId k v
negate :: BigMapId k v -> BigMapId k v
$cabs :: forall k (k :: k) k (v :: k). BigMapId k v -> BigMapId k v
abs :: BigMapId k v -> BigMapId k v
$csignum :: forall k (k :: k) k (v :: k). BigMapId k v -> BigMapId k v
signum :: BigMapId k v -> BigMapId k v
$cfromInteger :: forall k (k :: k) k (v :: k). Integer -> BigMapId k v
fromInteger :: Integer -> 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
$cshowsPrec :: forall k v. (Show k, Show v) => Int -> BigMap k v -> ShowS
showsPrec :: Int -> BigMap k v -> ShowS
$cshow :: forall k v. (Show k, Show v) => BigMap k v -> String
show :: BigMap k v -> String
$cshowList :: forall k v. (Show k, Show v) => [BigMap k v] -> ShowS
showList :: [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
$cfrom :: forall k v x. BigMap k v -> Rep (BigMap k v) x
from :: forall x. BigMap k v -> Rep (BigMap k v) x
$cto :: forall k v x. Rep (BigMap k v) x -> BigMap k v
to :: forall x. Rep (BigMap k v) x -> BigMap k v
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 -> Constr
BigMap k v -> DataType
(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 -> Constr
forall k v. (Data k, Data v, Ord k) => BigMap k v -> DataType
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))
$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)
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)
$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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BigMap k v)
$ctoConstr :: forall k v. (Data k, Data v, Ord k) => BigMap k v -> Constr
toConstr :: BigMap k v -> Constr
$cdataTypeOf :: forall k v. (Data k, Data v, Ord k) => BigMap k v -> DataType
dataTypeOf :: BigMap k v -> DataType
$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))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (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
gmapT :: (forall b. Data b => b -> b) -> BigMap k v -> BigMap k v
$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
gmapQl :: 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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BigMap k v -> r
$cgmapQ :: forall k v u.
(Data k, Data v, Ord k) =>
(forall d. Data d => d -> u) -> BigMap k v -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BigMap k v -> u
$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)
gmapM :: forall (m :: * -> *).
Monad 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)
gmapMp :: 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BigMap k v -> m (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
$cdef :: forall k v. BigMap k v
def :: 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
$ctoList :: forall k v. BigMap k v -> [Element (BigMap k v)]
toList :: BigMap k v -> [Element (BigMap k v)]
$cnull :: forall k v. BigMap k v -> Bool
null :: BigMap k v -> Bool
$cfoldr :: forall k v b.
(Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b
foldr :: forall b. (Element (BigMap k v) -> b -> 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
foldl' :: forall b. (b -> Element (BigMap k v) -> b) -> b -> BigMap k v -> b
$clength :: forall k v. BigMap k v -> Int
length :: BigMap k v -> Int
$celem :: forall k v.
Eq (Element (BigMap k v)) =>
Element (BigMap k v) -> BigMap k v -> Bool
elem :: Eq (Element (BigMap k v)) =>
Element (BigMap k v) -> BigMap k v -> Bool
$cfoldMap :: forall k v m.
Monoid m =>
(Element (BigMap k v) -> m) -> BigMap k v -> m
foldMap :: forall m.
Monoid m =>
(Element (BigMap k v) -> m) -> BigMap k v -> m
$cfold :: forall k v.
Monoid (Element (BigMap k v)) =>
BigMap k v -> Element (BigMap k v)
fold :: Monoid (Element (BigMap k v)) => BigMap k v -> Element (BigMap k v)
$cfoldr' :: forall k v b.
(Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b
foldr' :: forall b. (Element (BigMap k v) -> b -> b) -> b -> BigMap k v -> b
$cnotElem :: forall k v.
Eq (Element (BigMap k v)) =>
Element (BigMap k v) -> BigMap k v -> Bool
notElem :: Eq (Element (BigMap k v)) =>
Element (BigMap k v) -> BigMap k v -> Bool
$call :: forall k v. (Element (BigMap k v) -> Bool) -> BigMap k v -> Bool
all :: (Element (BigMap k v) -> Bool) -> BigMap k v -> Bool
$cany :: forall k v. (Element (BigMap k v) -> Bool) -> BigMap k v -> Bool
any :: (Element (BigMap k v) -> Bool) -> BigMap k v -> Bool
$cand :: forall k v. (Element (BigMap k v) ~ Bool) => BigMap k v -> Bool
and :: (Element (BigMap k v) ~ Bool) => BigMap k v -> Bool
$cor :: forall k v. (Element (BigMap k v) ~ Bool) => BigMap k v -> Bool
or :: (Element (BigMap k v) ~ Bool) => BigMap k v -> Bool
$cfind :: forall k v.
(Element (BigMap k v) -> Bool)
-> BigMap k v -> Maybe (Element (BigMap k v))
find :: (Element (BigMap k v) -> Bool)
-> BigMap k v -> Maybe (Element (BigMap k v))
$csafeHead :: forall k v. BigMap k v -> Maybe (Element (BigMap k v))
safeHead :: 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))
safeMaximum :: 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))
safeMinimum :: Ord (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))
safeFoldr1 :: (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))
safeFoldl1 :: (Element (BigMap k v)
 -> Element (BigMap k v) -> Element (BigMap k v))
-> BigMap k v -> Maybe (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)])
[Item (BigMap k v)] -> BigMap 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
[Item (BigMap 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)]
SizedList' n (k, v) -> [Element (SizedList' n (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 -> Doc
build = BigMap k v -> Doc
forall k v f.
(Buildable k, Buildable v, IsList f, Item f ~ (k, v)) =>
f -> Doc
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 v, Comparable k, ForbidBigMap 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
Value' Instr (ToT 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
Value' Instr (ToT 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 (GValueType x)
forall p. x p -> Value (GValueType x)
forall (x :: * -> *) p. GIsoValue x => x p -> Value (GValueType x)
gToValue (x p -> Value (GValueType x))
-> (M1 t i x p -> x p) -> M1 t i x p -> Value (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 (GValueType x) -> x p)
-> Value (GValueType x)
-> M1 t i x p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value (GValueType x) -> x p
forall p. Value (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 p. 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 p. 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 p. 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 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 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 p. 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 p. 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 p. 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 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' Instr 'TUnit
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, SingI (ToT 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 (ToT a)
forall a. IsoValue a => a -> Value (ToT a)
toVal (a -> Value (ToT a))
-> (Rec0 a p -> a) -> Rec0 a p -> Value (ToT a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec0 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 -> Rec0 a p
forall k i c (p :: k). c -> K1 i c p
G.K1 (a -> Rec0 a p)
-> (Value (ToT a) -> a) -> Value (ToT a) -> Rec0 a p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value (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, NiceGeneric t, ToT t ~ GValueType (GRep 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 '[]
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 '[])
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 (ToT x : ToTs xs))
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 b ~ ToTs b)
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
  ((ToT x : (ToTs xs ++ ToTs b)) ~ (ToT x : (ToTs xs ++ ToTs b)))
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
forall (a :: Constraint). a => Dict a
Dict