-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# OPTIONS_GHC -Wno-orphans #-}

{- | This module provides storage interfaces.

Whenever you need to write a generic code applicable to different storage
formats, consider using this module.

Use methods like 'stToField' and 'stUpdate' to work with storage from your code.

To explain how e.g. required fields are obtainable from your storage you define
'StoreHasField' instance (and a similar case is for other typeclasses).
We provide the most common building blocks for implementing these instances,
see @Implementations@ section.

-}
module Lorentz.StoreClass
  ( -- * Preliminary
    FieldRefKind
  , FieldRefTag
  , KnownFieldRef (..)
  , FieldName
  , FieldRef
  , FieldSymRef
  , fieldNameToLabel
  , fieldNameFromLabel
  , FieldRefHasFinalName (..)

    -- * 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
  , stToFieldNamed
  , stGetFieldNamed
  , stSetField
  , stMem
  , stGet
  , stUpdate
  , stGetAndUpdate
  , stDelete
  , stInsert
  , stInsertNew
  , stEntrypoint
  , stToEpLambda
  , stGetEpLambda
  , stSetEpLambda
  , stToEpStore
  , stGetEpStore
  , stSetEpStore
  , sopGetField
  , sopSetField

    -- * Implementations
  , storeFieldOpsADT
  , storeEntrypointOpsADT
  , storeEntrypointOpsFields
  , storeEntrypointOpsSubmapField
  , storeFieldOpsDeeper
  , storeSubmapOpsDeeper
  , storeEntrypointOpsDeeper
  , storeFieldOpsReferTo
  , storeSubmapOpsReferTo
  , mapStoreFieldOps
  , mapStoreSubmapOpsKey
  , mapStoreSubmapOpsValue
  , storeEntrypointOpsReferTo
  , composeStoreFieldOps
  , composeStoreSubmapOps
  , sequenceStoreSubmapOps
  , composeStoreEntrypointOps
  , zoomStoreSubmapOps

    -- * Storage generation
  , mkStoreEp

    -- * Complex field references
  , (:-|)(..)

  , SelfRef (..)
  , this

  , stNested

  , FieldAlias
  , stAlias
  , FieldNickname
  , stNickname
  ) where


import Data.Kind qualified as Kind
import GHC.TypeLits (KnownSymbol, Symbol)

import Lorentz.ADT
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Errors (failUnexpected)
import Lorentz.Ext
import Lorentz.Instr qualified as L
import Lorentz.Iso
import Lorentz.Lambda
import Lorentz.Macro qualified as L
import Lorentz.Value
import Morley.Michelson.Text (labelToMText)

-- $setup
-- >>> :m +Lorentz.Base Lorentz.Instr Lorentz.Run.Simple Morley.Michelson.Text

-- | Open kind for various field references.
--
-- The simplest field reference could be 'Label', pointing to a field
-- by its name, but we also support more complex scenarios like deep
-- fields identifiers.
type FieldRefKind = FieldRefTag -> Kind.Type
data FieldRefTag = FieldRefTag

-- | For a type-level field reference - an associated term-level representation.
--
-- This is similar to @singletons@ @Sing@ + @SingI@ pair but has small differences:
--
-- * Dedicated to field references, thus term-level thing has 'FieldRefKind' kind.
-- * The type of term-level value (@FieldRefObject ty@) determines the kind of
--   the reference type.
class KnownFieldRef (ty :: k) where
  type FieldRefObject ty = (fr :: FieldRefKind) | fr -> ty
  mkFieldRef :: FieldRefObject ty p

-- | Some kind of reference to a field.
--
-- The idea behind this type is that in trivial case (@name :: Symbol@) it can
-- be instantiated with a mere label, but it is generic enough to allow complex
-- field references as well.
type FieldRef name = FieldRefObject name 'FieldRefTag

-- | The simplest field reference - just a name. Behaves similarly to 'Label'.
data FieldName (n :: Symbol) (p :: FieldRefTag) =
  KnownSymbol n => FieldName

-- Thanks to @p@ type variable being of unique 'FieldRefKind' kind,
-- this instance won't overlap with 'IsLabel' instances from other modules.
instance (x ~ FieldName name, KnownSymbol name) =>
         IsLabel name (x p) where
  fromLabel = FieldName

instance KnownSymbol name => KnownFieldRef (name :: Symbol) where
  type FieldRefObject name = FieldName name
  mkFieldRef = FieldName

-- | Version of 'FieldRef' restricted to symbolic labels.
--
-- @FieldSymRef name ≡ FieldName name 'FieldRefTag@
type FieldSymRef name = FieldRef (name :: Symbol)

-- | Convert a symbolic 'FieldRef' to a label, useful for compatibility with
-- other interfaces.
fieldNameToLabel :: FieldSymRef n -> Label n
fieldNameToLabel FieldName = Label

-- | Convert a label to 'FieldRef', useful for compatibility with
-- other interfaces.
fieldNameFromLabel :: Label n -> FieldSymRef n
fieldNameFromLabel Label = FieldName

-- | Provides access to the direct name of the referred field.
--
-- This is used in 'stToFieldNamed'.
class FieldRefHasFinalName fr where
  type FieldRefFinalName fr :: Symbol
  fieldRefFinalName :: FieldRef fr -> Label (FieldRefFinalName fr)

instance FieldRefHasFinalName (name :: Symbol) where
  type FieldRefFinalName name = name
  fieldRefFinalName = fieldNameToLabel

----------------------------------------------------------------------------
-- 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
  { sopToField
      :: forall s.
         FieldRef fname -> store : s :-> ftype : s
  , sopGetFieldOpen
      :: forall res s. (HasDupableGetters store)
      => '[ftype] :-> '[res, ftype]
      -> '[ftype] :-> '[res]
      -> FieldRef fname -> store : s :-> res : store : s
    -- ^ See 'getFieldOpen' for explanation of the signature.
  , sopSetFieldOpen
      :: forall new s.
         '[new, ftype] :-> '[ftype]
      -> FieldRef fname -> new : store : s :-> store : s
    -- ^ See 'setFieldOpen' for explanation of the signature.
  }

-- | Simplified version of 'sopGetFieldOpen' where @res@ is @ftype@.
sopGetField
  :: (Dupable ftype, HasDupableGetters store)
  => StoreFieldOps store fname ftype
  -> FieldRef fname -> store : s :-> ftype : store : s
sopGetField ops = sopGetFieldOpen ops L.dup L.nop

-- | Simplified version of 'sopSetFieldOpen' where @res@ is @ftype@.
sopSetField
  :: StoreFieldOps store fname ftype
  -> FieldRef fname -> ftype : store : s :-> store : s
sopSetField ops = sopSetFieldOpen ops (L.dip L.drop)

-- 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

instance {-# OVERLAPPABLE #-}
         HasFieldOfType store fname ftype =>
         StoreHasField store fname ftype where
  storeFieldOps = storeFieldOpsADT

-- | Pick storage field.
stToField
  :: StoreHasField store fname ftype
  => FieldRef fname -> store : s :-> ftype : s
stToField = sopToField storeFieldOps

-- | Get storage field, preserving the storage itself on stack.
stGetField
  :: (StoreHasField store fname ftype, Dupable ftype, HasDupableGetters store)
  => FieldRef fname -> store : s :-> ftype : store : s
stGetField l = sopGetField storeFieldOps l

-- | Pick storage field retaining a name label attached.
--
-- For complex refs this tries to attach the immediate name of the referred field.
stToFieldNamed
  :: (StoreHasField store fname ftype, FieldRefHasFinalName fname)
  => FieldRef fname -> store : s :-> (FieldRefFinalName fname :! ftype) : s
stToFieldNamed fr = stToField fr # toNamed (fieldRefFinalName fr)

-- | Version of 'stToFieldNamed' that preserves the storage on stack.
stGetFieldNamed
  :: ( StoreHasField store fname ftype, FieldRefHasFinalName fname
     , Dupable ftype, HasDupableGetters store
     )
  => FieldRef fname -> store : s :-> (FieldRefFinalName fname :! ftype) : store : s
stGetFieldNamed fr = stGetField fr # toNamed (fieldRefFinalName fr)

-- | Update storage field.
stSetField
  :: (StoreHasField store fname ftype)
  => FieldRef fname -> ftype : store : s :-> store : s
stSetField = sopSetField 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
  { sopMem
      :: forall s.
         FieldRef mname -> key : store : s :-> Bool : s
  , sopGet
      :: forall s.
         (KnownValue value)
      => FieldRef mname -> key : store : s :-> Maybe value : s
  , sopUpdate
      :: forall s.
         FieldRef mname -> key : Maybe value : store : s :-> store : s

  , sopGetAndUpdate
      :: forall s.
         FieldRef mname -> key : Maybe value : store : s :-> Maybe value : store : s

    -- Methods below are derivatives of methods above, they can be provided
    -- if for given specific storage type more efficient implementation is
    -- available.
  , sopDelete
      :: forall s.
         FieldRef mname -> key : store : s :-> store : s
  , sopInsert
      :: forall s.
         FieldRef 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

-- | Provides access to the submap via the respective field.
--
-- Tricky storages that consolidate submaps in a non-trivial way
-- can define instances overlapping this one.
instance ( StoreHasField store name submap
         , StoreHasSubmap submap SelfRef key value
         , KnownSymbol name
         , HasDupableGetters store, Dupable submap
         ) => StoreHasSubmap store (name :: Symbol) key value where
  storeSubmapOps = storeSubmapOpsReferTo (fromLabel @name :-| this) storeSubmapOps

-- | Check value presence in storage.
stMem
  :: StoreHasSubmap store mname key value
  => FieldRef mname -> key : store : s :-> Bool : s
stMem = sopMem storeSubmapOps

-- | Get value in storage.
stGet
  :: (StoreHasSubmap store mname key value, KnownValue value)
  => FieldRef mname -> key : store : s :-> Maybe value : s
stGet = sopGet storeSubmapOps

-- | Update a value in storage.
stUpdate
  :: StoreHasSubmap store mname key value
  => FieldRef mname -> key : Maybe value : store : s :-> store : s
stUpdate = sopUpdate storeSubmapOps

-- | Atomically get and update a value in storage.
stGetAndUpdate
  :: StoreHasSubmap store mname key value
  => FieldRef mname -> key : Maybe value : store : s :-> Maybe value : store : s
stGetAndUpdate = sopGetAndUpdate storeSubmapOps

-- | Delete a value in storage.
stDelete
  :: forall store mname key value s.
     (StoreHasSubmap store mname key value)
  => FieldRef mname -> key : store : s :-> store : s
stDelete = sopDelete storeSubmapOps

-- | Add a value in storage.
stInsert
  :: StoreHasSubmap store mname key value
  => FieldRef mname -> key : value : store : s :-> store : s
stInsert = sopInsert storeSubmapOps

-- | Add a value in storage, but fail if it will overwrite some existing entry.
stInsertNew
  :: (StoreHasSubmap store mname key value, Dupable key)
  => FieldRef mname
  -> (forall s0 any. key : s0 :-> any)
  -> key : value : store : s
  :-> store : s
stInsertNew l doFail =
  L.dip L.some # L.dup #
  L.dip (stGetAndUpdate l) # L.swap #
  L.ifNone L.drop (L.drop # doFail)

----------------------------------------------------------------------------
-- 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
  { sopToEpLambda
      :: forall s.
         Label epName
      -> store : s :-> (EntrypointLambda epParam epStore) : s
  , sopSetEpLambda
      :: forall s. (HasDupableGetters store)
      => Label epName
      -> (EntrypointLambda epParam epStore) : store : s :-> store : s
  , sopToEpStore
      :: forall s.
         Label epName
      -> store : s :-> epStore : s
  , sopSetEpStore
      :: forall s.
         Label epName
      -> epStore : store : s :-> store : s
  }

-- | 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, Dupable store)
  => Label epName -> epParam : store : s :-> ([Operation], store) : s
stEntrypoint l =
  L.dip (stGetEpStore l # L.dip (stGetEpLambda l)) #
  L.pair # L.exec # L.unpair #
  L.dip (stSetEpStore l) # L.pair

-- | Pick stored entrypoint lambda.
stToEpLambda
  :: StoreHasEntrypoint store epName epParam epStore
  => Label epName -> store : s :-> (EntrypointLambda epParam epStore) : s
stToEpLambda = sopToEpLambda storeEpOps

-- | Get stored entrypoint lambda, preserving the storage itself on the stack.
stGetEpLambda
  :: (StoreHasEntrypoint store epName epParam epStore, Dupable store)
  => Label epName -> store : s :-> (EntrypointLambda epParam epStore) : store : s
stGetEpLambda l = L.dup # stToEpLambda l

-- | Stores the entrypoint lambda in the storage. Fails if already set.
stSetEpLambda
  :: (StoreHasEntrypoint store epName epParam epStore, HasDupableGetters store)
  => Label epName -> (EntrypointLambda epParam epStore) : store : s :-> store : s
stSetEpLambda = sopSetEpLambda storeEpOps

-- | Pick the sub-storage that the entrypoint operates on.
stToEpStore
  :: StoreHasEntrypoint store epName epParam epStore
  => Label epName -> store : s :-> epStore : s
stToEpStore = sopToEpStore storeEpOps

-- | Get the sub-storage that the entrypoint operates on, preserving the storage
-- itself on the stack.
stGetEpStore
  :: (StoreHasEntrypoint store epName epParam epStore, Dupable store)
  => Label epName -> store : s :-> epStore : store : s
stGetEpStore l = L.dup # stToEpStore l

-- | Update the sub-storage that the entrypoint operates on.
stSetEpStore
  :: StoreHasEntrypoint store epName epParam epStore
  => Label epName -> epStore : store : s :-> store : s
stSetEpStore = sopSetEpStore storeEpOps

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

-- | Implementation of 'StoreHasField' for case of datatype
-- keeping a pack of fields.
storeFieldOpsADT
  :: HasFieldOfType dt fname ftype
  => StoreFieldOps dt (fname :: Symbol) ftype
storeFieldOpsADT = StoreFieldOps
  { sopToField = toField . fieldNameToLabel
  , sopGetFieldOpen = \cont1 cont2 l ->
      getFieldOpen cont1 cont2 (fieldNameToLabel l)
  , sopSetFieldOpen = \cont l ->
      setFieldOpen cont (fieldNameToLabel l)
  }

-- | Implementation of 'StoreHasEntrypoint' for a datatype keeping a pack of
-- fields, among which one 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 mapLabel fieldLabel = StoreEntrypointOps
  { sopToEpLambda = \l -> toField mapLabel # pushStEp l # L.get # someStEp l
  , sopSetEpLambda = \l -> L.dip (getField mapLabel) # setStEp this l # setField mapLabel
  , sopToEpStore = \_l -> toField fieldLabel
  , sopSetEpStore = \_l -> setField 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 mapLabel fieldLabel = StoreEntrypointOps
  { sopToEpLambda = \l ->
      stToField (fieldNameFromLabel mapLabel) # pushStEp l # L.get # someStEp l
  , sopSetEpLambda = \l ->
      L.dip (stGetField $ fieldNameFromLabel mapLabel) # setStEp this l #
      stSetField (fieldNameFromLabel mapLabel)
  , sopToEpStore = \_l ->
      stToField $ fieldNameFromLabel fieldLabel
  , sopSetEpStore = \_l ->
      stSetField $ fieldNameFromLabel 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 mapLabel fieldLabel = StoreEntrypointOps
  { sopToEpLambda = \l -> pushStEp l # stGet (fieldNameFromLabel mapLabel) # someStEp l
  , sopSetEpLambda = \l -> setStEp (fieldNameFromLabel mapLabel) l
  , sopToEpStore = \_l -> stToField (fieldNameFromLabel fieldLabel)
  , sopSetEpStore = \_l -> stSetField (fieldNameFromLabel 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
     , HasDupableGetters fields
     )
  => FieldRef fieldsPartName
  -> StoreFieldOps storage fname ftype
storeFieldOpsDeeper fieldsLabel =
  composeStoreFieldOps fieldsLabel storeFieldOpsADT 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 SelfRef key value
     , HasDupableGetters storage
     , Dupable fields
     )
  => FieldRef bigMapPartName
  -> StoreSubmapOps storage mname key value
storeSubmapOpsDeeper submapLabel =
  storeSubmapOpsReferTo this $
    composeStoreSubmapOps submapLabel storeFieldOpsADT 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
     , HasDupableGetters store, Dupable substore
     )
  => FieldRef nameInStore
  -> StoreEntrypointOps store epName epParam epStore
storeEntrypointOpsDeeper fieldsLabel =
  composeStoreEntrypointOps fieldsLabel storeFieldOpsADT 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
  :: FieldRef name
  -> StoreSubmapOps storage name key value
  -> StoreSubmapOps storage desiredName key value
storeSubmapOpsReferTo l StoreSubmapOps{..} =
  StoreSubmapOps
  { sopMem = \_l -> sopMem l
  , sopGet = \_l -> sopGet l
  , sopUpdate = \_l -> sopUpdate l
  , sopGetAndUpdate = \_l -> sopGetAndUpdate l
  , sopDelete = \_l -> sopDelete l
  , sopInsert = \_l -> sopInsert l
  }

-- | 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
  :: FieldRef name
  -> StoreFieldOps storage name field
  -> StoreFieldOps storage desiredName field
storeFieldOpsReferTo l StoreFieldOps{..} =
  StoreFieldOps
  { sopToField = \_l -> sopToField l
  , sopGetFieldOpen = \cont1 cont2 _l -> sopGetFieldOpen cont1 cont2 l
  , sopSetFieldOpen = \cont _l -> sopSetFieldOpen cont 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 l StoreEntrypointOps{..} = StoreEntrypointOps
  { sopToEpLambda = \_l -> sopToEpLambda l
  , sopSetEpLambda = \_l -> sopSetEpLambda l
  , sopToEpStore = \_l -> sopToEpStore l
  , sopSetEpStore = \_l -> sopSetEpStore l
  }

-- | Change field operations so that they work on a modified field.
--
-- For instance, to go from
-- @StoreFieldOps Storage "name" Integer@
-- to
-- @StoreFieldOps Storage "name" (value :! Integer)@
-- you can use
-- @mapStoreFieldOps (namedIso #value)@
mapStoreFieldOps
  :: forall field1 field2 store name.
     KnownValue field1
  => LIso field1 field2
  -> StoreFieldOps store name field1
  -> StoreFieldOps store name field2
mapStoreFieldOps LIso{..} StoreFieldOps{..} = StoreFieldOps
  { sopToField = \l -> sopToField l # liTo
  , sopGetFieldOpen = \contWDup contWoDup l ->
      let ourContWoDup = liTo # contWoDup
          ourContWDup = case decideOnDupable @field1 of
            -- We can avoid an iso roundtrip if we manage to duplicate `field1`
            IsDupable -> L.dup # liTo # L.framed contWoDup
            IsNotDupable -> liTo # contWDup # L.dip liFrom
      in sopGetFieldOpen ourContWDup ourContWoDup l
  , sopSetFieldOpen = \cont l ->
      -- TODO [#560]: make sure @L.framed@ is transparent for the optimizer.
      -- Calling @liTo@ is often redundant here since @cont@ is usually just
      -- @L.dip L.drop@, this is not so only if we compose result of
      -- @mapStoreFieldOps@ with other 'StoreFieldOps'.
      sopSetFieldOpen (L.dip liTo # L.framed cont # liFrom) l
  }

-- | Change submap operations so that they work on a modified key.
mapStoreSubmapOpsKey
  :: Fn key2 key1
  -> StoreSubmapOps store name key1 value
  -> StoreSubmapOps store name key2 value
mapStoreSubmapOpsKey mapper StoreSubmapOps{..} = StoreSubmapOps
  { sopMem = \l ->
      L.framed mapper # sopMem l
  , sopGet = \l ->
      L.framed mapper # sopGet l
  , sopUpdate = \l ->
      L.framed mapper # sopUpdate l
  , sopGetAndUpdate = \l ->
      L.framed mapper # sopGetAndUpdate l
  , sopDelete = \l ->
      L.framed mapper # sopDelete l
  , sopInsert = \l ->
      L.framed mapper # sopInsert l
  }

-- | Change submap operations so that they work on a modified value.
mapStoreSubmapOpsValue
  :: (KnownValue value1, KnownValue value2)
  => LIso value1 value2
  -> StoreSubmapOps store name key value1
  -> StoreSubmapOps store name key value2
mapStoreSubmapOpsValue LIso{..} StoreSubmapOps{..} = StoreSubmapOps
  { sopMem = \l ->
      sopMem l
  , sopGet = \l ->
      sopGet l # L.lmap liTo
  , sopUpdate = \l ->
      L.dip (L.lmap liFrom) # sopUpdate l
  , sopGetAndUpdate = \l ->
      L.dip (L.lmap liFrom) # sopGetAndUpdate l # L.lmap liTo
  , sopInsert = \l ->
      L.dip liFrom # sopInsert l
  , sopDelete = \l ->
      sopDelete 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
  :: HasDupableGetters substore
  => FieldRef nameInStore
  -> StoreFieldOps store nameInStore substore
  -> StoreFieldOps substore nameInSubstore field
  -> StoreFieldOps store nameInSubstore field
composeStoreFieldOps l1 ops1 ops2 =
  StoreFieldOps
  { sopToField = \l2 ->
      sopToField ops1 l1 # sopToField ops2 l2
  , sopGetFieldOpen = \contWDup contWoDup l2 ->
      sopGetFieldOpen ops1
        (sopGetFieldOpen ops2 contWDup contWoDup l2)
        (sopToField ops2 l2 # contWoDup)
        l1
  , sopSetFieldOpen = \cont l2 ->
      sopSetFieldOpen ops1 (sopSetFieldOpen ops2 cont l2) l1
  }

-- | Chain implementations of field and submap operations.
--
-- This requires @Dupable substore@ for simplicity, in most cases it is
-- possible to use a different chaining (@nameInStore :-| mname :-| this@)
-- to avoid that constraint.
-- If this constraint is still an issue, please create a ticket.
composeStoreSubmapOps
  :: (HasDupableGetters store, Dupable substore)
  => FieldRef nameInStore
  -> StoreFieldOps store nameInStore substore
  -> StoreSubmapOps substore mname key value
  -> StoreSubmapOps store mname key value
composeStoreSubmapOps l1 ops1 ops2 =
  StoreSubmapOps
  { sopMem = \l2 ->
      L.dip (sopToField ops1 l1) # sopMem ops2 l2
  , sopGet = \l2 ->
      L.dip (sopToField ops1 l1) # sopGet ops2 l2
  , sopUpdate = \l2 ->
      L.dip (L.dip (sopGetField ops1 l1)) #
      sopUpdate ops2 l2 #
      sopSetField ops1 l1
  , sopGetAndUpdate = \l2 ->
      L.dip (L.dip (sopGetField ops1 l1)) #
      sopGetAndUpdate ops2 l2 #
      L.dip (sopSetField ops1 l1)
  , sopDelete = \l2 ->
      L.dip (sopGetField ops1 l1) #
      sopDelete ops2 l2 #
      sopSetField ops1 l1
  , sopInsert = \l2 ->
      L.dip (L.dip (sopGetField ops1 l1)) #
      sopInsert ops2 l2 #
      sopSetField ops1 l1
  }

-- | Chain implementations of two submap operations sets.
-- Used to provide shortcut access to a nested submap.
--
-- This is very inefficient since on each access to substore
-- it has to be serialized/deserialized. Use this implementation
-- only if due to historical reasons migrating storage is difficult.
--
-- @LIso (Maybe substore) substore@ argument describes how to get
-- @substore@ value if it was absent in map and how to detect when
-- it can be safely removed.
--
-- Example of use:
-- @sequenceStoreSubmapOps #mySubmap nonDefIso storeSubmapOps storeSubmapOps@
sequenceStoreSubmapOps
  :: forall store substore value name subName key1 key2.
     ( NiceConstant substore, KnownValue value
     , Dupable (key1, key2), Dupable store
     )
  => FieldRef name
  -> LIso (Maybe substore) substore
  -> StoreSubmapOps store name key1 substore
  -> StoreSubmapOps substore subName key2 value
  -> StoreSubmapOps store subName (key1, key2) value
sequenceStoreSubmapOps l1 substoreIso ops1 ops2 =
  fix $ \res ->
  StoreSubmapOps
  { sopMem = \l2 ->
      L.unpair # L.swap #
      L.dip (sopGet ops1 l1) # L.swap #
      L.ifSome
        (L.swap # sopMem ops2 l2)
        (L.drop # L.push False)
  , sopGet = \l2 ->
      L.unpair # L.swap #
      L.dip (sopGet ops1 l1) # L.swap #
      L.ifSome
        (L.swap # sopGet ops2 l2)
        (L.drop # L.none)
  , sopUpdate = \l2 ->
      prepareUpdate #
      L.dip (sopUpdate ops2 l2 # liFrom substoreIso) #
      sopUpdate ops1 l1
  , sopGetAndUpdate = \l2 ->
      prepareUpdate #
      L.dip (sopGetAndUpdate ops2 l2 # L.dip (liFrom substoreIso)) #
      L.swap # L.dip (sopUpdate ops1 l1)
  , sopDelete = \l2 ->
      L.dip L.none # sopUpdate res l2
  , sopInsert = \l2 ->
      prepareUpdate #
      L.dip (sopInsert ops2 l2) #
      sopInsert ops1 l1
  }
  where
    -- Extract all the necessary things prior to update
    prepareUpdate
      :: (key1, key2) : value' : store : s
         :-> key1 : key2 : value' : substore : store : s
    prepareUpdate =
      L.dup # L.car #
      L.dip
        ( L.swap #
          L.dip
            ( L.unpair # L.swap #
              L.dip
                ( L.dip (L.dup @store) #
                  sopGet ops1 l1 # liTo substoreIso
                )
            ) #
          L.swap
        )

-- We still require 'Dupable substore' because substore with entrypoints
-- is likely to contain only lambdas and thus be dupable.
-- If there is a case when it is not, create an issue to generalize this code.
composeStoreEntrypointOps
  :: (HasDupableGetters store, Dupable substore)
  => FieldRef nameInStore
  -> StoreFieldOps store nameInStore substore
  -> StoreEntrypointOps substore epName epParam epStore
  -> StoreEntrypointOps store epName epParam epStore
composeStoreEntrypointOps l1 ops1 ops2 = StoreEntrypointOps
  { sopToEpLambda = \l2 ->
      sopToField ops1 l1 # sopToEpLambda ops2 l2
  , sopSetEpLambda = \l2 ->
      L.dip (sopGetField ops1 l1) #
      sopSetEpLambda ops2 l2 #
      sopSetField ops1 l1
  , sopToEpStore = \l2 ->
      sopToField ops1 l1 # sopToEpStore ops2 l2
  , sopSetEpStore = \l2 ->
      L.dip (sopGetField ops1 l1) #
      sopSetEpStore ops2 l2 #
      sopSetField ops1 l1
  }


{- | Turn submap operations into operations on a part of the submap value.

Normally, if you need this set of operations, it would be better to split your
submap into several separate submaps, each operating with its own part of the value.
This set of operations is pretty inefficient and exists only as a temporary
measure, if due to historical reasons you have to leave storage format intact.

This implementation puts no distinction between @value == Nothing@ and
@value == Just defValue@ cases.
Getters, when notice a value equal to the default value, report its absence.
Setters tend to remove the value from submap when possible.

@LIso (Maybe value) value@ and @LIso (Maybe subvalue) subvalue@ arguments
describe how to get a value if it was absent in map and how to detect when
it can be safely removed from map.

Example of use:
@zoomStoreSubmapOps #mySubmap nonDefIso nonDefIso storeSubmapOps storeFieldOpsADT@
-}
zoomStoreSubmapOps
  :: forall store submapName nameInSubmap key value subvalue.
     ( NiceConstant value, NiceConstant subvalue
     , Dupable key, Dupable store
     )
  => FieldRef submapName
  -> LIso (Maybe value) value
  -> LIso (Maybe subvalue) subvalue
  -> StoreSubmapOps store submapName key value
  -> StoreFieldOps value nameInSubmap subvalue
  -> StoreSubmapOps store nameInSubmap key subvalue
zoomStoreSubmapOps l1 valueIso subvalueIso ops1 ops2 =
  fix $ \res ->
  StoreSubmapOps
  { sopMem = \l2 ->
      sopGet ops1 l1 #
      L.ifSome
        (sopToField ops2 l2 # liFrom subvalueIso # L.isSome)
        (L.push False)
  , sopGet = \l2 ->
      sopGet ops1 l1 #
      L.ifSome
        (sopToField ops2 l2 # liFrom subvalueIso)
        L.none
  , sopUpdate = \l2 ->
      L.dip (liTo subvalueIso) #
      useSubmapValue l2 #
      L.dip (liFrom valueIso) #
      sopUpdate ops1 l1
  , sopGetAndUpdate = \l2 ->
      -- here we can't efficiently use @sopGetAndUpdate ops1@,
      -- so implementing with simpler primitives
      L.dip (liTo subvalueIso) #
      getSubmapValue #
      L.dip (L.dup @subvalue) # L.swap #
      L.dip @subvalue
        ( stackType @(key : subvalue : value : store : _) #
          L.dip (sopSetField ops2 l2) #
          L.dip (liFrom valueIso) #
          sopUpdate ops1 l1
        ) #
      liFrom subvalueIso
  , sopDelete = \l2 ->
      L.dip L.none # sopUpdate res l2
  , sopInsert = \l2 ->
      useSubmapValue l2 #
      sopInsert ops1 l1
  }
  where
    -- preparation: get current value in map
    getSubmapValue
      :: key : subvalue : store : s
         :-> key : subvalue : value : store : s
    getSubmapValue =
      L.dup #
      L.dip
        ( L.swap #
          L.dip (L.dip L.dup # sopGet ops1 l1 # liTo valueIso)
        )

    -- preparation: update value with subvalue from map
    useSubmapValue
      :: FieldRef nameInSubmap
      -> key : subvalue : store : s
         :-> key : value : store : s
    useSubmapValue l2 =
      getSubmapValue # L.dip (sopSetField ops2 l2)

-- | Utility to 'L.push' the 'MText' name of and entrypoint from its 'Label'
pushStEp :: Label name -> s :-> MText : s
pushStEp = L.push . 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 l = L.ifSome L.nop $
  failUnexpected ([mt|unknown storage entrypoint: |] <> labelToMText 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)
  => FieldRef epmName -> Label epsName
  -> (EntrypointLambda epParam epStore) : store : s :-> store : s
setStEp ml l = pushStEp l # stInsertNew ml failAlreadySetEp
  where
    failAlreadySetEp :: MText : s :-> any
    failAlreadySetEp =
      L.push [mt|Storage entrypoint already set: |] # L.concat # 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 l lambda = one (labelToMText l, lambda)

----------------------------------------------------------------------------
-- Complex field references
----------------------------------------------------------------------------

-- | Refer to a nested entry in storage.
--
-- Example: @stToField (#a :-| #b)@ fetches field @b@ in the type under field @a@.
--
-- If not favouring this name much, you can try an alias from
-- "Lorentz.StoreClass.Extra".
infixr 8 :-|
data (:-|) (l :: k1) (r :: k2) (p :: FieldRefTag) =
  FieldRef l :-| FieldRef r

instance (KnownFieldRef l, KnownFieldRef r) => KnownFieldRef (l :-| r) where
  type FieldRefObject (l :-| r) = l :-| r
  mkFieldRef = mkFieldRef :-| mkFieldRef

instance FieldRefHasFinalName r => FieldRefHasFinalName (l :-| r) where
  type FieldRefFinalName (l :-| r) = FieldRefFinalName r
  fieldRefFinalName (_ :-| r) = fieldRefFinalName r

instance ( StoreHasField store field substore
         , StoreHasField substore subfield ty
         , KnownFieldRef field, KnownFieldRef subfield
         , HasDupableGetters substore
         ) =>
         StoreHasField store (field :-| subfield) ty where
  storeFieldOps =
    storeFieldOpsReferTo (mkFieldRef @_ @subfield) $
      composeStoreFieldOps (mkFieldRef @_ @field) storeFieldOps storeFieldOps

instance ( StoreHasField store field substore
         , StoreHasSubmap substore subfield key value
         , KnownFieldRef field, KnownFieldRef subfield
         , HasDupableGetters store, Dupable substore
         ) =>
         StoreHasSubmap store (field :-| subfield) key value where
  storeSubmapOps =
    storeSubmapOpsReferTo (mkFieldRef @_ @subfield) $
      composeStoreSubmapOps (mkFieldRef @_ @field) storeFieldOps storeSubmapOps

-- | Refer to no particular field, access itself.
data SelfRef (p :: FieldRefTag) = SelfRef

{- | An alias for 'SelfRef'.

Examples:

>>> push 5 # stMem this -$ (mempty :: Map Integer MText)
False

>>> stGetField this # pair -$ (5 :: Integer)
(5,5)

-}
this :: SelfRef p
this = SelfRef

instance KnownFieldRef SelfRef where
  type FieldRefObject SelfRef = SelfRef
  mkFieldRef = SelfRef

instance StoreHasField store SelfRef store where
  storeFieldOps = StoreFieldOps
    { sopToField = \SelfRef -> L.nop
    , sopGetFieldOpen = \contWDup _ SelfRef -> L.framed contWDup
    , sopSetFieldOpen = \cont SelfRef -> L.framed cont
    }

instance (NiceComparable key, KnownValue value) =>
         StoreHasSubmap (BigMap key value) SelfRef key value where
  storeSubmapOps = StoreSubmapOps
    { sopMem = \SelfRef -> L.mem
    , sopGet = \SelfRef -> L.get
    , sopUpdate = \SelfRef -> L.update
    , sopGetAndUpdate = \SelfRef -> L.getAndUpdate
    , sopDelete = \SelfRef -> L.deleteMap
    , sopInsert = \SelfRef -> L.mapInsert
    }

instance (NiceComparable key, KnownValue value) =>
         StoreHasSubmap (Map key value) SelfRef key value where
  storeSubmapOps = StoreSubmapOps
    { sopMem = \SelfRef -> L.mem
    , sopGet = \SelfRef -> L.get
    , sopUpdate = \SelfRef -> L.update
    , sopGetAndUpdate = \SelfRef -> L.getAndUpdate
    , sopDelete = \SelfRef -> L.deleteMap
    , sopInsert = \SelfRef -> L.mapInsert
    }

instance (NiceComparable key, Ord key, Dupable key) =>
         StoreHasSubmap (Set key) SelfRef key () where
  storeSubmapOps = StoreSubmapOps
    { sopMem = \SelfRef -> L.mem
    , sopGet = \SelfRef -> doGet
    , sopUpdate = \SelfRef -> doUpdate
    , sopGetAndUpdate = \SelfRef ->
        L.dupN @3 # L.dupN @2 # doGet # L.dip doUpdate
    , sopDelete = \SelfRef -> L.setDelete
    , sopInsert = \SelfRef -> L.dip (L.drop @()) # L.setInsert
    }
    where
      doGet = L.mem # L.if_ (L.push $ Just ()) (L.push Nothing)
      doUpdate = L.dip L.isSome # L.update

-- | Provides alternative variadic interface for deep entries access.
--
-- Example: @stToField (stNested #a #b #c)@
stNested :: StNestedImpl f SelfRef => f
stNested = stNestedImpl this

class StNestedImpl f acc | f -> acc where
  stNestedImpl :: FieldRef acc -> f

instance (p ~ 'FieldRefTag, res p ~ FieldRef acc) =>
         StNestedImpl (res p) acc where
  stNestedImpl acc = acc

instance ( label ~ FieldRef name
         , StNestedImpl f (acc :-| name)
         ) =>
         StNestedImpl (label -> f) acc where
  stNestedImpl acc l = stNestedImpl (acc :-| l)

{- | Alias for a field reference.

This allows creating _custom_ field references; you will have to define
the respective 'StoreHasField' and 'StoreHasSubmap' instances manually.
Since this type occupies a different "namespace" than string labels
and ':-|', no overlappable instances will be necessary.

Example:

@
-- Shortcut for a deeply nested field X
data FieldX

instance StoreHasField Storage (FieldAlias FieldX) Integer where
  ...

accessX = stToField (stAlias @FieldX)
@

Note that @alias@ type argument allows instantiations of any kind.
-}
data FieldAlias (alias :: k) (p :: FieldRefTag)
  = FieldAlias (Proxy alias)

-- | Construct an alias at term level.
--
-- This requires passing the alias via type annotation.
stAlias :: forall alias. FieldRef (FieldAlias alias)
stAlias = mkFieldRef

-- | Kind-restricted version of 'FieldAlias' to work solely with string labels.
type FieldNickname alias = FieldAlias (alias :: Symbol)

-- | Version of 'stAlias' adopted to labels.
stNickname :: Label name -> FieldRef (FieldAlias name)
stNickname _ = mkFieldRef

instance KnownFieldRef (FieldAlias alias) where
  type FieldRefObject (FieldAlias alias) = FieldAlias alias
  mkFieldRef = FieldAlias Proxy

----------------------------------------------------------------------------
-- 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
  ]
@

Note that this won't work with complex field references, they have to be
included using e.g. 'StoreHasField' manually.

-}
type family StorageContains store (content :: [NamedField]) :: Constraint where
  StorageContains _ '[] = ()
  StorageContains store ((n := Identity ty) ': ct) =
    (StoreHasField store n ty, StorageContains store ct)
  StorageContains store ((n := k ~> v) ': ct) =
    (StoreHasSubmap store n k v, StorageContains store ct)
  StorageContains store ((n := ep ::-> es) ': ct) =
    (StoreHasEntrypoint store n ep es, StorageContains store ct)
  -- Convenient default case, but not applicable when field type is polymorphic
  StorageContains store ((n := ty) ': ct) =
    (StoreHasField store n ty, StorageContains store ct)