{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Lorentz.StoreClass
(
FieldRefKind
, FieldRefTag
, KnownFieldRef (..)
, FieldName
, FieldRef
, FieldSymRef
, fieldNameToLabel
, fieldNameFromLabel
, FieldRefHasFinalName (..)
, StoreHasField (..)
, StoreFieldOps (..)
, StoreHasSubmap (..)
, StoreSubmapOps (..)
, StoreHasEntrypoint (..)
, StoreEntrypointOps (..)
, EntrypointLambda
, EntrypointsField
, type (~>)
, type (::->)
, StorageContains
, stToField
, stGetField
, stToFieldNamed
, stGetFieldNamed
, stSetField
, stMem
, stGet
, stUpdate
, stGetAndUpdate
, stDelete
, stInsert
, stInsertNew
, stEntrypoint
, stToEpLambda
, stGetEpLambda
, stSetEpLambda
, stToEpStore
, stGetEpStore
, stSetEpStore
, sopGetField
, sopSetField
, storeFieldOpsADT
, storeEntrypointOpsADT
, storeEntrypointOpsFields
, storeEntrypointOpsSubmapField
, storeFieldOpsDeeper
, storeSubmapOpsDeeper
, storeEntrypointOpsDeeper
, storeFieldOpsReferTo
, storeSubmapOpsReferTo
, mapStoreFieldOps
, mapStoreSubmapOpsKey
, mapStoreSubmapOpsValue
, storeEntrypointOpsReferTo
, composeStoreFieldOps
, composeStoreSubmapOps
, sequenceStoreSubmapOps
, composeStoreEntrypointOps
, zoomStoreSubmapOps
, mkStoreEp
, (:-|)(..)
, SelfRef (..)
, this
, stNested
, FieldAlias
, stAlias
, FieldNickname
, stNickname
) where
import Data.Kind qualified as Kind
import GHC.Records qualified as GHC
import GHC.TypeLits (KnownSymbol, Symbol)
import Lorentz.ADT
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Errors (failUnexpected)
import Lorentz.Ext
import Lorentz.Instr qualified as L
import Lorentz.Iso
import Lorentz.Lambda
import Lorentz.Macro qualified as L
import Lorentz.Value
import Morley.Michelson.Text (labelToMText)
type FieldRefKind = FieldRefTag -> Kind.Type
data FieldRefTag = FieldRefTag
class KnownFieldRef (ty :: k) where
type FieldRefObject ty = (fr :: FieldRefKind) | fr -> ty
mkFieldRef :: FieldRefObject ty p
type FieldRef name = FieldRefObject name 'FieldRefTag
data FieldName (n :: Symbol) (p :: FieldRefTag) =
KnownSymbol n => FieldName
instance (x ~ FieldName name, KnownSymbol name) =>
IsLabel name (x p) where
fromLabel :: x p
fromLabel = x p
FieldName name p
forall (n :: Symbol) (p :: FieldRefTag).
KnownSymbol n =>
FieldName n p
FieldName
instance (KnownSymbol field, y ~ FieldRefObject (SelfRef :-| field), p ~ 'FieldRefTag)
=> GHC.HasField field (SelfRef p) (y p) where
getField :: SelfRef p -> y p
getField SelfRef p
l = SelfRef p
FieldRefObject SelfRef 'FieldRefTag
l FieldRefObject SelfRef 'FieldRefTag
-> FieldRef field -> (:-|) SelfRef field p
forall k1 k2 (l :: k1) (r :: k2) (p :: FieldRefTag).
FieldRef l -> FieldRef r -> (:-|) l r p
:-| FieldName field 'FieldRefTag
FieldRef field
forall (n :: Symbol) (p :: FieldRefTag).
KnownSymbol n =>
FieldName n p
FieldName
instance (KnownSymbol field, y ~ FieldRefObject ((l :-| r) :-| field), p ~ 'FieldRefTag)
=> GHC.HasField field ((l :-| r) p) (y p) where
getField :: (:-|) l r p -> y p
getField (:-|) l r p
l = (:-|) l r p
FieldRefObject (l :-| r) 'FieldRefTag
l FieldRefObject (l :-| r) 'FieldRefTag
-> FieldRef field -> (:-|) (l :-| r) field p
forall k1 k2 (l :: k1) (r :: k2) (p :: FieldRefTag).
FieldRef l -> FieldRef r -> (:-|) l r p
:-| FieldName field 'FieldRefTag
FieldRef field
forall (n :: Symbol) (p :: FieldRefTag).
KnownSymbol n =>
FieldName n p
FieldName
instance KnownSymbol name => KnownFieldRef (name :: Symbol) where
type FieldRefObject name = FieldName name
mkFieldRef :: forall (p :: FieldRefTag). FieldRefObject name p
mkFieldRef = FieldName name p
FieldRefObject name p
forall (n :: Symbol) (p :: FieldRefTag).
KnownSymbol n =>
FieldName n p
FieldName
type FieldSymRef name = FieldRef (name :: Symbol)
fieldNameToLabel :: FieldSymRef n -> Label n
fieldNameToLabel :: forall (n :: Symbol). FieldSymRef n -> Label n
fieldNameToLabel FieldName n 'FieldRefTag
FieldSymRef n
FieldName = Label n
forall (name :: Symbol). KnownSymbol name => Label name
Label
fieldNameFromLabel :: Label n -> FieldSymRef n
fieldNameFromLabel :: forall (n :: Symbol). Label n -> FieldSymRef n
fieldNameFromLabel Label n
Label = FieldName n 'FieldRefTag
FieldRefObject n 'FieldRefTag
forall (n :: Symbol) (p :: FieldRefTag).
KnownSymbol n =>
FieldName n p
FieldName
class FieldRefHasFinalName fr where
type FieldRefFinalName fr :: Symbol
fieldRefFinalName :: FieldRef fr -> Label (FieldRefFinalName fr)
instance FieldRefHasFinalName (name :: Symbol) where
type FieldRefFinalName name = name
fieldRefFinalName :: FieldRef name -> Label (FieldRefFinalName name)
fieldRefFinalName = FieldRef name -> Label name
FieldRef name -> Label (FieldRefFinalName name)
forall (n :: Symbol). FieldSymRef n -> Label n
fieldNameToLabel
data StoreFieldOps store fname ftype = StoreFieldOps
{ forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField
:: forall s.
FieldRef fname -> store : s :-> ftype : s
, forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall res (s :: [*]).
HasDupableGetters store =>
('[ftype] :-> '[res, ftype])
-> ('[ftype] :-> '[res])
-> FieldRef fname
-> (store : s) :-> (res : store : s)
sopGetFieldOpen
:: forall res s. (HasDupableGetters store)
=> '[ftype] :-> '[res, ftype]
-> '[ftype] :-> '[res]
-> FieldRef fname -> store : s :-> res : store : s
, forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall new (s :: [*]).
('[new, ftype] :-> '[ftype])
-> FieldRef fname -> (new : store : s) :-> (store : s)
sopSetFieldOpen
:: forall new s.
'[new, ftype] :-> '[ftype]
-> FieldRef fname -> new : store : s :-> store : s
}
sopGetField
:: (Dupable ftype, HasDupableGetters store)
=> StoreFieldOps store fname ftype
-> FieldRef fname -> store : s :-> ftype : store : s
sopGetField :: forall {k} ftype store (fname :: k) (s :: [*]).
(Dupable ftype, HasDupableGetters store) =>
StoreFieldOps store fname ftype
-> FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField StoreFieldOps store fname ftype
ops = StoreFieldOps store fname ftype
-> forall res (s :: [*]).
HasDupableGetters store =>
('[ftype] :-> '[res, ftype])
-> ('[ftype] :-> '[res])
-> FieldRefObject fname 'FieldRefTag
-> (store : s) :-> (res : store : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall res (s :: [*]).
HasDupableGetters store =>
('[ftype] :-> '[res, ftype])
-> ('[ftype] :-> '[res])
-> FieldRef fname
-> (store : s) :-> (res : store : s)
sopGetFieldOpen StoreFieldOps store fname ftype
ops '[ftype] :-> '[ftype, ftype]
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup '[ftype] :-> '[ftype]
forall (s :: [*]). s :-> s
L.nop
sopSetField
:: StoreFieldOps store fname ftype
-> FieldRef fname -> ftype : store : s :-> store : s
sopSetField :: forall {k} store (fname :: k) ftype (s :: [*]).
StoreFieldOps store fname ftype
-> FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store fname ftype
ops = StoreFieldOps store fname ftype
-> forall new (s :: [*]).
('[new, ftype] :-> '[ftype])
-> FieldRefObject fname 'FieldRefTag
-> (new : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall new (s :: [*]).
('[new, ftype] :-> '[ftype])
-> FieldRef fname -> (new : store : s) :-> (store : s)
sopSetFieldOpen StoreFieldOps store fname ftype
ops (('[ftype] :-> '[]) -> '[ftype, ftype] :-> '[ftype]
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip '[ftype] :-> '[]
forall a (s :: [*]). (a : s) :-> s
L.drop)
class StoreHasField store fname ftype | store fname -> ftype where
storeFieldOps :: StoreFieldOps store fname ftype
instance {-# OVERLAPPABLE #-}
HasFieldOfType store fname ftype =>
StoreHasField store fname ftype where
storeFieldOps :: StoreFieldOps store fname ftype
storeFieldOps = StoreFieldOps store fname ftype
forall store (fname :: Symbol) ftype.
HasFieldOfType store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOpsADT
stToField
:: StoreHasField store fname ftype
=> FieldRef fname -> store : s :-> ftype : s
stToField :: forall {k} store (fname :: k) ftype (s :: [*]).
StoreHasField store fname ftype =>
FieldRef fname -> (store : s) :-> (ftype : s)
stToField = StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store fname ftype
forall {k} store (fname :: k) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps
stGetField
:: (StoreHasField store fname ftype, Dupable ftype, HasDupableGetters store)
=> FieldRef fname -> store : s :-> ftype : store : s
stGetField :: forall {k} store (fname :: k) ftype (s :: [*]).
(StoreHasField store fname ftype, Dupable ftype,
HasDupableGetters store) =>
FieldRef fname -> (store : s) :-> (ftype : store : s)
stGetField FieldRef fname
l = StoreFieldOps store fname ftype
-> FieldRef fname -> (store : s) :-> (ftype : store : s)
forall {k} ftype store (fname :: k) (s :: [*]).
(Dupable ftype, HasDupableGetters store) =>
StoreFieldOps store fname ftype
-> FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField StoreFieldOps store fname ftype
forall {k} store (fname :: k) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps FieldRef fname
l
stToFieldNamed
:: (StoreHasField store fname ftype, FieldRefHasFinalName fname)
=> FieldRef fname -> store : s :-> (FieldRefFinalName fname :! ftype) : s
stToFieldNamed :: forall {k} store (fname :: k) ftype (s :: [*]).
(StoreHasField store fname ftype, FieldRefHasFinalName fname) =>
FieldRef fname
-> (store : s) :-> ((FieldRefFinalName fname :! ftype) : s)
stToFieldNamed FieldRef fname
fr = FieldRef fname -> (store : s) :-> (ftype : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreHasField store fname ftype =>
FieldRef fname -> (store : s) :-> (ftype : s)
stToField FieldRef fname
fr ((store : s) :-> (ftype : s))
-> ((ftype : s)
:-> (NamedF Identity ftype (FieldRefFinalName fname) : s))
-> (store : s)
:-> (NamedF Identity ftype (FieldRefFinalName fname) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label (FieldRefFinalName fname)
-> (ftype : s)
:-> (NamedF Identity ftype (FieldRefFinalName fname) : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed (FieldRef fname -> Label (FieldRefFinalName fname)
forall {k} (fr :: k).
FieldRefHasFinalName fr =>
FieldRef fr -> Label (FieldRefFinalName fr)
fieldRefFinalName FieldRef fname
fr)
stGetFieldNamed
:: ( StoreHasField store fname ftype, FieldRefHasFinalName fname
, Dupable ftype, HasDupableGetters store
)
=> FieldRef fname -> store : s :-> (FieldRefFinalName fname :! ftype) : store : s
stGetFieldNamed :: forall {k} store (fname :: k) ftype (s :: [*]).
(StoreHasField store fname ftype, FieldRefHasFinalName fname,
Dupable ftype, HasDupableGetters store) =>
FieldRef fname
-> (store : s) :-> ((FieldRefFinalName fname :! ftype) : store : s)
stGetFieldNamed FieldRef fname
fr = FieldRef fname -> (store : s) :-> (ftype : store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
(StoreHasField store fname ftype, Dupable ftype,
HasDupableGetters store) =>
FieldRef fname -> (store : s) :-> (ftype : store : s)
stGetField FieldRef fname
fr ((store : s) :-> (ftype : store : s))
-> ((ftype : store : s)
:-> (NamedF Identity ftype (FieldRefFinalName fname) : store : s))
-> (store : s)
:-> (NamedF Identity ftype (FieldRefFinalName fname) : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label (FieldRefFinalName fname)
-> (ftype : store : s)
:-> (NamedF Identity ftype (FieldRefFinalName fname) : store : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed (FieldRef fname -> Label (FieldRefFinalName fname)
forall {k} (fr :: k).
FieldRefHasFinalName fr =>
FieldRef fr -> Label (FieldRefFinalName fr)
fieldRefFinalName FieldRef fname
fr)
stSetField
:: (StoreHasField store fname ftype)
=> FieldRef fname -> ftype : store : s :-> store : s
stSetField :: forall {k} store (fname :: k) ftype (s :: [*]).
StoreHasField store fname ftype =>
FieldRef fname -> (ftype : store : s) :-> (store : s)
stSetField = StoreFieldOps store fname ftype
-> FieldRefObject fname 'FieldRefTag
-> (ftype : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreFieldOps store fname ftype
-> FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store fname ftype
forall {k} store (fname :: k) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps
data StoreSubmapOps store mname key value = StoreSubmapOps
{ forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
sopMem
:: forall s.
FieldRef mname -> key : store : s :-> Bool : s
, forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet
:: forall s.
(KnownValue value)
=> FieldRef mname -> key : store : s :-> Maybe value : s
, forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate
:: forall s.
FieldRef mname -> key : Maybe value : store : s :-> store : s
, forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopGetAndUpdate
:: forall s.
FieldRef mname -> key : Maybe value : store : s :-> Maybe value : store : s
, forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopDelete
:: forall s.
FieldRef mname -> key : store : s :-> store : s
, forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopInsert
:: forall s.
FieldRef mname -> key : value : store : s :-> store : s
}
class StoreHasSubmap store mname key value | store mname -> key value where
storeSubmapOps :: StoreSubmapOps store mname key value
instance ( StoreHasField store name submap
, StoreHasSubmap submap SelfRef key value
, KnownSymbol name
, HasDupableGetters store, Dupable submap
) => StoreHasSubmap store (name :: Symbol) key value where
storeSubmapOps :: StoreSubmapOps store name key value
storeSubmapOps = FieldRef (name :-| SelfRef)
-> StoreSubmapOps store (name :-| SelfRef) key value
-> StoreSubmapOps store name key value
forall {k} {k} (name :: k) storage key value (desiredName :: k).
FieldRef name
-> StoreSubmapOps storage name key value
-> StoreSubmapOps storage desiredName key value
storeSubmapOpsReferTo (forall (x :: Symbol) a. IsLabel x a => a
fromLabel @name FieldRefObject name 'FieldRefTag
-> FieldRefObject SelfRef 'FieldRefTag
-> (:-|) name SelfRef 'FieldRefTag
forall k1 k2 (l :: k1) (r :: k2) (p :: FieldRefTag).
FieldRef l -> FieldRef r -> (:-|) l r p
:-| SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
forall (p :: FieldRefTag). SelfRef p
this) StoreSubmapOps store (name :-| SelfRef) key value
forall {k} store (mname :: k) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps
stMem
:: StoreHasSubmap store mname key value
=> FieldRef mname -> key : store : s :-> Bool : s
stMem :: forall {k} store (mname :: k) key value (s :: [*]).
StoreHasSubmap store mname key value =>
FieldRef mname -> (key : store : s) :-> (Bool : s)
stMem = StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
sopMem StoreSubmapOps store mname key value
forall {k} store (mname :: k) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps
stGet
:: (StoreHasSubmap store mname key value, KnownValue value)
=> FieldRef mname -> key : store : s :-> Maybe value : s
stGet :: forall {k} store (mname :: k) key value (s :: [*]).
(StoreHasSubmap store mname key value, KnownValue value) =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
stGet = StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps store mname key value
forall {k} store (mname :: k) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps
stUpdate
:: StoreHasSubmap store mname key value
=> FieldRef mname -> key : Maybe value : store : s :-> store : s
stUpdate :: forall {k} store (mname :: k) key value (s :: [*]).
StoreHasSubmap store mname key value =>
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
stUpdate = StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps store mname key value
forall {k} store (mname :: k) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps
stGetAndUpdate
:: StoreHasSubmap store mname key value
=> FieldRef mname -> key : Maybe value : store : s :-> Maybe value : store : s
stGetAndUpdate :: forall {k} store (mname :: k) key value (s :: [*]).
StoreHasSubmap store mname key value =>
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
stGetAndUpdate = StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopGetAndUpdate StoreSubmapOps store mname key value
forall {k} store (mname :: k) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps
stDelete
:: forall store mname key value s.
(StoreHasSubmap store mname key value)
=> FieldRef mname -> key : store : s :-> store : s
stDelete :: forall {k} store (mname :: k) key value (s :: [*]).
StoreHasSubmap store mname key value =>
FieldRef mname -> (key : store : s) :-> (store : s)
stDelete = StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopDelete StoreSubmapOps store mname key value
forall {k} store (mname :: k) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps
stInsert
:: StoreHasSubmap store mname key value
=> FieldRef mname -> key : value : store : s :-> store : s
stInsert :: forall {k} store (mname :: k) key value (s :: [*]).
StoreHasSubmap store mname key value =>
FieldRef mname -> (key : value : store : s) :-> (store : s)
stInsert = StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopInsert StoreSubmapOps store mname key value
forall {k} store (mname :: k) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps
stInsertNew
:: (StoreHasSubmap store mname key value, Dupable key)
=> FieldRef mname
-> (forall s0 any. key : s0 :-> any)
-> key : value : store : s
:-> store : s
stInsertNew :: forall {k} store (mname :: k) key value (s :: [*]).
(StoreHasSubmap store mname key value, Dupable key) =>
FieldRef mname
-> (forall (s0 :: [*]) (any :: [*]). (key : s0) :-> any)
-> (key : value : store : s) :-> (store : s)
stInsertNew FieldRef mname
l forall (s0 :: [*]) (any :: [*]). (key : s0) :-> any
doFail =
((value : store : s) :-> (Maybe value : store : s))
-> (key : value : store : s) :-> (key : Maybe value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (value : store : s) :-> (Maybe value : store : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
L.some ((key : value : store : s) :-> (key : Maybe value : store : s))
-> ((key : Maybe value : store : s)
:-> (key : key : Maybe value : store : s))
-> (key : value : store : s)
:-> (key : key : Maybe value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key : Maybe value : store : s)
:-> (key : key : Maybe value : store : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup ((key : value : store : s)
:-> (key : key : Maybe value : store : s))
-> ((key : key : Maybe value : store : s)
:-> (key : Maybe value : store : s))
-> (key : value : store : s) :-> (key : Maybe value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((key : Maybe value : store : s) :-> (Maybe value : store : s))
-> (key : key : Maybe value : store : s)
:-> (key : Maybe value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
forall {k} store (mname :: k) key value (s :: [*]).
StoreHasSubmap store mname key value =>
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
stGetAndUpdate FieldRef mname
l) ((key : value : store : s) :-> (key : Maybe value : store : s))
-> ((key : Maybe value : store : s)
:-> (Maybe value : key : store : s))
-> (key : value : store : s) :-> (Maybe value : key : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key : Maybe value : store : s) :-> (Maybe value : key : store : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap ((key : value : store : s) :-> (Maybe value : key : store : s))
-> ((Maybe value : key : store : s) :-> (store : s))
-> (key : value : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((key : store : s) :-> (store : s))
-> ((value : key : store : s) :-> (store : s))
-> (Maybe value : key : store : s) :-> (store : s)
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
L.ifNone (key : store : s) :-> (store : s)
forall a (s :: [*]). (a : s) :-> s
L.drop ((value : key : store : s) :-> (key : store : s)
forall a (s :: [*]). (a : s) :-> s
L.drop ((value : key : store : s) :-> (key : store : s))
-> ((key : store : s) :-> (store : s))
-> (value : key : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key : store : s) :-> (store : s)
forall (s0 :: [*]) (any :: [*]). (key : s0) :-> any
doFail)
type EntrypointLambda param store = Lambda (param, store) ([Operation], store)
type EntrypointsField param store = BigMap MText (EntrypointLambda param store)
data StoreEntrypointOps store epName epParam epStore = StoreEntrypointOps
{ forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopToEpLambda
:: forall s.
Label epName
-> store : s :-> (EntrypointLambda epParam epStore) : s
, forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda
:: forall s. (HasDupableGetters store)
=> Label epName
-> (EntrypointLambda epParam epStore) : store : s :-> store : s
, forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore
:: forall s.
Label epName
-> store : s :-> epStore : s
, forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore
:: forall s.
Label epName
-> epStore : store : s :-> store : s
}
class StoreHasEntrypoint store epName epParam epStore | store epName -> epParam epStore where
storeEpOps :: StoreEntrypointOps store epName epParam epStore
stEntrypoint
:: (StoreHasEntrypoint store epName epParam epStore, Dupable store)
=> Label epName -> epParam : store : s :-> ([Operation], store) : s
stEntrypoint :: forall store (epName :: Symbol) epParam epStore (s :: [*]).
(StoreHasEntrypoint store epName epParam epStore, Dupable store) =>
Label epName
-> (epParam : store : s) :-> (([Operation], store) : s)
stEntrypoint Label epName
l =
((store : s)
:-> (epStore : EntrypointLambda epParam epStore : store : s))
-> (epParam : store : s)
:-> (epParam
: epStore : EntrypointLambda epParam epStore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (Label epName -> (store : s) :-> (epStore : store : s)
forall store (epName :: Symbol) epParam epStore (s :: [*]).
(StoreHasEntrypoint store epName epParam epStore, Dupable store) =>
Label epName -> (store : s) :-> (epStore : store : s)
stGetEpStore Label epName
l ((store : s) :-> (epStore : store : s))
-> ((epStore : store : s)
:-> (epStore : EntrypointLambda epParam epStore : store : s))
-> (store : s)
:-> (epStore : EntrypointLambda epParam epStore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((store : s) :-> (EntrypointLambda epParam epStore : store : s))
-> (epStore : store : s)
:-> (epStore : EntrypointLambda epParam epStore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : store : s)
forall store (epName :: Symbol) epParam epStore (s :: [*]).
(StoreHasEntrypoint store epName epParam epStore, Dupable store) =>
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : store : s)
stGetEpLambda Label epName
l)) ((epParam : store : s)
:-> (epParam
: epStore : EntrypointLambda epParam epStore : store : s))
-> ((epParam
: epStore : EntrypointLambda epParam epStore : store : s)
:-> ((epParam, epStore)
: EntrypointLambda epParam epStore : store : s))
-> (epParam : store : s)
:-> ((epParam, epStore)
: EntrypointLambda epParam epStore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(epParam : epStore : EntrypointLambda epParam epStore : store : s)
:-> ((epParam, epStore)
: EntrypointLambda epParam epStore : store : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
L.pair ((epParam : store : s)
:-> ((epParam, epStore)
: EntrypointLambda epParam epStore : store : s))
-> (((epParam, epStore)
: EntrypointLambda epParam epStore : store : s)
:-> (([Operation], epStore) : store : s))
-> (epParam : store : s) :-> (([Operation], epStore) : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((epParam, epStore) : EntrypointLambda epParam epStore : store : s)
:-> (([Operation], epStore) : store : s)
forall a b (s :: [*]). (a : Lambda a b : s) :-> (b : s)
L.exec ((epParam : store : s) :-> (([Operation], epStore) : store : s))
-> ((([Operation], epStore) : store : s)
:-> ([Operation] : epStore : store : s))
-> (epParam : store : s) :-> ([Operation] : epStore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (([Operation], epStore) : store : s)
:-> ([Operation] : epStore : store : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
L.unpair ((epParam : store : s) :-> ([Operation] : epStore : store : s))
-> (([Operation] : epStore : store : s)
:-> ([Operation] : store : s))
-> (epParam : store : s) :-> ([Operation] : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((epStore : store : s) :-> (store : s))
-> ([Operation] : epStore : store : s)
:-> ([Operation] : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (Label epName -> (epStore : store : s) :-> (store : s)
forall store (epName :: Symbol) epParam epStore (s :: [*]).
StoreHasEntrypoint store epName epParam epStore =>
Label epName -> (epStore : store : s) :-> (store : s)
stSetEpStore Label epName
l) ((epParam : store : s) :-> ([Operation] : store : s))
-> (([Operation] : store : s) :-> (([Operation], store) : s))
-> (epParam : store : s) :-> (([Operation], store) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ([Operation] : store : s) :-> (([Operation], store) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
L.pair
stToEpLambda
:: StoreHasEntrypoint store epName epParam epStore
=> Label epName -> store : s :-> (EntrypointLambda epParam epStore) : s
stToEpLambda :: forall store (epName :: Symbol) epParam epStore (s :: [*]).
StoreHasEntrypoint store epName epParam epStore =>
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
stToEpLambda = StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopToEpLambda StoreEntrypointOps store epName epParam epStore
forall store (epName :: Symbol) epParam epStore.
StoreHasEntrypoint store epName epParam epStore =>
StoreEntrypointOps store epName epParam epStore
storeEpOps
stGetEpLambda
:: (StoreHasEntrypoint store epName epParam epStore, Dupable store)
=> Label epName -> store : s :-> (EntrypointLambda epParam epStore) : store : s
stGetEpLambda :: forall store (epName :: Symbol) epParam epStore (s :: [*]).
(StoreHasEntrypoint store epName epParam epStore, Dupable store) =>
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : store : s)
stGetEpLambda Label epName
l = (store : s) :-> (store : store : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup ((store : s) :-> (store : store : s))
-> ((store : store : s)
:-> (EntrypointLambda epParam epStore : store : s))
-> (store : s) :-> (EntrypointLambda epParam epStore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label epName
-> (store : store : s)
:-> (EntrypointLambda epParam epStore : store : s)
forall store (epName :: Symbol) epParam epStore (s :: [*]).
StoreHasEntrypoint store epName epParam epStore =>
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
stToEpLambda Label epName
l
stSetEpLambda
:: (StoreHasEntrypoint store epName epParam epStore, HasDupableGetters store)
=> Label epName -> (EntrypointLambda epParam epStore) : store : s :-> store : s
stSetEpLambda :: forall store (epName :: Symbol) epParam epStore (s :: [*]).
(StoreHasEntrypoint store epName epParam epStore,
HasDupableGetters store) =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
stSetEpLambda = StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda StoreEntrypointOps store epName epParam epStore
forall store (epName :: Symbol) epParam epStore.
StoreHasEntrypoint store epName epParam epStore =>
StoreEntrypointOps store epName epParam epStore
storeEpOps
stToEpStore
:: StoreHasEntrypoint store epName epParam epStore
=> Label epName -> store : s :-> epStore : s
stToEpStore :: forall store (epName :: Symbol) epParam epStore (s :: [*]).
StoreHasEntrypoint store epName epParam epStore =>
Label epName -> (store : s) :-> (epStore : s)
stToEpStore = StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore StoreEntrypointOps store epName epParam epStore
forall store (epName :: Symbol) epParam epStore.
StoreHasEntrypoint store epName epParam epStore =>
StoreEntrypointOps store epName epParam epStore
storeEpOps
stGetEpStore
:: (StoreHasEntrypoint store epName epParam epStore, Dupable store)
=> Label epName -> store : s :-> epStore : store : s
stGetEpStore :: forall store (epName :: Symbol) epParam epStore (s :: [*]).
(StoreHasEntrypoint store epName epParam epStore, Dupable store) =>
Label epName -> (store : s) :-> (epStore : store : s)
stGetEpStore Label epName
l = (store : s) :-> (store : store : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup ((store : s) :-> (store : store : s))
-> ((store : store : s) :-> (epStore : store : s))
-> (store : s) :-> (epStore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label epName -> (store : store : s) :-> (epStore : store : s)
forall store (epName :: Symbol) epParam epStore (s :: [*]).
StoreHasEntrypoint store epName epParam epStore =>
Label epName -> (store : s) :-> (epStore : s)
stToEpStore Label epName
l
stSetEpStore
:: StoreHasEntrypoint store epName epParam epStore
=> Label epName -> epStore : store : s :-> store : s
stSetEpStore :: forall store (epName :: Symbol) epParam epStore (s :: [*]).
StoreHasEntrypoint store epName epParam epStore =>
Label epName -> (epStore : store : s) :-> (store : s)
stSetEpStore = StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore StoreEntrypointOps store epName epParam epStore
forall store (epName :: Symbol) epParam epStore.
StoreHasEntrypoint store epName epParam epStore =>
StoreEntrypointOps store epName epParam epStore
storeEpOps
storeFieldOpsADT
:: HasFieldOfType dt fname ftype
=> StoreFieldOps dt (fname :: Symbol) ftype
storeFieldOpsADT :: forall store (fname :: Symbol) ftype.
HasFieldOfType store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOpsADT = StoreFieldOps
{ sopToField :: forall (s :: [*]). FieldRef fname -> (dt : s) :-> (ftype : s)
sopToField = Label fname -> (dt : s) :-> (ftype : s)
Label fname -> (dt : s) :-> (GetFieldType dt fname : s)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField (Label fname -> (dt : s) :-> (ftype : s))
-> (FieldName fname 'FieldRefTag -> Label fname)
-> FieldName fname 'FieldRefTag
-> (dt : s) :-> (ftype : s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldName fname 'FieldRefTag -> Label fname
FieldRef fname -> Label fname
forall (n :: Symbol). FieldSymRef n -> Label n
fieldNameToLabel
, sopGetFieldOpen :: forall res (s :: [*]).
HasDupableGetters dt =>
('[ftype] :-> '[res, ftype])
-> ('[ftype] :-> '[res])
-> FieldRef fname
-> (dt : s) :-> (res : dt : s)
sopGetFieldOpen = \'[ftype] :-> '[res, ftype]
cont1 '[ftype] :-> '[res]
cont2 FieldRef fname
l ->
('[GetFieldType dt fname] :-> '[res, GetFieldType dt fname])
-> ('[GetFieldType dt fname] :-> '[res])
-> Label fname
-> (dt : s) :-> (res : dt : s)
forall dt (name :: Symbol) res (st :: [*]).
(InstrGetFieldC dt name, HasDupableGetters dt) =>
('[GetFieldType dt name] :-> '[res, GetFieldType dt name])
-> ('[GetFieldType dt name] :-> '[res])
-> Label name
-> (dt : st) :-> (res : dt : st)
getFieldOpen '[ftype] :-> '[res, ftype]
'[GetFieldType dt fname] :-> '[res, GetFieldType dt fname]
cont1 '[ftype] :-> '[res]
'[GetFieldType dt fname] :-> '[res]
cont2 (FieldRef fname -> Label fname
forall (n :: Symbol). FieldSymRef n -> Label n
fieldNameToLabel FieldRef fname
l)
, sopSetFieldOpen :: forall new (s :: [*]).
('[new, ftype] :-> '[ftype])
-> FieldRef fname -> (new : dt : s) :-> (dt : s)
sopSetFieldOpen = \'[new, ftype] :-> '[ftype]
cont FieldRef fname
l ->
('[new, GetFieldType dt fname] :-> '[GetFieldType dt fname])
-> Label fname -> (new : dt : s) :-> (dt : s)
forall dt (name :: Symbol) new (st :: [*]).
InstrSetFieldC dt name =>
('[new, GetFieldType dt name] :-> '[GetFieldType dt name])
-> Label name -> (new : dt : st) :-> (dt : st)
setFieldOpen '[new, ftype] :-> '[ftype]
'[new, GetFieldType dt fname] :-> '[GetFieldType dt fname]
cont (FieldRef fname -> Label fname
forall (n :: Symbol). FieldSymRef n -> Label n
fieldNameToLabel FieldRef fname
l)
}
storeEntrypointOpsADT
:: ( HasFieldOfType store epmName (EntrypointsField epParam epStore)
, HasFieldOfType store epsName epStore
, KnownValue epParam, KnownValue epStore
)
=> Label epmName -> Label epsName
-> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsADT :: forall store (epmName :: Symbol) epParam epStore
(epsName :: Symbol) (epName :: Symbol).
(HasFieldOfType store epmName (EntrypointsField epParam epStore),
HasFieldOfType store epsName epStore, KnownValue epParam,
KnownValue epStore) =>
Label epmName
-> Label epsName -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsADT Label epmName
mapLabel Label epsName
fieldLabel = StoreEntrypointOps
{ sopToEpLambda :: forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopToEpLambda = \Label epName
l -> Label epmName -> (store : s) :-> (GetFieldType store epmName : s)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField Label epmName
mapLabel ((store : s) :-> (EntrypointsField epParam epStore : s))
-> ((EntrypointsField epParam epStore : s)
:-> (MText : EntrypointsField epParam epStore : s))
-> (store : s) :-> (MText : EntrypointsField epParam epStore : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label epName
-> (EntrypointsField epParam epStore : s)
:-> (MText : EntrypointsField epParam epStore : s)
forall (name :: Symbol) (s :: [*]). Label name -> s :-> (MText : s)
pushStEp Label epName
l ((store : s) :-> (MText : EntrypointsField epParam epStore : s))
-> ((MText : EntrypointsField epParam epStore : s)
:-> (Maybe (EntrypointLambda epParam epStore) : s))
-> (store : s) :-> (Maybe (EntrypointLambda epParam epStore) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (MText : EntrypointsField epParam epStore : s)
:-> (Maybe (EntrypointLambda epParam epStore) : s)
(GetOpKeyHs (EntrypointsField epParam epStore)
: EntrypointsField epParam epStore : s)
:-> (Maybe (GetOpValHs (EntrypointsField epParam epStore)) : s)
forall c (s :: [*]).
(GetOpHs c, KnownValue (GetOpValHs c)) =>
(GetOpKeyHs c : c : s) :-> (Maybe (GetOpValHs c) : s)
L.get ((store : s) :-> (Maybe (EntrypointLambda epParam epStore) : s))
-> ((Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s))
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label epName
-> (Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s)
forall (epName :: Symbol) epParam epStore (s :: [*]).
Label epName
-> (Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s)
someStEp Label epName
l
, sopSetEpLambda :: forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda = \Label epName
l -> ((store : s) :-> (EntrypointsField epParam epStore : store : s))
-> (EntrypointLambda epParam epStore : store : s)
:-> (EntrypointLambda epParam epStore
: EntrypointsField epParam epStore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (Label epmName
-> (store : s) :-> (GetFieldType store epmName : store : s)
forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable (GetFieldType dt name),
HasDupableGetters dt) =>
Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
getField Label epmName
mapLabel) ((EntrypointLambda epParam epStore : store : s)
:-> (EntrypointLambda epParam epStore
: EntrypointsField epParam epStore : store : s))
-> ((EntrypointLambda epParam epStore
: EntrypointsField epParam epStore : store : s)
:-> (EntrypointsField epParam epStore : store : s))
-> (EntrypointLambda epParam epStore : store : s)
:-> (EntrypointsField epParam epStore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRefObject SelfRef 'FieldRefTag
-> Label epName
-> (EntrypointLambda epParam epStore
: EntrypointsField epParam epStore : store : s)
:-> (EntrypointsField epParam epStore : store : s)
forall {k} store (epmName :: k) epParam epStore (epsName :: Symbol)
(s :: [*]).
StoreHasSubmap
store epmName MText (EntrypointLambda epParam epStore) =>
FieldRef epmName
-> Label epsName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
setStEp SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
forall (p :: FieldRefTag). SelfRef p
this Label epName
l ((EntrypointLambda epParam epStore : store : s)
:-> (EntrypointsField epParam epStore : store : s))
-> ((EntrypointsField epParam epStore : store : s) :-> (store : s))
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label epmName
-> (GetFieldType store epmName : store : s) :-> (store : s)
forall dt (name :: Symbol) (st :: [*]).
InstrSetFieldC dt name =>
Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
setField Label epmName
mapLabel
, sopToEpStore :: forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore = \Label epName
_l -> Label epsName -> (store : s) :-> (GetFieldType store epsName : s)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField Label epsName
fieldLabel
, sopSetEpStore :: forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore = \Label epName
_l -> Label epsName
-> (GetFieldType store epsName : store : s) :-> (store : s)
forall dt (name :: Symbol) (st :: [*]).
InstrSetFieldC dt name =>
Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
setField Label epsName
fieldLabel
}
storeEntrypointOpsFields
:: ( StoreHasField store epmName (EntrypointsField epParam epStore)
, StoreHasField store epsName epStore
, KnownValue epParam, KnownValue epStore
)
=> Label epmName -> Label epsName
-> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsFields :: forall store (epmName :: Symbol) epParam epStore
(epsName :: Symbol) (epName :: Symbol).
(StoreHasField store epmName (EntrypointsField epParam epStore),
StoreHasField store epsName epStore, KnownValue epParam,
KnownValue epStore) =>
Label epmName
-> Label epsName -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsFields Label epmName
mapLabel Label epsName
fieldLabel = StoreEntrypointOps
{ sopToEpLambda :: forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopToEpLambda = \Label epName
l ->
FieldRef epmName
-> (store : s) :-> (EntrypointsField epParam epStore : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreHasField store fname ftype =>
FieldRef fname -> (store : s) :-> (ftype : s)
stToField (Label epmName -> FieldRef epmName
forall (n :: Symbol). Label n -> FieldSymRef n
fieldNameFromLabel Label epmName
mapLabel) ((store : s) :-> (EntrypointsField epParam epStore : s))
-> ((EntrypointsField epParam epStore : s)
:-> (MText : EntrypointsField epParam epStore : s))
-> (store : s) :-> (MText : EntrypointsField epParam epStore : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label epName
-> (EntrypointsField epParam epStore : s)
:-> (MText : EntrypointsField epParam epStore : s)
forall (name :: Symbol) (s :: [*]). Label name -> s :-> (MText : s)
pushStEp Label epName
l ((store : s) :-> (MText : EntrypointsField epParam epStore : s))
-> ((MText : EntrypointsField epParam epStore : s)
:-> (Maybe (EntrypointLambda epParam epStore) : s))
-> (store : s) :-> (Maybe (EntrypointLambda epParam epStore) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (MText : EntrypointsField epParam epStore : s)
:-> (Maybe (EntrypointLambda epParam epStore) : s)
(GetOpKeyHs (EntrypointsField epParam epStore)
: EntrypointsField epParam epStore : s)
:-> (Maybe (GetOpValHs (EntrypointsField epParam epStore)) : s)
forall c (s :: [*]).
(GetOpHs c, KnownValue (GetOpValHs c)) =>
(GetOpKeyHs c : c : s) :-> (Maybe (GetOpValHs c) : s)
L.get ((store : s) :-> (Maybe (EntrypointLambda epParam epStore) : s))
-> ((Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s))
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label epName
-> (Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s)
forall (epName :: Symbol) epParam epStore (s :: [*]).
Label epName
-> (Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s)
someStEp Label epName
l
, sopSetEpLambda :: forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda = \Label epName
l ->
((store : s) :-> (EntrypointsField epParam epStore : store : s))
-> (EntrypointLambda epParam epStore : store : s)
:-> (EntrypointLambda epParam epStore
: EntrypointsField epParam epStore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (FieldRef epmName
-> (store : s) :-> (EntrypointsField epParam epStore : store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
(StoreHasField store fname ftype, Dupable ftype,
HasDupableGetters store) =>
FieldRef fname -> (store : s) :-> (ftype : store : s)
stGetField (FieldRef epmName
-> (store : s) :-> (EntrypointsField epParam epStore : store : s))
-> FieldRef epmName
-> (store : s) :-> (EntrypointsField epParam epStore : store : s)
forall a b. (a -> b) -> a -> b
$ Label epmName -> FieldRef epmName
forall (n :: Symbol). Label n -> FieldSymRef n
fieldNameFromLabel Label epmName
mapLabel) ((EntrypointLambda epParam epStore : store : s)
:-> (EntrypointLambda epParam epStore
: EntrypointsField epParam epStore : store : s))
-> ((EntrypointLambda epParam epStore
: EntrypointsField epParam epStore : store : s)
:-> (EntrypointsField epParam epStore : store : s))
-> (EntrypointLambda epParam epStore : store : s)
:-> (EntrypointsField epParam epStore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRefObject SelfRef 'FieldRefTag
-> Label epName
-> (EntrypointLambda epParam epStore
: EntrypointsField epParam epStore : store : s)
:-> (EntrypointsField epParam epStore : store : s)
forall {k} store (epmName :: k) epParam epStore (epsName :: Symbol)
(s :: [*]).
StoreHasSubmap
store epmName MText (EntrypointLambda epParam epStore) =>
FieldRef epmName
-> Label epsName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
setStEp SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
forall (p :: FieldRefTag). SelfRef p
this Label epName
l ((EntrypointLambda epParam epStore : store : s)
:-> (EntrypointsField epParam epStore : store : s))
-> ((EntrypointsField epParam epStore : store : s) :-> (store : s))
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
FieldRef epmName
-> (EntrypointsField epParam epStore : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreHasField store fname ftype =>
FieldRef fname -> (ftype : store : s) :-> (store : s)
stSetField (Label epmName -> FieldRef epmName
forall (n :: Symbol). Label n -> FieldSymRef n
fieldNameFromLabel Label epmName
mapLabel)
, sopToEpStore :: forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore = \Label epName
_l ->
FieldRef epsName -> (store : s) :-> (epStore : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreHasField store fname ftype =>
FieldRef fname -> (store : s) :-> (ftype : s)
stToField (FieldRef epsName -> (store : s) :-> (epStore : s))
-> FieldRef epsName -> (store : s) :-> (epStore : s)
forall a b. (a -> b) -> a -> b
$ Label epsName -> FieldRef epsName
forall (n :: Symbol). Label n -> FieldSymRef n
fieldNameFromLabel Label epsName
fieldLabel
, sopSetEpStore :: forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore = \Label epName
_l ->
FieldRef epsName -> (epStore : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreHasField store fname ftype =>
FieldRef fname -> (ftype : store : s) :-> (store : s)
stSetField (FieldRef epsName -> (epStore : store : s) :-> (store : s))
-> FieldRef epsName -> (epStore : store : s) :-> (store : s)
forall a b. (a -> b) -> a -> b
$ Label epsName -> FieldRef epsName
forall (n :: Symbol). Label n -> FieldSymRef n
fieldNameFromLabel Label epsName
fieldLabel
}
storeEntrypointOpsSubmapField
:: ( StoreHasSubmap store epmName MText (EntrypointLambda epParam epStore)
, StoreHasField store epsName epStore
, KnownValue epParam, KnownValue epStore
)
=> Label epmName -> Label epsName
-> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsSubmapField :: forall store (epmName :: Symbol) epParam epStore
(epsName :: Symbol) (epName :: Symbol).
(StoreHasSubmap
store epmName MText (EntrypointLambda epParam epStore),
StoreHasField store epsName epStore, KnownValue epParam,
KnownValue epStore) =>
Label epmName
-> Label epsName -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsSubmapField Label epmName
mapLabel Label epsName
fieldLabel = StoreEntrypointOps
{ sopToEpLambda :: forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopToEpLambda = \Label epName
l -> Label epName -> (store : s) :-> (MText : store : s)
forall (name :: Symbol) (s :: [*]). Label name -> s :-> (MText : s)
pushStEp Label epName
l ((store : s) :-> (MText : store : s))
-> ((MText : store : s)
:-> (Maybe (EntrypointLambda epParam epStore) : s))
-> (store : s) :-> (Maybe (EntrypointLambda epParam epStore) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef epmName
-> (MText : store : s)
:-> (Maybe (EntrypointLambda epParam epStore) : s)
forall {k} store (mname :: k) key value (s :: [*]).
(StoreHasSubmap store mname key value, KnownValue value) =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
stGet (Label epmName -> FieldRef epmName
forall (n :: Symbol). Label n -> FieldSymRef n
fieldNameFromLabel Label epmName
mapLabel) ((store : s) :-> (Maybe (EntrypointLambda epParam epStore) : s))
-> ((Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s))
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label epName
-> (Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s)
forall (epName :: Symbol) epParam epStore (s :: [*]).
Label epName
-> (Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s)
someStEp Label epName
l
, sopSetEpLambda :: forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda = \Label epName
l -> FieldRef epmName
-> Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
forall {k} store (epmName :: k) epParam epStore (epsName :: Symbol)
(s :: [*]).
StoreHasSubmap
store epmName MText (EntrypointLambda epParam epStore) =>
FieldRef epmName
-> Label epsName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
setStEp (Label epmName -> FieldRef epmName
forall (n :: Symbol). Label n -> FieldSymRef n
fieldNameFromLabel Label epmName
mapLabel) Label epName
l
, sopToEpStore :: forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore = \Label epName
_l -> FieldRef epsName -> (store : s) :-> (epStore : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreHasField store fname ftype =>
FieldRef fname -> (store : s) :-> (ftype : s)
stToField (Label epsName -> FieldRef epsName
forall (n :: Symbol). Label n -> FieldSymRef n
fieldNameFromLabel Label epsName
fieldLabel)
, sopSetEpStore :: forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore = \Label epName
_l -> FieldRef epsName -> (epStore : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreHasField store fname ftype =>
FieldRef fname -> (ftype : store : s) :-> (store : s)
stSetField (Label epsName -> FieldRef epsName
forall (n :: Symbol). Label n -> FieldSymRef n
fieldNameFromLabel Label epsName
fieldLabel)
}
storeFieldOpsDeeper
:: ( HasFieldOfType storage fieldsPartName fields
, StoreHasField fields fname ftype
, HasDupableGetters fields
)
=> FieldRef fieldsPartName
-> StoreFieldOps storage fname ftype
storeFieldOpsDeeper :: forall {k} storage (fieldsPartName :: Symbol) fields (fname :: k)
ftype.
(HasFieldOfType storage fieldsPartName fields,
StoreHasField fields fname ftype, HasDupableGetters fields) =>
FieldRef fieldsPartName -> StoreFieldOps storage fname ftype
storeFieldOpsDeeper FieldRef fieldsPartName
fieldsLabel =
FieldRef fieldsPartName
-> StoreFieldOps storage fieldsPartName fields
-> StoreFieldOps fields fname ftype
-> StoreFieldOps storage fname ftype
forall {k} {k} substore (nameInStore :: k) store
(nameInSubstore :: k) field.
HasDupableGetters substore =>
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreFieldOps substore nameInSubstore field
-> StoreFieldOps store nameInSubstore field
composeStoreFieldOps FieldRef fieldsPartName
fieldsLabel StoreFieldOps storage fieldsPartName fields
forall store (fname :: Symbol) ftype.
HasFieldOfType store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOpsADT StoreFieldOps fields fname ftype
forall {k} store (fname :: k) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps
storeSubmapOpsDeeper
:: ( HasFieldOfType storage bigMapPartName fields
, StoreHasSubmap fields SelfRef key value
, HasDupableGetters storage
, Dupable fields
)
=> FieldRef bigMapPartName
-> StoreSubmapOps storage mname key value
storeSubmapOpsDeeper :: forall {k} storage (bigMapPartName :: Symbol) fields key value
(mname :: k).
(HasFieldOfType storage bigMapPartName fields,
StoreHasSubmap fields SelfRef key value, HasDupableGetters storage,
Dupable fields) =>
FieldRef bigMapPartName -> StoreSubmapOps storage mname key value
storeSubmapOpsDeeper FieldRef bigMapPartName
submapLabel =
FieldRefObject SelfRef 'FieldRefTag
-> StoreSubmapOps storage SelfRef key value
-> StoreSubmapOps storage mname key value
forall {k} {k} (name :: k) storage key value (desiredName :: k).
FieldRef name
-> StoreSubmapOps storage name key value
-> StoreSubmapOps storage desiredName key value
storeSubmapOpsReferTo SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
forall (p :: FieldRefTag). SelfRef p
this (StoreSubmapOps storage SelfRef key value
-> StoreSubmapOps storage mname key value)
-> StoreSubmapOps storage SelfRef key value
-> StoreSubmapOps storage mname key value
forall a b. (a -> b) -> a -> b
$
FieldRef bigMapPartName
-> StoreFieldOps storage bigMapPartName fields
-> StoreSubmapOps fields SelfRef key value
-> StoreSubmapOps storage SelfRef key value
forall {k} {k} store substore (nameInStore :: k) (mname :: k) key
value.
(HasDupableGetters store, Dupable substore) =>
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreSubmapOps substore mname key value
-> StoreSubmapOps store mname key value
composeStoreSubmapOps FieldRef bigMapPartName
submapLabel StoreFieldOps storage bigMapPartName fields
forall store (fname :: Symbol) ftype.
HasFieldOfType store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOpsADT StoreSubmapOps fields SelfRef key value
forall {k} store (mname :: k) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps
storeEntrypointOpsDeeper
:: ( HasFieldOfType store nameInStore substore
, StoreHasEntrypoint substore epName epParam epStore
, HasDupableGetters store, Dupable substore
)
=> FieldRef nameInStore
-> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsDeeper :: forall store (nameInStore :: Symbol) substore (epName :: Symbol)
epParam epStore.
(HasFieldOfType store nameInStore substore,
StoreHasEntrypoint substore epName epParam epStore,
HasDupableGetters store, Dupable substore) =>
FieldRef nameInStore
-> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsDeeper FieldRef nameInStore
fieldsLabel =
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreEntrypointOps substore epName epParam epStore
-> StoreEntrypointOps store epName epParam epStore
forall {k} store substore (nameInStore :: k) (epName :: Symbol)
epParam epStore.
(HasDupableGetters store, Dupable substore) =>
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreEntrypointOps substore epName epParam epStore
-> StoreEntrypointOps store epName epParam epStore
composeStoreEntrypointOps FieldRef nameInStore
fieldsLabel StoreFieldOps store nameInStore substore
forall store (fname :: Symbol) ftype.
HasFieldOfType store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOpsADT StoreEntrypointOps substore epName epParam epStore
forall store (epName :: Symbol) epParam epStore.
StoreHasEntrypoint store epName epParam epStore =>
StoreEntrypointOps store epName epParam epStore
storeEpOps
storeSubmapOpsReferTo
:: FieldRef name
-> StoreSubmapOps storage name key value
-> StoreSubmapOps storage desiredName key value
storeSubmapOpsReferTo :: forall {k} {k} (name :: k) storage key value (desiredName :: k).
FieldRef name
-> StoreSubmapOps storage name key value
-> StoreSubmapOps storage desiredName key value
storeSubmapOpsReferTo FieldRef name
l StoreSubmapOps{forall (s :: [*]).
KnownValue value =>
FieldRef name -> (key : storage : s) :-> (Maybe value : s)
forall (s :: [*]).
FieldRef name -> (key : storage : s) :-> (storage : s)
forall (s :: [*]).
FieldRef name -> (key : storage : s) :-> (Bool : s)
forall (s :: [*]).
FieldRef name -> (key : value : storage : s) :-> (storage : s)
forall (s :: [*]).
FieldRef name
-> (key : Maybe value : storage : s) :-> (storage : s)
forall (s :: [*]).
FieldRef name
-> (key : Maybe value : storage : s)
:-> (Maybe value : storage : s)
sopMem :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
sopGet :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopUpdate :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopGetAndUpdate :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopDelete :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopInsert :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopMem :: forall (s :: [*]).
FieldRef name -> (key : storage : s) :-> (Bool : s)
sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRef name -> (key : storage : s) :-> (Maybe value : s)
sopUpdate :: forall (s :: [*]).
FieldRef name
-> (key : Maybe value : storage : s) :-> (storage : s)
sopGetAndUpdate :: forall (s :: [*]).
FieldRef name
-> (key : Maybe value : storage : s)
:-> (Maybe value : storage : s)
sopDelete :: forall (s :: [*]).
FieldRef name -> (key : storage : s) :-> (storage : s)
sopInsert :: forall (s :: [*]).
FieldRef name -> (key : value : storage : s) :-> (storage : s)
..} =
StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef desiredName -> (key : storage : s) :-> (Bool : s)
sopMem = \FieldRef desiredName
_l -> FieldRef name -> (key : storage : s) :-> (Bool : s)
forall (s :: [*]).
FieldRef name -> (key : storage : s) :-> (Bool : s)
sopMem FieldRef name
l
, sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRef desiredName -> (key : storage : s) :-> (Maybe value : s)
sopGet = \FieldRef desiredName
_l -> FieldRef name -> (key : storage : s) :-> (Maybe value : s)
forall (s :: [*]).
KnownValue value =>
FieldRef name -> (key : storage : s) :-> (Maybe value : s)
sopGet FieldRef name
l
, sopUpdate :: forall (s :: [*]).
FieldRef desiredName
-> (key : Maybe value : storage : s) :-> (storage : s)
sopUpdate = \FieldRef desiredName
_l -> FieldRef name
-> (key : Maybe value : storage : s) :-> (storage : s)
forall (s :: [*]).
FieldRef name
-> (key : Maybe value : storage : s) :-> (storage : s)
sopUpdate FieldRef name
l
, sopGetAndUpdate :: forall (s :: [*]).
FieldRef desiredName
-> (key : Maybe value : storage : s)
:-> (Maybe value : storage : s)
sopGetAndUpdate = \FieldRef desiredName
_l -> FieldRef name
-> (key : Maybe value : storage : s)
:-> (Maybe value : storage : s)
forall (s :: [*]).
FieldRef name
-> (key : Maybe value : storage : s)
:-> (Maybe value : storage : s)
sopGetAndUpdate FieldRef name
l
, sopDelete :: forall (s :: [*]).
FieldRef desiredName -> (key : storage : s) :-> (storage : s)
sopDelete = \FieldRef desiredName
_l -> FieldRef name -> (key : storage : s) :-> (storage : s)
forall (s :: [*]).
FieldRef name -> (key : storage : s) :-> (storage : s)
sopDelete FieldRef name
l
, sopInsert :: forall (s :: [*]).
FieldRef desiredName
-> (key : value : storage : s) :-> (storage : s)
sopInsert = \FieldRef desiredName
_l -> FieldRef name -> (key : value : storage : s) :-> (storage : s)
forall (s :: [*]).
FieldRef name -> (key : value : storage : s) :-> (storage : s)
sopInsert FieldRef name
l
}
storeFieldOpsReferTo
:: FieldRef name
-> StoreFieldOps storage name field
-> StoreFieldOps storage desiredName field
storeFieldOpsReferTo :: forall {k} {k} (name :: k) storage field (desiredName :: k).
FieldRef name
-> StoreFieldOps storage name field
-> StoreFieldOps storage desiredName field
storeFieldOpsReferTo FieldRef name
l StoreFieldOps{forall (s :: [*]). FieldRef name -> (storage : s) :-> (field : s)
forall new (s :: [*]).
('[new, field] :-> '[field])
-> FieldRef name -> (new : storage : s) :-> (storage : s)
forall res (s :: [*]).
HasDupableGetters storage =>
('[field] :-> '[res, field])
-> ('[field] :-> '[res])
-> FieldRef name
-> (storage : s) :-> (res : storage : s)
sopToField :: forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopGetFieldOpen :: forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall res (s :: [*]).
HasDupableGetters store =>
('[ftype] :-> '[res, ftype])
-> ('[ftype] :-> '[res])
-> FieldRef fname
-> (store : s) :-> (res : store : s)
sopSetFieldOpen :: forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall new (s :: [*]).
('[new, ftype] :-> '[ftype])
-> FieldRef fname -> (new : store : s) :-> (store : s)
sopToField :: forall (s :: [*]). FieldRef name -> (storage : s) :-> (field : s)
sopGetFieldOpen :: forall res (s :: [*]).
HasDupableGetters storage =>
('[field] :-> '[res, field])
-> ('[field] :-> '[res])
-> FieldRef name
-> (storage : s) :-> (res : storage : s)
sopSetFieldOpen :: forall new (s :: [*]).
('[new, field] :-> '[field])
-> FieldRef name -> (new : storage : s) :-> (storage : s)
..} =
StoreFieldOps
{ sopToField :: forall (s :: [*]).
FieldRef desiredName -> (storage : s) :-> (field : s)
sopToField = \FieldRef desiredName
_l -> FieldRef name -> (storage : s) :-> (field : s)
forall (s :: [*]). FieldRef name -> (storage : s) :-> (field : s)
sopToField FieldRef name
l
, sopGetFieldOpen :: forall res (s :: [*]).
HasDupableGetters storage =>
('[field] :-> '[res, field])
-> ('[field] :-> '[res])
-> FieldRef desiredName
-> (storage : s) :-> (res : storage : s)
sopGetFieldOpen = \'[field] :-> '[res, field]
cont1 '[field] :-> '[res]
cont2 FieldRef desiredName
_l -> ('[field] :-> '[res, field])
-> ('[field] :-> '[res])
-> FieldRef name
-> (storage : s) :-> (res : storage : s)
forall res (s :: [*]).
HasDupableGetters storage =>
('[field] :-> '[res, field])
-> ('[field] :-> '[res])
-> FieldRef name
-> (storage : s) :-> (res : storage : s)
sopGetFieldOpen '[field] :-> '[res, field]
cont1 '[field] :-> '[res]
cont2 FieldRef name
l
, sopSetFieldOpen :: forall new (s :: [*]).
('[new, field] :-> '[field])
-> FieldRef desiredName -> (new : storage : s) :-> (storage : s)
sopSetFieldOpen = \'[new, field] :-> '[field]
cont FieldRef desiredName
_l -> ('[new, field] :-> '[field])
-> FieldRef name -> (new : storage : s) :-> (storage : s)
forall new (s :: [*]).
('[new, field] :-> '[field])
-> FieldRef name -> (new : storage : s) :-> (storage : s)
sopSetFieldOpen '[new, field] :-> '[field]
cont FieldRef name
l
}
storeEntrypointOpsReferTo
:: Label epName
-> StoreEntrypointOps store epName epParam epStore
-> StoreEntrypointOps store desiredName epParam epStore
storeEntrypointOpsReferTo :: forall (epName :: Symbol) store epParam epStore
(desiredName :: Symbol).
Label epName
-> StoreEntrypointOps store epName epParam epStore
-> StoreEntrypointOps store desiredName epParam epStore
storeEntrypointOpsReferTo Label epName
l StoreEntrypointOps{forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopToEpLambda :: forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopSetEpLambda :: forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopToEpStore :: forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopSetEpStore :: forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopToEpLambda :: forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopSetEpLambda :: forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopToEpStore :: forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopSetEpStore :: forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
..} = StoreEntrypointOps
{ sopToEpLambda :: forall (s :: [*]).
Label desiredName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopToEpLambda = \Label desiredName
_l -> Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopToEpLambda Label epName
l
, sopSetEpLambda :: forall (s :: [*]).
HasDupableGetters store =>
Label desiredName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda = \Label desiredName
_l -> Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda Label epName
l
, sopToEpStore :: forall (s :: [*]).
Label desiredName -> (store : s) :-> (epStore : s)
sopToEpStore = \Label desiredName
_l -> Label epName -> (store : s) :-> (epStore : s)
forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore Label epName
l
, sopSetEpStore :: forall (s :: [*]).
Label desiredName -> (epStore : store : s) :-> (store : s)
sopSetEpStore = \Label desiredName
_l -> Label epName -> (epStore : store : s) :-> (store : s)
forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore Label epName
l
}
mapStoreFieldOps
:: forall field1 field2 store name.
KnownValue field1
=> LIso field1 field2
-> StoreFieldOps store name field1
-> StoreFieldOps store name field2
mapStoreFieldOps :: forall {k} field1 field2 store (name :: k).
KnownValue field1 =>
LIso field1 field2
-> StoreFieldOps store name field1
-> StoreFieldOps store name field2
mapStoreFieldOps LIso{forall (s :: [*]). (field1 : s) :-> (field2 : s)
forall (s :: [*]). (field2 : s) :-> (field1 : s)
liTo :: forall (s :: [*]). (field1 : s) :-> (field2 : s)
liFrom :: forall (s :: [*]). (field2 : s) :-> (field1 : s)
liTo :: forall a b. LIso a b -> forall (s :: [*]). (a : s) :-> (b : s)
liFrom :: forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
..} StoreFieldOps{forall (s :: [*]). FieldRef name -> (store : s) :-> (field1 : s)
forall new (s :: [*]).
('[new, field1] :-> '[field1])
-> FieldRef name -> (new : store : s) :-> (store : s)
forall res (s :: [*]).
HasDupableGetters store =>
('[field1] :-> '[res, field1])
-> ('[field1] :-> '[res])
-> FieldRef name
-> (store : s) :-> (res : store : s)
sopToField :: forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopGetFieldOpen :: forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall res (s :: [*]).
HasDupableGetters store =>
('[ftype] :-> '[res, ftype])
-> ('[ftype] :-> '[res])
-> FieldRef fname
-> (store : s) :-> (res : store : s)
sopSetFieldOpen :: forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall new (s :: [*]).
('[new, ftype] :-> '[ftype])
-> FieldRef fname -> (new : store : s) :-> (store : s)
sopToField :: forall (s :: [*]). FieldRef name -> (store : s) :-> (field1 : s)
sopGetFieldOpen :: forall res (s :: [*]).
HasDupableGetters store =>
('[field1] :-> '[res, field1])
-> ('[field1] :-> '[res])
-> FieldRef name
-> (store : s) :-> (res : store : s)
sopSetFieldOpen :: forall new (s :: [*]).
('[new, field1] :-> '[field1])
-> FieldRef name -> (new : store : s) :-> (store : s)
..} = StoreFieldOps
{ sopToField :: forall (s :: [*]). FieldRef name -> (store : s) :-> (field2 : s)
sopToField = \FieldRef name
l -> FieldRef name -> (store : s) :-> (field1 : s)
forall (s :: [*]). FieldRef name -> (store : s) :-> (field1 : s)
sopToField FieldRef name
l ((store : s) :-> (field1 : s))
-> ((field1 : s) :-> (field2 : s)) -> (store : s) :-> (field2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (field1 : s) :-> (field2 : s)
forall (s :: [*]). (field1 : s) :-> (field2 : s)
liTo
, sopGetFieldOpen :: forall res (s :: [*]).
HasDupableGetters store =>
('[field2] :-> '[res, field2])
-> ('[field2] :-> '[res])
-> FieldRef name
-> (store : s) :-> (res : store : s)
sopGetFieldOpen = \'[field2] :-> '[res, field2]
contWDup '[field2] :-> '[res]
contWoDup FieldRef name
l ->
let ourContWoDup :: '[field1] :-> '[res]
ourContWoDup = '[field1] :-> '[field2]
forall (s :: [*]). (field1 : s) :-> (field2 : s)
liTo ('[field1] :-> '[field2])
-> ('[field2] :-> '[res]) -> '[field1] :-> '[res]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# '[field2] :-> '[res]
contWoDup
ourContWDup :: '[field1] :-> '[res, field1]
ourContWDup = case forall a. KnownValue a => DupableDecision a
decideOnDupable @field1 of
DupableDecision field1
IsDupable -> '[field1] :-> '[field1, field1]
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup ('[field1] :-> '[field1, field1])
-> ('[field1, field1] :-> '[field2, field1])
-> '[field1] :-> '[field2, field1]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# '[field1, field1] :-> '[field2, field1]
forall (s :: [*]). (field1 : s) :-> (field2 : s)
liTo ('[field1] :-> '[field2, field1])
-> ('[field2, field1] :-> '[res, field1])
-> '[field1] :-> '[res, field1]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ('[field2] :-> '[res])
-> ('[field2] ++ '[field1]) :-> ('[res] ++ '[field1])
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed '[field2] :-> '[res]
contWoDup
DupableDecision field1
IsNotDupable -> '[field1] :-> '[field2]
forall (s :: [*]). (field1 : s) :-> (field2 : s)
liTo ('[field1] :-> '[field2])
-> ('[field2] :-> '[res, field2]) -> '[field1] :-> '[res, field2]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# '[field2] :-> '[res, field2]
contWDup ('[field1] :-> '[res, field2])
-> ('[res, field2] :-> '[res, field1])
-> '[field1] :-> '[res, field1]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ('[field2] :-> '[field1]) -> '[res, field2] :-> '[res, field1]
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip '[field2] :-> '[field1]
forall (s :: [*]). (field2 : s) :-> (field1 : s)
liFrom
in ('[field1] :-> '[res, field1])
-> ('[field1] :-> '[res])
-> FieldRef name
-> (store : s) :-> (res : store : s)
forall res (s :: [*]).
HasDupableGetters store =>
('[field1] :-> '[res, field1])
-> ('[field1] :-> '[res])
-> FieldRef name
-> (store : s) :-> (res : store : s)
sopGetFieldOpen '[field1] :-> '[res, field1]
ourContWDup '[field1] :-> '[res]
ourContWoDup FieldRef name
l
, sopSetFieldOpen :: forall new (s :: [*]).
('[new, field2] :-> '[field2])
-> FieldRef name -> (new : store : s) :-> (store : s)
sopSetFieldOpen = \'[new, field2] :-> '[field2]
cont FieldRef name
l ->
('[new, field1] :-> '[field1])
-> FieldRef name -> (new : store : s) :-> (store : s)
forall new (s :: [*]).
('[new, field1] :-> '[field1])
-> FieldRef name -> (new : store : s) :-> (store : s)
sopSetFieldOpen (('[field1] :-> '[field2]) -> '[new, field1] :-> '[new, field2]
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip '[field1] :-> '[field2]
forall (s :: [*]). (field1 : s) :-> (field2 : s)
liTo ('[new, field1] :-> '[new, field2])
-> ('[new, field2] :-> '[field2]) -> '[new, field1] :-> '[field2]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ('[new, field2] :-> '[field2])
-> ('[new, field2] ++ '[]) :-> ('[field2] ++ '[])
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed '[new, field2] :-> '[field2]
cont ('[new, field1] :-> '[field2])
-> ('[field2] :-> '[field1]) -> '[new, field1] :-> '[field1]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# '[field2] :-> '[field1]
forall (s :: [*]). (field2 : s) :-> (field1 : s)
liFrom) FieldRef name
l
}
mapStoreSubmapOpsKey
:: Fn key2 key1
-> StoreSubmapOps store name key1 value
-> StoreSubmapOps store name key2 value
mapStoreSubmapOpsKey :: forall {k} key2 key1 store (name :: k) value.
Fn key2 key1
-> StoreSubmapOps store name key1 value
-> StoreSubmapOps store name key2 value
mapStoreSubmapOpsKey Fn key2 key1
mapper StoreSubmapOps{forall (s :: [*]).
KnownValue value =>
FieldRef name -> (key1 : store : s) :-> (Maybe value : s)
forall (s :: [*]).
FieldRef name -> (key1 : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (key1 : store : s) :-> (Bool : s)
forall (s :: [*]).
FieldRef name -> (key1 : value : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (key1 : Maybe value : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name
-> (key1 : Maybe value : store : s) :-> (Maybe value : store : s)
sopMem :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
sopGet :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopUpdate :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopGetAndUpdate :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopDelete :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopInsert :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopMem :: forall (s :: [*]).
FieldRef name -> (key1 : store : s) :-> (Bool : s)
sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRef name -> (key1 : store : s) :-> (Maybe value : s)
sopUpdate :: forall (s :: [*]).
FieldRef name -> (key1 : Maybe value : store : s) :-> (store : s)
sopGetAndUpdate :: forall (s :: [*]).
FieldRef name
-> (key1 : Maybe value : store : s) :-> (Maybe value : store : s)
sopDelete :: forall (s :: [*]).
FieldRef name -> (key1 : store : s) :-> (store : s)
sopInsert :: forall (s :: [*]).
FieldRef name -> (key1 : value : store : s) :-> (store : s)
..} = StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef name -> (key2 : store : s) :-> (Bool : s)
sopMem = \FieldRef name
l ->
Fn key2 key1
-> ('[key2] ++ (store : s)) :-> ('[key1] ++ (store : s))
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed Fn key2 key1
mapper ((key2 : store : s) :-> (key1 : store : s))
-> ((key1 : store : s) :-> (Bool : s))
-> (key2 : store : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef name -> (key1 : store : s) :-> (Bool : s)
forall (s :: [*]).
FieldRef name -> (key1 : store : s) :-> (Bool : s)
sopMem FieldRef name
l
, sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRef name -> (key2 : store : s) :-> (Maybe value : s)
sopGet = \FieldRef name
l ->
Fn key2 key1
-> ('[key2] ++ (store : s)) :-> ('[key1] ++ (store : s))
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed Fn key2 key1
mapper ((key2 : store : s) :-> (key1 : store : s))
-> ((key1 : store : s) :-> (Maybe value : s))
-> (key2 : store : s) :-> (Maybe value : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef name -> (key1 : store : s) :-> (Maybe value : s)
forall (s :: [*]).
KnownValue value =>
FieldRef name -> (key1 : store : s) :-> (Maybe value : s)
sopGet FieldRef name
l
, sopUpdate :: forall (s :: [*]).
FieldRef name -> (key2 : Maybe value : store : s) :-> (store : s)
sopUpdate = \FieldRef name
l ->
Fn key2 key1
-> ('[key2] ++ (Maybe value : store : s))
:-> ('[key1] ++ (Maybe value : store : s))
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed Fn key2 key1
mapper ((key2 : Maybe value : store : s)
:-> (key1 : Maybe value : store : s))
-> ((key1 : Maybe value : store : s) :-> (store : s))
-> (key2 : Maybe value : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef name -> (key1 : Maybe value : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (key1 : Maybe value : store : s) :-> (store : s)
sopUpdate FieldRef name
l
, sopGetAndUpdate :: forall (s :: [*]).
FieldRef name
-> (key2 : Maybe value : store : s) :-> (Maybe value : store : s)
sopGetAndUpdate = \FieldRef name
l ->
Fn key2 key1
-> ('[key2] ++ (Maybe value : store : s))
:-> ('[key1] ++ (Maybe value : store : s))
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed Fn key2 key1
mapper ((key2 : Maybe value : store : s)
:-> (key1 : Maybe value : store : s))
-> ((key1 : Maybe value : store : s) :-> (Maybe value : store : s))
-> (key2 : Maybe value : store : s) :-> (Maybe value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef name
-> (key1 : Maybe value : store : s) :-> (Maybe value : store : s)
forall (s :: [*]).
FieldRef name
-> (key1 : Maybe value : store : s) :-> (Maybe value : store : s)
sopGetAndUpdate FieldRef name
l
, sopDelete :: forall (s :: [*]).
FieldRef name -> (key2 : store : s) :-> (store : s)
sopDelete = \FieldRef name
l ->
Fn key2 key1
-> ('[key2] ++ (store : s)) :-> ('[key1] ++ (store : s))
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed Fn key2 key1
mapper ((key2 : store : s) :-> (key1 : store : s))
-> ((key1 : store : s) :-> (store : s))
-> (key2 : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef name -> (key1 : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (key1 : store : s) :-> (store : s)
sopDelete FieldRef name
l
, sopInsert :: forall (s :: [*]).
FieldRef name -> (key2 : value : store : s) :-> (store : s)
sopInsert = \FieldRef name
l ->
Fn key2 key1
-> ('[key2] ++ (value : store : s))
:-> ('[key1] ++ (value : store : s))
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed Fn key2 key1
mapper ((key2 : value : store : s) :-> (key1 : value : store : s))
-> ((key1 : value : store : s) :-> (store : s))
-> (key2 : value : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef name -> (key1 : value : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (key1 : value : store : s) :-> (store : s)
sopInsert FieldRef name
l
}
mapStoreSubmapOpsValue
:: (KnownValue value1, KnownValue value2)
=> LIso value1 value2
-> StoreSubmapOps store name key value1
-> StoreSubmapOps store name key value2
mapStoreSubmapOpsValue :: forall {k} value1 value2 store (name :: k) key.
(KnownValue value1, KnownValue value2) =>
LIso value1 value2
-> StoreSubmapOps store name key value1
-> StoreSubmapOps store name key value2
mapStoreSubmapOpsValue LIso{forall (s :: [*]). (value1 : s) :-> (value2 : s)
forall (s :: [*]). (value2 : s) :-> (value1 : s)
liTo :: forall a b. LIso a b -> forall (s :: [*]). (a : s) :-> (b : s)
liFrom :: forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liTo :: forall (s :: [*]). (value1 : s) :-> (value2 : s)
liFrom :: forall (s :: [*]). (value2 : s) :-> (value1 : s)
..} StoreSubmapOps{forall (s :: [*]).
KnownValue value1 =>
FieldRef name -> (key : store : s) :-> (Maybe value1 : s)
forall (s :: [*]).
FieldRef name -> (key : value1 : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (key : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (key : store : s) :-> (Bool : s)
forall (s :: [*]).
FieldRef name -> (key : Maybe value1 : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name
-> (key : Maybe value1 : store : s) :-> (Maybe value1 : store : s)
sopMem :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
sopGet :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopUpdate :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopGetAndUpdate :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopDelete :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopInsert :: forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopMem :: forall (s :: [*]).
FieldRef name -> (key : store : s) :-> (Bool : s)
sopGet :: forall (s :: [*]).
KnownValue value1 =>
FieldRef name -> (key : store : s) :-> (Maybe value1 : s)
sopUpdate :: forall (s :: [*]).
FieldRef name -> (key : Maybe value1 : store : s) :-> (store : s)
sopGetAndUpdate :: forall (s :: [*]).
FieldRef name
-> (key : Maybe value1 : store : s) :-> (Maybe value1 : store : s)
sopDelete :: forall (s :: [*]).
FieldRef name -> (key : store : s) :-> (store : s)
sopInsert :: forall (s :: [*]).
FieldRef name -> (key : value1 : store : s) :-> (store : s)
..} = StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef name -> (key : store : s) :-> (Bool : s)
sopMem = \FieldRef name
l ->
FieldRef name -> (key : store : s) :-> (Bool : s)
forall (s :: [*]).
FieldRef name -> (key : store : s) :-> (Bool : s)
sopMem FieldRef name
l
, sopGet :: forall (s :: [*]).
KnownValue value2 =>
FieldRef name -> (key : store : s) :-> (Maybe value2 : s)
sopGet = \FieldRef name
l ->
FieldRef name -> (key : store : s) :-> (Maybe value1 : s)
forall (s :: [*]).
KnownValue value1 =>
FieldRef name -> (key : store : s) :-> (Maybe value1 : s)
sopGet FieldRef name
l ((key : store : s) :-> (Maybe value1 : s))
-> ((Maybe value1 : s) :-> (Maybe value2 : s))
-> (key : store : s) :-> (Maybe value2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ('[value1] :-> '[value2])
-> (Maybe value1 : s) :-> (Maybe value2 : s)
forall (s :: [*]).
KnownValue value2 =>
('[value1] :-> '[value2])
-> (Maybe value1 : s) :-> (Maybe value2 : s)
forall (c :: * -> *) a b (s :: [*]).
(LorentzFunctor c a b, KnownValue b) =>
('[a] :-> '[b]) -> (c a : s) :-> (c b : s)
L.lmap '[value1] :-> '[value2]
forall (s :: [*]). (value1 : s) :-> (value2 : s)
liTo
, sopUpdate :: forall (s :: [*]).
FieldRef name -> (key : Maybe value2 : store : s) :-> (store : s)
sopUpdate = \FieldRef name
l ->
((Maybe value2 : store : s) :-> (Maybe value1 : store : s))
-> (key : Maybe value2 : store : s)
:-> (key : Maybe value1 : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (('[value2] :-> '[value1])
-> (Maybe value2 : store : s) :-> (Maybe value1 : store : s)
forall (s :: [*]).
KnownValue value1 =>
('[value2] :-> '[value1])
-> (Maybe value2 : s) :-> (Maybe value1 : s)
forall (c :: * -> *) a b (s :: [*]).
(LorentzFunctor c a b, KnownValue b) =>
('[a] :-> '[b]) -> (c a : s) :-> (c b : s)
L.lmap '[value2] :-> '[value1]
forall (s :: [*]). (value2 : s) :-> (value1 : s)
liFrom) ((key : Maybe value2 : store : s)
:-> (key : Maybe value1 : store : s))
-> ((key : Maybe value1 : store : s) :-> (store : s))
-> (key : Maybe value2 : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef name -> (key : Maybe value1 : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (key : Maybe value1 : store : s) :-> (store : s)
sopUpdate FieldRef name
l
, sopGetAndUpdate :: forall (s :: [*]).
FieldRef name
-> (key : Maybe value2 : store : s) :-> (Maybe value2 : store : s)
sopGetAndUpdate = \FieldRef name
l ->
((Maybe value2 : store : s) :-> (Maybe value1 : store : s))
-> (key : Maybe value2 : store : s)
:-> (key : Maybe value1 : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (('[value2] :-> '[value1])
-> (Maybe value2 : store : s) :-> (Maybe value1 : store : s)
forall (s :: [*]).
KnownValue value1 =>
('[value2] :-> '[value1])
-> (Maybe value2 : s) :-> (Maybe value1 : s)
forall (c :: * -> *) a b (s :: [*]).
(LorentzFunctor c a b, KnownValue b) =>
('[a] :-> '[b]) -> (c a : s) :-> (c b : s)
L.lmap '[value2] :-> '[value1]
forall (s :: [*]). (value2 : s) :-> (value1 : s)
liFrom) ((key : Maybe value2 : store : s)
:-> (key : Maybe value1 : store : s))
-> ((key : Maybe value1 : store : s)
:-> (Maybe value1 : store : s))
-> (key : Maybe value2 : store : s) :-> (Maybe value1 : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef name
-> (key : Maybe value1 : store : s) :-> (Maybe value1 : store : s)
forall (s :: [*]).
FieldRef name
-> (key : Maybe value1 : store : s) :-> (Maybe value1 : store : s)
sopGetAndUpdate FieldRef name
l ((key : Maybe value2 : store : s) :-> (Maybe value1 : store : s))
-> ((Maybe value1 : store : s) :-> (Maybe value2 : store : s))
-> (key : Maybe value2 : store : s) :-> (Maybe value2 : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ('[value1] :-> '[value2])
-> (Maybe value1 : store : s) :-> (Maybe value2 : store : s)
forall (s :: [*]).
KnownValue value2 =>
('[value1] :-> '[value2])
-> (Maybe value1 : s) :-> (Maybe value2 : s)
forall (c :: * -> *) a b (s :: [*]).
(LorentzFunctor c a b, KnownValue b) =>
('[a] :-> '[b]) -> (c a : s) :-> (c b : s)
L.lmap '[value1] :-> '[value2]
forall (s :: [*]). (value1 : s) :-> (value2 : s)
liTo
, sopInsert :: forall (s :: [*]).
FieldRef name -> (key : value2 : store : s) :-> (store : s)
sopInsert = \FieldRef name
l ->
((value2 : store : s) :-> (value1 : store : s))
-> (key : value2 : store : s) :-> (key : value1 : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (value2 : store : s) :-> (value1 : store : s)
forall (s :: [*]). (value2 : s) :-> (value1 : s)
liFrom ((key : value2 : store : s) :-> (key : value1 : store : s))
-> ((key : value1 : store : s) :-> (store : s))
-> (key : value2 : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef name -> (key : value1 : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (key : value1 : store : s) :-> (store : s)
sopInsert FieldRef name
l
, sopDelete :: forall (s :: [*]).
FieldRef name -> (key : store : s) :-> (store : s)
sopDelete = \FieldRef name
l ->
FieldRef name -> (key : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (key : store : s) :-> (store : s)
sopDelete FieldRef name
l
}
composeStoreFieldOps
:: HasDupableGetters substore
=> FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreFieldOps substore nameInSubstore field
-> StoreFieldOps store nameInSubstore field
composeStoreFieldOps :: forall {k} {k} substore (nameInStore :: k) store
(nameInSubstore :: k) field.
HasDupableGetters substore =>
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreFieldOps substore nameInSubstore field
-> StoreFieldOps store nameInSubstore field
composeStoreFieldOps FieldRef nameInStore
l1 StoreFieldOps store nameInStore substore
ops1 StoreFieldOps substore nameInSubstore field
ops2 =
StoreFieldOps
{ sopToField :: forall (s :: [*]).
FieldRef nameInSubstore -> (store : s) :-> (field : s)
sopToField = \FieldRef nameInSubstore
l2 ->
StoreFieldOps store nameInStore substore
-> forall (s :: [*]).
FieldRef nameInStore -> (store : s) :-> (substore : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1 ((store : s) :-> (substore : s))
-> ((substore : s) :-> (field : s)) -> (store : s) :-> (field : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreFieldOps substore nameInSubstore field
-> forall (s :: [*]).
FieldRef nameInSubstore -> (substore : s) :-> (field : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps substore nameInSubstore field
ops2 FieldRef nameInSubstore
l2
, sopGetFieldOpen :: forall res (s :: [*]).
HasDupableGetters store =>
('[field] :-> '[res, field])
-> ('[field] :-> '[res])
-> FieldRef nameInSubstore
-> (store : s) :-> (res : store : s)
sopGetFieldOpen = \'[field] :-> '[res, field]
contWDup '[field] :-> '[res]
contWoDup FieldRef nameInSubstore
l2 ->
StoreFieldOps store nameInStore substore
-> forall res (s :: [*]).
HasDupableGetters store =>
('[substore] :-> '[res, substore])
-> ('[substore] :-> '[res])
-> FieldRef nameInStore
-> (store : s) :-> (res : store : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall res (s :: [*]).
HasDupableGetters store =>
('[ftype] :-> '[res, ftype])
-> ('[ftype] :-> '[res])
-> FieldRef fname
-> (store : s) :-> (res : store : s)
sopGetFieldOpen StoreFieldOps store nameInStore substore
ops1
(StoreFieldOps substore nameInSubstore field
-> forall res (s :: [*]).
HasDupableGetters substore =>
('[field] :-> '[res, field])
-> ('[field] :-> '[res])
-> FieldRef nameInSubstore
-> (substore : s) :-> (res : substore : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall res (s :: [*]).
HasDupableGetters store =>
('[ftype] :-> '[res, ftype])
-> ('[ftype] :-> '[res])
-> FieldRef fname
-> (store : s) :-> (res : store : s)
sopGetFieldOpen StoreFieldOps substore nameInSubstore field
ops2 '[field] :-> '[res, field]
contWDup '[field] :-> '[res]
contWoDup FieldRef nameInSubstore
l2)
(StoreFieldOps substore nameInSubstore field
-> forall (s :: [*]).
FieldRef nameInSubstore -> (substore : s) :-> (field : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps substore nameInSubstore field
ops2 FieldRef nameInSubstore
l2 ('[substore] :-> '[field])
-> ('[field] :-> '[res]) -> '[substore] :-> '[res]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# '[field] :-> '[res]
contWoDup)
FieldRef nameInStore
l1
, sopSetFieldOpen :: forall new (s :: [*]).
('[new, field] :-> '[field])
-> FieldRef nameInSubstore -> (new : store : s) :-> (store : s)
sopSetFieldOpen = \'[new, field] :-> '[field]
cont FieldRef nameInSubstore
l2 ->
StoreFieldOps store nameInStore substore
-> forall new (s :: [*]).
('[new, substore] :-> '[substore])
-> FieldRef nameInStore -> (new : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall new (s :: [*]).
('[new, ftype] :-> '[ftype])
-> FieldRef fname -> (new : store : s) :-> (store : s)
sopSetFieldOpen StoreFieldOps store nameInStore substore
ops1 (StoreFieldOps substore nameInSubstore field
-> forall new (s :: [*]).
('[new, field] :-> '[field])
-> FieldRef nameInSubstore
-> (new : substore : s) :-> (substore : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall new (s :: [*]).
('[new, ftype] :-> '[ftype])
-> FieldRef fname -> (new : store : s) :-> (store : s)
sopSetFieldOpen StoreFieldOps substore nameInSubstore field
ops2 '[new, field] :-> '[field]
cont FieldRef nameInSubstore
l2) FieldRef nameInStore
l1
}
composeStoreSubmapOps
:: (HasDupableGetters store, Dupable substore)
=> FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreSubmapOps substore mname key value
-> StoreSubmapOps store mname key value
composeStoreSubmapOps :: forall {k} {k} store substore (nameInStore :: k) (mname :: k) key
value.
(HasDupableGetters store, Dupable substore) =>
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreSubmapOps substore mname key value
-> StoreSubmapOps store mname key value
composeStoreSubmapOps FieldRef nameInStore
l1 StoreFieldOps store nameInStore substore
ops1 StoreSubmapOps substore mname key value
ops2 =
StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
sopMem = \FieldRef mname
l2 ->
((store : s) :-> (substore : s))
-> (key : store : s) :-> (key : substore : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps store nameInStore substore
-> forall (s :: [*]).
FieldRef nameInStore -> (store : s) :-> (substore : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1) ((key : store : s) :-> (key : substore : s))
-> ((key : substore : s) :-> (Bool : s))
-> (key : store : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreSubmapOps substore mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : substore : s) :-> (Bool : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
sopMem StoreSubmapOps substore mname key value
ops2 FieldRef mname
l2
, sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet = \FieldRef mname
l2 ->
((store : s) :-> (substore : s))
-> (key : store : s) :-> (key : substore : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps store nameInStore substore
-> forall (s :: [*]).
FieldRef nameInStore -> (store : s) :-> (substore : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1) ((key : store : s) :-> (key : substore : s))
-> ((key : substore : s) :-> (Maybe value : s))
-> (key : store : s) :-> (Maybe value : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreSubmapOps substore mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : substore : s) :-> (Maybe value : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps substore mname key value
ops2 FieldRef mname
l2
, sopUpdate :: forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate = \FieldRef mname
l2 ->
((Maybe value : store : s)
:-> (Maybe value : substore : store : s))
-> (key : Maybe value : store : s)
:-> (key : Maybe value : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (((store : s) :-> (substore : store : s))
-> (Maybe value : store : s)
:-> (Maybe value : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (store : s) :-> (substore : store : s)
forall {k} ftype store (fname :: k) (s :: [*]).
(Dupable ftype, HasDupableGetters store) =>
StoreFieldOps store fname ftype
-> FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1)) ((key : Maybe value : store : s)
:-> (key : Maybe value : substore : store : s))
-> ((key : Maybe value : substore : store : s)
:-> (substore : store : s))
-> (key : Maybe value : store : s) :-> (substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreSubmapOps substore mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : substore : s) :-> (substore : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps substore mname key value
ops2 FieldRef mname
l2 ((key : Maybe value : store : s) :-> (substore : store : s))
-> ((substore : store : s) :-> (store : s))
-> (key : Maybe value : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (substore : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreFieldOps store fname ftype
-> FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1
, sopGetAndUpdate :: forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopGetAndUpdate = \FieldRef mname
l2 ->
((Maybe value : store : s)
:-> (Maybe value : substore : store : s))
-> (key : Maybe value : store : s)
:-> (key : Maybe value : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (((store : s) :-> (substore : store : s))
-> (Maybe value : store : s)
:-> (Maybe value : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (store : s) :-> (substore : store : s)
forall {k} ftype store (fname :: k) (s :: [*]).
(Dupable ftype, HasDupableGetters store) =>
StoreFieldOps store fname ftype
-> FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1)) ((key : Maybe value : store : s)
:-> (key : Maybe value : substore : store : s))
-> ((key : Maybe value : substore : store : s)
:-> (Maybe value : substore : store : s))
-> (key : Maybe value : store : s)
:-> (Maybe value : substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreSubmapOps substore mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : substore : s)
:-> (Maybe value : substore : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopGetAndUpdate StoreSubmapOps substore mname key value
ops2 FieldRef mname
l2 ((key : Maybe value : store : s)
:-> (Maybe value : substore : store : s))
-> ((Maybe value : substore : store : s)
:-> (Maybe value : store : s))
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((substore : store : s) :-> (store : s))
-> (Maybe value : substore : store : s)
:-> (Maybe value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (substore : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreFieldOps store fname ftype
-> FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1)
, sopDelete :: forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopDelete = \FieldRef mname
l2 ->
((store : s) :-> (substore : store : s))
-> (key : store : s) :-> (key : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (store : s) :-> (substore : store : s)
forall {k} ftype store (fname :: k) (s :: [*]).
(Dupable ftype, HasDupableGetters store) =>
StoreFieldOps store fname ftype
-> FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1) ((key : store : s) :-> (key : substore : store : s))
-> ((key : substore : store : s) :-> (substore : store : s))
-> (key : store : s) :-> (substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreSubmapOps substore mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : substore : s) :-> (substore : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopDelete StoreSubmapOps substore mname key value
ops2 FieldRef mname
l2 ((key : store : s) :-> (substore : store : s))
-> ((substore : store : s) :-> (store : s))
-> (key : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (substore : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreFieldOps store fname ftype
-> FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1
, sopInsert :: forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopInsert = \FieldRef mname
l2 ->
((value : store : s) :-> (value : substore : store : s))
-> (key : value : store : s)
:-> (key : value : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (((store : s) :-> (substore : store : s))
-> (value : store : s) :-> (value : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (store : s) :-> (substore : store : s)
forall {k} ftype store (fname :: k) (s :: [*]).
(Dupable ftype, HasDupableGetters store) =>
StoreFieldOps store fname ftype
-> FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1)) ((key : value : store : s)
:-> (key : value : substore : store : s))
-> ((key : value : substore : store : s)
:-> (substore : store : s))
-> (key : value : store : s) :-> (substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreSubmapOps substore mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : substore : s) :-> (substore : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopInsert StoreSubmapOps substore mname key value
ops2 FieldRef mname
l2 ((key : value : store : s) :-> (substore : store : s))
-> ((substore : store : s) :-> (store : s))
-> (key : value : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (substore : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreFieldOps store fname ftype
-> FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1
}
sequenceStoreSubmapOps
:: forall store substore value name subName key1 key2.
( NiceConstant substore, KnownValue value
, Dupable (key1, key2), Dupable store
)
=> FieldRef name
-> LIso (Maybe substore) substore
-> StoreSubmapOps store name key1 substore
-> StoreSubmapOps substore subName key2 value
-> StoreSubmapOps store subName (key1, key2) value
sequenceStoreSubmapOps :: forall {k} {k} store substore value (name :: k) (subName :: k) key1
key2.
(NiceConstant substore, KnownValue value, Dupable (key1, key2),
Dupable store) =>
FieldRef name
-> LIso (Maybe substore) substore
-> StoreSubmapOps store name key1 substore
-> StoreSubmapOps substore subName key2 value
-> StoreSubmapOps store subName (key1, key2) value
sequenceStoreSubmapOps FieldRef name
l1 LIso (Maybe substore) substore
substoreIso StoreSubmapOps store name key1 substore
ops1 StoreSubmapOps substore subName key2 value
ops2 =
(StoreSubmapOps store subName (key1, key2) value
-> StoreSubmapOps store subName (key1, key2) value)
-> StoreSubmapOps store subName (key1, key2) value
forall a. (a -> a) -> a
fix ((StoreSubmapOps store subName (key1, key2) value
-> StoreSubmapOps store subName (key1, key2) value)
-> StoreSubmapOps store subName (key1, key2) value)
-> (StoreSubmapOps store subName (key1, key2) value
-> StoreSubmapOps store subName (key1, key2) value)
-> StoreSubmapOps store subName (key1, key2) value
forall a b. (a -> b) -> a -> b
$ \StoreSubmapOps store subName (key1, key2) value
res ->
StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef subName -> ((key1, key2) : store : s) :-> (Bool : s)
sopMem = \FieldRef subName
l2 ->
((key1, key2) : store : s) :-> (key1 : key2 : store : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
L.unpair (((key1, key2) : store : s) :-> (key1 : key2 : store : s))
-> ((key1 : key2 : store : s) :-> (key2 : key1 : store : s))
-> ((key1, key2) : store : s) :-> (key2 : key1 : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key1 : key2 : store : s) :-> (key2 : key1 : store : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap (((key1, key2) : store : s) :-> (key2 : key1 : store : s))
-> ((key2 : key1 : store : s) :-> (key2 : Maybe substore : s))
-> ((key1, key2) : store : s) :-> (key2 : Maybe substore : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((key1 : store : s) :-> (Maybe substore : s))
-> (key2 : key1 : store : s) :-> (key2 : Maybe substore : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreSubmapOps store name key1 substore
-> forall (s :: [*]).
KnownValue substore =>
FieldRef name -> (key1 : store : s) :-> (Maybe substore : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps store name key1 substore
ops1 FieldRef name
l1) (((key1, key2) : store : s) :-> (key2 : Maybe substore : s))
-> ((key2 : Maybe substore : s) :-> (Maybe substore : key2 : s))
-> ((key1, key2) : store : s) :-> (Maybe substore : key2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key2 : Maybe substore : s) :-> (Maybe substore : key2 : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap (((key1, key2) : store : s) :-> (Maybe substore : key2 : s))
-> ((Maybe substore : key2 : s) :-> (Bool : s))
-> ((key1, key2) : store : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((substore : key2 : s) :-> (Bool : s))
-> ((key2 : s) :-> (Bool : s))
-> (Maybe substore : key2 : s) :-> (Bool : s)
forall a (s :: [*]) (s' :: [*]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
L.ifSome
((substore : key2 : s) :-> (key2 : substore : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap ((substore : key2 : s) :-> (key2 : substore : s))
-> ((key2 : substore : s) :-> (Bool : s))
-> (substore : key2 : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreSubmapOps substore subName key2 value
-> forall (s :: [*]).
FieldRef subName -> (key2 : substore : s) :-> (Bool : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
sopMem StoreSubmapOps substore subName key2 value
ops2 FieldRef subName
l2)
((key2 : s) :-> s
forall a (s :: [*]). (a : s) :-> s
L.drop ((key2 : s) :-> s)
-> (s :-> (Bool : s)) -> (key2 : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Bool -> s :-> (Bool : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
L.push Bool
False)
, sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRef subName
-> ((key1, key2) : store : s) :-> (Maybe value : s)
sopGet = \FieldRef subName
l2 ->
((key1, key2) : store : s) :-> (key1 : key2 : store : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
L.unpair (((key1, key2) : store : s) :-> (key1 : key2 : store : s))
-> ((key1 : key2 : store : s) :-> (key2 : key1 : store : s))
-> ((key1, key2) : store : s) :-> (key2 : key1 : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key1 : key2 : store : s) :-> (key2 : key1 : store : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap (((key1, key2) : store : s) :-> (key2 : key1 : store : s))
-> ((key2 : key1 : store : s) :-> (key2 : Maybe substore : s))
-> ((key1, key2) : store : s) :-> (key2 : Maybe substore : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((key1 : store : s) :-> (Maybe substore : s))
-> (key2 : key1 : store : s) :-> (key2 : Maybe substore : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreSubmapOps store name key1 substore
-> forall (s :: [*]).
KnownValue substore =>
FieldRef name -> (key1 : store : s) :-> (Maybe substore : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps store name key1 substore
ops1 FieldRef name
l1) (((key1, key2) : store : s) :-> (key2 : Maybe substore : s))
-> ((key2 : Maybe substore : s) :-> (Maybe substore : key2 : s))
-> ((key1, key2) : store : s) :-> (Maybe substore : key2 : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key2 : Maybe substore : s) :-> (Maybe substore : key2 : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap (((key1, key2) : store : s) :-> (Maybe substore : key2 : s))
-> ((Maybe substore : key2 : s) :-> (Maybe value : s))
-> ((key1, key2) : store : s) :-> (Maybe value : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((substore : key2 : s) :-> (Maybe value : s))
-> ((key2 : s) :-> (Maybe value : s))
-> (Maybe substore : key2 : s) :-> (Maybe value : s)
forall a (s :: [*]) (s' :: [*]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
L.ifSome
((substore : key2 : s) :-> (key2 : substore : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap ((substore : key2 : s) :-> (key2 : substore : s))
-> ((key2 : substore : s) :-> (Maybe value : s))
-> (substore : key2 : s) :-> (Maybe value : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreSubmapOps substore subName key2 value
-> forall (s :: [*]).
KnownValue value =>
FieldRef subName -> (key2 : substore : s) :-> (Maybe value : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps substore subName key2 value
ops2 FieldRef subName
l2)
((key2 : s) :-> s
forall a (s :: [*]). (a : s) :-> s
L.drop ((key2 : s) :-> s)
-> (s :-> (Maybe value : s)) -> (key2 : s) :-> (Maybe value : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# s :-> (Maybe value : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
L.none)
, sopUpdate :: forall (s :: [*]).
FieldRef subName
-> ((key1, key2) : Maybe value : store : s) :-> (store : s)
sopUpdate = \FieldRef subName
l2 ->
((key1, key2) : Maybe value : store : s)
:-> (key1 : key2 : Maybe value : substore : store : s)
forall value' (s :: [*]).
((key1, key2) : value' : store : s)
:-> (key1 : key2 : value' : substore : store : s)
prepareUpdate (((key1, key2) : Maybe value : store : s)
:-> (key1 : key2 : Maybe value : substore : store : s))
-> ((key1 : key2 : Maybe value : substore : store : s)
:-> (key1 : Maybe substore : store : s))
-> ((key1, key2) : Maybe value : store : s)
:-> (key1 : Maybe substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((key2 : Maybe value : substore : store : s)
:-> (Maybe substore : store : s))
-> (key1 : key2 : Maybe value : substore : store : s)
:-> (key1 : Maybe substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreSubmapOps substore subName key2 value
-> forall (s :: [*]).
FieldRef subName
-> (key2 : Maybe value : substore : s) :-> (substore : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps substore subName key2 value
ops2 FieldRef subName
l2 ((key2 : Maybe value : substore : store : s)
:-> (substore : store : s))
-> ((substore : store : s) :-> (Maybe substore : store : s))
-> (key2 : Maybe value : substore : store : s)
:-> (Maybe substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# LIso (Maybe substore) substore
-> forall (s :: [*]). (substore : s) :-> (Maybe substore : s)
forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liFrom LIso (Maybe substore) substore
substoreIso) (((key1, key2) : Maybe value : store : s)
:-> (key1 : Maybe substore : store : s))
-> ((key1 : Maybe substore : store : s) :-> (store : s))
-> ((key1, key2) : Maybe value : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreSubmapOps store name key1 substore
-> forall (s :: [*]).
FieldRef name
-> (key1 : Maybe substore : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps store name key1 substore
ops1 FieldRef name
l1
, sopGetAndUpdate :: forall (s :: [*]).
FieldRef subName
-> ((key1, key2) : Maybe value : store : s)
:-> (Maybe value : store : s)
sopGetAndUpdate = \FieldRef subName
l2 ->
((key1, key2) : Maybe value : store : s)
:-> (key1 : key2 : Maybe value : substore : store : s)
forall value' (s :: [*]).
((key1, key2) : value' : store : s)
:-> (key1 : key2 : value' : substore : store : s)
prepareUpdate (((key1, key2) : Maybe value : store : s)
:-> (key1 : key2 : Maybe value : substore : store : s))
-> ((key1 : key2 : Maybe value : substore : store : s)
:-> (key1 : Maybe value : Maybe substore : store : s))
-> ((key1, key2) : Maybe value : store : s)
:-> (key1 : Maybe value : Maybe substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((key2 : Maybe value : substore : store : s)
:-> (Maybe value : Maybe substore : store : s))
-> (key1 : key2 : Maybe value : substore : store : s)
:-> (key1 : Maybe value : Maybe substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreSubmapOps substore subName key2 value
-> forall (s :: [*]).
FieldRef subName
-> (key2 : Maybe value : substore : s)
:-> (Maybe value : substore : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopGetAndUpdate StoreSubmapOps substore subName key2 value
ops2 FieldRef subName
l2 ((key2 : Maybe value : substore : store : s)
:-> (Maybe value : substore : store : s))
-> ((Maybe value : substore : store : s)
:-> (Maybe value : Maybe substore : store : s))
-> (key2 : Maybe value : substore : store : s)
:-> (Maybe value : Maybe substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((substore : store : s) :-> (Maybe substore : store : s))
-> (Maybe value : substore : store : s)
:-> (Maybe value : Maybe substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (LIso (Maybe substore) substore
-> forall (s :: [*]). (substore : s) :-> (Maybe substore : s)
forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liFrom LIso (Maybe substore) substore
substoreIso)) (((key1, key2) : Maybe value : store : s)
:-> (key1 : Maybe value : Maybe substore : store : s))
-> ((key1 : Maybe value : Maybe substore : store : s)
:-> (Maybe value : key1 : Maybe substore : store : s))
-> ((key1, key2) : Maybe value : store : s)
:-> (Maybe value : key1 : Maybe substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(key1 : Maybe value : Maybe substore : store : s)
:-> (Maybe value : key1 : Maybe substore : store : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap (((key1, key2) : Maybe value : store : s)
:-> (Maybe value : key1 : Maybe substore : store : s))
-> ((Maybe value : key1 : Maybe substore : store : s)
:-> (Maybe value : store : s))
-> ((key1, key2) : Maybe value : store : s)
:-> (Maybe value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((key1 : Maybe substore : store : s) :-> (store : s))
-> (Maybe value : key1 : Maybe substore : store : s)
:-> (Maybe value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreSubmapOps store name key1 substore
-> forall (s :: [*]).
FieldRef name
-> (key1 : Maybe substore : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps store name key1 substore
ops1 FieldRef name
l1)
, sopDelete :: forall (s :: [*]).
FieldRef subName -> ((key1, key2) : store : s) :-> (store : s)
sopDelete = \FieldRef subName
l2 ->
((store : s) :-> (Maybe value : store : s))
-> ((key1, key2) : store : s)
:-> ((key1, key2) : Maybe value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (store : s) :-> (Maybe value : store : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
L.none (((key1, key2) : store : s)
:-> ((key1, key2) : Maybe value : store : s))
-> (((key1, key2) : Maybe value : store : s) :-> (store : s))
-> ((key1, key2) : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreSubmapOps store subName (key1, key2) value
-> forall (s :: [*]).
FieldRef subName
-> ((key1, key2) : Maybe value : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps store subName (key1, key2) value
res FieldRef subName
l2
, sopInsert :: forall (s :: [*]).
FieldRef subName
-> ((key1, key2) : value : store : s) :-> (store : s)
sopInsert = \FieldRef subName
l2 ->
((key1, key2) : value : store : s)
:-> (key1 : key2 : value : substore : store : s)
forall value' (s :: [*]).
((key1, key2) : value' : store : s)
:-> (key1 : key2 : value' : substore : store : s)
prepareUpdate (((key1, key2) : value : store : s)
:-> (key1 : key2 : value : substore : store : s))
-> ((key1 : key2 : value : substore : store : s)
:-> (key1 : substore : store : s))
-> ((key1, key2) : value : store : s)
:-> (key1 : substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((key2 : value : substore : store : s) :-> (substore : store : s))
-> (key1 : key2 : value : substore : store : s)
:-> (key1 : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreSubmapOps substore subName key2 value
-> forall (s :: [*]).
FieldRef subName
-> (key2 : value : substore : s) :-> (substore : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopInsert StoreSubmapOps substore subName key2 value
ops2 FieldRef subName
l2) (((key1, key2) : value : store : s)
:-> (key1 : substore : store : s))
-> ((key1 : substore : store : s) :-> (store : s))
-> ((key1, key2) : value : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreSubmapOps store name key1 substore
-> forall (s :: [*]).
FieldRef name -> (key1 : substore : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopInsert StoreSubmapOps store name key1 substore
ops1 FieldRef name
l1
}
where
prepareUpdate
:: (key1, key2) : value' : store : s
:-> key1 : key2 : value' : substore : store : s
prepareUpdate :: forall value' (s :: [*]).
((key1, key2) : value' : store : s)
:-> (key1 : key2 : value' : substore : store : s)
prepareUpdate =
((key1, key2) : value' : store : s)
:-> ((key1, key2) : (key1, key2) : value' : store : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup (((key1, key2) : value' : store : s)
:-> ((key1, key2) : (key1, key2) : value' : store : s))
-> (((key1, key2) : (key1, key2) : value' : store : s)
:-> (key1 : (key1, key2) : value' : store : s))
-> ((key1, key2) : value' : store : s)
:-> (key1 : (key1, key2) : value' : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((key1, key2) : (key1, key2) : value' : store : s)
:-> (key1 : (key1, key2) : value' : store : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
L.car (((key1, key2) : value' : store : s)
:-> (key1 : (key1, key2) : value' : store : s))
-> ((key1 : (key1, key2) : value' : store : s)
:-> (key1 : key2 : value' : substore : store : s))
-> ((key1, key2) : value' : store : s)
:-> (key1 : key2 : value' : substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(((key1, key2) : value' : store : s)
:-> (key2 : value' : substore : store : s))
-> (key1 : (key1, key2) : value' : store : s)
:-> (key1 : key2 : value' : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip
( ((key1, key2) : value' : store : s)
:-> (value' : (key1, key2) : store : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap (((key1, key2) : value' : store : s)
:-> (value' : (key1, key2) : store : s))
-> ((value' : (key1, key2) : store : s)
:-> (value' : key2 : substore : store : s))
-> ((key1, key2) : value' : store : s)
:-> (value' : key2 : substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(((key1, key2) : store : s) :-> (key2 : substore : store : s))
-> (value' : (key1, key2) : store : s)
:-> (value' : key2 : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip
( ((key1, key2) : store : s) :-> (key1 : key2 : store : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
L.unpair (((key1, key2) : store : s) :-> (key1 : key2 : store : s))
-> ((key1 : key2 : store : s) :-> (key2 : key1 : store : s))
-> ((key1, key2) : store : s) :-> (key2 : key1 : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key1 : key2 : store : s) :-> (key2 : key1 : store : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap (((key1, key2) : store : s) :-> (key2 : key1 : store : s))
-> ((key2 : key1 : store : s) :-> (key2 : substore : store : s))
-> ((key1, key2) : store : s) :-> (key2 : substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((key1 : store : s) :-> (substore : store : s))
-> (key2 : key1 : store : s) :-> (key2 : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip
( ((store : s) :-> (store : store : s))
-> (key1 : store : s) :-> (key1 : store : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup @store) ((key1 : store : s) :-> (key1 : store : store : s))
-> ((key1 : store : store : s) :-> (Maybe substore : store : s))
-> (key1 : store : s) :-> (Maybe substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreSubmapOps store name key1 substore
-> forall (s :: [*]).
KnownValue substore =>
FieldRef name -> (key1 : store : s) :-> (Maybe substore : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps store name key1 substore
ops1 FieldRef name
l1 ((key1 : store : s) :-> (Maybe substore : store : s))
-> ((Maybe substore : store : s) :-> (substore : store : s))
-> (key1 : store : s) :-> (substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# LIso (Maybe substore) substore
-> forall (s :: [*]). (Maybe substore : s) :-> (substore : s)
forall a b. LIso a b -> forall (s :: [*]). (a : s) :-> (b : s)
liTo LIso (Maybe substore) substore
substoreIso
)
) (((key1, key2) : value' : store : s)
:-> (value' : key2 : substore : store : s))
-> ((value' : key2 : substore : store : s)
:-> (key2 : value' : substore : store : s))
-> ((key1, key2) : value' : store : s)
:-> (key2 : value' : substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(value' : key2 : substore : store : s)
:-> (key2 : value' : substore : store : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap
)
composeStoreEntrypointOps
:: (HasDupableGetters store, Dupable substore)
=> FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreEntrypointOps substore epName epParam epStore
-> StoreEntrypointOps store epName epParam epStore
composeStoreEntrypointOps :: forall {k} store substore (nameInStore :: k) (epName :: Symbol)
epParam epStore.
(HasDupableGetters store, Dupable substore) =>
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreEntrypointOps substore epName epParam epStore
-> StoreEntrypointOps store epName epParam epStore
composeStoreEntrypointOps FieldRef nameInStore
l1 StoreFieldOps store nameInStore substore
ops1 StoreEntrypointOps substore epName epParam epStore
ops2 = StoreEntrypointOps
{ sopToEpLambda :: forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopToEpLambda = \Label epName
l2 ->
StoreFieldOps store nameInStore substore
-> forall (s :: [*]).
FieldRef nameInStore -> (store : s) :-> (substore : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1 ((store : s) :-> (substore : s))
-> ((substore : s) :-> (EntrypointLambda epParam epStore : s))
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreEntrypointOps substore epName epParam epStore
-> forall (s :: [*]).
Label epName
-> (substore : s) :-> (EntrypointLambda epParam epStore : s)
forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopToEpLambda StoreEntrypointOps substore epName epParam epStore
ops2 Label epName
l2
, sopSetEpLambda :: forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda = \Label epName
l2 ->
((store : s) :-> (substore : store : s))
-> (EntrypointLambda epParam epStore : store : s)
:-> (EntrypointLambda epParam epStore : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (store : s) :-> (substore : store : s)
forall {k} ftype store (fname :: k) (s :: [*]).
(Dupable ftype, HasDupableGetters store) =>
StoreFieldOps store fname ftype
-> FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1) ((EntrypointLambda epParam epStore : store : s)
:-> (EntrypointLambda epParam epStore : substore : store : s))
-> ((EntrypointLambda epParam epStore : substore : store : s)
:-> (substore : store : s))
-> (EntrypointLambda epParam epStore : store : s)
:-> (substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreEntrypointOps substore epName epParam epStore
-> forall (s :: [*]).
HasDupableGetters substore =>
Label epName
-> (EntrypointLambda epParam epStore : substore : s)
:-> (substore : s)
forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
HasDupableGetters store =>
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda StoreEntrypointOps substore epName epParam epStore
ops2 Label epName
l2 ((EntrypointLambda epParam epStore : store : s)
:-> (substore : store : s))
-> ((substore : store : s) :-> (store : s))
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (substore : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreFieldOps store fname ftype
-> FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1
, sopToEpStore :: forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore = \Label epName
l2 ->
StoreFieldOps store nameInStore substore
-> forall (s :: [*]).
FieldRef nameInStore -> (store : s) :-> (substore : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1 ((store : s) :-> (substore : s))
-> ((substore : s) :-> (epStore : s))
-> (store : s) :-> (epStore : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreEntrypointOps substore epName epParam epStore
-> forall (s :: [*]).
Label epName -> (substore : s) :-> (epStore : s)
forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore StoreEntrypointOps substore epName epParam epStore
ops2 Label epName
l2
, sopSetEpStore :: forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore = \Label epName
l2 ->
((store : s) :-> (substore : store : s))
-> (epStore : store : s) :-> (epStore : substore : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (store : s) :-> (substore : store : s)
forall {k} ftype store (fname :: k) (s :: [*]).
(Dupable ftype, HasDupableGetters store) =>
StoreFieldOps store fname ftype
-> FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1) ((epStore : store : s) :-> (epStore : substore : store : s))
-> ((epStore : substore : store : s) :-> (substore : store : s))
-> (epStore : store : s) :-> (substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreEntrypointOps substore epName epParam epStore
-> forall (s :: [*]).
Label epName -> (epStore : substore : s) :-> (substore : s)
forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore StoreEntrypointOps substore epName epParam epStore
ops2 Label epName
l2 ((epStore : store : s) :-> (substore : store : s))
-> ((substore : store : s) :-> (store : s))
-> (epStore : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (substore : store : s) :-> (store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreFieldOps store fname ftype
-> FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1
}
zoomStoreSubmapOps
:: forall store submapName nameInSubmap key value subvalue.
( NiceConstant value, NiceConstant subvalue
, Dupable key, Dupable store
)
=> FieldRef submapName
-> LIso (Maybe value) value
-> LIso (Maybe subvalue) subvalue
-> StoreSubmapOps store submapName key value
-> StoreFieldOps value nameInSubmap subvalue
-> StoreSubmapOps store nameInSubmap key subvalue
zoomStoreSubmapOps :: forall {k} {k} store (submapName :: k) (nameInSubmap :: k) key
value subvalue.
(NiceConstant value, NiceConstant subvalue, Dupable key,
Dupable store) =>
FieldRef submapName
-> LIso (Maybe value) value
-> LIso (Maybe subvalue) subvalue
-> StoreSubmapOps store submapName key value
-> StoreFieldOps value nameInSubmap subvalue
-> StoreSubmapOps store nameInSubmap key subvalue
zoomStoreSubmapOps FieldRef submapName
l1 LIso (Maybe value) value
valueIso LIso (Maybe subvalue) subvalue
subvalueIso StoreSubmapOps store submapName key value
ops1 StoreFieldOps value nameInSubmap subvalue
ops2 =
(StoreSubmapOps store nameInSubmap key subvalue
-> StoreSubmapOps store nameInSubmap key subvalue)
-> StoreSubmapOps store nameInSubmap key subvalue
forall a. (a -> a) -> a
fix ((StoreSubmapOps store nameInSubmap key subvalue
-> StoreSubmapOps store nameInSubmap key subvalue)
-> StoreSubmapOps store nameInSubmap key subvalue)
-> (StoreSubmapOps store nameInSubmap key subvalue
-> StoreSubmapOps store nameInSubmap key subvalue)
-> StoreSubmapOps store nameInSubmap key subvalue
forall a b. (a -> b) -> a -> b
$ \StoreSubmapOps store nameInSubmap key subvalue
res ->
StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef nameInSubmap -> (key : store : s) :-> (Bool : s)
sopMem = \FieldRef nameInSubmap
l2 ->
StoreSubmapOps store submapName key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef submapName -> (key : store : s) :-> (Maybe value : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps store submapName key value
ops1 FieldRef submapName
l1 ((key : store : s) :-> (Maybe value : s))
-> ((Maybe value : s) :-> (Bool : s))
-> (key : store : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((value : s) :-> (Bool : s))
-> (s :-> (Bool : s)) -> (Maybe value : s) :-> (Bool : s)
forall a (s :: [*]) (s' :: [*]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
L.ifSome
(StoreFieldOps value nameInSubmap subvalue
-> forall (s :: [*]).
FieldRef nameInSubmap -> (value : s) :-> (subvalue : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps value nameInSubmap subvalue
ops2 FieldRef nameInSubmap
l2 ((value : s) :-> (subvalue : s))
-> ((subvalue : s) :-> (Maybe subvalue : s))
-> (value : s) :-> (Maybe subvalue : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# LIso (Maybe subvalue) subvalue
-> forall (s :: [*]). (subvalue : s) :-> (Maybe subvalue : s)
forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liFrom LIso (Maybe subvalue) subvalue
subvalueIso ((value : s) :-> (Maybe subvalue : s))
-> ((Maybe subvalue : s) :-> (Bool : s))
-> (value : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Maybe subvalue : s) :-> (Bool : s)
forall a (s :: [*]). (Maybe a : s) :-> (Bool : s)
L.isSome)
(Bool -> s :-> (Bool : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
L.push Bool
False)
, sopGet :: forall (s :: [*]).
KnownValue subvalue =>
FieldRef nameInSubmap -> (key : store : s) :-> (Maybe subvalue : s)
sopGet = \FieldRef nameInSubmap
l2 ->
StoreSubmapOps store submapName key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef submapName -> (key : store : s) :-> (Maybe value : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps store submapName key value
ops1 FieldRef submapName
l1 ((key : store : s) :-> (Maybe value : s))
-> ((Maybe value : s) :-> (Maybe subvalue : s))
-> (key : store : s) :-> (Maybe subvalue : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((value : s) :-> (Maybe subvalue : s))
-> (s :-> (Maybe subvalue : s))
-> (Maybe value : s) :-> (Maybe subvalue : s)
forall a (s :: [*]) (s' :: [*]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
L.ifSome
(StoreFieldOps value nameInSubmap subvalue
-> forall (s :: [*]).
FieldRef nameInSubmap -> (value : s) :-> (subvalue : s)
forall {k} store (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps value nameInSubmap subvalue
ops2 FieldRef nameInSubmap
l2 ((value : s) :-> (subvalue : s))
-> ((subvalue : s) :-> (Maybe subvalue : s))
-> (value : s) :-> (Maybe subvalue : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# LIso (Maybe subvalue) subvalue
-> forall (s :: [*]). (subvalue : s) :-> (Maybe subvalue : s)
forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liFrom LIso (Maybe subvalue) subvalue
subvalueIso)
s :-> (Maybe subvalue : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
L.none
, sopUpdate :: forall (s :: [*]).
FieldRef nameInSubmap
-> (key : Maybe subvalue : store : s) :-> (store : s)
sopUpdate = \FieldRef nameInSubmap
l2 ->
((Maybe subvalue : store : s) :-> (subvalue : store : s))
-> (key : Maybe subvalue : store : s)
:-> (key : subvalue : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (LIso (Maybe subvalue) subvalue
-> forall (s :: [*]). (Maybe subvalue : s) :-> (subvalue : s)
forall a b. LIso a b -> forall (s :: [*]). (a : s) :-> (b : s)
liTo LIso (Maybe subvalue) subvalue
subvalueIso) ((key : Maybe subvalue : store : s)
:-> (key : subvalue : store : s))
-> ((key : subvalue : store : s) :-> (key : value : store : s))
-> (key : Maybe subvalue : store : s) :-> (key : value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
FieldRef nameInSubmap
-> (key : subvalue : store : s) :-> (key : value : store : s)
forall (s :: [*]).
FieldRef nameInSubmap
-> (key : subvalue : store : s) :-> (key : value : store : s)
useSubmapValue FieldRef nameInSubmap
l2 ((key : Maybe subvalue : store : s) :-> (key : value : store : s))
-> ((key : value : store : s) :-> (key : Maybe value : store : s))
-> (key : Maybe subvalue : store : s)
:-> (key : Maybe value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((value : store : s) :-> (Maybe value : store : s))
-> (key : value : store : s) :-> (key : Maybe value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (LIso (Maybe value) value
-> forall (s :: [*]). (value : s) :-> (Maybe value : s)
forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liFrom LIso (Maybe value) value
valueIso) ((key : Maybe subvalue : store : s)
:-> (key : Maybe value : store : s))
-> ((key : Maybe value : store : s) :-> (store : s))
-> (key : Maybe subvalue : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreSubmapOps store submapName key value
-> forall (s :: [*]).
FieldRef submapName
-> (key : Maybe value : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps store submapName key value
ops1 FieldRef submapName
l1
, sopGetAndUpdate :: forall (s :: [*]).
FieldRef nameInSubmap
-> (key : Maybe subvalue : store : s)
:-> (Maybe subvalue : store : s)
sopGetAndUpdate = \FieldRef nameInSubmap
l2 ->
((Maybe subvalue : store : s) :-> (subvalue : store : s))
-> (key : Maybe subvalue : store : s)
:-> (key : subvalue : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (LIso (Maybe subvalue) subvalue
-> forall (s :: [*]). (Maybe subvalue : s) :-> (subvalue : s)
forall a b. LIso a b -> forall (s :: [*]). (a : s) :-> (b : s)
liTo LIso (Maybe subvalue) subvalue
subvalueIso) ((key : Maybe subvalue : store : s)
:-> (key : subvalue : store : s))
-> ((key : subvalue : store : s)
:-> (key : subvalue : value : store : s))
-> (key : Maybe subvalue : store : s)
:-> (key : subvalue : value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
(key : subvalue : store : s)
:-> (key : subvalue : value : store : s)
forall (s :: [*]).
(key : subvalue : store : s)
:-> (key : subvalue : value : store : s)
getSubmapValue ((key : Maybe subvalue : store : s)
:-> (key : subvalue : value : store : s))
-> ((key : subvalue : value : store : s)
:-> (key : subvalue : subvalue : value : store : s))
-> (key : Maybe subvalue : store : s)
:-> (key : subvalue : subvalue : value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((subvalue : value : store : s)
:-> (subvalue : subvalue : value : store : s))
-> (key : subvalue : value : store : s)
:-> (key : subvalue : subvalue : value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup @subvalue) ((key : Maybe subvalue : store : s)
:-> (key : subvalue : subvalue : value : store : s))
-> ((key : subvalue : subvalue : value : store : s)
:-> (subvalue : key : subvalue : value : store : s))
-> (key : Maybe subvalue : store : s)
:-> (subvalue : key : subvalue : value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key : subvalue : subvalue : value : store : s)
:-> (subvalue : key : subvalue : value : store : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap ((key : Maybe subvalue : store : s)
:-> (subvalue : key : subvalue : value : store : s))
-> ((subvalue : key : subvalue : value : store : s)
:-> (subvalue : store : s))
-> (key : Maybe subvalue : store : s) :-> (subvalue : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip @subvalue
( forall (s :: [*]). s :-> s
stackType @(key : subvalue : value : store : _) ((key : subvalue : value : store : s)
:-> (key : subvalue : value : store : s))
-> ((key : subvalue : value : store : s)
:-> (key : value : store : s))
-> (key : subvalue : value : store : s)
:-> (key : value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((subvalue : value : store : s) :-> (value : store : s))
-> (key : subvalue : value : store : s)
:-> (key : value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps value nameInSubmap subvalue
-> FieldRef nameInSubmap
-> (subvalue : value : store : s) :-> (value : store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreFieldOps store fname ftype
-> FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps value nameInSubmap subvalue
ops2 FieldRef nameInSubmap
l2) ((key : subvalue : value : store : s)
:-> (key : value : store : s))
-> ((key : value : store : s) :-> (key : Maybe value : store : s))
-> (key : subvalue : value : store : s)
:-> (key : Maybe value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((value : store : s) :-> (Maybe value : store : s))
-> (key : value : store : s) :-> (key : Maybe value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (LIso (Maybe value) value
-> forall (s :: [*]). (value : s) :-> (Maybe value : s)
forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liFrom LIso (Maybe value) value
valueIso) ((key : subvalue : value : store : s)
:-> (key : Maybe value : store : s))
-> ((key : Maybe value : store : s) :-> (store : s))
-> (key : subvalue : value : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreSubmapOps store submapName key value
-> forall (s :: [*]).
FieldRef submapName
-> (key : Maybe value : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps store submapName key value
ops1 FieldRef submapName
l1
) ((key : Maybe subvalue : store : s) :-> (subvalue : store : s))
-> ((subvalue : store : s) :-> (Maybe subvalue : store : s))
-> (key : Maybe subvalue : store : s)
:-> (Maybe subvalue : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
LIso (Maybe subvalue) subvalue
-> forall (s :: [*]). (subvalue : s) :-> (Maybe subvalue : s)
forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liFrom LIso (Maybe subvalue) subvalue
subvalueIso
, sopDelete :: forall (s :: [*]).
FieldRef nameInSubmap -> (key : store : s) :-> (store : s)
sopDelete = \FieldRef nameInSubmap
l2 ->
((store : s) :-> (Maybe subvalue : store : s))
-> (key : store : s) :-> (key : Maybe subvalue : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (store : s) :-> (Maybe subvalue : store : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
L.none ((key : store : s) :-> (key : Maybe subvalue : store : s))
-> ((key : Maybe subvalue : store : s) :-> (store : s))
-> (key : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreSubmapOps store nameInSubmap key subvalue
-> forall (s :: [*]).
FieldRef nameInSubmap
-> (key : Maybe subvalue : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps store nameInSubmap key subvalue
res FieldRef nameInSubmap
l2
, sopInsert :: forall (s :: [*]).
FieldRef nameInSubmap
-> (key : subvalue : store : s) :-> (store : s)
sopInsert = \FieldRef nameInSubmap
l2 ->
FieldRef nameInSubmap
-> (key : subvalue : store : s) :-> (key : value : store : s)
forall (s :: [*]).
FieldRef nameInSubmap
-> (key : subvalue : store : s) :-> (key : value : store : s)
useSubmapValue FieldRef nameInSubmap
l2 ((key : subvalue : store : s) :-> (key : value : store : s))
-> ((key : value : store : s) :-> (store : s))
-> (key : subvalue : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreSubmapOps store submapName key value
-> forall (s :: [*]).
FieldRef submapName -> (key : value : store : s) :-> (store : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopInsert StoreSubmapOps store submapName key value
ops1 FieldRef submapName
l1
}
where
getSubmapValue
:: key : subvalue : store : s
:-> key : subvalue : value : store : s
getSubmapValue :: forall (s :: [*]).
(key : subvalue : store : s)
:-> (key : subvalue : value : store : s)
getSubmapValue =
(key : subvalue : store : s) :-> (key : key : subvalue : store : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup ((key : subvalue : store : s)
:-> (key : key : subvalue : store : s))
-> ((key : key : subvalue : store : s)
:-> (key : subvalue : value : store : s))
-> (key : subvalue : store : s)
:-> (key : subvalue : value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((key : subvalue : store : s) :-> (subvalue : value : store : s))
-> (key : key : subvalue : store : s)
:-> (key : subvalue : value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip
( (key : subvalue : store : s) :-> (subvalue : key : store : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
L.swap ((key : subvalue : store : s) :-> (subvalue : key : store : s))
-> ((subvalue : key : store : s)
:-> (subvalue : value : store : s))
-> (key : subvalue : store : s) :-> (subvalue : value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
((key : store : s) :-> (value : store : s))
-> (subvalue : key : store : s) :-> (subvalue : value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (((store : s) :-> (store : store : s))
-> (key : store : s) :-> (key : store : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (store : s) :-> (store : store : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup ((key : store : s) :-> (key : store : store : s))
-> ((key : store : store : s) :-> (Maybe value : store : s))
-> (key : store : s) :-> (Maybe value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreSubmapOps store submapName key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef submapName -> (key : store : s) :-> (Maybe value : s)
forall {k} store (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps store submapName key value
ops1 FieldRef submapName
l1 ((key : store : s) :-> (Maybe value : store : s))
-> ((Maybe value : store : s) :-> (value : store : s))
-> (key : store : s) :-> (value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# LIso (Maybe value) value
-> forall (s :: [*]). (Maybe value : s) :-> (value : s)
forall a b. LIso a b -> forall (s :: [*]). (a : s) :-> (b : s)
liTo LIso (Maybe value) value
valueIso)
)
useSubmapValue
:: FieldRef nameInSubmap
-> key : subvalue : store : s
:-> key : value : store : s
useSubmapValue :: forall (s :: [*]).
FieldRef nameInSubmap
-> (key : subvalue : store : s) :-> (key : value : store : s)
useSubmapValue FieldRef nameInSubmap
l2 =
(key : subvalue : store : s)
:-> (key : subvalue : value : store : s)
forall (s :: [*]).
(key : subvalue : store : s)
:-> (key : subvalue : value : store : s)
getSubmapValue ((key : subvalue : store : s)
:-> (key : subvalue : value : store : s))
-> ((key : subvalue : value : store : s)
:-> (key : value : store : s))
-> (key : subvalue : store : s) :-> (key : value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((subvalue : value : store : s) :-> (value : store : s))
-> (key : subvalue : value : store : s)
:-> (key : value : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (StoreFieldOps value nameInSubmap subvalue
-> FieldRef nameInSubmap
-> (subvalue : value : store : s) :-> (value : store : s)
forall {k} store (fname :: k) ftype (s :: [*]).
StoreFieldOps store fname ftype
-> FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps value nameInSubmap subvalue
ops2 FieldRef nameInSubmap
l2)
pushStEp :: Label name -> s :-> MText : s
pushStEp :: forall (name :: Symbol) (s :: [*]). Label name -> s :-> (MText : s)
pushStEp = MText -> s :-> (MText : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
L.push (MText -> s :-> (MText : s))
-> (Label name -> MText) -> Label name -> s :-> (MText : s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label name -> MText
forall (name :: Symbol). Label name -> MText
labelToMText
someStEp
:: Label epName
-> Maybe (EntrypointLambda epParam epStore) : s :-> (EntrypointLambda epParam epStore) : s
someStEp :: forall (epName :: Symbol) epParam epStore (s :: [*]).
Label epName
-> (Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s)
someStEp Label epName
l = ((EntrypointLambda epParam epStore : s)
:-> (EntrypointLambda epParam epStore : s))
-> (s :-> (EntrypointLambda epParam epStore : s))
-> (Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s)
forall a (s :: [*]) (s' :: [*]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
L.ifSome (EntrypointLambda epParam epStore : s)
:-> (EntrypointLambda epParam epStore : s)
forall (s :: [*]). s :-> s
L.nop ((s :-> (EntrypointLambda epParam epStore : s))
-> (Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s))
-> (s :-> (EntrypointLambda epParam epStore : s))
-> (Maybe (EntrypointLambda epParam epStore) : s)
:-> (EntrypointLambda epParam epStore : s)
forall a b. (a -> b) -> a -> b
$
MText -> s :-> (EntrypointLambda epParam epStore : s)
forall (s :: [*]) (t :: [*]). MText -> s :-> t
failUnexpected ([mt|unknown storage entrypoint: |] MText -> MText -> MText
forall a. Semigroup a => a -> a -> a
<> Label epName -> MText
forall (name :: Symbol). Label name -> MText
labelToMText Label epName
l)
setStEp
:: StoreHasSubmap store epmName MText (EntrypointLambda epParam epStore)
=> FieldRef epmName -> Label epsName
-> (EntrypointLambda epParam epStore) : store : s :-> store : s
setStEp :: forall {k} store (epmName :: k) epParam epStore (epsName :: Symbol)
(s :: [*]).
StoreHasSubmap
store epmName MText (EntrypointLambda epParam epStore) =>
FieldRef epmName
-> Label epsName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
setStEp FieldRef epmName
ml Label epsName
l = Label epsName
-> (EntrypointLambda epParam epStore : store : s)
:-> (MText : EntrypointLambda epParam epStore : store : s)
forall (name :: Symbol) (s :: [*]). Label name -> s :-> (MText : s)
pushStEp Label epsName
l ((EntrypointLambda epParam epStore : store : s)
:-> (MText : EntrypointLambda epParam epStore : store : s))
-> ((MText : EntrypointLambda epParam epStore : store : s)
:-> (store : s))
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef epmName
-> (forall (s0 :: [*]) (any :: [*]). (MText : s0) :-> any)
-> (MText : EntrypointLambda epParam epStore : store : s)
:-> (store : s)
forall {k} store (mname :: k) key value (s :: [*]).
(StoreHasSubmap store mname key value, Dupable key) =>
FieldRef mname
-> (forall (s0 :: [*]) (any :: [*]). (key : s0) :-> any)
-> (key : value : store : s) :-> (store : s)
stInsertNew FieldRef epmName
ml (MText : s0) :-> any
forall (s0 :: [*]) (any :: [*]). (MText : s0) :-> any
failAlreadySetEp
where
failAlreadySetEp :: MText : s :-> any
failAlreadySetEp :: forall (s0 :: [*]) (any :: [*]). (MText : s0) :-> any
failAlreadySetEp =
MText -> (MText : s) :-> (MText : MText : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
L.push [mt|Storage entrypoint already set: |] ((MText : s) :-> (MText : MText : s))
-> ((MText : MText : s) :-> (MText : s))
-> (MText : s) :-> (MText : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (MText : MText : s) :-> (MText : s)
forall c (s :: [*]). ConcatOpHs c => (c : c : s) :-> (c : s)
L.concat ((MText : s) :-> (MText : s))
-> ((MText : s) :-> any) -> (MText : s) :-> any
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (MText : s) :-> any
forall a (s :: [*]) (t :: [*]). NiceConstant a => (a : s) :-> t
L.failWith
mkStoreEp
:: Label epName
-> EntrypointLambda epParam epStore
-> EntrypointsField epParam epStore
mkStoreEp :: forall (epName :: Symbol) epParam epStore.
Label epName
-> EntrypointLambda epParam epStore
-> EntrypointsField epParam epStore
mkStoreEp Label epName
l EntrypointLambda epParam epStore
lambda = OneItem (EntrypointsField epParam epStore)
-> EntrypointsField epParam epStore
forall x. One x => OneItem x -> x
one (Label epName -> MText
forall (name :: Symbol). Label name -> MText
labelToMText Label epName
l, EntrypointLambda epParam epStore
lambda)
infixr 8 :-|
data (:-|) (l :: k1) (r :: k2) (p :: FieldRefTag) =
FieldRef l :-| FieldRef r
instance (KnownFieldRef l, KnownFieldRef r) => KnownFieldRef (l :-| r) where
type FieldRefObject (l :-| r) = l :-| r
mkFieldRef :: forall (p :: FieldRefTag). FieldRefObject (l :-| r) p
mkFieldRef = FieldRefObject l 'FieldRefTag
forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty p
forall (p :: FieldRefTag). FieldRefObject l p
mkFieldRef FieldRefObject l 'FieldRefTag -> FieldRef r -> (:-|) l r p
forall k1 k2 (l :: k1) (r :: k2) (p :: FieldRefTag).
FieldRef l -> FieldRef r -> (:-|) l r p
:-| FieldRef r
forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty p
forall (p :: FieldRefTag). FieldRefObject r p
mkFieldRef
instance FieldRefHasFinalName r => FieldRefHasFinalName (l :-| r) where
type FieldRefFinalName (l :-| r) = FieldRefFinalName r
fieldRefFinalName :: FieldRef (l :-| r) -> Label (FieldRefFinalName (l :-| r))
fieldRefFinalName (FieldRef l
_ :-| FieldRef r
r) = FieldRef r -> Label (FieldRefFinalName r)
forall {k} (fr :: k).
FieldRefHasFinalName fr =>
FieldRef fr -> Label (FieldRefFinalName fr)
fieldRefFinalName FieldRef r
r
instance ( StoreHasField store field substore
, StoreHasField substore subfield ty
, KnownFieldRef field, KnownFieldRef subfield
, HasDupableGetters substore
) =>
StoreHasField store (field :-| subfield) ty where
storeFieldOps :: StoreFieldOps store (field :-| subfield) ty
storeFieldOps =
FieldRef subfield
-> StoreFieldOps store subfield ty
-> StoreFieldOps store (field :-| subfield) ty
forall {k} {k} (name :: k) storage field (desiredName :: k).
FieldRef name
-> StoreFieldOps storage name field
-> StoreFieldOps storage desiredName field
storeFieldOpsReferTo (forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty p
mkFieldRef @_ @subfield) (StoreFieldOps store subfield ty
-> StoreFieldOps store (field :-| subfield) ty)
-> StoreFieldOps store subfield ty
-> StoreFieldOps store (field :-| subfield) ty
forall a b. (a -> b) -> a -> b
$
FieldRef field
-> StoreFieldOps store field substore
-> StoreFieldOps substore subfield ty
-> StoreFieldOps store subfield ty
forall {k} {k} substore (nameInStore :: k) store
(nameInSubstore :: k) field.
HasDupableGetters substore =>
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreFieldOps substore nameInSubstore field
-> StoreFieldOps store nameInSubstore field
composeStoreFieldOps (forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty p
mkFieldRef @_ @field) StoreFieldOps store field substore
forall {k} store (fname :: k) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps StoreFieldOps substore subfield ty
forall {k} store (fname :: k) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps
instance ( StoreHasField store field substore
, StoreHasSubmap substore subfield key value
, KnownFieldRef field, KnownFieldRef subfield
, HasDupableGetters store, Dupable substore
) =>
StoreHasSubmap store (field :-| subfield) key value where
storeSubmapOps :: StoreSubmapOps store (field :-| subfield) key value
storeSubmapOps =
FieldRef subfield
-> StoreSubmapOps store subfield key value
-> StoreSubmapOps store (field :-| subfield) key value
forall {k} {k} (name :: k) storage key value (desiredName :: k).
FieldRef name
-> StoreSubmapOps storage name key value
-> StoreSubmapOps storage desiredName key value
storeSubmapOpsReferTo (forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty p
mkFieldRef @_ @subfield) (StoreSubmapOps store subfield key value
-> StoreSubmapOps store (field :-| subfield) key value)
-> StoreSubmapOps store subfield key value
-> StoreSubmapOps store (field :-| subfield) key value
forall a b. (a -> b) -> a -> b
$
FieldRef field
-> StoreFieldOps store field substore
-> StoreSubmapOps substore subfield key value
-> StoreSubmapOps store subfield key value
forall {k} {k} store substore (nameInStore :: k) (mname :: k) key
value.
(HasDupableGetters store, Dupable substore) =>
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreSubmapOps substore mname key value
-> StoreSubmapOps store mname key value
composeStoreSubmapOps (forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty p
mkFieldRef @_ @field) StoreFieldOps store field substore
forall {k} store (fname :: k) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps StoreSubmapOps substore subfield key value
forall {k} store (mname :: k) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps
data SelfRef (p :: FieldRefTag) = SelfRef
this :: SelfRef p
this :: forall (p :: FieldRefTag). SelfRef p
this = SelfRef p
forall (p :: FieldRefTag). SelfRef p
SelfRef
instance KnownFieldRef SelfRef where
type FieldRefObject SelfRef = SelfRef
mkFieldRef :: forall (p :: FieldRefTag). FieldRefObject SelfRef p
mkFieldRef = SelfRef p
FieldRefObject SelfRef p
forall (p :: FieldRefTag). SelfRef p
SelfRef
instance StoreHasField store SelfRef store where
storeFieldOps :: StoreFieldOps store SelfRef store
storeFieldOps = StoreFieldOps
{ sopToField :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag -> (store : s) :-> (store : s)
sopToField = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (store : s) :-> (store : s)
forall (s :: [*]). s :-> s
L.nop
, sopGetFieldOpen :: forall res (s :: [*]).
HasDupableGetters store =>
('[store] :-> '[res, store])
-> ('[store] :-> '[res])
-> FieldRefObject SelfRef 'FieldRefTag
-> (store : s) :-> (res : store : s)
sopGetFieldOpen = \'[store] :-> '[res, store]
contWDup '[store] :-> '[res]
_ SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> ('[store] :-> '[res, store])
-> ('[store] ++ s) :-> ('[res, store] ++ s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed '[store] :-> '[res, store]
contWDup
, sopSetFieldOpen :: forall new (s :: [*]).
('[new, store] :-> '[store])
-> FieldRefObject SelfRef 'FieldRefTag
-> (new : store : s) :-> (store : s)
sopSetFieldOpen = \'[new, store] :-> '[store]
cont SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> ('[new, store] :-> '[store])
-> ('[new, store] ++ s) :-> ('[store] ++ s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed '[new, store] :-> '[store]
cont
}
instance (NiceComparable key, KnownValue value) =>
StoreHasSubmap (BigMap key value) SelfRef key value where
storeSubmapOps :: StoreSubmapOps (BigMap key value) SelfRef key value
storeSubmapOps = StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : BigMap key value : s) :-> (Bool : s)
sopMem = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : BigMap key value : s) :-> (Bool : s)
(MemOpKeyHs (BigMap key value) : BigMap key value : s)
:-> (Bool : s)
forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c : c : s) :-> (Bool : s)
L.mem
, sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRefObject SelfRef 'FieldRefTag
-> (key : BigMap key value : s) :-> (Maybe value : s)
sopGet = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : BigMap key value : s) :-> (Maybe value : s)
(GetOpKeyHs (BigMap key value) : BigMap key value : s)
:-> (Maybe (GetOpValHs (BigMap key value)) : s)
forall c (s :: [*]).
(GetOpHs c, KnownValue (GetOpValHs c)) =>
(GetOpKeyHs c : c : s) :-> (Maybe (GetOpValHs c) : s)
L.get
, sopUpdate :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : Maybe value : BigMap key value : s)
:-> (BigMap key value : s)
sopUpdate = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Maybe value : BigMap key value : s)
:-> (BigMap key value : s)
(UpdOpKeyHs (BigMap key value)
: UpdOpParamsHs (BigMap key value) : BigMap key value : s)
:-> (BigMap key value : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s) :-> (c : s)
L.update
, sopGetAndUpdate :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : Maybe value : BigMap key value : s)
:-> (Maybe value : BigMap key value : s)
sopGetAndUpdate = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Maybe value : BigMap key value : s)
:-> (Maybe value : BigMap key value : s)
(UpdOpKeyHs (BigMap key value)
: UpdOpParamsHs (BigMap key value) : BigMap key value : s)
:-> (Maybe (GetOpValHs (BigMap key value)) : BigMap key value : s)
forall c (s :: [*]).
(GetOpHs c, UpdOpHs c, KnownValue (GetOpValHs c),
UpdOpKeyHs c ~ GetOpKeyHs c) =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s)
:-> (Maybe (GetOpValHs c) : c : s)
L.getAndUpdate
, sopDelete :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : BigMap key value : s) :-> (BigMap key value : s)
sopDelete = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : BigMap key value : s) :-> (BigMap key value : s)
forall k v (s :: [*]).
(NiceComparable k, KnownValue v) =>
(k : BigMap k v : s) :-> (BigMap k v : s)
forall (map :: * -> * -> *) k v (s :: [*]).
(MapInstrs map, NiceComparable k, KnownValue v) =>
(k : map k v : s) :-> (map k v : s)
L.deleteMap
, sopInsert :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : value : BigMap key value : s) :-> (BigMap key value : s)
sopInsert = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : value : BigMap key value : s) :-> (BigMap key value : s)
forall k v (s :: [*]).
NiceComparable k =>
(k : v : BigMap k v : s) :-> (BigMap k v : s)
forall (map :: * -> * -> *) k v (s :: [*]).
(MapInstrs map, NiceComparable k) =>
(k : v : map k v : s) :-> (map k v : s)
L.mapInsert
}
instance (NiceComparable key, KnownValue value) =>
StoreHasSubmap (Map key value) SelfRef key value where
storeSubmapOps :: StoreSubmapOps (Map key value) SelfRef key value
storeSubmapOps = StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : Map key value : s) :-> (Bool : s)
sopMem = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Map key value : s) :-> (Bool : s)
(MemOpKeyHs (Map key value) : Map key value : s) :-> (Bool : s)
forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c : c : s) :-> (Bool : s)
L.mem
, sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRefObject SelfRef 'FieldRefTag
-> (key : Map key value : s) :-> (Maybe value : s)
sopGet = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Map key value : s) :-> (Maybe value : s)
(GetOpKeyHs (Map key value) : Map key value : s)
:-> (Maybe (GetOpValHs (Map key value)) : s)
forall c (s :: [*]).
(GetOpHs c, KnownValue (GetOpValHs c)) =>
(GetOpKeyHs c : c : s) :-> (Maybe (GetOpValHs c) : s)
L.get
, sopUpdate :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : Maybe value : Map key value : s) :-> (Map key value : s)
sopUpdate = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Maybe value : Map key value : s) :-> (Map key value : s)
(UpdOpKeyHs (Map key value)
: UpdOpParamsHs (Map key value) : Map key value : s)
:-> (Map key value : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s) :-> (c : s)
L.update
, sopGetAndUpdate :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : Maybe value : Map key value : s)
:-> (Maybe value : Map key value : s)
sopGetAndUpdate = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Maybe value : Map key value : s)
:-> (Maybe value : Map key value : s)
(UpdOpKeyHs (Map key value)
: UpdOpParamsHs (Map key value) : Map key value : s)
:-> (Maybe (GetOpValHs (Map key value)) : Map key value : s)
forall c (s :: [*]).
(GetOpHs c, UpdOpHs c, KnownValue (GetOpValHs c),
UpdOpKeyHs c ~ GetOpKeyHs c) =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s)
:-> (Maybe (GetOpValHs c) : c : s)
L.getAndUpdate
, sopDelete :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : Map key value : s) :-> (Map key value : s)
sopDelete = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Map key value : s) :-> (Map key value : s)
forall k v (s :: [*]).
(NiceComparable k, KnownValue v) =>
(k : Map k v : s) :-> (Map k v : s)
forall (map :: * -> * -> *) k v (s :: [*]).
(MapInstrs map, NiceComparable k, KnownValue v) =>
(k : map k v : s) :-> (map k v : s)
L.deleteMap
, sopInsert :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : value : Map key value : s) :-> (Map key value : s)
sopInsert = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : value : Map key value : s) :-> (Map key value : s)
forall k v (s :: [*]).
NiceComparable k =>
(k : v : Map k v : s) :-> (Map k v : s)
forall (map :: * -> * -> *) k v (s :: [*]).
(MapInstrs map, NiceComparable k) =>
(k : v : map k v : s) :-> (map k v : s)
L.mapInsert
}
instance (NiceComparable key, Ord key, Dupable key) =>
StoreHasSubmap (Set key) SelfRef key () where
storeSubmapOps :: StoreSubmapOps (Set key) SelfRef key ()
storeSubmapOps = StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : Set key : s) :-> (Bool : s)
sopMem = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Set key : s) :-> (Bool : s)
(MemOpKeyHs (Set key) : Set key : s) :-> (Bool : s)
forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c : c : s) :-> (Bool : s)
L.mem
, sopGet :: forall (s :: [*]).
KnownValue () =>
FieldRefObject SelfRef 'FieldRefTag
-> (key : Set key : s) :-> (Maybe () : s)
sopGet = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Set key : s) :-> (Maybe () : s)
(MemOpKeyHs (Set key) : Set key : s) :-> (Maybe () : s)
forall {s :: [*]}.
(MemOpKeyHs (Set key) : Set key : s) :-> (Maybe () : s)
doGet
, sopUpdate :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : Maybe () : Set key : s) :-> (Set key : s)
sopUpdate = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Maybe () : Set key : s) :-> (Set key : s)
(UpdOpKeyHs (Set key) : Maybe () : Set key : s) :-> (Set key : s)
forall {a} {s :: [*]}.
(UpdOpKeyHs (Set key) : Maybe a : Set key : s) :-> (Set key : s)
doUpdate
, sopGetAndUpdate :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : Maybe () : Set key : s) :-> (Maybe () : Set key : s)
sopGetAndUpdate = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef ->
forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
L.dupN @3 ((key : Maybe () : Set key : s)
:-> (Set key : key : Maybe () : Set key : s))
-> ((Set key : key : Maybe () : Set key : s)
:-> (key : Set key : key : Maybe () : Set key : s))
-> (key : Maybe () : Set key : s)
:-> (key : Set key : key : Maybe () : Set key : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
L.dupN @2 ((key : Maybe () : Set key : s)
:-> (key : Set key : key : Maybe () : Set key : s))
-> ((key : Set key : key : Maybe () : Set key : s)
:-> (Maybe () : key : Maybe () : Set key : s))
-> (key : Maybe () : Set key : s)
:-> (Maybe () : key : Maybe () : Set key : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key : Set key : key : Maybe () : Set key : s)
:-> (Maybe () : key : Maybe () : Set key : s)
(MemOpKeyHs (Set key) : Set key : key : Maybe () : Set key : s)
:-> (Maybe () : key : Maybe () : Set key : s)
forall {s :: [*]}.
(MemOpKeyHs (Set key) : Set key : s) :-> (Maybe () : s)
doGet ((key : Maybe () : Set key : s)
:-> (Maybe () : key : Maybe () : Set key : s))
-> ((Maybe () : key : Maybe () : Set key : s)
:-> (Maybe () : Set key : s))
-> (key : Maybe () : Set key : s) :-> (Maybe () : Set key : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((key : Maybe () : Set key : s) :-> (Set key : s))
-> (Maybe () : key : Maybe () : Set key : s)
:-> (Maybe () : Set key : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (key : Maybe () : Set key : s) :-> (Set key : s)
(UpdOpKeyHs (Set key) : Maybe () : Set key : s) :-> (Set key : s)
forall {a} {s :: [*]}.
(UpdOpKeyHs (Set key) : Maybe a : Set key : s) :-> (Set key : s)
doUpdate
, sopDelete :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : Set key : s) :-> (Set key : s)
sopDelete = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> (key : Set key : s) :-> (Set key : s)
forall e (s :: [*]).
NiceComparable e =>
(e : Set e : s) :-> (Set e : s)
L.setDelete
, sopInsert :: forall (s :: [*]).
FieldRefObject SelfRef 'FieldRefTag
-> (key : () : Set key : s) :-> (Set key : s)
sopInsert = \SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
SelfRef -> ((() : Set key : s) :-> (Set key : s))
-> (key : () : Set key : s) :-> (key : Set key : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (forall a (s :: [*]). (a : s) :-> s
L.drop @()) ((key : () : Set key : s) :-> (key : Set key : s))
-> ((key : Set key : s) :-> (Set key : s))
-> (key : () : Set key : s) :-> (Set key : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (key : Set key : s) :-> (Set key : s)
forall e (s :: [*]).
NiceComparable e =>
(e : Set e : s) :-> (Set e : s)
L.setInsert
}
where
doGet :: (MemOpKeyHs (Set key) : Set key : s) :-> (Maybe () : s)
doGet = (MemOpKeyHs (Set key) : Set key : s) :-> (Bool : s)
forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c : c : s) :-> (Bool : s)
L.mem ((MemOpKeyHs (Set key) : Set key : s) :-> (Bool : s))
-> ((Bool : s) :-> (Maybe () : s))
-> (MemOpKeyHs (Set key) : Set key : s) :-> (Maybe () : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> (Maybe () : s))
-> (s :-> (Maybe () : s)) -> (Bool : s) :-> (Maybe () : s)
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
L.if_ (Maybe () -> s :-> (Maybe () : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
L.push (Maybe () -> s :-> (Maybe () : s))
-> Maybe () -> s :-> (Maybe () : s)
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()) (Maybe () -> s :-> (Maybe () : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
L.push Maybe ()
forall a. Maybe a
Nothing)
doUpdate :: (UpdOpKeyHs (Set key) : Maybe a : Set key : s) :-> (Set key : s)
doUpdate = ((Maybe a : Set key : s) :-> (Bool : Set key : s))
-> (UpdOpKeyHs (Set key) : Maybe a : Set key : s)
:-> (UpdOpKeyHs (Set key) : Bool : Set key : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (Maybe a : Set key : s) :-> (Bool : Set key : s)
forall a (s :: [*]). (Maybe a : s) :-> (Bool : s)
L.isSome ((UpdOpKeyHs (Set key) : Maybe a : Set key : s)
:-> (UpdOpKeyHs (Set key) : Bool : Set key : s))
-> ((UpdOpKeyHs (Set key) : Bool : Set key : s) :-> (Set key : s))
-> (UpdOpKeyHs (Set key) : Maybe a : Set key : s) :-> (Set key : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (UpdOpKeyHs (Set key) : Bool : Set key : s) :-> (Set key : s)
(UpdOpKeyHs (Set key) : UpdOpParamsHs (Set key) : Set key : s)
:-> (Set key : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s) :-> (c : s)
L.update
stNested :: StNestedImpl f SelfRef => f
stNested :: forall f. StNestedImpl f SelfRef => f
stNested = FieldRefObject SelfRef 'FieldRefTag -> f
forall {k} f (acc :: k). StNestedImpl f acc => FieldRef acc -> f
stNestedImpl SelfRef 'FieldRefTag
FieldRefObject SelfRef 'FieldRefTag
forall (p :: FieldRefTag). SelfRef p
this
class StNestedImpl f acc | f -> acc where
stNestedImpl :: FieldRef acc -> f
instance (p ~ 'FieldRefTag, res p ~ FieldRef acc) =>
StNestedImpl (res p) acc where
stNestedImpl :: FieldRef acc -> res p
stNestedImpl FieldRef acc
acc = res p
FieldRef acc
acc
instance ( label ~ FieldRef name
, StNestedImpl f (acc :-| name)
) =>
StNestedImpl (label -> f) acc where
stNestedImpl :: FieldRef acc -> label -> f
stNestedImpl FieldRef acc
acc label
l = FieldRef (acc :-| name) -> f
forall {k} f (acc :: k). StNestedImpl f acc => FieldRef acc -> f
stNestedImpl (FieldRef acc
acc FieldRef acc -> FieldRef name -> (:-|) acc name 'FieldRefTag
forall k1 k2 (l :: k1) (r :: k2) (p :: FieldRefTag).
FieldRef l -> FieldRef r -> (:-|) l r p
:-| label
FieldRef name
l)
data FieldAlias (alias :: k) (p :: FieldRefTag)
= FieldAlias (Proxy alias)
stAlias :: forall alias. FieldRef (FieldAlias alias)
stAlias :: forall {k} (alias :: k). FieldRef (FieldAlias alias)
stAlias = FieldRefObject (FieldAlias alias) 'FieldRefTag
forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty p
forall (p :: FieldRefTag). FieldRefObject (FieldAlias alias) p
mkFieldRef
type FieldNickname alias = FieldAlias (alias :: Symbol)
stNickname :: Label name -> FieldRef (FieldAlias name)
stNickname :: forall (name :: Symbol). Label name -> FieldRef (FieldAlias name)
stNickname Label name
_ = FieldRefObject (FieldAlias name) 'FieldRefTag
forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty p
forall (p :: FieldRefTag). FieldRefObject (FieldAlias name) p
mkFieldRef
instance KnownFieldRef (FieldAlias alias) where
type FieldRefObject (FieldAlias alias) = FieldAlias alias
mkFieldRef :: forall (p :: FieldRefTag). FieldRefObject (FieldAlias alias) p
mkFieldRef = Proxy alias -> FieldAlias alias p
forall k (alias :: k) (p :: FieldRefTag).
Proxy alias -> FieldAlias alias p
FieldAlias Proxy alias
forall {k} (t :: k). Proxy t
Proxy
data k ~> v
infix 9 ~>
data param ::-> store
infix 9 ::->
type family StorageContains store (content :: [NamedField]) :: Constraint where
StorageContains _ '[] = ()
StorageContains store ((n := Identity ty) ': ct) =
(StoreHasField store n ty, StorageContains store ct)
StorageContains store ((n := k ~> v) ': ct) =
(StoreHasSubmap store n k v, StorageContains store ct)
StorageContains store ((n := ep ::-> es) ': ct) =
(StoreHasEntrypoint store n ep es, StorageContains store ct)
StorageContains store ((n := ty) ': ct) =
(StoreHasField store n ty, StorageContains store ct)