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

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

-- | Conversions between haskell types/values and Michelson ones.
module Michelson.Typed.Haskell.Value
  ( -- * Value conversions
    IsoValue (..)
  , KnownIsoT
  , KnownT
  , GIsoValue (GValueType)
  , ToT'
  , SomeIsoValue (..)
  , AnyIsoValue (..)
  , GenericIsoValue
  , WellTyped
  , WellTypedIsoValue
  , WellTypedToT

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

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

    -- * Stack conversion
  , ToTs
  , ToTs'
  , IsoValuesStack (..)
  , totsKnownLemma
  , totsAppendLemma
  ) where

import Data.Constraint ((:-)(..), Dict(..))
import Data.Default (Default(..))
import qualified Data.Kind as Kind
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Data.Vinyl.Core (Rec(..))
import Fmt (Buildable(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import qualified GHC.Generics as G
import Named (NamedF(..))
import Test.QuickCheck (Arbitrary(..))

import Michelson.Text
import Michelson.Typed.Aliases
import Michelson.Typed.Entrypoints
import Michelson.Typed.Sing
import Michelson.Typed.T
import Michelson.Typed.Value
import Tezos.Address (Address)
import Tezos.Core (ChainId, Mutez, Timestamp)
import Tezos.Crypto (KeyHash, PublicKey, Signature)
import Util.Type

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

type KnownIsoT a = KnownT (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 (ToT a) -> Rep a Any) -> Value (ToT a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value (ToT 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 family ToT' (t :: k) :: T where
  ToT' (t :: T) = t
  ToT' (t :: Kind.Type) = ToT t

-- | Hides some Haskell value put in line with Michelson 'Value'.
data SomeIsoValue where
  SomeIsoValue :: (KnownIsoT a) => a -> SomeIsoValue

-- | Any Haskell value which can be converted to Michelson 'Value'.
newtype AnyIsoValue = AnyIsoValue (forall a. IsoValue a => a)

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

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 x :: 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 x :: 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 x :: MText
x) = MText
x

instance DoNotUseTextError => IsoValue Text where
  type ToT Text = ToT MText
  toVal :: Text -> Value (ToT Text)
toVal = Text -> Text -> Value 'TString
forall a. HasCallStack => Text -> a
error "impossible"
  fromVal :: Value (ToT Text) -> Text
fromVal = Text -> Value 'TString -> Text
forall a. HasCallStack => Text -> a
error "impossible"

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 x :: 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 x :: 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 x :: 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 x :: KeyHash
x) = KeyHash
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 x :: Timestamp
x) = Timestamp
x

instance IsoValue Address where
  type ToT Address = 'TAddress
  toVal :: Address -> Value (ToT Address)
toVal addr :: Address
addr = EpAddress -> Value (ToT Address)
forall (instr :: [T] -> [T] -> *).
EpAddress -> Value' instr 'TAddress
VAddress (EpAddress -> Value (ToT Address))
-> EpAddress -> Value (ToT Address)
forall a b. (a -> b) -> a -> b
$ Address -> EpName -> EpAddress
EpAddress Address
addr EpName
DefEpName
  fromVal :: Value (ToT Address) -> Address
fromVal (VAddress x :: 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 x :: 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 x :: 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 x :: 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 x :: ChainId
x) = ChainId
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 (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
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 x :: [Value' Instr t]
x) = (Value' Instr t -> a) -> [Value' Instr t] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map Value' Instr t -> a
forall a. IsoValue a => Value (ToT a) -> a
fromVal [Value' Instr t]
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 (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
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 x :: Maybe (Value' Instr t)
x) = (Value' Instr t -> a) -> Maybe (Value' Instr t) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Value' Instr t -> a
forall a. IsoValue a => Value (ToT a) -> a
fromVal Maybe (Value' Instr t)
x

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 (t :: T) (instr :: [T] -> [T] -> *).
(KnownT t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
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 x :: Set (Value' Instr t)
x) = (Value' Instr t -> c) -> Set (Value' Instr t) -> Set c
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Value' Instr t -> c
forall a. IsoValue a => Value (ToT a) -> a
fromVal Set (Value' Instr t)
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] -> *).
(KnownT k, KnownT 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 x :: 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 x :: Operation
x) = Operation
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 = WellTyped (ToT a)
type WellTypedIsoValue a = (WellTyped (ToT a), IsoValue 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 :: Kind.Type) = ContractRef
  { ContractRef arg -> Address
crAddress :: Address
  , 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 (WellTypedToT 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 (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 -> Value' Instr ('TContract (ToT arg))
forall (arg :: T) (instr :: [T] -> [T] -> *).
Address -> SomeEntrypointCallT arg -> Value' instr ('TContract arg)
VContract Address
crAddress SomeEntrypointCall arg
crEntrypoint
  fromVal :: Value (ToT (ContractRef arg)) -> ContractRef arg
fromVal (VContract addr :: Address
addr epc :: 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 'ContractAddr' with isomorphic one.
coerceContractRef :: (ToT a ~ ToT b) => ContractRef a -> ContractRef b
coerceContractRef :: ContractRef a -> ContractRef b
coerceContractRef ContractRef{..} = $WContractRef :: forall arg. Address -> SomeEntrypointCall arg -> ContractRef arg
ContractRef{..}

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

newtype BigMap k v = BigMap { BigMap k v -> Map k v
unBigMap :: Map k v }
  deriving stock (BigMap k v -> BigMap k v -> Bool
(BigMap k v -> BigMap k v -> Bool)
-> (BigMap k v -> BigMap k v -> Bool) -> Eq (BigMap k v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k v. (Eq k, Eq v) => BigMap k v -> BigMap k v -> Bool
/= :: BigMap k v -> BigMap k v -> Bool
$c/= :: forall k v. (Eq k, Eq v) => BigMap k v -> BigMap k v -> Bool
== :: BigMap k v -> BigMap k v -> Bool
$c== :: forall k v. (Eq k, Eq v) => BigMap k v -> BigMap k v -> Bool
Eq, 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)
  deriving newtype (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, b -> BigMap k v -> BigMap k v
NonEmpty (BigMap k v) -> BigMap k v
BigMap k v -> BigMap k v -> BigMap k v
(BigMap k v -> BigMap k v -> BigMap k v)
-> (NonEmpty (BigMap k v) -> BigMap k v)
-> (forall b. Integral b => b -> BigMap k v -> BigMap k v)
-> Semigroup (BigMap k v)
forall b. Integral b => b -> BigMap k v -> BigMap k v
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall k v. Ord k => NonEmpty (BigMap k v) -> BigMap k v
forall k v. Ord k => BigMap k v -> BigMap k v -> BigMap k v
forall k v b. (Ord k, Integral b) => b -> BigMap k v -> BigMap k v
stimes :: b -> BigMap k v -> BigMap k v
$cstimes :: forall k v b. (Ord k, Integral b) => b -> BigMap k v -> BigMap k v
sconcat :: NonEmpty (BigMap k v) -> BigMap k v
$csconcat :: forall k v. Ord k => NonEmpty (BigMap k v) -> BigMap k v
<> :: BigMap k v -> BigMap k v -> BigMap k v
$c<> :: forall k v. Ord k => BigMap k v -> BigMap k v -> BigMap k v
Semigroup, Semigroup (BigMap k v)
BigMap k v
Semigroup (BigMap k v) =>
BigMap k v
-> (BigMap k v -> BigMap k v -> BigMap k v)
-> ([BigMap k v] -> BigMap k v)
-> Monoid (BigMap k v)
[BigMap k v] -> BigMap k v
BigMap k v -> BigMap k v -> BigMap k v
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall k v. Ord k => Semigroup (BigMap k v)
forall k v. Ord k => BigMap k v
forall k v. Ord k => [BigMap k v] -> BigMap k v
forall k v. Ord k => BigMap k v -> BigMap k v -> BigMap k v
mconcat :: [BigMap k v] -> BigMap k v
$cmconcat :: forall k v. Ord k => [BigMap k v] -> BigMap k v
mappend :: BigMap k v -> BigMap k v -> BigMap k v
$cmappend :: forall k v. Ord k => BigMap k v -> BigMap k v -> BigMap k v
mempty :: BigMap k v
$cmempty :: forall k v. Ord k => BigMap k v
$cp1Monoid :: forall k v. Ord k => Semigroup (BigMap k v)
Monoid)

instance
  ( WellTypedToT k, WellTypedToT v, Comparable (ToT k)
  , Ord k, IsoValue k, IsoValue 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 = Map (Value' Instr (ToT k)) (Value' Instr (ToT v))
-> Value' Instr ('TBigMap (ToT k) (ToT v))
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap (Map (Value' Instr (ToT k)) (Value' Instr (ToT v))
 -> Value' Instr ('TBigMap (ToT k) (ToT v)))
-> (BigMap k v
    -> Map (Value' Instr (ToT k)) (Value' Instr (ToT v)))
-> BigMap k v
-> Value' Instr ('TBigMap (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)))
-> (BigMap k v -> Map k (Value' Instr (ToT v)))
-> BigMap 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 (Map k v -> Map k (Value' Instr (ToT v)))
-> (BigMap k v -> Map k v)
-> BigMap k v
-> Map k (Value' Instr (ToT v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BigMap k v -> Map k v
forall k v. BigMap k v -> Map k v
unBigMap
  fromVal :: Value (ToT (BigMap k v)) -> BigMap k v
fromVal (VBigMap x :: Map (Value' Instr k) (Value' Instr v)
x) = Map k v -> BigMap k v
forall k v. Map k v -> BigMap k v
BigMap (Map k v -> BigMap k v) -> Map k v -> BigMap k v
forall a b. (a -> b) -> a -> b
$ (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
  ( WellTypedToT k, WellTypedToT v, Comparable (ToT k), Arbitrary k
  , Arbitrary v, Ord k
  ) => Arbitrary (BigMap k v) where
  arbitrary :: Gen (BigMap k v)
arbitrary = Map k v -> BigMap k v
forall k v. Map k v -> BigMap k v
BigMap (Map k v -> BigMap k v) -> Gen (Map k v) -> Gen (BigMap k v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Map k v)
forall a. Arbitrary a => Gen a
arbitrary

-- 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 'Util.Generics' module.
class KnownT (GValueType x) =>
      GIsoValue (x :: Kind.Type -> Kind.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 :: 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 i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
  gFromValue :: 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 :: (:+:) 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] -> *).
(KnownT l, KnownT 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 :: 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 :: 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 :: Value (GValueType (x :+: y)) -> (:+:) x y p
gFromValue (VOr e :: Either (Value' Instr l) (Value' Instr r)
e) = case Either (Value' Instr l) (Value' Instr r)
e of
    Left vx :: 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 vy :: 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 :: (:*:) x y p -> Value (GValueType (x :*: y))
gToValue (x :: x p
x :*: y :: 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 :: Value (GValueType (x :*: y)) -> (:*:) x y p
gFromValue (VPair (vx :: Value' Instr l
vx, vy :: 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 :: U1 p -> Value (GValueType U1)
gToValue G.U1 = Value (GValueType U1)
forall (instr :: [T] -> [T] -> *). Value' instr 'TUnit
VUnit
  gFromValue :: Value (GValueType U1) -> U1 p
gFromValue VUnit = U1 p
forall k (p :: k). U1 p
G.U1

instance IsoValue a => GIsoValue (G.Rec0 a) where
  type GValueType (G.Rec0 a) = ToT a
  gToValue :: 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))
-> (Rec0 a p -> a) -> Rec0 a p -> Value' Instr (ToT a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec0 a p -> a
forall i c k (p :: k). K1 i c p -> c
G.unK1
  gFromValue :: 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' Instr (ToT a) -> a) -> Value' Instr (ToT a) -> Rec0 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 :: [Kind.Type]) :: [T] where
  ToTs '[] = '[]
  ToTs (x ': xs) = ToT x ': ToTs xs

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

-- | Isomorphism between Michelson stack and its Haskell reflection.
class IsoValuesStack (ts :: [Kind.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 RNil = Rec Value (ToTs '[])
forall u (a :: u -> *). Rec a '[]
RNil
  fromValStack :: Rec Value (ToTs '[]) -> Rec Identity '[]
fromValStack 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 (v :: Identity r
v :& vs :: 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 (v :: Value r
v :& vs :: 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 :: 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 KnownList s => KList s
forall k (l :: [k]). KnownList l => KList l
klist @s of
  KNil -> Dict (KnownList (ToTs s))
forall (a :: Constraint). a => Dict a
Dict
  KCons _ (Proxy xs
_ :: Proxy a') ->
    case KnownList xs :- KnownList (ToTs xs)
forall (s :: [*]). KnownList s :- KnownList (ToTs s)
totsKnownLemma @a' of Sub 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 :: Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma = case KnownList a => KList a
forall k (l :: [k]). KnownList l => KList l
klist @a of
  KNil -> Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
forall (a :: Constraint). a => Dict a
Dict
  KCons _ (Proxy xs
_ :: Proxy a') ->
    case KnownList xs => Dict (ToTs (xs ++ b) ~ (ToTs xs ++ ToTs b))
forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma @a' @b of Dict -> Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
forall (a :: Constraint). a => Dict a
Dict

-- | This class encodes Michelson rules w.r.t where it requires comparable
-- types. Earlier we had a dedicated type for representing comparable types @CT@.
-- But then we integreated those types into @T@. This meant that some of the
-- types that could be formed with various combinations of @T@ would be
-- illegal as per Michelson typing rule. Using this class, we inductively
-- enforce that a type and all types it contains are well typed as per
-- Michelson's rules.
class KnownT t => WellTyped (t :: T) where

instance WellTyped 'TKey where
instance WellTyped 'TUnit where
instance WellTyped 'TSignature where
instance WellTyped 'TChainId where
instance (WellTyped t) => WellTyped ('TOption t) where
instance (WellTyped t) => WellTyped ('TList t) where
instance (Comparable t, WellTyped t) => WellTyped ('TSet t) where
instance WellTyped 'TOperation where
instance (WellTyped t) => WellTyped ('TContract t) where
instance (WellTyped t1, WellTyped t2) => WellTyped ('TPair t1 t2)
instance (WellTyped t1, WellTyped t2) => WellTyped ('TOr t1 t2)
instance (WellTyped t1, WellTyped t2) => WellTyped ('TLambda t1 t2)
instance (Comparable k, WellTyped k, WellTyped v) => WellTyped ('TMap k v)
instance (Comparable k, WellTyped k, WellTyped v) => WellTyped ('TBigMap k v)
instance WellTyped 'TInt
instance WellTyped 'TNat
instance WellTyped 'TString
instance WellTyped 'TBytes
instance WellTyped 'TMutez
instance WellTyped 'TBool
instance WellTyped 'TKeyHash
instance WellTyped 'TTimestamp
instance WellTyped 'TAddress