{-# LANGUAGE DeriveAnyClass, DerivingStrategies #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Lorentz.Store
(
Store (..)
, type (|->)
, GetStoreKey
, GetStoreValue
, storeMem
, storeGet
, storeInsert
, storeInsertNew
, storeDelete
, StoreMemC
, StoreGetC
, StoreInsertC
, StoreDeleteC
, HasStore
, HasStoreForAllIn
, StorageSkeleton (..)
, storageUnpack
, storagePack
, storageMem
, storageGet
, storageInsert
, storageInsertNew
, storageDelete
, storePiece
, storeLookup
, StorePieceC
) where
import Data.Constraint (Dict(..))
import Data.Default (Default)
import qualified Data.Kind as Kind
import qualified Data.Map as Map
import Data.Singletons (SingI)
import Data.Type.Bool (If, type (||))
import Data.Type.Equality (type (==))
import Data.Vinyl.Derived (Label)
import GHC.Generics ((:+:))
import qualified GHC.Generics as G
import GHC.TypeLits (AppendSymbol, ErrorMessage(..), KnownSymbol, Symbol, TypeError)
import GHC.TypeNats (type (+))
import Type.Reflection ((:~:)(Refl))
import Lorentz.ADT
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Instr
import Lorentz.Macro
import Michelson.Interpret.Pack
import Michelson.Typed.Haskell.Instr.Sum
import Michelson.Typed.Haskell.Value
import Michelson.Typed.Instr
import Michelson.Typed.Scope
{-# ANN module ("HLint: ignore Use 'natVal' from Universum" :: Text) #-}
newtype Store a = Store { unStore :: BigMap ByteString a }
deriving stock (Eq, Show)
deriving newtype (Default, Semigroup, Monoid, IsoValue)
data k |-> v = BigMapImage v
deriving stock Generic
deriving anyclass IsoValue
type CtorIdx = Nat
type CtorsNum = Nat
data MapSignature = MapSignature Kind.Type Kind.Type CtorIdx
type family MSKey ms where
MSKey ('MapSignature k _ _) = k
type family MSValue ms where
MSValue ('MapSignature _ v _) = v
type family MSCtorIdx ms where
MSCtorIdx ('MapSignature _ _ ci) = ci
type GetStore name a = MSRequireFound name a (GLookupStore name (G.Rep a))
data MapLookupRes
= MapFound MapSignature
| MapAbsent CtorsNum
type family MSRequireFound
(name :: Symbol)
(a :: Kind.Type)
(mlr :: MapLookupRes)
:: MapSignature where
MSRequireFound _ _ ('MapFound ms) = ms
MSRequireFound name a ('MapAbsent _) = TypeError
('Text "Failed to find store template: datatype " ':<>: 'ShowType a ':<>:
'Text " has no constructor " ':<>: 'ShowType name)
type CtorNameToLabel name = "c" `AppendSymbol` name
type family GLookupStore (name :: Symbol) (x :: Kind.Type -> Kind.Type)
:: MapLookupRes where
GLookupStore name (G.D1 _ x) = GLookupStore name x
GLookupStore name (x :+: y) = LSMergeFound name (GLookupStore name x)
(GLookupStore name y)
GLookupStore name (G.C1 ('G.MetaCons ctorName _ _) x) =
If (IsLeafCtor x)
(If (name == ctorName || name == CtorNameToLabel ctorName)
('MapFound $ GExtractMapSignature ctorName x)
('MapAbsent 1)
)
(GLookupStoreDeeper name x)
GLookupStore _ G.V1 = 'MapAbsent 0
type family IsLeafCtor (x :: Kind.Type -> Kind.Type) :: Bool where
IsLeafCtor (G.S1 _ (G.Rec0 (_ |-> _))) = 'True
IsLeafCtor _ = 'False
type family GLookupStoreDeeper (name :: Symbol) (x :: Kind.Type -> Kind.Type)
:: MapLookupRes where
GLookupStoreDeeper name (G.S1 _ (G.Rec0 y)) = GLookupStore name (G.Rep y)
GLookupStoreDeeper name _ = TypeError
('Text "Attempt to go deeper failed while looking for" ':<>: 'ShowType name
':$$:
'Text "Make sure that all constructors have exactly one field inside.")
type family LSMergeFound (name :: Symbol)
(f1 :: MapLookupRes) (f2 :: MapLookupRes)
:: MapLookupRes where
LSMergeFound _ ('MapAbsent n1) ('MapAbsent n2) = 'MapAbsent (n1 + n2)
LSMergeFound _ ('MapFound ms) ('MapAbsent _) = 'MapFound ms
LSMergeFound _ ('MapAbsent n) ('MapFound ('MapSignature k v i)) =
'MapFound ('MapSignature k v (n + i))
LSMergeFound ctor ('MapFound _) ('MapFound _) = TypeError
('Text "Found more than one constructor matching " ':<>: 'ShowType ctor)
type family GExtractMapSignature (ctor :: Symbol) (x :: Kind.Type -> Kind.Type)
:: MapSignature where
GExtractMapSignature _ (G.S1 _ (G.Rec0 (k |-> v))) = 'MapSignature k v 0
GExtractMapSignature ctor _ = TypeError
('Text "Expected exactly one field of type `k |-> v`" ':$$:
'Text "In constructor " ':<>: 'ShowType ctor)
type GetStoreKey store name = MSKey (GetStore name store)
type GetStoreValue store name = MSValue (GetStore name store)
packKey
:: forall (idx :: CtorIdx) t s.
(KnownNat idx, Typeable t, SingI t, HasNoOp t, HasNoBigMap t)
=> Instr (t : s) (ToT ByteString : s)
packKey =
PUSH (toVal . natVal $ Proxy @idx) `Seq`
PAIR @(ToT Natural) @t `Seq`
PACK
type StoreOpC store name =
( Each [Typeable, SingI, HasNoOp, HasNoBigMap] '[ToT (MSKey (GetStore name store))]
, KnownNat (MSCtorIdx (GetStore name store))
)
storeMem
:: forall store name s.
(StoreMemC store name)
=> Label name
-> GetStoreKey store name : Store store : s :-> Bool : s
storeMem _ = I $
packKey @(MSCtorIdx (GetStore name store)) `Seq`
MEM
type StoreMemC store name = StoreOpC store name
storeGet
:: forall store name s.
StoreGetC store name
=> Label name
-> GetStoreKey store name : Store store : s
:-> Maybe (GetStoreValue store name) : s
storeGet label = I $
packKey @(MSCtorIdx (GetStore name store)) `Seq`
GET `Seq`
IF_NONE (NONE) (instrUnwrapUnsafe @store label `Seq` SOME)
type StoreGetC store name =
( StoreOpC store name
, InstrUnwrapC store name
, SingI (ToT (GetStoreValue store name))
, CtorHasOnlyField name store
(GetStoreKey store name |-> GetStoreValue store name)
)
storeInsert
:: forall store name s.
StoreInsertC store name
=> Label name
-> GetStoreKey store name
: GetStoreValue store name
: Store store
: s
:-> Store store : s
storeInsert label = I $
packKey @(MSCtorIdx (GetStore name store)) `Seq`
DIP (instrWrap @store label `Seq` SOME) `Seq`
UPDATE
type StoreInsertC store name =
( StoreOpC store name
, InstrWrapC store name
, CtorHasOnlyField name store
(GetStoreKey store name |-> GetStoreValue store name)
)
storeInsertNew
:: forall store name err s.
(StoreInsertC store name, KnownSymbol name, KnownValue err)
=> Label name
-> (forall s0. GetStoreKey store name : s0 :-> err : s0)
-> GetStoreKey store name
: GetStoreValue store name
: Store store
: s
:-> Store store : s
storeInsertNew label mkErr =
duupX @3 # duupX @2 # storeMem label #
if_ (mkErr # failWith)
(storeInsert label)
storeDelete
:: forall store name s.
( StoreDeleteC store name
)
=> Label name
-> GetStoreKey store name : Store store : s
:-> Store store : s
storeDelete _ = I $
packKey @(MSCtorIdx (GetStore name store)) `Seq`
DIP (NONE @(ToT store)) `Seq`
UPDATE
type StoreDeleteC store name =
( StoreOpC store name
, SingI (ToT store)
)
type HasStore name key value store =
( StoreGetC store name
, StoreInsertC store name
, StoreDeleteC store name
, GetStoreKey store name ~ key
, GetStoreValue store name ~ value
, StorePieceC store name key value
)
type HasStoreForAllIn store constrained =
GForAllHasStore constrained (G.Rep store)
type family GForAllHasStore (store :: Kind.Type) (x :: Kind.Type -> Kind.Type)
:: Constraint where
GForAllHasStore store (G.D1 _ x) = GForAllHasStore store x
GForAllHasStore store (x :+: y) = ( GForAllHasStore store x
, GForAllHasStore store y )
GForAllHasStore store (G.C1 ('G.MetaCons ctorName _ _)
(G.S1 _ (G.Rec0 (key |-> value)))) =
HasStore (CtorNameToLabel ctorName) key value store
GForAllHasStore _ (G.C1 _ _) = ()
GForAllHasStore _ G.V1 = ()
data MyStoreTemplate
= IntsStore (Integer |-> ())
| BytesStore (ByteString |-> ByteString)
deriving stock Generic
deriving anyclass IsoValue
type MyStore = Store MyStoreTemplate
_sample1 :: Integer : MyStore : s :-> MyStore : s
_sample1 = storeDelete @MyStoreTemplate #cIntsStore
_sample2 :: ByteString : ByteString : MyStore : s :-> MyStore : s
_sample2 = storeInsert @MyStoreTemplate #cBytesStore
data MyStoreTemplate2
= BoolsStore (Bool |-> Bool)
| IntsStore2 (Integer |-> Integer)
| IntsStore3 (Integer |-> Bool)
deriving stock Generic
deriving anyclass IsoValue
newtype MyNatural = MyNatural Natural
deriving stock Generic
deriving newtype (IsoCValue, IsoValue)
data MyStoreTemplate3 = MyStoreTemplate3 (Natural |-> MyNatural)
deriving stock Generic
deriving anyclass IsoValue
data MyStoreTemplateBig
= BigTemplatePart1 MyStoreTemplate
| BigTemplatePart2 MyStoreTemplate2
| BigTemplatePart3 MyStoreTemplate3
deriving stock Generic
deriving anyclass IsoValue
_MyStoreTemplateBigTextsStore ::
GetStore "cBytesStore" MyStoreTemplateBig :~: 'MapSignature ByteString ByteString 1
_MyStoreTemplateBigTextsStore = Refl
_MyStoreTemplateBigBoolsStore ::
GetStore "cBoolsStore" MyStoreTemplateBig :~: 'MapSignature Bool Bool 2
_MyStoreTemplateBigBoolsStore = Refl
_MyStoreTemplateBigMyStoreTemplate3 ::
GetStore "cMyStoreTemplate3" MyStoreTemplateBig :~: 'MapSignature Natural MyNatural 5
_MyStoreTemplateBigMyStoreTemplate3 = Refl
_MyStoreBigHasAllStores
:: HasStoreForAllIn MyStoreTemplate store
=> Dict ( HasStore "cIntsStore" Integer () store
, HasStore "cBytesStore" ByteString ByteString store
)
_MyStoreBigHasAllStores = Dict
type MyStoreBig = Store MyStoreTemplateBig
_sample3 :: Integer : MyStoreBig : s :-> MyStoreBig : s
_sample3 = storeDelete @MyStoreTemplateBig #cIntsStore2
_sample4 :: ByteString : MyStoreBig : s :-> Bool : s
_sample4 = storeMem @MyStoreTemplateBig #cBytesStore
_sample5 :: Natural : MyNatural : MyStoreBig : s :-> MyStoreBig : s
_sample5 = storeInsert @MyStoreTemplateBig #cMyStoreTemplate3
_sample6
:: forall store s.
HasStoreForAllIn MyStoreTemplate3 store
=> Natural : MyNatural : Store store : s :-> Store store : s
_sample6 = storeInsert @store #cMyStoreTemplate3
_sample6' :: Natural : MyNatural : MyStoreBig : s :-> MyStoreBig : s
_sample6' = _sample6
data StorageSkeleton storeTemplate other = StorageSkeleton
{ sMap :: Store storeTemplate
, sFields :: other
} deriving stock (Eq, Show, Generic)
deriving anyclass (Default, IsoValue)
storageUnpack :: StorageSkeleton store fields : s :-> (Store store, fields) : s
storageUnpack = coerce_
storagePack :: (Store store, fields) : s :-> StorageSkeleton store fields : s
storagePack = coerce_
storageMem
:: forall store name fields s.
(StoreMemC store name)
=> Label name
-> GetStoreKey store name : StorageSkeleton store fields : s :-> Bool : s
storageMem label = dip (storageUnpack # car) # storeMem label
storageGet
:: forall store name fields s.
StoreGetC store name
=> Label name
-> GetStoreKey store name : StorageSkeleton store fields : s
:-> Maybe (GetStoreValue store name) : s
storageGet label = dip (storageUnpack # car) # storeGet label
storageInsert
:: forall store name fields s.
StoreInsertC store name
=> Label name
-> GetStoreKey store name
: GetStoreValue store name
: StorageSkeleton store fields
: s
:-> StorageSkeleton store fields : s
storageInsert label =
dip (dip (storageUnpack # dup # car # dip cdr)) #
storeInsert label #
pair # storagePack
storageInsertNew
:: forall store name fields err s.
(StoreInsertC store name, KnownSymbol name, KnownValue err)
=> Label name
-> (forall s0. GetStoreKey store name : s0 :-> err : s0)
-> GetStoreKey store name
: GetStoreValue store name
: StorageSkeleton store fields
: s
:-> StorageSkeleton store fields : s
storageInsertNew label mkErr =
dip (dip (storageUnpack # dup # car # dip cdr)) #
storeInsertNew label mkErr #
pair # storagePack
storageDelete
:: forall store name fields s.
( StoreDeleteC store name
)
=> Label name
-> GetStoreKey store name : StorageSkeleton store fields : s
:-> StorageSkeleton store fields : s
storageDelete label =
dip (storageUnpack # dup # car # dip cdr) #
storeDelete label #
pair # storagePack
type MyStorage = StorageSkeleton MyStoreTemplate (Integer, ByteString)
_storageSample1 :: Integer : MyStorage : s :-> MyStorage : s
_storageSample1 = storageDelete @MyStoreTemplate #cIntsStore
_storageSample2 :: MyStorage : s :-> Integer : s
_storageSample2 = toField #sFields # car
packHsKey
:: forall ctorIdx key.
( IsoValue key, KnownValue key, HasNoOp (ToT key), HasNoBigMap (ToT key)
, KnownNat ctorIdx
)
=> key -> ByteString
packHsKey key =
packValue' $ toVal (natVal (Proxy @ctorIdx), key)
storePiece
:: forall name store key value.
StorePieceC store name key value
=> Label name
-> key
-> value
-> Store store
storePiece label key val =
Store . BigMap $ one
( packHsKey @(MSCtorIdx (GetStore name store)) key
, hsWrap @store label (BigMapImage val)
)
type StorePieceC store name key value =
( key ~ GetStoreKey store name
, value ~ GetStoreValue store name
, IsoValue key, KnownValue key, HasNoOp (ToT key), HasNoBigMap (ToT key)
, KnownNat (MSCtorIdx (GetStore name store))
, InstrWrapC store name, Generic store
, ExtractCtorField (GetCtorField store name) ~ (key |-> value)
)
storeLookup
:: forall name store key value ctorIdx.
( key ~ GetStoreKey store name
, value ~ GetStoreValue store name
, ctorIdx ~ MSCtorIdx (GetStore name store)
, IsoValue key, KnownValue key, HasNoOp (ToT key), HasNoBigMap (ToT key)
, KnownNat ctorIdx
, InstrUnwrapC store name, Generic store
, CtorOnlyField name store ~ (key |-> value)
)
=> Label name
-> key
-> Store store
-> Maybe value
storeLookup label key (Store (BigMap m)) =
Map.lookup (packHsKey @ctorIdx key) m <&> \val ->
case hsUnwrap label val of
Nothing -> error "Invalid store, keys and values types \
\correspondence is violated"
Just (BigMapImage x) -> x
_storeSample :: Store MyStoreTemplate
_storeSample = mconcat
[ storePiece #cIntsStore 1 ()
, storePiece #cBytesStore "a" "b"
]
_lookupSample :: Maybe ByteString
_lookupSample = storeLookup #cBytesStore "a" _storeSample
_storeSampleBig :: Store MyStoreTemplateBig
_storeSampleBig = mconcat
[ storePiece #cIntsStore 1 ()
, storePiece #cBoolsStore True True
, storePiece #cIntsStore3 2 False
]
_lookupSampleBig :: Maybe Bool
_lookupSampleBig = storeLookup #cIntsStore3 2 _storeSampleBig