{-# 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
, 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 qualified Data.Kind as Kind
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 qualified Lorentz.Instr as L
import Lorentz.Iso
import qualified Lorentz.Macro 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
forall (n :: Symbol) (p :: FieldRefTag).
KnownSymbol n =>
FieldName n p
FieldName
instance KnownSymbol name => KnownFieldRef (name :: Symbol) where
type FieldRefObject name = FieldName name
mkFieldRef :: FieldRefObject name p
mkFieldRef = 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 :: FieldSymRef n -> Label n
fieldNameToLabel FieldSymRef n
FieldName = Label n
forall (name :: Symbol). KnownSymbol name => Label name
Label
fieldNameFromLabel :: Label n -> FieldSymRef n
fieldNameFromLabel :: Label n -> FieldSymRef n
fieldNameFromLabel Label n
Label = FieldSymRef n
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 (FieldRefFinalName name)
forall (n :: Symbol). FieldSymRef n -> Label n
fieldNameToLabel
data StoreFieldOps store fname ftype = StoreFieldOps
{ StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField
:: forall s.
FieldRef fname -> store : s :-> ftype : s
, StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField
:: forall s. (Dupable store)
=> FieldRef fname -> store : s :-> ftype : store : s
, StoreFieldOps store fname ftype
-> forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField
:: forall s.
FieldRef fname -> ftype : store : s :-> store : s
}
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 :: FieldRef fname -> (store : s) :-> (ftype : s)
stToField = StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
forall store k (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 store)
=> FieldRef fname -> store : s :-> ftype : store : s
stGetField :: FieldRef fname -> (store : s) :-> (ftype : store : s)
stGetField FieldRef fname
l = StoreFieldOps store fname ftype
-> FieldRef fname -> (store : s) :-> (ftype : store : s)
forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
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 :: 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) :-> ((FieldRefFinalName fname :! ftype) : s))
-> (store : s) :-> ((FieldRefFinalName fname :! ftype) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label (FieldRefFinalName fname)
-> (ftype : s) :-> ((FieldRefFinalName fname :! ftype) : 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)
=> FieldRef fname -> store : s :-> (FieldRefFinalName fname :! ftype) : store : s
stGetFieldNamed :: FieldRef fname
-> (store : s) :-> ((FieldRefFinalName fname :! ftype) : store : s)
stGetFieldNamed FieldRef fname
fr = FieldRef fname
-> (store : s) :-> ((FieldRefFinalName fname :! ftype) : store : s)
forall k store (fname :: k) ftype (s :: [*]).
(StoreHasField store fname ftype, FieldRefHasFinalName fname,
Dupable ftype) =>
FieldRef fname
-> (store : s) :-> ((FieldRefFinalName fname :! ftype) : store : s)
stGetFieldNamed FieldRef fname
fr
stSetField
:: (StoreHasField store fname ftype)
=> FieldRef fname -> ftype : store : s :-> store : s
stSetField :: FieldRef fname -> (ftype : store : s) :-> (store : s)
stSetField = StoreFieldOps store fname ftype
-> forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s)
forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
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
{ StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
sopMem
:: forall s.
FieldRef mname -> key : store : s :-> Bool : s
, 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
, 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
, 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
, StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopDelete
:: forall s.
FieldRef mname -> key : store : s :-> store : s
, 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
, Dupable store
) => 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 a. IsLabel name a => a
forall (x :: Symbol) a. IsLabel x a => a
fromLabel @name FieldRefObject name 'FieldRefTag
-> FieldRef SelfRef -> (:-|) name SelfRef 'FieldRefTag
forall k1 k2 (l :: k1) (r :: k2) (p :: FieldRefTag).
FieldRef l -> FieldRef r -> (:-|) l r p
:-| FieldRef SelfRef
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 :: FieldRef mname -> (key : store : s) :-> (Bool : s)
stMem = StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
forall store k (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 :: 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 store k (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 :: 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 store k (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 :: 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 store k (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 :: FieldRef mname -> (key : store : s) :-> (store : s)
stDelete = StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
forall store k (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 :: 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 store k (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 :: 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
{ 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
, StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda
:: forall s.
Label epName
-> (EntrypointLambda epParam epStore) : store : s :-> store : s
, StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore
:: forall s.
Label epName
-> store : s :-> epStore : s
, 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 :: 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 :: 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 :: 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
=> Label epName -> (EntrypointLambda epParam epStore) : store : s :-> store : s
stSetEpLambda :: Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
stSetEpLambda = StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
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 :: 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 :: 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 :: 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 :: StoreFieldOps dt fname ftype
storeFieldOpsADT = StoreFieldOps :: forall k store (fname :: k) ftype.
(forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s))
-> (forall (s :: [*]).
Dupable store =>
FieldRef fname -> (store : s) :-> (ftype : store : s))
-> (forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s))
-> StoreFieldOps store fname ftype
StoreFieldOps
{ sopToField :: forall (s :: [*]). FieldRef fname -> (dt : s) :-> (ftype : s)
sopToField = Label fname -> (dt : s) :-> (ftype : 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
forall (n :: Symbol). FieldSymRef n -> Label n
fieldNameToLabel
, sopGetField :: forall (s :: [*]).
Dupable dt =>
FieldRef fname -> (dt : s) :-> (ftype : dt : s)
sopGetField = Label fname -> (dt : s) :-> (ftype : dt : s)
forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable dt) =>
Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
getField (Label fname -> (dt : s) :-> (ftype : dt : s))
-> (FieldName fname 'FieldRefTag -> Label fname)
-> FieldName fname 'FieldRefTag
-> (dt : s) :-> (ftype : dt : s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldName fname 'FieldRefTag -> Label fname
forall (n :: Symbol). FieldSymRef n -> Label n
fieldNameToLabel
, sopSetField :: forall (s :: [*]). FieldRef fname -> (ftype : dt : s) :-> (dt : s)
sopSetField = Label fname -> (ftype : dt : s) :-> (dt : s)
forall dt (name :: Symbol) (st :: [*]).
InstrSetFieldC dt name =>
Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
setField (Label fname -> (ftype : dt : s) :-> (dt : s))
-> (FieldName fname 'FieldRefTag -> Label fname)
-> FieldName fname 'FieldRefTag
-> (ftype : dt : s) :-> (dt : s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldName fname 'FieldRefTag -> Label fname
forall (n :: Symbol). FieldSymRef n -> Label n
fieldNameToLabel
}
storeEntrypointOpsADT
:: ( HasFieldOfType store epmName (EntrypointsField epParam epStore)
, HasFieldOfType store epsName epStore
, KnownValue epParam, KnownValue epStore
, Dupable store
)
=> Label epmName -> Label epsName
-> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsADT :: Label epmName
-> Label epsName -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsADT Label epmName
mapLabel Label epsName
fieldLabel = StoreEntrypointOps :: forall store (epName :: Symbol) epParam epStore.
(forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s))
-> (forall (s :: [*]).
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s))
-> (forall (s :: [*]).
Label epName -> (store : s) :-> (epStore : s))
-> (forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s))
-> StoreEntrypointOps store epName epParam epStore
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)
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 :: [*]).
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 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
# FieldRef SelfRef
-> 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 FieldRef SelfRef
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
, Dupable store
)
=> Label epmName -> Label epsName
-> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsFields :: Label epmName
-> Label epsName -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsFields Label epmName
mapLabel Label epsName
fieldLabel = StoreEntrypointOps :: forall store (epName :: Symbol) epParam epStore.
(forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s))
-> (forall (s :: [*]).
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s))
-> (forall (s :: [*]).
Label epName -> (store : s) :-> (epStore : s))
-> (forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s))
-> StoreEntrypointOps store epName epParam epStore
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)
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 :: [*]).
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 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
# FieldRef SelfRef
-> 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 FieldRef SelfRef
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 :: Label epmName
-> Label epsName -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsSubmapField Label epmName
mapLabel Label epsName
fieldLabel = StoreEntrypointOps :: forall store (epName :: Symbol) epParam epStore.
(forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s))
-> (forall (s :: [*]).
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s))
-> (forall (s :: [*]).
Label epName -> (store : s) :-> (epStore : s))
-> (forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s))
-> StoreEntrypointOps store epName epParam epStore
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 :: [*]).
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
, Dupable storage
)
=> FieldRef fieldsPartName
-> StoreFieldOps storage fname ftype
storeFieldOpsDeeper :: 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 store (nameInStore :: k) substore (nameInSubstore :: k)
field.
Dupable store =>
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
, Dupable storage
)
=> FieldRef bigMapPartName
-> StoreSubmapOps storage mname key value
storeSubmapOpsDeeper :: FieldRef bigMapPartName -> StoreSubmapOps storage mname key value
storeSubmapOpsDeeper FieldRef bigMapPartName
submapLabel =
FieldRef SelfRef
-> 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 FieldRef SelfRef
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 (nameInStore :: k) substore (mname :: k) key
value.
Dupable store =>
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
, Dupable store
)
=> FieldRef nameInStore
-> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsDeeper :: 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 (nameInStore :: k) substore (epName :: Symbol)
epParam epStore.
Dupable store =>
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 :: 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)
sopInsert :: forall (s :: [*]).
FieldRef name -> (key : value : storage : s) :-> (storage : s)
sopDelete :: forall (s :: [*]).
FieldRef name -> (key : storage : s) :-> (storage : s)
sopGetAndUpdate :: forall (s :: [*]).
FieldRef name
-> (key : Maybe value : storage : s)
:-> (Maybe value : storage : s)
sopUpdate :: forall (s :: [*]).
FieldRef name
-> (key : Maybe value : storage : s) :-> (storage : s)
sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRef name -> (key : storage : s) :-> (Maybe value : s)
sopMem :: forall (s :: [*]).
FieldRef name -> (key : storage : s) :-> (Bool : s)
sopInsert :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopDelete :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopGetAndUpdate :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopUpdate :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopGet :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopMem :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
..} =
StoreSubmapOps :: forall k store (mname :: k) key value.
(forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s))
-> StoreSubmapOps store mname key value
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 :: FieldRef name
-> StoreFieldOps storage name field
-> StoreFieldOps storage desiredName field
storeFieldOpsReferTo FieldRef name
l StoreFieldOps{forall (s :: [*]).
Dupable storage =>
FieldRef name -> (storage : s) :-> (field : storage : s)
forall (s :: [*]). FieldRef name -> (storage : s) :-> (field : s)
forall (s :: [*]).
FieldRef name -> (field : storage : s) :-> (storage : s)
sopSetField :: forall (s :: [*]).
FieldRef name -> (field : storage : s) :-> (storage : s)
sopGetField :: forall (s :: [*]).
Dupable storage =>
FieldRef name -> (storage : s) :-> (field : storage : s)
sopToField :: forall (s :: [*]). FieldRef name -> (storage : s) :-> (field : s)
sopSetField :: forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s)
sopGetField :: forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
FieldRef fname -> (store : s) :-> (ftype : store : s)
sopToField :: forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
..} =
StoreFieldOps :: forall k store (fname :: k) ftype.
(forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s))
-> (forall (s :: [*]).
Dupable store =>
FieldRef fname -> (store : s) :-> (ftype : store : s))
-> (forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s))
-> StoreFieldOps store fname ftype
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
, sopGetField :: forall (s :: [*]).
Dupable storage =>
FieldRef desiredName -> (storage : s) :-> (field : storage : s)
sopGetField = \FieldRef desiredName
_l -> FieldRef name -> (storage : s) :-> (field : storage : s)
forall (s :: [*]).
Dupable storage =>
FieldRef name -> (storage : s) :-> (field : storage : s)
sopGetField FieldRef name
l
, sopSetField :: forall (s :: [*]).
FieldRef desiredName -> (field : storage : s) :-> (storage : s)
sopSetField = \FieldRef desiredName
_l -> FieldRef name -> (field : storage : s) :-> (storage : s)
forall (s :: [*]).
FieldRef name -> (field : storage : s) :-> (storage : s)
sopSetField FieldRef name
l
}
storeEntrypointOpsReferTo
:: Label epName
-> StoreEntrypointOps store epName epParam epStore
-> StoreEntrypointOps store desiredName epParam epStore
storeEntrypointOpsReferTo :: 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 :: [*]).
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpStore :: forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopToEpStore :: forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopSetEpLambda :: forall (s :: [*]).
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopToEpLambda :: forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopSetEpStore :: forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
Label epName -> (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)
sopSetEpLambda :: forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
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)
..} = StoreEntrypointOps :: forall store (epName :: Symbol) epParam epStore.
(forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s))
-> (forall (s :: [*]).
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s))
-> (forall (s :: [*]).
Label epName -> (store : s) :-> (epStore : s))
-> (forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s))
-> StoreEntrypointOps store epName epParam epStore
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 :: [*]).
Label desiredName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
sopSetEpLambda = \Label desiredName
_l -> Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
forall (s :: [*]).
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
:: LIso field1 field2
-> StoreFieldOps store name field1
-> StoreFieldOps store name field2
mapStoreFieldOps :: 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)
liFrom :: forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liTo :: forall a b. LIso a b -> forall (s :: [*]). (a : s) :-> (b : s)
liFrom :: forall (s :: [*]). (field2 : s) :-> (field1 : s)
liTo :: forall (s :: [*]). (field1 : s) :-> (field2 : s)
..} StoreFieldOps{forall (s :: [*]).
Dupable store =>
FieldRef name -> (store : s) :-> (field1 : store : s)
forall (s :: [*]).
FieldRef name -> (field1 : store : s) :-> (store : s)
forall (s :: [*]). FieldRef name -> (store : s) :-> (field1 : s)
sopSetField :: forall (s :: [*]).
FieldRef name -> (field1 : store : s) :-> (store : s)
sopGetField :: forall (s :: [*]).
Dupable store =>
FieldRef name -> (store : s) :-> (field1 : store : s)
sopToField :: forall (s :: [*]). FieldRef name -> (store : s) :-> (field1 : s)
sopSetField :: forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s)
sopGetField :: forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
FieldRef fname -> (store : s) :-> (ftype : store : s)
sopToField :: forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
..} = StoreFieldOps :: forall k store (fname :: k) ftype.
(forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s))
-> (forall (s :: [*]).
Dupable store =>
FieldRef fname -> (store : s) :-> (ftype : store : s))
-> (forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s))
-> StoreFieldOps store fname ftype
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
, sopGetField :: forall (s :: [*]).
Dupable store =>
FieldRef name -> (store : s) :-> (field2 : store : s)
sopGetField = \FieldRef name
l -> FieldRef name -> (store : s) :-> (field1 : store : s)
forall (s :: [*]).
Dupable store =>
FieldRef name -> (store : s) :-> (field1 : store : s)
sopGetField FieldRef name
l ((store : s) :-> (field1 : store : s))
-> ((field1 : store : s) :-> (field2 : store : s))
-> (store : s) :-> (field2 : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (field1 : store : s) :-> (field2 : store : s)
forall (s :: [*]). (field1 : s) :-> (field2 : s)
liTo
, sopSetField :: forall (s :: [*]).
FieldRef name -> (field2 : store : s) :-> (store : s)
sopSetField = \FieldRef name
l -> (field2 : store : s) :-> (field1 : store : s)
forall (s :: [*]). (field2 : s) :-> (field1 : s)
liFrom ((field2 : store : s) :-> (field1 : store : s))
-> ((field1 : store : s) :-> (store : s))
-> (field2 : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# FieldRef name -> (field1 : store : s) :-> (store : s)
forall (s :: [*]).
FieldRef name -> (field1 : store : s) :-> (store : s)
sopSetField FieldRef name
l
}
mapStoreSubmapOpsKey
:: Lambda key2 key1
-> StoreSubmapOps store name key1 value
-> StoreSubmapOps store name key2 value
mapStoreSubmapOpsKey :: Lambda key2 key1
-> StoreSubmapOps store name key1 value
-> StoreSubmapOps store name key2 value
mapStoreSubmapOpsKey Lambda 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)
sopInsert :: forall (s :: [*]).
FieldRef name -> (key1 : value : store : s) :-> (store : s)
sopDelete :: forall (s :: [*]).
FieldRef name -> (key1 : store : s) :-> (store : s)
sopGetAndUpdate :: forall (s :: [*]).
FieldRef name
-> (key1 : Maybe value : store : s) :-> (Maybe value : store : s)
sopUpdate :: forall (s :: [*]).
FieldRef name -> (key1 : Maybe value : store : s) :-> (store : s)
sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRef name -> (key1 : store : s) :-> (Maybe value : s)
sopMem :: forall (s :: [*]).
FieldRef name -> (key1 : store : s) :-> (Bool : s)
sopInsert :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopDelete :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopGetAndUpdate :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopUpdate :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopGet :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopMem :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
..} = StoreSubmapOps :: forall k store (mname :: k) key value.
(forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s))
-> StoreSubmapOps store mname key value
StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef name -> (key2 : store : s) :-> (Bool : s)
sopMem = \FieldRef name
l ->
Lambda key2 key1
-> ('[key2] ++ (store : s)) :-> ('[key1] ++ (store : s))
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed Lambda 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 ->
Lambda key2 key1
-> ('[key2] ++ (store : s)) :-> ('[key1] ++ (store : s))
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed Lambda 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 ->
Lambda 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 Lambda 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 ->
Lambda 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 Lambda 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 ->
Lambda key2 key1
-> ('[key2] ++ (store : s)) :-> ('[key1] ++ (store : s))
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
L.framed Lambda 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 ->
Lambda 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 Lambda 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 :: 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)
liFrom :: forall (s :: [*]). (value2 : s) :-> (value1 : s)
liTo :: forall (s :: [*]). (value1 : s) :-> (value2 : s)
liFrom :: forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liTo :: forall a b. LIso a b -> forall (s :: [*]). (a : s) :-> (b : 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)
sopInsert :: forall (s :: [*]).
FieldRef name -> (key : value1 : store : s) :-> (store : s)
sopDelete :: forall (s :: [*]).
FieldRef name -> (key : store : s) :-> (store : s)
sopGetAndUpdate :: forall (s :: [*]).
FieldRef name
-> (key : Maybe value1 : store : s) :-> (Maybe value1 : store : s)
sopUpdate :: forall (s :: [*]).
FieldRef name -> (key : Maybe value1 : store : s) :-> (store : s)
sopGet :: forall (s :: [*]).
KnownValue value1 =>
FieldRef name -> (key : store : s) :-> (Maybe value1 : s)
sopMem :: forall (s :: [*]).
FieldRef name -> (key : store : s) :-> (Bool : s)
sopInsert :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s)
sopDelete :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s)
sopGetAndUpdate :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s)
sopUpdate :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s)
sopGet :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s)
sopMem :: forall store k (mname :: k) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s)
..} = StoreSubmapOps :: forall k store (mname :: k) key value.
(forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s))
-> StoreSubmapOps store mname key value
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 : s) :-> (value2 : s))
-> (Maybe value1 : s) :-> (Maybe value2 : s)
forall (c :: * -> *) b a (s :: [*]).
(LorentzFunctor c, KnownValue b) =>
((a : s) :-> (b : s)) -> (c a : s) :-> (c b : s)
L.lmap (value1 : s) :-> (value2 : s)
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 : store : s) :-> (value1 : store : s))
-> (Maybe value2 : store : s) :-> (Maybe value1 : store : s)
forall (c :: * -> *) b a (s :: [*]).
(LorentzFunctor c, KnownValue b) =>
((a : s) :-> (b : s)) -> (c a : s) :-> (c b : s)
L.lmap (value2 : store : s) :-> (value1 : store : s)
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 : store : s) :-> (value1 : store : s))
-> (Maybe value2 : store : s) :-> (Maybe value1 : store : s)
forall (c :: * -> *) b a (s :: [*]).
(LorentzFunctor c, KnownValue b) =>
((a : s) :-> (b : s)) -> (c a : s) :-> (c b : s)
L.lmap (value2 : store : s) :-> (value1 : store : s)
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 : store : s) :-> (value2 : store : s))
-> (Maybe value1 : store : s) :-> (Maybe value2 : store : s)
forall (c :: * -> *) b a (s :: [*]).
(LorentzFunctor c, KnownValue b) =>
((a : s) :-> (b : s)) -> (c a : s) :-> (c b : s)
L.lmap (value1 : store : s) :-> (value2 : store : s)
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
:: (Dupable store)
=> FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreFieldOps substore nameInSubstore field
-> StoreFieldOps store nameInSubstore field
composeStoreFieldOps :: 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 :: forall k store (fname :: k) ftype.
(forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s))
-> (forall (s :: [*]).
Dupable store =>
FieldRef fname -> (store : s) :-> (ftype : store : s))
-> (forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s))
-> StoreFieldOps store fname ftype
StoreFieldOps
{ sopToField :: forall (s :: [*]).
FieldRef nameInSubstore -> (store : s) :-> (field : s)
sopToField = \FieldRef nameInSubstore
l2 ->
StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (store : s) :-> (substore : s)
forall store k (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
-> FieldRef nameInSubstore -> (substore : s) :-> (field : s)
forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps substore nameInSubstore field
ops2 FieldRef nameInSubstore
l2
, sopGetField :: forall (s :: [*]).
Dupable store =>
FieldRef nameInSubstore -> (store : s) :-> (field : store : s)
sopGetField = \FieldRef nameInSubstore
l2 ->
StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (store : s) :-> (substore : store : s)
forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1 ((store : s) :-> (substore : store : s))
-> ((substore : store : s) :-> (field : store : s))
-> (store : s) :-> (field : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreFieldOps substore nameInSubstore field
-> FieldRef nameInSubstore
-> (substore : store : s) :-> (field : store : s)
forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps substore nameInSubstore field
ops2 FieldRef nameInSubstore
l2
, sopSetField :: forall (s :: [*]).
FieldRef nameInSubstore -> (field : store : s) :-> (store : s)
sopSetField = \FieldRef nameInSubstore
l2 ->
((store : s) :-> (substore : store : s))
-> (field : store : s) :-> (field : 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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
FieldRef fname -> (store : s) :-> (ftype : store : s)
sopGetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1) ((field : store : s) :-> (field : substore : store : s))
-> ((field : substore : store : s) :-> (substore : store : s))
-> (field : store : s) :-> (substore : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
StoreFieldOps substore nameInSubstore field
-> FieldRef nameInSubstore
-> (field : substore : store : s) :-> (substore : store : s)
forall store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps substore nameInSubstore field
ops2 FieldRef nameInSubstore
l2 ((field : store : s) :-> (substore : store : s))
-> ((substore : store : s) :-> (store : s))
-> (field : 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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 FieldRef nameInStore
l1
}
composeStoreSubmapOps
:: (Dupable store)
=> FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreSubmapOps substore mname key value
-> StoreSubmapOps store mname key value
composeStoreSubmapOps :: 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 :: forall k store (mname :: k) key value.
(forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s))
-> StoreSubmapOps store mname key value
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
-> FieldRef nameInStore -> (store : s) :-> (substore : s)
forall store k (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
-> FieldRef mname -> (key : substore : s) :-> (Bool : s)
forall store k (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
-> FieldRef nameInStore -> (store : s) :-> (substore : s)
forall store k (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
-> FieldRef mname -> (key : substore : s) :-> (Maybe value : s)
forall store k (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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
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
-> FieldRef mname
-> (key : Maybe value : substore : store : s)
:-> (substore : store : s)
forall store k (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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
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
-> FieldRef mname
-> (key : Maybe value : substore : store : s)
:-> (Maybe value : substore : store : s)
forall store k (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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
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
-> FieldRef mname
-> (key : substore : store : s) :-> (substore : store : s)
forall store k (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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
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
-> FieldRef mname
-> (key : value : substore : store : s) :-> (substore : store : s)
forall store k (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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
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 :: 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 :: forall k store (mname :: k) key value.
(forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s))
-> StoreSubmapOps store mname key value
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
-> FieldRef name -> (key1 : store : s) :-> (Maybe substore : s)
forall store k (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
-> FieldRef subName -> (key2 : substore : s) :-> (Bool : s)
forall store k (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
-> FieldRef name -> (key1 : store : s) :-> (Maybe substore : s)
forall store k (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
-> FieldRef subName -> (key2 : substore : s) :-> (Maybe value : s)
forall store k (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
-> FieldRef subName
-> (key2 : Maybe value : substore : store : s)
:-> (substore : store : s)
forall store k (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
-> FieldRef name
-> (key1 : Maybe substore : store : s) :-> (store : s)
forall store k (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
-> FieldRef subName
-> (key2 : Maybe value : substore : store : s)
:-> (Maybe value : substore : store : s)
forall store k (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
-> FieldRef name
-> (key1 : Maybe substore : store : s) :-> (store : s)
forall store k (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
-> FieldRef subName
-> ((key1, key2) : Maybe value : store : s) :-> (store : s)
forall store k (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
-> FieldRef subName
-> (key2 : value : substore : store : s) :-> (substore : store : s)
forall store k (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
-> FieldRef name -> (key1 : substore : store : s) :-> (store : s)
forall store k (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 :: ((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 (s :: [*]).
Dupable store =>
(store : s) :-> (store : store : s)
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
-> FieldRef name
-> (key1 : store : store : s) :-> (Maybe substore : store : s)
forall store k (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
:: (Dupable store)
=> FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreEntrypointOps substore epName epParam epStore
-> StoreEntrypointOps store epName epParam epStore
composeStoreEntrypointOps :: 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 :: forall store (epName :: Symbol) epParam epStore.
(forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s))
-> (forall (s :: [*]).
Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s))
-> (forall (s :: [*]).
Label epName -> (store : s) :-> (epStore : s))
-> (forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s))
-> StoreEntrypointOps store epName epParam epStore
StoreEntrypointOps
{ sopToEpLambda :: forall (s :: [*]).
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : s)
sopToEpLambda = \Label epName
l2 ->
StoreFieldOps store nameInStore substore
-> FieldRef nameInStore -> (store : s) :-> (substore : s)
forall store k (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
-> 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 :: [*]).
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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
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
-> Label epName
-> (EntrypointLambda epParam epStore : substore : store : s)
:-> (substore : store : s)
forall store (epName :: Symbol) epParam epStore.
StoreEntrypointOps store epName epParam epStore
-> forall (s :: [*]).
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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
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
-> FieldRef nameInStore -> (store : s) :-> (substore : s)
forall store k (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
-> 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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
Dupable store =>
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
-> Label epName
-> (epStore : substore : store : s) :-> (substore : store : 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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
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 :: 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 :: forall k store (mname :: k) key value.
(forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s))
-> StoreSubmapOps store mname key value
StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef nameInSubmap -> (key : store : s) :-> (Bool : s)
sopMem = \FieldRef nameInSubmap
l2 ->
StoreSubmapOps store submapName key value
-> FieldRef submapName -> (key : store : s) :-> (Maybe value : s)
forall store k (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
-> FieldRef nameInSubmap -> (value : s) :-> (subvalue : s)
forall store k (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
-> FieldRef submapName -> (key : store : s) :-> (Maybe value : s)
forall store k (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
-> FieldRef nameInSubmap -> (value : s) :-> (subvalue : s)
forall store k (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
-> FieldRef submapName
-> (key : Maybe value : store : s) :-> (store : s)
forall store k (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 (s :: [*]).
Dupable subvalue =>
(subvalue : s) :-> (subvalue : subvalue : s)
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
#
((key : subvalue : value : store : s) :-> (store : s))
-> (subvalue : key : subvalue : value : store : s)
:-> (subvalue : store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip @subvalue
( (key : subvalue : value : store : s)
:-> (key : subvalue : value : store : s)
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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
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
-> FieldRef submapName
-> (key : Maybe value : store : s) :-> (store : s)
forall store k (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
-> FieldRef nameInSubmap
-> (key : Maybe subvalue : store : s) :-> (store : s)
forall store k (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
-> FieldRef submapName -> (key : value : store : s) :-> (store : s)
forall store k (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 :: (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
-> FieldRef submapName
-> (key : store : store : s) :-> (Maybe value : store : s)
forall store k (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 :: 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 store k (fname :: k) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps value nameInSubmap subvalue
ops2 FieldRef nameInSubmap
l2)
pushStEp :: Label name -> s :-> MText : s
pushStEp :: 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 :: 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 :: 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 forall (s0 :: [*]) (any :: [*]). (MText : s0) :-> any
failAlreadySetEp
where
failAlreadySetEp :: MText : s :-> any
failAlreadySetEp :: (MText : s) :-> 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 :: 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 :: FieldRefObject (l :-| r) p
mkFieldRef = FieldRefObject l 'FieldRefTag
forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty 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
mkFieldRef
instance FieldRefHasFinalName r => FieldRefHasFinalName (l :-| r) where
type FieldRefFinalName (l :-| r) = FieldRefFinalName r
fieldRefFinalName :: FieldRef (l :-| r) -> Label (FieldRefFinalName (l :-| r))
fieldRefFinalName (_ :-| 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
, Dupable store
) =>
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 (p :: FieldRefTag).
KnownFieldRef subfield =>
FieldRefObject subfield p
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 store (nameInStore :: k) substore (nameInSubstore :: k)
field.
Dupable store =>
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreFieldOps substore nameInSubstore field
-> StoreFieldOps store nameInSubstore field
composeStoreFieldOps (forall (p :: FieldRefTag).
KnownFieldRef field =>
FieldRefObject field p
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
, Dupable store
) =>
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 (p :: FieldRefTag).
KnownFieldRef subfield =>
FieldRefObject subfield p
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 (nameInStore :: k) substore (mname :: k) key
value.
Dupable store =>
FieldRef nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreSubmapOps substore mname key value
-> StoreSubmapOps store mname key value
composeStoreSubmapOps (forall (p :: FieldRefTag).
KnownFieldRef field =>
FieldRefObject field p
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 :: SelfRef p
this = SelfRef p
forall (p :: FieldRefTag). SelfRef p
SelfRef
instance KnownFieldRef SelfRef where
type FieldRefObject SelfRef = SelfRef
mkFieldRef :: FieldRefObject SelfRef p
mkFieldRef = FieldRefObject SelfRef p
forall (p :: FieldRefTag). SelfRef p
SelfRef
instance StoreHasField store SelfRef store where
storeFieldOps :: StoreFieldOps store SelfRef store
storeFieldOps = StoreFieldOps :: forall k store (fname :: k) ftype.
(forall (s :: [*]). FieldRef fname -> (store : s) :-> (ftype : s))
-> (forall (s :: [*]).
Dupable store =>
FieldRef fname -> (store : s) :-> (ftype : store : s))
-> (forall (s :: [*]).
FieldRef fname -> (ftype : store : s) :-> (store : s))
-> StoreFieldOps store fname ftype
StoreFieldOps
{ sopToField :: forall (s :: [*]). FieldRef SelfRef -> (store : s) :-> (store : s)
sopToField = \FieldRef SelfRef
SelfRef -> (store : s) :-> (store : s)
forall (s :: [*]). s :-> s
L.nop
, sopGetField :: forall (s :: [*]).
Dupable store =>
FieldRef SelfRef -> (store : s) :-> (store : store : s)
sopGetField = \FieldRef SelfRef
SelfRef -> (store : s) :-> (store : store : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
L.dup
, sopSetField :: forall (s :: [*]).
FieldRef SelfRef -> (store : store : s) :-> (store : s)
sopSetField = \FieldRef SelfRef
SelfRef -> ((store : s) :-> s) -> (store : store : s) :-> (store : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (store : s) :-> s
forall a (s :: [*]). (a : s) :-> s
L.drop
}
instance (NiceComparable key, KnownValue value) =>
StoreHasSubmap (BigMap key value) SelfRef key value where
storeSubmapOps :: StoreSubmapOps (BigMap key value) SelfRef key value
storeSubmapOps = StoreSubmapOps :: forall k store (mname :: k) key value.
(forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s))
-> StoreSubmapOps store mname key value
StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef SelfRef -> (key : BigMap key value : s) :-> (Bool : s)
sopMem = \FieldRef SelfRef
SelfRef -> (key : BigMap key value : s) :-> (Bool : s)
forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c : c : s) :-> (Bool : s)
L.mem
, sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRef SelfRef
-> (key : BigMap key value : s) :-> (Maybe value : s)
sopGet = \FieldRef SelfRef
SelfRef -> (key : BigMap key value : s) :-> (Maybe value : s)
forall c (s :: [*]).
(GetOpHs c, KnownValue (GetOpValHs c)) =>
(GetOpKeyHs c : c : s) :-> (Maybe (GetOpValHs c) : s)
L.get
, sopUpdate :: forall (s :: [*]).
FieldRef SelfRef
-> (key : Maybe value : BigMap key value : s)
:-> (BigMap key value : s)
sopUpdate = \FieldRef SelfRef
SelfRef -> (key : Maybe 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 :: [*]).
FieldRef SelfRef
-> (key : Maybe value : BigMap key value : s)
:-> (Maybe value : BigMap key value : s)
sopGetAndUpdate = \FieldRef SelfRef
SelfRef -> (key : Maybe value : BigMap key value : s)
:-> (Maybe 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 :: [*]).
FieldRef SelfRef
-> (key : BigMap key value : s) :-> (BigMap key value : s)
sopDelete = \FieldRef SelfRef
SelfRef -> (key : BigMap key value : s) :-> (BigMap key value : 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 :: [*]).
FieldRef SelfRef
-> (key : value : BigMap key value : s) :-> (BigMap key value : s)
sopInsert = \FieldRef SelfRef
SelfRef -> (key : value : BigMap key value : s) :-> (BigMap key value : 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 :: forall k store (mname :: k) key value.
(forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s))
-> StoreSubmapOps store mname key value
StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef SelfRef -> (key : Map key value : s) :-> (Bool : s)
sopMem = \FieldRef SelfRef
SelfRef -> (key : Map key value : s) :-> (Bool : s)
forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c : c : s) :-> (Bool : s)
L.mem
, sopGet :: forall (s :: [*]).
KnownValue value =>
FieldRef SelfRef -> (key : Map key value : s) :-> (Maybe value : s)
sopGet = \FieldRef SelfRef
SelfRef -> (key : Map key value : s) :-> (Maybe value : s)
forall c (s :: [*]).
(GetOpHs c, KnownValue (GetOpValHs c)) =>
(GetOpKeyHs c : c : s) :-> (Maybe (GetOpValHs c) : s)
L.get
, sopUpdate :: forall (s :: [*]).
FieldRef SelfRef
-> (key : Maybe value : Map key value : s) :-> (Map key value : s)
sopUpdate = \FieldRef SelfRef
SelfRef -> (key : Maybe 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 :: [*]).
FieldRef SelfRef
-> (key : Maybe value : Map key value : s)
:-> (Maybe value : Map key value : s)
sopGetAndUpdate = \FieldRef SelfRef
SelfRef -> (key : Maybe value : Map key value : s)
:-> (Maybe 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 :: [*]).
FieldRef SelfRef
-> (key : Map key value : s) :-> (Map key value : s)
sopDelete = \FieldRef SelfRef
SelfRef -> (key : Map key value : s) :-> (Map key value : 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 :: [*]).
FieldRef SelfRef
-> (key : value : Map key value : s) :-> (Map key value : s)
sopInsert = \FieldRef SelfRef
SelfRef -> (key : value : Map key value : s) :-> (Map key value : 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 :: forall k store (mname :: k) key value.
(forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
KnownValue value =>
FieldRef mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname
-> (key : Maybe value : store : s) :-> (Maybe value : store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : store : s) :-> (store : s))
-> (forall (s :: [*]).
FieldRef mname -> (key : value : store : s) :-> (store : s))
-> StoreSubmapOps store mname key value
StoreSubmapOps
{ sopMem :: forall (s :: [*]).
FieldRef SelfRef -> (key : Set key : s) :-> (Bool : s)
sopMem = \FieldRef SelfRef
SelfRef -> (key : Set key : s) :-> (Bool : s)
forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c : c : s) :-> (Bool : s)
L.mem
, sopGet :: forall (s :: [*]).
KnownValue () =>
FieldRef SelfRef -> (key : Set key : s) :-> (Maybe () : s)
sopGet = \FieldRef SelfRef
SelfRef -> (key : Set key : s) :-> (Maybe () : s)
forall (s :: [*]).
(MemOpKeyHs (Set key) : Set key : s) :-> (Maybe () : s)
doGet
, sopUpdate :: forall (s :: [*]).
FieldRef SelfRef
-> (key : Maybe () : Set key : s) :-> (Set key : s)
sopUpdate = \FieldRef SelfRef
SelfRef -> (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 :: [*]).
FieldRef SelfRef
-> (key : Maybe () : Set key : s) :-> (Maybe () : Set key : s)
sopGetAndUpdate = \FieldRef SelfRef
SelfRef ->
forall a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano 3) inp out a, Dupable a) =>
inp :-> out
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)
:-> (MemOpKeyHs (Set key)
: Set key : UpdOpKeyHs (Set key) : Maybe () : Set key : s))
-> (key : Maybe () : Set key : s)
:-> (MemOpKeyHs (Set key)
: Set key : UpdOpKeyHs (Set key) : Maybe () : Set key : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano 2) inp out a, Dupable a) =>
inp :-> out
forall (n :: Nat) a (inp :: [*]) (out :: [*]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
L.dupN @2 ((key : Maybe () : Set key : s)
:-> (MemOpKeyHs (Set key)
: Set key : UpdOpKeyHs (Set key) : Maybe () : Set key : s))
-> ((MemOpKeyHs (Set key)
: Set key : UpdOpKeyHs (Set key) : Maybe () : Set key : s)
:-> (Maybe () : UpdOpKeyHs (Set key) : Maybe () : Set key : s))
-> (key : Maybe () : Set key : s)
:-> (Maybe () : UpdOpKeyHs (Set key) : Maybe () : Set key : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (MemOpKeyHs (Set key)
: Set key : UpdOpKeyHs (Set key) : Maybe () : Set key : s)
:-> (Maybe () : UpdOpKeyHs (Set key) : Maybe () : Set key : s)
forall (s :: [*]).
(MemOpKeyHs (Set key) : Set key : s) :-> (Maybe () : s)
doGet ((key : Maybe () : Set key : s)
:-> (Maybe () : UpdOpKeyHs (Set key) : Maybe () : Set key : s))
-> ((Maybe () : UpdOpKeyHs (Set 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
# ((UpdOpKeyHs (Set key) : Maybe () : Set key : s) :-> (Set key : s))
-> (Maybe () : UpdOpKeyHs (Set key) : Maybe () : Set key : s)
:-> (Maybe () : Set key : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
L.dip (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 :: [*]).
FieldRef SelfRef -> (key : Set key : s) :-> (Set key : s)
sopDelete = \FieldRef SelfRef
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 :: [*]).
FieldRef SelfRef -> (key : () : Set key : s) :-> (Set key : s)
sopInsert = \FieldRef SelfRef
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 (s :: [*]). (() : s) :-> s
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)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s) :-> (c : s)
L.update
stNested :: StNestedImpl f SelfRef => f
stNested :: f
stNested = FieldRef SelfRef -> f
forall k f (acc :: k). StNestedImpl f acc => FieldRef acc -> f
stNestedImpl FieldRef SelfRef
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 :: FieldRef (FieldAlias alias)
stAlias = FieldRef (FieldAlias alias)
forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty p
mkFieldRef
type FieldNickname alias = FieldAlias (alias :: Symbol)
stNickname :: Label name -> FieldRef (FieldAlias name)
stNickname :: Label name -> FieldRef (FieldAlias name)
stNickname Label name
_ = FieldRef (FieldAlias name)
forall k (ty :: k) (p :: FieldRefTag).
KnownFieldRef ty =>
FieldRefObject ty p
mkFieldRef
instance KnownFieldRef (FieldAlias alias) where
type FieldRefObject (FieldAlias alias) = FieldAlias alias
mkFieldRef :: 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)