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

{-# LANGUAGE FunctionalDependencies #-}

-- | This module provides storage interfaces.
module Lorentz.StoreClass
  ( -- * Class
    StoreHasField (..)
  , StoreFieldOps (..)
  , StoreHasSubmap (..)
  , StoreSubmapOps (..)
  , StoreHasEntrypoint (..)
  , StoreEntrypointOps (..)

    -- * Useful type synonyms
  , EntrypointLambda
  , EntrypointsField

    -- * Expressing constraints on storage
  , type (~>)
  , type (::->)
  , StorageContains

    -- * Methods to work with storage
  , stToField
  , stGetField
  , stSetField
  , stMem
  , stGet
  , stUpdate
  , stDelete
  , stInsert
  , stInsertNew
  , stEntrypoint
  , stToEpLambda
  , stGetEpLambda
  , stSetEpLambda
  , stToEpStore
  , stGetEpStore
  , stSetEpStore

    -- * Implementations
  , storeFieldOpsADT
  , storeEntrypointOpsADT
  , storeEntrypointOpsFields
  , storeEntrypointOpsSubmapField
  , storeFieldOpsDeeper
  , storeSubmapOpsDeeper
  , storeEntrypointOpsDeeper
  , storeFieldOpsReferTo
  , storeSubmapOpsReferTo
  , storeEntrypointOpsReferTo
  , composeStoreFieldOps
  , composeStoreSubmapOps
  , composeStoreEntrypointOps

    -- * Storage generation
  , mkStoreEp
  ) where

import Data.Map (singleton)

import Lorentz.ADT
import Lorentz.Base
import Lorentz.Errors (failUnexpected)
import Lorentz.Constraints
import qualified Lorentz.Instr as L
import qualified Lorentz.Macro as L
import Lorentz.Value
import Michelson.Text (labelToMText)

----------------------------------------------------------------------------
-- Fields
----------------------------------------------------------------------------

-- | Datatype containing the full implementation of 'StoreHasField' typeclass.
--
-- We use this grouping because in most cases the implementation will be chosen
-- among the default ones, and initializing all methods at once is simpler
-- and more consistent.
-- (One can say that we are trying to emulate the @DerivingVia@ extension.)
data StoreFieldOps store fname ftype = StoreFieldOps
  { StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField
      :: forall s.
         Label fname -> store : s :-> ftype : s
  , StoreFieldOps store fname ftype
-> forall (s :: [*]).
   Label fname -> (ftype : store : s) :-> (store : s)
sopSetField
      :: forall s.
         Label fname -> ftype : store : s :-> store : s
  }

-- Using fundeps here for the sake of less amount of boilerplate on user side,
-- switch to type families if having any issues with that.
-- | Provides operations on fields for storage.
class StoreHasField store fname ftype | store fname -> ftype where
  storeFieldOps :: StoreFieldOps store fname ftype

-- | Pick storage field.
stToField
  :: StoreHasField store fname ftype
  => Label fname -> store : s :-> ftype : s
stToField :: Label fname -> (store : s) :-> (ftype : s)
stToField = StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store fname ftype
forall store (fname :: Symbol) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps

-- | Get storage field, preserving the storage itself on stack.
stGetField
  :: StoreHasField store fname ftype
  => Label fname -> store : s :-> ftype : store : s
stGetField :: Label fname -> (store : s) :-> (ftype : store : s)
stGetField l :: Label fname
l = (store : s) :-> (store & (store : s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
L.dup ((store : s) :-> (store & (store : s)))
-> ((store & (store : s)) :-> (ftype : store : s))
-> (store : s) :-> (ftype : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreFieldOps store fname ftype
-> Label fname -> (store & (store : s)) :-> (ftype : store : s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store fname ftype
forall store (fname :: Symbol) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps Label fname
l

-- | Update storage field.
stSetField
  :: StoreHasField store fname ftype
  => Label fname -> ftype : store : s :-> store : s
stSetField :: Label fname -> (ftype : store : s) :-> (store : s)
stSetField = StoreFieldOps store fname ftype
-> forall (s :: [*]).
   Label fname -> (ftype : store : s) :-> (store : s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
   Label fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store fname ftype
forall store (fname :: Symbol) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps

----------------------------------------------------------------------------
-- Virtual big maps
----------------------------------------------------------------------------

-- | Datatype containing the full implementation of 'StoreHasSubmap' typeclass.
--
-- We use this grouping because in most cases the implementation will be chosen
-- among the default ones, and initializing all methods at once is simpler
-- and more consistent.
-- (One can say that we are trying to emulate the @DerivingVia@ extension.)
data StoreSubmapOps store mname key value = StoreSubmapOps
  { StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Label mname -> (key : store : s) :-> (Bool : s)
sopMem
      :: forall s.
         Label mname -> key : store : s :-> Bool : s
  , StoreSubmapOps store mname key value
-> forall (s :: [*]).
   KnownValue value =>
   Label mname -> (key : store : s) :-> (Maybe value : s)
sopGet
      :: forall s.
         (KnownValue value)
      => Label mname -> key : store : s :-> Maybe value : s
  , StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Label mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate
      :: forall s.
         Label mname -> key : Maybe value : store : s :-> store : s

    -- Methods below are derivatives of methods above, they can be provided
    -- if for given specific storage type more efficient implementation is
    -- available.
  , StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Maybe (Label mname -> (key : store : s) :-> (store : s))
sopDelete
      :: forall s.
         Maybe (Label mname -> key : store : s :-> store : s)
  , StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Maybe (Label mname -> (key : value : store : s) :-> (store : s))
sopInsert
      :: forall s.
         Maybe (Label mname -> key : value : store : s :-> store : s)
  }

-- | Provides operations on submaps of storage.
class StoreHasSubmap store mname key value | store mname -> key value where
  storeSubmapOps :: StoreSubmapOps store mname key value

-- | Check value presence in storage.
stMem
  :: StoreHasSubmap store mname key value
  => Label mname -> key : store : s :-> Bool : s
stMem :: Label mname -> (key : store : s) :-> (Bool : s)
stMem = StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Label mname -> (key : store : s) :-> (Bool : s)
forall store (mname :: Symbol) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Label mname -> (key : store : s) :-> (Bool : s)
sopMem StoreSubmapOps store mname key value
forall store (mname :: Symbol) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps

-- | Get value in storage.
stGet
  :: (StoreHasSubmap store mname key value, KnownValue value)
  => Label mname -> key : store : s :-> Maybe value : s
stGet :: Label mname -> (key : store : s) :-> (Maybe value : s)
stGet = StoreSubmapOps store mname key value
-> forall (s :: [*]).
   KnownValue value =>
   Label mname -> (key : store : s) :-> (Maybe value : s)
forall store (mname :: Symbol) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
   KnownValue value =>
   Label mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps store mname key value
forall store (mname :: Symbol) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps

-- | Update a value in storage.
stUpdate
  :: StoreHasSubmap store mname key value
  => Label mname -> key : Maybe value : store : s :-> store : s
stUpdate :: Label mname -> (key : Maybe value : store : s) :-> (store : s)
stUpdate = StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Label mname -> (key : Maybe value : store : s) :-> (store : s)
forall store (mname :: Symbol) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Label mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps store mname key value
forall store (mname :: Symbol) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps

-- | Delete a value in storage.
stDelete
  :: forall store mname key value s.
     (StoreHasSubmap store mname key value, KnownValue value)
  => Label mname -> key : store : s :-> store : s
stDelete :: Label mname -> (key : store : s) :-> (store : s)
stDelete l :: Label mname
l = case StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Maybe (Label mname -> (key : store : s) :-> (store : s))
forall store (mname :: Symbol) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Maybe (Label mname -> (key : store : s) :-> (store : s))
sopDelete StoreSubmapOps store mname key value
forall store (mname :: Symbol) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps of
  Just delOp :: Label mname -> (key : store : s) :-> (store : s)
delOp -> Label mname -> (key : store : s) :-> (store : s)
delOp Label mname
l
  Nothing -> ((store : s) :-> (Maybe value & (store : s)))
-> (key : store : s) :-> (key & (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 ((key : store : s) :-> (key & (Maybe value & (store : s))))
-> ((key & (Maybe value & (store : s))) :-> (store : s))
-> (key : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label mname -> (key & (Maybe value & (store : s))) :-> (store : s)
forall store (mname :: Symbol) key value (s :: [*]).
StoreHasSubmap store mname key value =>
Label mname -> (key : Maybe value : store : s) :-> (store : s)
stUpdate Label mname
l

-- | Add a value in storage.
stInsert
  :: StoreHasSubmap store mname key value
  => Label mname -> key : value : store : s :-> store : s
stInsert :: Label mname -> (key : value : store : s) :-> (store : s)
stInsert l :: Label mname
l = case StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Maybe (Label mname -> (key : value : store : s) :-> (store : s))
forall store (mname :: Symbol) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Maybe (Label mname -> (key : value : store : s) :-> (store : s))
sopInsert StoreSubmapOps store mname key value
forall store (mname :: Symbol) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps of
  Just insOp :: Label mname -> (key : value : store : s) :-> (store : s)
insOp -> Label mname -> (key : value : store : s) :-> (store : s)
insOp Label mname
l
  Nothing -> ((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))) :-> (store : s))
-> (key : value : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label mname -> (key & (Maybe value & (store : s))) :-> (store : s)
forall store (mname :: Symbol) key value (s :: [*]).
StoreHasSubmap store mname key value =>
Label mname -> (key : Maybe value : store : s) :-> (store : s)
stUpdate Label mname
l

-- | Add a value in storage, but fail if it will overwrite some existing entry.
stInsertNew
  :: StoreHasSubmap store mname key value
  => Label mname
  -> (forall s0 any. key : s0 :-> any)
  -> key : value : store : s
  :-> store : s
stInsertNew :: Label mname
-> (forall (s0 :: [*]) (any :: [*]). (key : s0) :-> any)
-> (key : value : store : s) :-> (store : s)
stInsertNew l :: Label mname
l doFail :: forall (s0 :: [*]) (any :: [*]). (key : s0) :-> any
doFail =
  forall a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (3 - 1)) s a s1 tail,
 DuupX (ToPeano 3) s a s1 tail) =>
s :-> (a : s)
forall (n :: Nat) a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (n - 1)) s a s1 tail,
 DuupX (ToPeano n) s a s1 tail) =>
s :-> (a : s)
L.duupX @3 ((key : value : store : s) :-> (store : key : value : store : s))
-> ((store : key : value : store : s)
    :-> (key : store : key : value : store : s))
-> (key : value : store : s)
   :-> (key : store : key : value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (2 - 1)) s a s1 tail,
 DuupX (ToPeano 2) s a s1 tail) =>
s :-> (a : s)
forall (n :: Nat) a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (n - 1)) s a s1 tail,
 DuupX (ToPeano n) s a s1 tail) =>
s :-> (a : s)
L.duupX @2 ((key : value : store : s)
 :-> (key : store : key : value : store : s))
-> ((key : store : key : value : store : s)
    :-> (Bool : key : value : store : s))
-> (key : value : store : s) :-> (Bool : key : value : store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label mname
-> (key : store : key : value : store : s)
   :-> (Bool : key : value : store : s)
forall store (mname :: Symbol) key value (s :: [*]).
StoreHasSubmap store mname key value =>
Label mname -> (key : store : s) :-> (Bool : s)
stMem Label mname
l ((key : value : store : s) :-> (Bool : key : value : store : s))
-> ((Bool : key : value : store : s) :-> (store : s))
-> (key : value : store : s) :-> (store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((key : value : store : s) :-> (store : s))
-> ((key : value : store : s) :-> (store : s))
-> (Bool : key : value : store : s) :-> (store : s)
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
L.if_ (key : value : store : s) :-> (store : s)
forall (s0 :: [*]) (any :: [*]). (key : s0) :-> any
doFail (Label mname -> (key : value : store : s) :-> (store : s)
forall store (mname :: Symbol) key value (s :: [*]).
StoreHasSubmap store mname key value =>
Label mname -> (key : value : store : s) :-> (store : s)
stInsert Label mname
l)

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

-- | 'BigMap' can be used as standalone key-value storage,
-- name of submap is not accounted in this case.
instance (key ~ key', value ~ value', NiceComparable key) =>
         StoreHasSubmap (BigMap key' value') name key value where
  storeSubmapOps :: StoreSubmapOps (BigMap key' value') name key value
storeSubmapOps = $WStoreSubmapOps :: forall store (mname :: Symbol) key value.
(forall (s :: [*]).
 Label mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
    KnownValue value =>
    Label mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
    Label mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
    Maybe (Label mname -> (key : store : s) :-> (store : s)))
-> (forall (s :: [*]).
    Maybe (Label mname -> (key : value : store : s) :-> (store : s)))
-> StoreSubmapOps store mname key value
StoreSubmapOps
    { sopMem :: forall (s :: [*]).
Label name -> (key : BigMap key' value' : s) :-> (Bool : s)
sopMem = \_label :: Label name
_label -> (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 =>
Label name -> (key : BigMap key' value' : s) :-> (Maybe value : s)
sopGet = \_label :: Label name
_label -> (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 :: [*]).
Label name
-> (key : Maybe value : BigMap key' value' : s)
   :-> (BigMap key' value' : s)
sopUpdate = \_label :: Label name
_label -> (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
    , sopDelete :: forall (s :: [*]).
Maybe
  (Label name
   -> (key : BigMap key' value' : s) :-> (BigMap key' value' : s))
sopDelete = forall (s :: [*]).
Maybe
  (Label name
   -> (key : BigMap key' value' : s) :-> (BigMap key' value' : s))
forall a. Maybe a
Nothing
    , sopInsert :: forall (s :: [*]).
Maybe
  (Label name
   -> (key : value : BigMap key' value' : s)
      :-> (BigMap key' value' : s))
sopInsert = forall (s :: [*]).
Maybe
  (Label name
   -> (key : value : BigMap key' value' : s)
      :-> (BigMap key' value' : s))
forall a. Maybe a
Nothing
    }

-- | 'Map' can be used as standalone key-value storage if very needed.
instance (key ~ key', value ~ value', NiceComparable key) =>
         StoreHasSubmap (Map key' value') name key value where
  storeSubmapOps :: StoreSubmapOps (Map key' value') name key value
storeSubmapOps = $WStoreSubmapOps :: forall store (mname :: Symbol) key value.
(forall (s :: [*]).
 Label mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
    KnownValue value =>
    Label mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
    Label mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
    Maybe (Label mname -> (key : store : s) :-> (store : s)))
-> (forall (s :: [*]).
    Maybe (Label mname -> (key : value : store : s) :-> (store : s)))
-> StoreSubmapOps store mname key value
StoreSubmapOps
    { sopMem :: forall (s :: [*]).
Label name -> (key : Map key' value' : s) :-> (Bool : s)
sopMem = \_label :: Label name
_label -> (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 =>
Label name -> (key : Map key' value' : s) :-> (Maybe value : s)
sopGet = \_label :: Label name
_label -> (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 :: [*]).
Label name
-> (key : Maybe value : Map key' value' : s)
   :-> (Map key' value' : s)
sopUpdate = \_label :: Label name
_label -> (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
    , sopDelete :: forall (s :: [*]).
Maybe
  (Label name
   -> (key : Map key' value' : s) :-> (Map key' value' : s))
sopDelete = forall (s :: [*]).
Maybe
  (Label name
   -> (key : Map key' value' : s) :-> (Map key' value' : s))
forall a. Maybe a
Nothing
    , sopInsert :: forall (s :: [*]).
Maybe
  (Label name
   -> (key : value : Map key' value' : s) :-> (Map key' value' : s))
sopInsert = forall (s :: [*]).
Maybe
  (Label name
   -> (key : value : Map key' value' : s) :-> (Map key' value' : s))
forall a. Maybe a
Nothing
    }

----------------------------------------------------------------------------
-- Stored Entrypoints
----------------------------------------------------------------------------

-- | Type synonym for a 'Lambda' that can be used as an entrypoint
type EntrypointLambda param store = Lambda (param, store) ([Operation], store)

-- | Type synonym of a 'BigMap' mapping 'MText' (entrypoint names) to
-- 'EntrypointLambda'.
--
-- This is useful when defining instances of 'StoreHasEntrypoint' as a storage
-- field containing one or more entrypoints (lambdas) of the same type.
type EntrypointsField param store = BigMap MText (EntrypointLambda param store)

-- | Datatype containing the full implementation of 'StoreHasEntrypoint' typeclass.
--
-- We use this grouping because in most cases the implementation will be chosen
-- among the default ones, and initializing all methods at once is simpler
-- and more consistent.
-- (One can say that we are trying to emulate the @DerivingVia@ extension.)
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
  }

-- | Provides operations on stored entrypoints.
--
-- @store@ is the storage containing both the entrypoint @epName@ (note: it has
-- to be in a 'BigMap' to take advantage of lazy evaluation) and the @epStore@
-- field this operates on.
class StoreHasEntrypoint store epName epParam epStore | store epName -> epParam epStore where
  storeEpOps :: StoreEntrypointOps store epName epParam epStore

-- | Extracts and executes the @epName@ entrypoint lambda from storage, returing
-- the updated full storage (@store@) and the produced 'Operation's.
stEntrypoint
  :: StoreHasEntrypoint store epName epParam epStore
  => Label epName -> epParam : store : s :-> ([Operation], store) : s
stEntrypoint :: Label epName
-> (epParam : store : s) :-> (([Operation], store) : s)
stEntrypoint l :: 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 ((store : s) :-> (store & (store : s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
L.dup ((store : s) :-> (store & (store : s)))
-> ((store & (store : s))
    :-> (EntrypointLambda epParam epStore : (store & (store : s))))
-> (store : s)
   :-> (EntrypointLambda epParam epStore : (store & (store : s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label epName
-> (store & (store : s))
   :-> (EntrypointLambda epParam epStore : (store & (store : s)))
forall store (epName :: Symbol) epParam epStore (s :: [*]).
StoreHasEntrypoint store epName epParam epStore =>
Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : store : s)
stGetEpLambda Label epName
l ((store : s)
 :-> (EntrypointLambda epParam epStore : (store & (store : s))))
-> ((EntrypointLambda epParam epStore : (store & (store : s)))
    :-> (store & (EntrypointLambda epParam epStore & (store : s))))
-> (store : s)
   :-> (store & (EntrypointLambda epParam epStore & (store : s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (EntrypointLambda epParam epStore : (store & (store : s)))
:-> (store & (EntrypointLambda epParam epStore & (store : s)))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
L.swap ((store : s)
 :-> (store & (EntrypointLambda epParam epStore & (store : s))))
-> ((store & (EntrypointLambda epParam 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
# Label epName
-> (store & (EntrypointLambda epParam epStore & (store : s)))
   :-> (epStore : (EntrypointLambda epParam 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) ((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

-- | Pick stored entrypoint lambda.
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

-- | Get stored entrypoint lambda, preserving the storage itself on the stack.
stGetEpLambda
  :: StoreHasEntrypoint store epName epParam epStore
  => Label epName -> store : s :-> (EntrypointLambda epParam epStore) : store : s
stGetEpLambda :: Label epName
-> (store : s) :-> (EntrypointLambda epParam epStore : store : s)
stGetEpLambda l :: Label epName
l = (store : s) :-> (store & (store : s))
forall a (s :: [*]). (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

-- | Stores the entrypoint lambda in the storage. Fails if already set.
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

-- | Pick the sub-storage that the entrypoint operates on.
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

-- | Get the sub-storage that the entrypoint operates on, preserving the storage
-- itself on the stack.
stGetEpStore
  :: StoreHasEntrypoint store epName epParam epStore
  => Label epName -> store : s :-> epStore : store : s
stGetEpStore :: Label epName -> (store : s) :-> (epStore : store : s)
stGetEpStore l :: Label epName
l = (store : s) :-> (store & (store : s))
forall a (s :: [*]). (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

-- | Update the sub-storage that the entrypoint operates on.
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

----------------------------------------------------------------------------
-- Implementations
----------------------------------------------------------------------------

-- | Implementation of 'StoreHasField' for case of datatype
-- keeping a pack of fields.
storeFieldOpsADT
  :: HasFieldOfType dt fname ftype
  => StoreFieldOps dt fname ftype
storeFieldOpsADT :: StoreFieldOps dt fname ftype
storeFieldOpsADT = $WStoreFieldOps :: forall store (fname :: Symbol) ftype.
(forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s))
-> (forall (s :: [*]).
    Label fname -> (ftype : store : s) :-> (store : s))
-> StoreFieldOps store fname ftype
StoreFieldOps
  { sopToField :: forall (s :: [*]). Label fname -> (dt : s) :-> (ftype : s)
sopToField = forall (s :: [*]). Label fname -> (dt : s) :-> (ftype : s)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt & st) :-> (GetFieldType dt name & st)
toField
  , sopSetField :: forall (s :: [*]). Label fname -> (ftype : dt : s) :-> (dt : s)
sopSetField = forall (s :: [*]). 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
  }

-- | Implementation of 'StoreHasEntrypoint' for a datatype keeping a pack of
-- fields, among which one has contains the entrypoint and another is what such
-- entrypoint operates on.
storeEntrypointOpsADT
  :: ( HasFieldOfType store epmName (EntrypointsField epParam epStore)
     , HasFieldOfType store epsName epStore
     , KnownValue epParam, KnownValue epStore
     )
  => Label epmName -> Label epsName
  -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsADT :: Label epmName
-> Label epsName -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsADT mapLabel :: Label epmName
mapLabel fieldLabel :: Label epsName
fieldLabel = $WStoreEntrypointOps :: 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 = \l :: 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 = \l :: 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 =>
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
# Label epmName
-> Label epName
-> (EntrypointLambda epParam epStore
    & (EntrypointsField epParam epStore : (store & s)))
   :-> (EntrypointsField epParam epStore : (store & s))
forall store (epmName :: Symbol) epParam epStore
       (epsName :: Symbol) (s :: [*]).
StoreHasSubmap
  store epmName MText (EntrypointLambda epParam epStore) =>
Label epmName
-> Label epsName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
setStEp Label epmName
mapLabel 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 = \_l :: 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 = \_l :: 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
  }

-- | Implementation of 'StoreHasEntrypoint' for a datatype that has a 'StoreHasField'
-- for an 'EntrypointsField' that contains the entrypoint and a 'StoreHasField'
-- for the field such entrypoint operates on.
storeEntrypointOpsFields
  :: ( StoreHasField store epmName (EntrypointsField epParam epStore)
     , StoreHasField store epsName epStore
     , KnownValue epParam, KnownValue epStore
     )
  => Label epmName -> Label epsName
  -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsFields :: Label epmName
-> Label epsName -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsFields mapLabel :: Label epmName
mapLabel fieldLabel :: Label epsName
fieldLabel = $WStoreEntrypointOps :: 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 = \l :: Label epName
l -> Label epmName
-> (store : s) :-> (EntrypointsField epParam epStore : s)
forall store (fname :: Symbol) ftype (s :: [*]).
StoreHasField store fname ftype =>
Label fname -> (store : s) :-> (ftype : s)
stToField 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 = \l :: 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) :-> (EntrypointsField epParam epStore : store : s)
forall store (fname :: Symbol) ftype (s :: [*]).
StoreHasField store fname ftype =>
Label fname -> (store : s) :-> (ftype : store : s)
stGetField 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
# Label epmName
-> Label epName
-> (EntrypointLambda epParam epStore
    & (EntrypointsField epParam epStore : store : s))
   :-> (EntrypointsField epParam epStore : store : s)
forall store (epmName :: Symbol) epParam epStore
       (epsName :: Symbol) (s :: [*]).
StoreHasSubmap
  store epmName MText (EntrypointLambda epParam epStore) =>
Label epmName
-> Label epsName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
setStEp Label epmName
mapLabel 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
-> (EntrypointsField epParam epStore : store : s) :-> (store : s)
forall store (fname :: Symbol) ftype (s :: [*]).
StoreHasField store fname ftype =>
Label fname -> (ftype : store : s) :-> (store : s)
stSetField Label epmName
mapLabel
  , sopToEpStore :: forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore = \_l :: Label epName
_l -> Label epsName -> (store : s) :-> (epStore : s)
forall store (fname :: Symbol) ftype (s :: [*]).
StoreHasField store fname ftype =>
Label fname -> (store : s) :-> (ftype : s)
stToField Label epsName
fieldLabel
  , sopSetEpStore :: forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore = \_l :: Label epName
_l -> Label epsName -> (epStore : store : s) :-> (store : s)
forall store (fname :: Symbol) ftype (s :: [*]).
StoreHasField store fname ftype =>
Label fname -> (ftype : store : s) :-> (store : s)
stSetField Label epsName
fieldLabel
  }

-- | Implementation of 'StoreHasEntrypoint' for a datatype that has a 'StoreHasSubmap'
-- that contains the entrypoint and a 'StoreHasField' for the field such
-- entrypoint operates on.
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 mapLabel :: Label epmName
mapLabel fieldLabel :: Label epsName
fieldLabel = $WStoreEntrypointOps :: 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 = \l :: 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
# Label epmName
-> (MText : store : s)
   :-> (Maybe (EntrypointLambda epParam epStore) : s)
forall store (mname :: Symbol) key value (s :: [*]).
(StoreHasSubmap store mname key value, KnownValue value) =>
Label mname -> (key : store : s) :-> (Maybe value : s)
stGet 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 = \l :: Label epName
l -> Label epmName
-> Label epName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
forall store (epmName :: Symbol) epParam epStore
       (epsName :: Symbol) (s :: [*]).
StoreHasSubmap
  store epmName MText (EntrypointLambda epParam epStore) =>
Label epmName
-> Label epsName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
setStEp Label epmName
mapLabel Label epName
l
  , sopToEpStore :: forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore = \_l :: Label epName
_l -> Label epsName -> (store : s) :-> (epStore : s)
forall store (fname :: Symbol) ftype (s :: [*]).
StoreHasField store fname ftype =>
Label fname -> (store : s) :-> (ftype : s)
stToField Label epsName
fieldLabel
  , sopSetEpStore :: forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore = \_l :: Label epName
_l -> Label epsName -> (epStore : store : s) :-> (store : s)
forall store (fname :: Symbol) ftype (s :: [*]).
StoreHasField store fname ftype =>
Label fname -> (ftype : store : s) :-> (store : s)
stSetField Label epsName
fieldLabel
  }

-- | Implementation of 'StoreHasField' for a data type which has an
-- instance of 'StoreHasField' inside.
-- For instance, it can be used for top-level storage.
storeFieldOpsDeeper
  :: ( HasFieldOfType storage fieldsPartName fields
     , StoreHasField fields fname ftype
     )
  => Label fieldsPartName
  -> StoreFieldOps storage fname ftype
storeFieldOpsDeeper :: Label fieldsPartName -> StoreFieldOps storage fname ftype
storeFieldOpsDeeper fieldsLabel :: Label fieldsPartName
fieldsLabel =
  Label fieldsPartName
-> StoreFieldOps storage fieldsPartName fields
-> StoreFieldOps fields fname ftype
-> StoreFieldOps storage fname ftype
forall (nameInStore :: Symbol) store substore
       (nameInSubstore :: Symbol) field.
Label nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreFieldOps substore nameInSubstore field
-> StoreFieldOps store nameInSubstore field
composeStoreFieldOps Label fieldsPartName
fieldsLabel StoreFieldOps storage fieldsPartName fields
forall dt (fname :: Symbol) ftype.
HasFieldOfType dt fname ftype =>
StoreFieldOps dt fname ftype
storeFieldOpsADT StoreFieldOps fields fname ftype
forall store (fname :: Symbol) ftype.
StoreHasField store fname ftype =>
StoreFieldOps store fname ftype
storeFieldOps

-- | Implementation of 'StoreHasSubmap' for a data type which has an
-- instance of 'StoreHasSubmap' inside.
-- For instance, it can be used for top-level storage.
storeSubmapOpsDeeper
  :: ( HasFieldOfType storage bigMapPartName fields
     , StoreHasSubmap fields mname key value
     )
  => Label bigMapPartName
  -> StoreSubmapOps storage mname key value
storeSubmapOpsDeeper :: Label bigMapPartName -> StoreSubmapOps storage mname key value
storeSubmapOpsDeeper submapLabel :: Label bigMapPartName
submapLabel =
  Label bigMapPartName
-> StoreFieldOps storage bigMapPartName fields
-> StoreSubmapOps fields mname key value
-> StoreSubmapOps storage mname key value
forall (nameInStore :: Symbol) store substore (mname :: Symbol) key
       value.
Label nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreSubmapOps substore mname key value
-> StoreSubmapOps store mname key value
composeStoreSubmapOps Label bigMapPartName
submapLabel StoreFieldOps storage bigMapPartName fields
forall dt (fname :: Symbol) ftype.
HasFieldOfType dt fname ftype =>
StoreFieldOps dt fname ftype
storeFieldOpsADT StoreSubmapOps fields mname key value
forall store (mname :: Symbol) key value.
StoreHasSubmap store mname key value =>
StoreSubmapOps store mname key value
storeSubmapOps

-- | Implementation of 'StoreHasEntrypoint' for a data type which has an
-- instance of 'StoreHasEntrypoint' inside.
-- For instance, it can be used for top-level storage.
storeEntrypointOpsDeeper
  :: ( HasFieldOfType store nameInStore substore
     , StoreHasEntrypoint substore epName epParam epStore
     )
  => Label nameInStore
  -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsDeeper :: Label nameInStore
-> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsDeeper fieldsLabel :: Label nameInStore
fieldsLabel =
  Label nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreEntrypointOps substore epName epParam epStore
-> StoreEntrypointOps store epName epParam epStore
forall (nameInStore :: Symbol) store substore (epName :: Symbol)
       epParam epStore.
Label nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreEntrypointOps substore epName epParam epStore
-> StoreEntrypointOps store epName epParam epStore
composeStoreEntrypointOps Label nameInStore
fieldsLabel StoreFieldOps store nameInStore substore
forall dt (fname :: Symbol) ftype.
HasFieldOfType dt fname ftype =>
StoreFieldOps dt 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

{- | Pretend that given 'StoreSubmapOps' implementation is made up
for submap with name @desiredName@, not its actual name.
Logic of the implementation remains the same.

Use case: imagine that your code requires access to submap named @X@,
but in your storage that submap is called @Y@.
Then you implement the instance which makes @X@ refer to @Y@:

@
instance StoreHasSubmap Store X Key Value where
  storeSubmapOps = storeSubmapOpsReferTo #Y storeSubmapOpsForY
@
-}
storeSubmapOpsReferTo
  :: Label name
  -> StoreSubmapOps storage name key value
  -> StoreSubmapOps storage desiredName key value
storeSubmapOpsReferTo :: Label name
-> StoreSubmapOps storage name key value
-> StoreSubmapOps storage desiredName key value
storeSubmapOpsReferTo l :: Label name
l StoreSubmapOps{..} =
  $WStoreSubmapOps :: forall store (mname :: Symbol) key value.
(forall (s :: [*]).
 Label mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
    KnownValue value =>
    Label mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
    Label mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
    Maybe (Label mname -> (key : store : s) :-> (store : s)))
-> (forall (s :: [*]).
    Maybe (Label mname -> (key : value : store : s) :-> (store : s)))
-> StoreSubmapOps store mname key value
StoreSubmapOps
  { sopMem :: forall (s :: [*]).
Label desiredName -> (key : storage : s) :-> (Bool : s)
sopMem = \_l :: Label desiredName
_l -> Label name -> (key : storage : s) :-> (Bool : s)
forall (s :: [*]). Label name -> (key : storage : s) :-> (Bool : s)
sopMem Label name
l
  , sopGet :: forall (s :: [*]).
KnownValue value =>
Label desiredName -> (key : storage : s) :-> (Maybe value : s)
sopGet = \_l :: Label desiredName
_l -> Label name -> (key : storage : s) :-> (Maybe value : s)
forall (s :: [*]).
KnownValue value =>
Label name -> (key : storage : s) :-> (Maybe value : s)
sopGet Label name
l
  , sopUpdate :: forall (s :: [*]).
Label desiredName
-> (key : Maybe value : storage : s) :-> (storage : s)
sopUpdate = \_l :: Label desiredName
_l -> Label name -> (key : Maybe value : storage : s) :-> (storage : s)
forall (s :: [*]).
Label name -> (key : Maybe value : storage : s) :-> (storage : s)
sopUpdate Label name
l
  , sopDelete :: forall (s :: [*]).
Maybe (Label desiredName -> (key : storage : s) :-> (storage : s))
sopDelete = (\op :: Label name -> (key : storage : s) :-> (storage : s)
op _l :: Label desiredName
_l -> Label name -> (key : storage : s) :-> (storage : s)
op Label name
l) ((Label name -> (key : storage : s) :-> (storage : s))
 -> Label desiredName -> (key : storage : s) :-> (storage : s))
-> Maybe (Label name -> (key : storage : s) :-> (storage : s))
-> Maybe
     (Label desiredName -> (key : storage : s) :-> (storage : s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Label name -> (key : storage : s) :-> (storage : s))
forall (s :: [*]).
Maybe (Label name -> (key : storage : s) :-> (storage : s))
sopDelete
  , sopInsert :: forall (s :: [*]).
Maybe
  (Label desiredName
   -> (key : value : storage : s) :-> (storage : s))
sopInsert = (\op :: Label name -> (key : value : storage : s) :-> (storage : s)
op _l :: Label desiredName
_l -> Label name -> (key : value : storage : s) :-> (storage : s)
op Label name
l) ((Label name -> (key : value : storage : s) :-> (storage : s))
 -> Label desiredName
 -> (key : value : storage : s) :-> (storage : s))
-> Maybe
     (Label name -> (key : value : storage : s) :-> (storage : s))
-> Maybe
     (Label desiredName
      -> (key : value : storage : s) :-> (storage : s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Label name -> (key : value : storage : s) :-> (storage : s))
forall (s :: [*]).
Maybe (Label name -> (key : value : storage : s) :-> (storage : s))
sopInsert
  }

-- | Pretend that given 'StoreFieldOps' implementation is made up
-- for field with name @desiredName@, not its actual name.
-- Logic of the implementation remains the same.
--
-- See also 'storeSubmapOpsReferTo'.
storeFieldOpsReferTo
  :: Label name
  -> StoreFieldOps storage name field
  -> StoreFieldOps storage desiredName field
storeFieldOpsReferTo :: Label name
-> StoreFieldOps storage name field
-> StoreFieldOps storage desiredName field
storeFieldOpsReferTo l :: Label name
l StoreFieldOps{..} =
  $WStoreFieldOps :: forall store (fname :: Symbol) ftype.
(forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s))
-> (forall (s :: [*]).
    Label fname -> (ftype : store : s) :-> (store : s))
-> StoreFieldOps store fname ftype
StoreFieldOps
  { sopToField :: forall (s :: [*]).
Label desiredName -> (storage : s) :-> (field : s)
sopToField = \_l :: Label desiredName
_l -> Label name -> (storage : s) :-> (field : s)
forall (s :: [*]). Label name -> (storage : s) :-> (field : s)
sopToField Label name
l
  , sopSetField :: forall (s :: [*]).
Label desiredName -> (field : storage : s) :-> (storage : s)
sopSetField = \_l :: Label desiredName
_l -> Label name -> (field : storage : s) :-> (storage : s)
forall (s :: [*]).
Label name -> (field : storage : s) :-> (storage : s)
sopSetField Label name
l
  }

-- | Pretend that given 'StoreEntrypointOps' implementation is made up
-- for entrypoint with name @desiredName@, not its actual name.
-- Logic of the implementation remains the same.
--
-- See also 'storeSubmapOpsReferTo'.
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 l :: Label epName
l StoreEntrypointOps{..} = $WStoreEntrypointOps :: 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 = \_l :: 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 = \_l :: 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 = \_l :: 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 = \_l :: Label desiredName
_l -> Label epName -> (epStore : store : s) :-> (store : s)
forall (s :: [*]).
Label epName -> (epStore : store : s) :-> (store : s)
sopSetEpStore Label epName
l
  }

-- | Chain two implementations of field operations.
--
-- Suits for a case when your store does not contain its fields directly
-- rather has a nested structure.
composeStoreFieldOps
  :: Label nameInStore
  -> StoreFieldOps store nameInStore substore
  -> StoreFieldOps substore nameInSubstore field
  -> StoreFieldOps store nameInSubstore field
composeStoreFieldOps :: Label nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreFieldOps substore nameInSubstore field
-> StoreFieldOps store nameInSubstore field
composeStoreFieldOps l1 :: Label nameInStore
l1 ops1 :: StoreFieldOps store nameInStore substore
ops1 ops2 :: StoreFieldOps substore nameInSubstore field
ops2 =
  $WStoreFieldOps :: forall store (fname :: Symbol) ftype.
(forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s))
-> (forall (s :: [*]).
    Label fname -> (ftype : store : s) :-> (store : s))
-> StoreFieldOps store fname ftype
StoreFieldOps
  { sopToField :: forall (s :: [*]).
Label nameInSubstore -> (store : s) :-> (field : s)
sopToField = \l2 :: Label nameInSubstore
l2 ->
      StoreFieldOps store nameInStore substore
-> Label nameInStore -> (store : s) :-> (substore : s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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
-> Label nameInSubstore -> (substore : s) :-> (field : s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps substore nameInSubstore field
ops2 Label nameInSubstore
l2
  , sopSetField :: forall (s :: [*]).
Label nameInSubstore -> (field : store : s) :-> (store : s)
sopSetField = \l2 :: Label 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 ((store & s) :-> (store & (store & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
L.dup ((store & s) :-> (store & (store & s)))
-> ((store & (store & s)) :-> (substore : (store & s)))
-> (store & s) :-> (substore : (store & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreFieldOps store nameInStore substore
-> Label nameInStore
-> (store & (store & s)) :-> (substore : (store & s))
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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
-> Label nameInSubstore
-> (field & (substore : (store & s))) :-> (substore : (store & s))
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
   Label fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps substore nameInSubstore field
ops2 Label 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
-> Label nameInStore -> (substore : (store & s)) :-> (store & s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
   Label fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 Label nameInStore
l1
  }

-- | Chain implementations of field and submap operations.
composeStoreSubmapOps
  :: Label nameInStore
  -> StoreFieldOps store nameInStore substore
  -> StoreSubmapOps substore mname key value
  -> StoreSubmapOps store mname key value
composeStoreSubmapOps :: Label nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreSubmapOps substore mname key value
-> StoreSubmapOps store mname key value
composeStoreSubmapOps l1 :: Label nameInStore
l1 ops1 :: StoreFieldOps store nameInStore substore
ops1 ops2 :: StoreSubmapOps substore mname key value
ops2 =
  $WStoreSubmapOps :: forall store (mname :: Symbol) key value.
(forall (s :: [*]).
 Label mname -> (key : store : s) :-> (Bool : s))
-> (forall (s :: [*]).
    KnownValue value =>
    Label mname -> (key : store : s) :-> (Maybe value : s))
-> (forall (s :: [*]).
    Label mname -> (key : Maybe value : store : s) :-> (store : s))
-> (forall (s :: [*]).
    Maybe (Label mname -> (key : store : s) :-> (store : s)))
-> (forall (s :: [*]).
    Maybe (Label mname -> (key : value : store : s) :-> (store : s)))
-> StoreSubmapOps store mname key value
StoreSubmapOps
  { sopMem :: forall (s :: [*]). Label mname -> (key : store : s) :-> (Bool : s)
sopMem = \l2 :: Label 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
-> Label nameInStore -> (store : s) :-> (substore : s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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
-> Label mname -> (key & (substore : s)) :-> (Bool : s)
forall store (mname :: Symbol) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Label mname -> (key : store : s) :-> (Bool : s)
sopMem StoreSubmapOps substore mname key value
ops2 Label mname
l2
  , sopGet :: forall (s :: [*]).
KnownValue value =>
Label mname -> (key : store : s) :-> (Maybe value : s)
sopGet = \l2 :: Label 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
-> Label nameInStore -> (store : s) :-> (substore : s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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
-> Label mname -> (key & (substore : s)) :-> (Maybe value : s)
forall store (mname :: Symbol) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
   KnownValue value =>
   Label mname -> (key : store : s) :-> (Maybe value : s)
sopGet StoreSubmapOps substore mname key value
ops2 Label mname
l2
  , sopUpdate :: forall (s :: [*]).
Label mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate = \l2 :: Label 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 ((store & s) :-> (store & (store & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
L.dup ((store & s) :-> (store & (store & s)))
-> ((store & (store & s)) :-> (substore : (store & s)))
-> (store & s) :-> (substore : (store & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreFieldOps store nameInStore substore
-> Label nameInStore
-> (store & (store & s)) :-> (substore : (store & s))
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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
-> Label mname
-> (key & (Maybe value & (substore : (store & s))))
   :-> (substore : (store & s))
forall store (mname :: Symbol) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Label mname -> (key : Maybe value : store : s) :-> (store : s)
sopUpdate StoreSubmapOps substore mname key value
ops2 Label 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
-> Label nameInStore -> (substore : (store & s)) :-> (store & s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
   Label fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 Label nameInStore
l1
  , sopDelete :: forall (s :: [*]).
Maybe (Label mname -> (key : store : s) :-> (store : s))
sopDelete = case StoreSubmapOps substore mname key value
-> forall (s :: [*]).
   Maybe (Label mname -> (key : substore : s) :-> (substore : s))
forall store (mname :: Symbol) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Maybe (Label mname -> (key : store : s) :-> (store : s))
sopDelete StoreSubmapOps substore mname key value
ops2 of
      Nothing -> Maybe (Label mname -> (key : (store & s)) :-> (store & s))
forall a. Maybe a
Nothing
      Just delOp :: Label mname
-> (key : substore : (store & s)) :-> (substore : (store & s))
delOp -> (Label mname -> (key : (store & s)) :-> (store & s))
-> Maybe (Label mname -> (key : (store & s)) :-> (store & s))
forall a. a -> Maybe a
Just ((Label mname -> (key : (store & s)) :-> (store & s))
 -> Maybe (Label mname -> (key : (store & s)) :-> (store & s)))
-> (Label mname -> (key : (store & s)) :-> (store & s))
-> Maybe (Label mname -> (key : (store & s)) :-> (store & s))
forall a b. (a -> b) -> a -> b
$ \l2 :: Label 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 ((store & s) :-> (store & (store & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
L.dup ((store & s) :-> (store & (store & s)))
-> ((store & (store & s)) :-> (substore : (store & s)))
-> (store & s) :-> (substore : (store & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreFieldOps store nameInStore substore
-> Label nameInStore
-> (store & (store & s)) :-> (substore : (store & s))
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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
#
        Label mname
-> (key : substore : (store & s)) :-> (substore : (store & s))
delOp Label 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
-> Label nameInStore -> (substore : (store & s)) :-> (store & s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
   Label fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 Label nameInStore
l1
  , sopInsert :: forall (s :: [*]).
Maybe (Label mname -> (key : value : store : s) :-> (store : s))
sopInsert = case StoreSubmapOps substore mname key value
-> forall (s :: [*]).
   Maybe
     (Label mname -> (key : value : substore : s) :-> (substore : s))
forall store (mname :: Symbol) key value.
StoreSubmapOps store mname key value
-> forall (s :: [*]).
   Maybe (Label mname -> (key : value : store : s) :-> (store : s))
sopInsert StoreSubmapOps substore mname key value
ops2 of
      Nothing -> Maybe (Label mname -> (key : value : (store & s)) :-> (store & s))
forall a. Maybe a
Nothing
      Just insOp :: Label mname
-> (key : value : substore : (store & s))
   :-> (substore : (store & s))
insOp -> (Label mname -> (key : value : (store & s)) :-> (store & s))
-> Maybe
     (Label mname -> (key : value : (store & s)) :-> (store & s))
forall a. a -> Maybe a
Just ((Label mname -> (key : value : (store & s)) :-> (store & s))
 -> Maybe
      (Label mname -> (key : value : (store & s)) :-> (store & s)))
-> (Label mname -> (key : value : (store & s)) :-> (store & s))
-> Maybe
     (Label mname -> (key : value : (store & s)) :-> (store & s))
forall a b. (a -> b) -> a -> b
$ \l2 :: Label 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 ((store & s) :-> (store & (store & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
L.dup ((store & s) :-> (store & (store & s)))
-> ((store & (store & s)) :-> (substore : (store & s)))
-> (store & s) :-> (substore : (store & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreFieldOps store nameInStore substore
-> Label nameInStore
-> (store & (store & s)) :-> (substore : (store & s))
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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
#
        Label mname
-> (key : value : substore : (store & s))
   :-> (substore : (store & s))
insOp Label 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
-> Label nameInStore -> (substore : (store & s)) :-> (store & s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
   Label fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 Label nameInStore
l1
  }

composeStoreEntrypointOps
  :: Label nameInStore
  -> StoreFieldOps store nameInStore substore
  -> StoreEntrypointOps substore epName epParam epStore
  -> StoreEntrypointOps store epName epParam epStore
composeStoreEntrypointOps :: Label nameInStore
-> StoreFieldOps store nameInStore substore
-> StoreEntrypointOps substore epName epParam epStore
-> StoreEntrypointOps store epName epParam epStore
composeStoreEntrypointOps l1 :: Label nameInStore
l1 ops1 :: StoreFieldOps store nameInStore substore
ops1 ops2 :: StoreEntrypointOps substore epName epParam epStore
ops2 = $WStoreEntrypointOps :: 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 = \l2 :: Label epName
l2 ->
      StoreFieldOps store nameInStore substore
-> Label nameInStore -> (store : s) :-> (substore : s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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 = \l2 :: 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 ((store & s) :-> (store & (store & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
L.dup ((store & s) :-> (store & (store & s)))
-> ((store & (store & s)) :-> (substore : (store & s)))
-> (store & s) :-> (substore : (store & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreFieldOps store nameInStore substore
-> Label nameInStore
-> (store & (store & s)) :-> (substore : (store & s))
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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
-> Label nameInStore -> (substore : (store & s)) :-> (store & s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
   Label fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 Label nameInStore
l1
  , sopToEpStore :: forall (s :: [*]). Label epName -> (store : s) :-> (epStore : s)
sopToEpStore = \l2 :: Label epName
l2 ->
      StoreFieldOps store nameInStore substore
-> Label nameInStore -> (store : s) :-> (substore : s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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 = \l2 :: 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 ((store & s) :-> (store & (store & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
L.dup ((store & s) :-> (store & (store & s)))
-> ((store & (store & s)) :-> (substore : (store & s)))
-> (store & s) :-> (substore : (store & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# StoreFieldOps store nameInStore substore
-> Label nameInStore
-> (store & (store & s)) :-> (substore : (store & s))
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]). Label fname -> (store : s) :-> (ftype : s)
sopToField StoreFieldOps store nameInStore substore
ops1 Label 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
-> Label nameInStore -> (substore : (store & s)) :-> (store & s)
forall store (fname :: Symbol) ftype.
StoreFieldOps store fname ftype
-> forall (s :: [*]).
   Label fname -> (ftype : store : s) :-> (store : s)
sopSetField StoreFieldOps store nameInStore substore
ops1 Label nameInStore
l1
  }

-- | Utility to 'push' the 'MText' name of and entrypoint from its 'Label'
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

-- | Utility to extract an 'EntrypointLambda' from a 'Maybe', fails in case of
-- 'Nothing'.
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 l :: 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)

-- | Utility to set an 'EntrypointLambda' into a store.
-- Fails in case the entrypoint is already set.
setStEp
  :: StoreHasSubmap store epmName MText (EntrypointLambda epParam epStore)
  => Label epmName -> Label epsName
  -> (EntrypointLambda epParam epStore) : store : s :-> store : s
setStEp :: Label epmName
-> Label epsName
-> (EntrypointLambda epParam epStore : store : s) :-> (store : s)
setStEp ml :: Label epmName
ml l :: 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
# Label epmName
-> (forall (s0 :: [*]) (any :: [*]). (MText : s0) :-> any)
-> (MText : EntrypointLambda epParam epStore : store : s)
   :-> (store : s)
forall store (mname :: Symbol) key value (s :: [*]).
StoreHasSubmap store mname key value =>
Label mname
-> (forall (s0 :: [*]) (any :: [*]). (key : s0) :-> any)
-> (key : value : store : s) :-> (store : s)
stInsertNew Label 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 :: [*]). KnownValue a => (a & s) :-> t
L.failWith

----------------------------------------------------------------------------
-- Storage generation
----------------------------------------------------------------------------

-- Note: we could make this safer with a 'StoreHasEntrypoint' constraint, but GHC
-- would flag it as redundant and we'd also need to annotate the @store@
--
-- | Utility to create 'EntrypointsField's from an entrypoint name (@epName@) and
-- an 'EntrypointLambda' implementation. Note that you need to merge multiple of
-- these (with '<>') if your field contains more than one entrypoint lambda.
mkStoreEp
  :: Label epName
  -> EntrypointLambda epParam epStore
  -> EntrypointsField epParam epStore
mkStoreEp :: Label epName
-> EntrypointLambda epParam epStore
-> EntrypointsField epParam epStore
mkStoreEp l :: Label epName
l = Map MText (EntrypointLambda epParam epStore)
-> EntrypointsField epParam epStore
forall k v. Map k v -> BigMap k v
BigMap (Map MText (EntrypointLambda epParam epStore)
 -> EntrypointsField epParam epStore)
-> (EntrypointLambda epParam epStore
    -> Map MText (EntrypointLambda epParam epStore))
-> EntrypointLambda epParam epStore
-> EntrypointsField epParam epStore
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MText
-> EntrypointLambda epParam epStore
-> Map MText (EntrypointLambda epParam epStore)
forall k a. k -> a -> Map k a
singleton (Label epName -> MText
forall (name :: Symbol). Label name -> MText
labelToMText Label epName
l)


----------------------------------------------------------------------------
-- Utilities
----------------------------------------------------------------------------

-- | Indicates a submap with given key and value types.
data k ~> v
infix 9 ~>

-- | Indicates a stored entrypoint with the given @param@ and @store@ types.
data param ::-> store
infix 9 ::->

{- | Concise way to write down constraints with expected content of a storage.

Use it like follows:

@
type StorageConstraint store = StorageContains store
  [ "fieldInt" := Int
  , "fieldNat" := Nat
  , "epsToNat" := Int ::-> Nat
  , "balances" := Address ~> Int
  ]
@

-}
type family StorageContains store (content :: [NamedField]) :: Constraint where
  StorageContains _ '[] = ()
  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)