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

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Instructions to work with 'UStore'.
module Lorentz.UStore.Instr
  ( unsafeEmptyUStore
  , ustoreMem
  , ustoreGet
  , ustoreUpdate
  , ustoreInsert
  , ustoreInsertNew
  , ustoreDelete

  , ustoreToField
  , ustoreGetField
  , ustoreSetField
  , ustoreRemoveFieldUnsafe

    -- ** Instruction constraints
  , HasUStore
  , HasUField
  , HasUStoreForAllIn

    -- ** Internals
  , packSubMapUKey
  ) where

import qualified Data.Kind as Kind
import GHC.Generics ((:*:), (:+:))
import qualified GHC.Generics as G
import GHC.TypeLits (KnownSymbol, Symbol)
import Type.Reflection ((:~:)(Refl))

import Lorentz.Base
import Lorentz.Coercions (coerceWrap)
import Lorentz.Errors
import Lorentz.Instr as L
import Lorentz.Macro
import Lorentz.Constraints
import Lorentz.UStore.Types
import Lorentz.UStore.Common
import Michelson.Text
import Michelson.Typed.Haskell.Value
import Util.Label (Label)

-- Helpers
----------------------------------------------------------------------------

type KeyAccessC store name =
  ( NiceFullPackedValue (GetUStoreKey store name)
  , KnownSymbol name
  )

type ValueAccessC store name =
  ( NiceFullPackedValue (GetUStoreValue store name)
  , KnownSymbol name
  )

type FieldAccessC store name =
  ( NiceFullPackedValue (GetUStoreField store name)
  , KnownUStoreMarker (GetUStoreFieldMarker store name)
  , KnownSymbol name
  )

packSubMapUKey
  :: forall (field :: Symbol) k s.
     (KnownSymbol field, NicePackedValue k)
  => (k : s) :-> (ByteString : s)
packSubMapUKey :: (k : s) :-> (ByteString : s)
packSubMapUKey = MText -> (k : s) :-> (MText & (k : s))
forall t (s :: [*]). NiceConstant t => t -> s :-> (t & s)
push MText
submapName ((k : s) :-> (MText & (k : s)))
-> ((MText & (k : s)) :-> ((MText, k) & s))
-> (k : s) :-> ((MText, k) & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (MText & (k : s)) :-> ((MText, k) & s)
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair ((k : s) :-> ((MText, k) & s))
-> (((MText, k) & s) :-> (ByteString : s))
-> (k : s) :-> (ByteString : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (s :: [*]).
NicePackedValue (MText, k) =>
((MText, k) & s) :-> (ByteString & s)
forall a (s :: [*]).
NicePackedValue a =>
(a & s) :-> (ByteString & s)
pack @(UStoreSubmapKey _)
  where
    submapName :: MText
submapName = KnownSymbol field => MText
forall (field :: Symbol). KnownSymbol field => MText
fieldNameToMText @field

unpackUValueUnsafe
  :: forall (field :: Symbol) val s.
     (KnownSymbol field, NiceUnpackedValue val)
  => (ByteString : s) :-> (val : s)
unpackUValueUnsafe :: (ByteString : s) :-> (val : s)
unpackUValueUnsafe = forall (s :: [*]).
NiceUnpackedValue val =>
(ByteString & s) :-> (Maybe val & s)
forall a (s :: [*]).
NiceUnpackedValue a =>
(ByteString & s) :-> (Maybe a & s)
unpack @val ((ByteString : s) :-> (Maybe val & s))
-> ((Maybe val & s) :-> (val : s))
-> (ByteString : s) :-> (val : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((val : s) :-> (val : s))
-> (s :-> (val : s)) -> (Maybe val & s) :-> (val : s)
forall a (s :: [*]) (s' :: [*]).
((a & s) :-> s') -> (s :-> s') -> (Maybe a & s) :-> s'
ifSome (val : s) :-> (val : s)
forall (s :: [*]). s :-> s
nop (MText -> s :-> (val : s)
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing MText
failErr)
  where
    failErr :: MText
failErr = [MText] -> MText
forall a. Monoid a => [a] -> a
mconcat
      [ [mt|UStore: failed to unpack |]
      , KnownSymbol field => MText
forall (field :: Symbol). KnownSymbol field => MText
fieldNameToMText @field
      ]

-- Main instructions
----------------------------------------------------------------------------

-- | Put an empty 'UStore' onto the stack. This function is generally unsafe:
-- if store template contains a 'UStoreField', the resulting 'UStore' is not
-- immediately usable.
-- If you are sure that 'UStore' contains only submaps, feel free to just use
-- the result of this function. Otherwise you must set all fields.
unsafeEmptyUStore :: forall store s. s :-> UStore store ': s
unsafeEmptyUStore :: s :-> (UStore store : s)
unsafeEmptyUStore = s :-> (BigMap ByteString ByteString & s)
forall k v (s :: [*]).
(NiceComparable k, KnownValue v) =>
s :-> (BigMap k v & s)
emptyBigMap (s :-> (BigMap ByteString ByteString & s))
-> ((BigMap ByteString ByteString & s) :-> (UStore store : s))
-> s :-> (UStore store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (BigMap ByteString ByteString & s) :-> (UStore store : s)
forall a (s :: [*]). Wrappable a => (Unwrappable a : s) :-> (a : s)
coerceWrap

ustoreMem
  :: forall store name s.
     (KeyAccessC store name)
  => Label name
  -> GetUStoreKey store name : UStore store : s :-> Bool : s
ustoreMem :: Label name
-> (GetUStoreKey store name : UStore store : s) :-> (Bool : s)
ustoreMem _ = forall k (s :: [*]).
(KnownSymbol name, NicePackedValue k) =>
(k : s) :-> (ByteString : s)
forall (field :: Symbol) k (s :: [*]).
(KnownSymbol field, NicePackedValue k) =>
(k : s) :-> (ByteString : s)
packSubMapUKey @name ((GetUStoreKey store name : UStore store : s)
 :-> (ByteString : UStore store : s))
-> ((ByteString : UStore store : s) :-> (Bool : s))
-> (GetUStoreKey store name : UStore store : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (ByteString : UStore store : s) :-> (Bool : s)
forall c (s :: [*]).
MemOpHs c =>
(MemOpKeyHs c & (c & s)) :-> (Bool & s)
mem

ustoreGet
  :: forall store name s.
     (KeyAccessC store name, ValueAccessC store name)
  => Label name
  -> GetUStoreKey store name : UStore store : s
       :-> Maybe (GetUStoreValue store name) : s
ustoreGet :: Label name
-> (GetUStoreKey store name : UStore store : s)
   :-> (Maybe (GetUStoreValue store name) : s)
ustoreGet _ =
  forall k (s :: [*]).
(KnownSymbol name, NicePackedValue k) =>
(k : s) :-> (ByteString : s)
forall (field :: Symbol) k (s :: [*]).
(KnownSymbol field, NicePackedValue k) =>
(k : s) :-> (ByteString : s)
packSubMapUKey @name ((GetUStoreKey store name : UStore store : s)
 :-> (ByteString : UStore store : s))
-> ((ByteString : UStore store : s) :-> (Maybe ByteString : s))
-> (GetUStoreKey store name : UStore store : s)
   :-> (Maybe ByteString : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (ByteString : UStore store : s) :-> (Maybe ByteString : s)
forall c (s :: [*]).
(GetOpHs c, KnownValue (GetOpValHs c)) =>
(GetOpKeyHs c & (c & s)) :-> (Maybe (GetOpValHs c) & s)
L.get ((GetUStoreKey store name : UStore store : s)
 :-> (Maybe ByteString : s))
-> ((Maybe ByteString : s)
    :-> (Maybe (GetUStoreValue store name) : s))
-> (GetUStoreKey store name : UStore store : s)
   :-> (Maybe (GetUStoreValue store name) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((ByteString : s) :-> (GetUStoreValue store name : s))
-> (Maybe ByteString : s)
   :-> (Maybe (GetUStoreValue store name) : s)
forall (c :: * -> *) b a (s :: [*]).
(LorentzFunctor c, KnownValue b) =>
((a : s) :-> (b : s)) -> (c a : s) :-> (c b : s)
lmap (forall (s :: [*]).
(KnownSymbol name,
 NiceUnpackedValue (GetUStoreValue store name)) =>
(ByteString : s) :-> (GetUStoreValue store name : s)
forall (field :: Symbol) val (s :: [*]).
(KnownSymbol field, NiceUnpackedValue val) =>
(ByteString : s) :-> (val : s)
unpackUValueUnsafe @name @(GetUStoreValue store name))

ustoreUpdate
  :: forall store name s.
     (KeyAccessC store name, ValueAccessC store name)
  => Label name
  -> GetUStoreKey store name
      : Maybe (GetUStoreValue store name)
      : UStore store
      : s
  :-> UStore store : s
ustoreUpdate :: Label name
-> (GetUStoreKey store name
      : Maybe (GetUStoreValue store name) : UStore store : s)
   :-> (UStore store : s)
ustoreUpdate _ =
  forall k (s :: [*]).
(KnownSymbol name, NicePackedValue k) =>
(k : s) :-> (ByteString : s)
forall (field :: Symbol) k (s :: [*]).
(KnownSymbol field, NicePackedValue k) =>
(k : s) :-> (ByteString : s)
packSubMapUKey @name ((GetUStoreKey store name
    : Maybe (GetUStoreValue store name) : UStore store : s)
 :-> (ByteString
        : Maybe (GetUStoreValue store name) : UStore store : s))
-> ((ByteString
       : Maybe (GetUStoreValue store name) : UStore store : s)
    :-> (ByteString & (Maybe ByteString : UStore store : s)))
-> (GetUStoreKey store name
      : Maybe (GetUStoreValue store name) : UStore store : s)
   :-> (ByteString & (Maybe ByteString : UStore store : s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((Maybe (GetUStoreValue store name) : UStore store : s)
 :-> (Maybe ByteString : UStore store : s))
-> (ByteString
      : Maybe (GetUStoreValue store name) : UStore store : s)
   :-> (ByteString & (Maybe ByteString : UStore store : s))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (((GetUStoreValue store name : UStore store : s)
 :-> (ByteString : UStore store : s))
-> (Maybe (GetUStoreValue store name) : UStore store : s)
   :-> (Maybe ByteString : UStore store : s)
forall (c :: * -> *) b a (s :: [*]).
(LorentzFunctor c, KnownValue b) =>
((a : s) :-> (b : s)) -> (c a : s) :-> (c b : s)
lmap (GetUStoreValue store name : UStore store : s)
:-> (ByteString : UStore store : s)
forall a (s :: [*]).
NicePackedValue a =>
(a & s) :-> (ByteString & s)
pack) ((GetUStoreKey store name
    : Maybe (GetUStoreValue store name) : UStore store : s)
 :-> (ByteString & (Maybe ByteString : UStore store : s)))
-> ((ByteString & (Maybe ByteString : UStore store : s))
    :-> (UStore store : s))
-> (GetUStoreKey store name
      : Maybe (GetUStoreValue store name) : UStore store : s)
   :-> (UStore store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (ByteString & (Maybe ByteString : UStore store : s))
:-> (UStore store : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
update

ustoreInsert
  :: forall store name s.
     (KeyAccessC store name, ValueAccessC store name)
  => Label name
  -> GetUStoreKey store name
      : GetUStoreValue store name
      : UStore store
      : s
  :-> UStore store : s
ustoreInsert :: Label name
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (UStore store : s)
ustoreInsert _ =
  forall k (s :: [*]).
(KnownSymbol name, NicePackedValue k) =>
(k : s) :-> (ByteString : s)
forall (field :: Symbol) k (s :: [*]).
(KnownSymbol field, NicePackedValue k) =>
(k : s) :-> (ByteString : s)
packSubMapUKey @name ((GetUStoreKey store name
    : GetUStoreValue store name : UStore store : s)
 :-> (ByteString : GetUStoreValue store name : UStore store : s))
-> ((ByteString : GetUStoreValue store name : UStore store : s)
    :-> (ByteString & (Maybe ByteString & (UStore store : s))))
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (ByteString & (Maybe ByteString & (UStore store : s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((GetUStoreValue store name : UStore store : s)
 :-> (Maybe ByteString & (UStore store : s)))
-> (ByteString : GetUStoreValue store name : UStore store : s)
   :-> (ByteString & (Maybe ByteString & (UStore store : s)))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip ((GetUStoreValue store name : UStore store : s)
:-> (ByteString & (UStore store : s))
forall a (s :: [*]).
NicePackedValue a =>
(a & s) :-> (ByteString & s)
pack ((GetUStoreValue store name : UStore store : s)
 :-> (ByteString & (UStore store : s)))
-> ((ByteString & (UStore store : s))
    :-> (Maybe ByteString & (UStore store : s)))
-> (GetUStoreValue store name : UStore store : s)
   :-> (Maybe ByteString & (UStore store : s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (ByteString & (UStore store : s))
:-> (Maybe ByteString & (UStore store : s))
forall a (s :: [*]). (a & s) :-> (Maybe a & s)
L.some) ((GetUStoreKey store name
    : GetUStoreValue store name : UStore store : s)
 :-> (ByteString & (Maybe ByteString & (UStore store : s))))
-> ((ByteString & (Maybe ByteString & (UStore store : s)))
    :-> (UStore store : s))
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (UStore store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (ByteString & (Maybe ByteString & (UStore store : s)))
:-> (UStore store : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
update

-- | Insert a key-value pair, but fail if it will overwrite some existing entry.
ustoreInsertNew
  :: forall store name s.
     (KeyAccessC store name, ValueAccessC store name)
  => Label name
  -> (forall s0 any. GetUStoreKey store name : s0 :-> any)
  -> GetUStoreKey store name
      : GetUStoreValue store name
      : UStore store
      : s
  :-> UStore store : s
ustoreInsertNew :: Label name
-> (forall (s0 :: [*]) (any :: [*]).
    (GetUStoreKey store name : s0) :-> any)
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (UStore store : s)
ustoreInsertNew label :: Label name
label doFail :: forall (s0 :: [*]) (any :: [*]).
(GetUStoreKey store name : 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)
duupX @3 ((GetUStoreKey store name
    : GetUStoreValue store name : UStore store : s)
 :-> (UStore store
        : GetUStoreKey store name : GetUStoreValue store name
        : UStore store : s))
-> ((UStore store
       : GetUStoreKey store name : GetUStoreValue store name
       : UStore store : s)
    :-> (GetUStoreKey store name
           : UStore store : GetUStoreKey store name
           : GetUStoreValue store name : UStore store : s))
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (GetUStoreKey store name
          : UStore store : GetUStoreKey store name
          : GetUStoreValue store name : UStore 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)
duupX @2 ((GetUStoreKey store name
    : GetUStoreValue store name : UStore store : s)
 :-> (GetUStoreKey store name
        : UStore store : GetUStoreKey store name
        : GetUStoreValue store name : UStore store : s))
-> ((GetUStoreKey store name
       : UStore store : GetUStoreKey store name
       : GetUStoreValue store name : UStore store : s)
    :-> (Bool
           : GetUStoreKey store name : GetUStoreValue store name
           : UStore store : s))
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (Bool
          : GetUStoreKey store name : GetUStoreValue store name
          : UStore store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label name
-> (GetUStoreKey store name
      : UStore store : GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (Bool
          : GetUStoreKey store name : GetUStoreValue store name
          : UStore store : s)
forall store (name :: Symbol) (s :: [*]).
KeyAccessC store name =>
Label name
-> (GetUStoreKey store name : UStore store : s) :-> (Bool : s)
ustoreMem Label name
label ((GetUStoreKey store name
    : GetUStoreValue store name : UStore store : s)
 :-> (Bool
        : GetUStoreKey store name : GetUStoreValue store name
        : UStore store : s))
-> ((Bool
       : GetUStoreKey store name : GetUStoreValue store name
       : UStore store : s)
    :-> (UStore store : s))
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (UStore store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((GetUStoreKey store name
    : GetUStoreValue store name : UStore store : s)
 :-> (UStore store : s))
-> ((GetUStoreKey store name
       : GetUStoreValue store name : UStore store : s)
    :-> (UStore store : s))
-> (Bool
      : GetUStoreKey store name : GetUStoreValue store name
      : UStore store : s)
   :-> (UStore store : s)
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ (GetUStoreKey store name
   : GetUStoreValue store name : UStore store : s)
:-> (UStore store : s)
forall (s0 :: [*]) (any :: [*]).
(GetUStoreKey store name : s0) :-> any
doFail (Label name
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (UStore store : s)
forall store (name :: Symbol) (s :: [*]).
(KeyAccessC store name, ValueAccessC store name) =>
Label name
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (UStore store : s)
ustoreInsert Label name
label)

ustoreDelete
  :: forall store name s.
     (KeyAccessC store name)
  => Label name
  -> GetUStoreKey store name : UStore store : s
     :-> UStore store : s
ustoreDelete :: Label name
-> (GetUStoreKey store name : UStore store : s)
   :-> (UStore store : s)
ustoreDelete _ =
  forall k (s :: [*]).
(KnownSymbol name, NicePackedValue k) =>
(k : s) :-> (ByteString : s)
forall (field :: Symbol) k (s :: [*]).
(KnownSymbol field, NicePackedValue k) =>
(k : s) :-> (ByteString : s)
packSubMapUKey @name ((GetUStoreKey store name : UStore store : s)
 :-> (ByteString : UStore store : s))
-> ((ByteString : UStore store : s)
    :-> (ByteString & (Maybe ByteString & (UStore store : s))))
-> (GetUStoreKey store name : UStore store : s)
   :-> (ByteString & (Maybe ByteString & (UStore store : s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((UStore store : s) :-> (Maybe ByteString & (UStore store : s)))
-> (ByteString : UStore store : s)
   :-> (ByteString & (Maybe ByteString & (UStore store : s)))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (UStore store : s) :-> (Maybe ByteString & (UStore store : s))
forall a (s :: [*]). KnownValue a => s :-> (Maybe a & s)
none ((GetUStoreKey store name : UStore store : s)
 :-> (ByteString & (Maybe ByteString & (UStore store : s))))
-> ((ByteString & (Maybe ByteString & (UStore store : s)))
    :-> (UStore store : s))
-> (GetUStoreKey store name : UStore store : s)
   :-> (UStore store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (ByteString & (Maybe ByteString & (UStore store : s)))
:-> (UStore store : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
update

-- | Like 'toField', but for 'UStore'.
--
-- This may fail only if 'UStore' was made up incorrectly during contract
-- initialization.
ustoreToField
  :: forall store name s.
     (FieldAccessC store name)
  => Label name
  -> UStore store : s
     :-> GetUStoreField store name : s
ustoreToField :: Label name
-> (UStore store : s) :-> (GetUStoreField store name : s)
ustoreToField l :: Label name
l =
  ByteString
-> (UStore store : s) :-> (ByteString & (UStore store : s))
forall t (s :: [*]). NiceConstant t => t -> s :-> (t & s)
push (Label name -> ByteString
forall store (field :: Symbol).
KnownUStoreMarker (GetUStoreFieldMarker store field) =>
Label field -> ByteString
mkFieldUKey @store Label name
l) ((UStore store : s) :-> (ByteString & (UStore store : s)))
-> ((ByteString & (UStore store : s)) :-> (Maybe ByteString & s))
-> (UStore store : s) :-> (Maybe ByteString & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (ByteString & (UStore store : s)) :-> (Maybe ByteString & s)
forall c (s :: [*]).
(GetOpHs c, KnownValue (GetOpValHs c)) =>
(GetOpKeyHs c & (c & s)) :-> (Maybe (GetOpValHs c) & s)
L.get ((UStore store : s) :-> (Maybe ByteString & s))
-> ((Maybe ByteString & s) :-> (ByteString & s))
-> (UStore store : s) :-> (ByteString & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (Maybe ByteString & s) :-> (ByteString & s)
ensureFieldIsPresent ((UStore store : s) :-> (ByteString & s))
-> ((ByteString & s) :-> (GetUStoreField store name : s))
-> (UStore store : s) :-> (GetUStoreField store name : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  forall (s :: [*]).
(KnownSymbol name,
 NiceUnpackedValue (GetUStoreField store name)) =>
(ByteString : s) :-> (GetUStoreField store name : s)
forall (field :: Symbol) val (s :: [*]).
(KnownSymbol field, NiceUnpackedValue val) =>
(ByteString : s) :-> (val : s)
unpackUValueUnsafe @name @(GetUStoreField store name)
  where
    ensureFieldIsPresent :: (Maybe ByteString & s) :-> (ByteString & s)
ensureFieldIsPresent =
      ((ByteString & s) :-> (ByteString & s))
-> (s :-> (ByteString & s))
-> (Maybe ByteString & s) :-> (ByteString & s)
forall a (s :: [*]) (s' :: [*]).
((a & s) :-> s') -> (s :-> s') -> (Maybe a & s) :-> s'
ifSome (ByteString & s) :-> (ByteString & s)
forall (s :: [*]). s :-> s
nop ((s :-> (ByteString & s))
 -> (Maybe ByteString & s) :-> (ByteString & s))
-> (s :-> (ByteString & s))
-> (Maybe ByteString & s) :-> (ByteString & s)
forall a b. (a -> b) -> a -> b
$ MText -> s :-> (ByteString & s)
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing (MText -> s :-> (ByteString & s))
-> MText -> s :-> (ByteString & s)
forall a b. (a -> b) -> a -> b
$ [MText] -> MText
forall a. Monoid a => [a] -> a
mconcat
        [ [mt|UStore: no field |]
        , KnownSymbol name => MText
forall (field :: Symbol). KnownSymbol field => MText
fieldNameToMText @name
        ]

-- | Like 'getField', but for 'UStore'.
--
-- This may fail only if 'UStore' was made up incorrectly during contract
-- initialization.
ustoreGetField
  :: forall store name s.
     (FieldAccessC store name)
  => Label name
  -> UStore store : s
     :-> GetUStoreField store name : UStore store : s
ustoreGetField :: Label name
-> (UStore store : s)
   :-> (GetUStoreField store name : UStore store : s)
ustoreGetField label :: Label name
label = (UStore store : s) :-> (UStore store & (UStore store : s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup ((UStore store : s) :-> (UStore store & (UStore store : s)))
-> ((UStore store & (UStore store : s))
    :-> (GetUStoreField store name : UStore store : s))
-> (UStore store : s)
   :-> (GetUStoreField store name : UStore store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label name
-> (UStore store & (UStore store : s))
   :-> (GetUStoreField store name : UStore store : s)
forall store (name :: Symbol) (s :: [*]).
FieldAccessC store name =>
Label name
-> (UStore store : s) :-> (GetUStoreField store name : s)
ustoreToField Label name
label

-- | Like 'setField', but for 'UStore'.
ustoreSetField
  :: forall store name s.
     (FieldAccessC store name)
  => Label name
  -> GetUStoreField store name : UStore store : s
     :-> UStore store : s
ustoreSetField :: Label name
-> (GetUStoreField store name : UStore store : s)
   :-> (UStore store : s)
ustoreSetField l :: Label name
l =
  (GetUStoreField store name : UStore store : s)
:-> (ByteString & (UStore store : s))
forall a (s :: [*]).
NicePackedValue a =>
(a & s) :-> (ByteString & s)
pack ((GetUStoreField store name : UStore store : s)
 :-> (ByteString & (UStore store : s)))
-> ((ByteString & (UStore store : s))
    :-> (Maybe ByteString & (UStore store : s)))
-> (GetUStoreField store name : UStore store : s)
   :-> (Maybe ByteString & (UStore store : s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (ByteString & (UStore store : s))
:-> (Maybe ByteString & (UStore store : s))
forall a (s :: [*]). (a & s) :-> (Maybe a & s)
L.some ((GetUStoreField store name : UStore store : s)
 :-> (Maybe ByteString & (UStore store : s)))
-> ((Maybe ByteString & (UStore store : s))
    :-> (ByteString & (Maybe ByteString & (UStore store : s))))
-> (GetUStoreField store name : UStore store : s)
   :-> (ByteString & (Maybe ByteString & (UStore store : s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ByteString
-> (Maybe ByteString & (UStore store : s))
   :-> (ByteString & (Maybe ByteString & (UStore store : s)))
forall t (s :: [*]). NiceConstant t => t -> s :-> (t & s)
push (Label name -> ByteString
forall store (field :: Symbol).
KnownUStoreMarker (GetUStoreFieldMarker store field) =>
Label field -> ByteString
mkFieldUKey @store Label name
l) ((GetUStoreField store name : UStore store : s)
 :-> (ByteString & (Maybe ByteString & (UStore store : s))))
-> ((ByteString & (Maybe ByteString & (UStore store : s)))
    :-> (UStore store : s))
-> (GetUStoreField store name : UStore store : s)
   :-> (UStore store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (ByteString & (Maybe ByteString & (UStore store : s)))
:-> (UStore store : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
L.update

-- | Remove a field from 'UStore', for internal purposes only.
ustoreRemoveFieldUnsafe
  :: forall store name s.
     (FieldAccessC store name)
  => Label name
  -> UStore store : s
     :-> UStore store : s
ustoreRemoveFieldUnsafe :: Label name -> (UStore store : s) :-> (UStore store : s)
ustoreRemoveFieldUnsafe l :: Label name
l =
  (UStore store : s) :-> (Maybe ByteString & (UStore store : s))
forall a (s :: [*]). KnownValue a => s :-> (Maybe a & s)
L.none ((UStore store : s) :-> (Maybe ByteString & (UStore store : s)))
-> ((Maybe ByteString & (UStore store : s))
    :-> (ByteString & (Maybe ByteString & (UStore store : s))))
-> (UStore store : s)
   :-> (ByteString & (Maybe ByteString & (UStore store : s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ByteString
-> (Maybe ByteString & (UStore store : s))
   :-> (ByteString & (Maybe ByteString & (UStore store : s)))
forall t (s :: [*]). NiceConstant t => t -> s :-> (t & s)
push (Label name -> ByteString
forall store (field :: Symbol).
KnownUStoreMarker (GetUStoreFieldMarker store field) =>
Label field -> ByteString
mkFieldUKey @store Label name
l) ((UStore store : s)
 :-> (ByteString & (Maybe ByteString & (UStore store : s))))
-> ((ByteString & (Maybe ByteString & (UStore store : s)))
    :-> (UStore store : s))
-> (UStore store : s) :-> (UStore store : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (ByteString & (Maybe ByteString & (UStore store : s)))
:-> (UStore store : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
L.update

-- | This constraint can be used if a function needs to work with
-- /big/ store, but needs to know only about some submap(s) of it.
--
-- It can use all UStore operations for a particular name, key and
-- value without knowing whole template.
type HasUStore name key value store =
   ( KeyAccessC store name, ValueAccessC store name
   , GetUStoreKey store name ~ key
   , GetUStoreValue store name ~ value
   )

-- | This constraint can be used if a function needs to work with
-- /big/ store, but needs to know only about some field of it.
type HasUField name ty store =
   ( FieldAccessC store name
   , GetUStoreField store name ~ ty
   )

-- | Write down all sensisble constraints which given @store@ satisfies
-- and apply them to @constrained@.
--
-- This store should have '|~>' and 'UStoreField' fields in its immediate fields,
-- no deep inspection is performed.
type HasUStoreForAllIn store constrained =
  (Generic store, GHasStoreForAllIn constrained (G.Rep store))

type family GHasStoreForAllIn (store :: Kind.Type) (x :: Kind.Type -> Kind.Type)
            :: Constraint where
  GHasStoreForAllIn store (G.D1 _ x) = GHasStoreForAllIn store x
  GHasStoreForAllIn store (x :+: y) =
    (GHasStoreForAllIn store x, GHasStoreForAllIn store y)
  GHasStoreForAllIn store (x :*: y) =
    (GHasStoreForAllIn store x, GHasStoreForAllIn store y)
  GHasStoreForAllIn store (G.C1 _ x) = GHasStoreForAllIn store x
  GHasStoreForAllIn store (G.S1 ('G.MetaSel ('Just name) _ _ _)
                            (G.Rec0 (key |~> value))) =
    HasUStore name key value store
  GHasStoreForAllIn store (G.S1 ('G.MetaSel ('Just name) _ _ _)
                            (G.Rec0 (UStoreFieldExt _ value))) =
    HasUField name value store
  GHasStoreForAllIn _ G.V1 = ()
  GHasStoreForAllIn _ G.U1 = ()

----------------------------------------------------------------------------
-- Examples
----------------------------------------------------------------------------

data MyStoreTemplate = MyStoreTemplate
  { MyStoreTemplate -> Integer |~> ()
ints :: Integer |~> ()
  , MyStoreTemplate -> ByteString |~> ByteString
bytes :: ByteString |~> ByteString
  , MyStoreTemplate -> UStoreField Bool
flag :: UStoreField Bool
  , MyStoreTemplate -> UStoreFieldExt Marker1 Integer
entrypoint :: UStoreFieldExt Marker1 Integer
  }
  deriving stock ((forall x. MyStoreTemplate -> Rep MyStoreTemplate x)
-> (forall x. Rep MyStoreTemplate x -> MyStoreTemplate)
-> Generic MyStoreTemplate
forall x. Rep MyStoreTemplate x -> MyStoreTemplate
forall x. MyStoreTemplate -> Rep MyStoreTemplate x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MyStoreTemplate x -> MyStoreTemplate
$cfrom :: forall x. MyStoreTemplate -> Rep MyStoreTemplate x
Generic)

type MyStore = UStore MyStoreTemplate

data Marker1 :: UStoreMarkerType
  deriving anyclass MText -> ByteString
(MText -> ByteString) -> KnownUStoreMarker Marker1
forall (marker :: UStoreMarkerType).
(MText -> ByteString) -> KnownUStoreMarker marker
mkFieldMarkerUKey :: MText -> ByteString
$cmkFieldMarkerUKey :: MText -> ByteString
KnownUStoreMarker

_sample1 :: Integer : MyStore : s :-> MyStore : s
_sample1 :: (Integer : MyStore : s) :-> (MyStore : s)
_sample1 = Label "ints"
-> (GetUStoreKey MyStoreTemplate "ints" : MyStore : s)
   :-> (MyStore : s)
forall store (name :: Symbol) (s :: [*]).
KeyAccessC store name =>
Label name
-> (GetUStoreKey store name : UStore store : s)
   :-> (UStore store : s)
ustoreDelete @MyStoreTemplate IsLabel "ints" (Label "ints")
Label "ints"
#ints

_sample2 :: ByteString : ByteString : MyStore : s :-> MyStore : s
_sample2 :: (ByteString : ByteString : MyStore : s) :-> (MyStore : s)
_sample2 = Label "bytes"
-> (GetUStoreKey MyStoreTemplate "bytes"
      : GetUStoreValue MyStoreTemplate "bytes" : MyStore : s)
   :-> (MyStore : s)
forall store (name :: Symbol) (s :: [*]).
(KeyAccessC store name, ValueAccessC store name) =>
Label name
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (UStore store : s)
ustoreInsert @MyStoreTemplate IsLabel "bytes" (Label "bytes")
Label "bytes"
#bytes

_sample3 :: MyStore : s :-> Bool : s
_sample3 :: (MyStore : s) :-> (Bool : s)
_sample3 = Label "flag"
-> (MyStore : s) :-> (GetUStoreField MyStoreTemplate "flag" : s)
forall store (name :: Symbol) (s :: [*]).
FieldAccessC store name =>
Label name
-> (UStore store : s) :-> (GetUStoreField store name : s)
ustoreToField @MyStoreTemplate IsLabel "flag" (Label "flag")
Label "flag"
#flag

_sample3'5 :: MyStore : s :-> Integer : s
_sample3'5 :: (MyStore : s) :-> (Integer : s)
_sample3'5 = Label "entrypoint"
-> (MyStore : s)
   :-> (GetUStoreField MyStoreTemplate "entrypoint" : s)
forall store (name :: Symbol) (s :: [*]).
FieldAccessC store name =>
Label name
-> (UStore store : s) :-> (GetUStoreField store name : s)
ustoreToField @MyStoreTemplate IsLabel "entrypoint" (Label "entrypoint")
Label "entrypoint"
#entrypoint

data MyStoreTemplate2 = MyStoreTemplate2
  { MyStoreTemplate2 -> Bool |~> Bool
bools :: Bool |~> Bool
  , MyStoreTemplate2 -> Integer |~> Integer
ints2 :: Integer |~> Integer
  , MyStoreTemplate2 -> Integer |~> Bool
ints3 :: Integer |~> Bool
  }
  deriving stock ((forall x. MyStoreTemplate2 -> Rep MyStoreTemplate2 x)
-> (forall x. Rep MyStoreTemplate2 x -> MyStoreTemplate2)
-> Generic MyStoreTemplate2
forall x. Rep MyStoreTemplate2 x -> MyStoreTemplate2
forall x. MyStoreTemplate2 -> Rep MyStoreTemplate2 x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MyStoreTemplate2 x -> MyStoreTemplate2
$cfrom :: forall x. MyStoreTemplate2 -> Rep MyStoreTemplate2 x
Generic)

newtype MyNatural = MyNatural Natural
  deriving newtype (WellTypedToT MyNatural
WellTypedToT MyNatural =>
(MyNatural -> Value (ToT MyNatural))
-> (Value (ToT MyNatural) -> MyNatural) -> IsoValue MyNatural
Value (ToT MyNatural) -> MyNatural
MyNatural -> Value (ToT MyNatural)
forall a.
WellTypedToT a =>
(a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
fromVal :: Value (ToT MyNatural) -> MyNatural
$cfromVal :: Value (ToT MyNatural) -> MyNatural
toVal :: MyNatural -> Value (ToT MyNatural)
$ctoVal :: MyNatural -> Value (ToT MyNatural)
$cp1IsoValue :: WellTypedToT MyNatural
IsoValue)

data MyStoreTemplate3 = MyStoreTemplate3 { MyStoreTemplate3 -> Natural |~> MyNatural
store3 :: Natural |~> MyNatural }
  deriving stock (forall x. MyStoreTemplate3 -> Rep MyStoreTemplate3 x)
-> (forall x. Rep MyStoreTemplate3 x -> MyStoreTemplate3)
-> Generic MyStoreTemplate3
forall x. Rep MyStoreTemplate3 x -> MyStoreTemplate3
forall x. MyStoreTemplate3 -> Rep MyStoreTemplate3 x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MyStoreTemplate3 x -> MyStoreTemplate3
$cfrom :: forall x. MyStoreTemplate3 -> Rep MyStoreTemplate3 x
Generic

data MyStoreTemplateBig = MyStoreTemplateBig
  MyStoreTemplate
  MyStoreTemplate2
  MyStoreTemplate3
  deriving stock (forall x. MyStoreTemplateBig -> Rep MyStoreTemplateBig x)
-> (forall x. Rep MyStoreTemplateBig x -> MyStoreTemplateBig)
-> Generic MyStoreTemplateBig
forall x. Rep MyStoreTemplateBig x -> MyStoreTemplateBig
forall x. MyStoreTemplateBig -> Rep MyStoreTemplateBig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MyStoreTemplateBig x -> MyStoreTemplateBig
$cfrom :: forall x. MyStoreTemplateBig -> Rep MyStoreTemplateBig x
Generic

_MyStoreTemplateBigTextsStore ::
  GetUStore "bytes" MyStoreTemplateBig :~: 'MapSignature ByteString ByteString
_MyStoreTemplateBigTextsStore :: GetUStore "bytes" MyStoreTemplateBig
:~: 'MapSignature ByteString ByteString
_MyStoreTemplateBigTextsStore = GetUStore "bytes" MyStoreTemplateBig
:~: 'MapSignature ByteString ByteString
forall k (a :: k). a :~: a
Refl

_MyStoreTemplateBigBoolsStore ::
  GetUStore "bools" MyStoreTemplateBig :~: 'MapSignature Bool Bool
_MyStoreTemplateBigBoolsStore :: GetUStore "bools" MyStoreTemplateBig :~: 'MapSignature Bool Bool
_MyStoreTemplateBigBoolsStore = GetUStore "bools" MyStoreTemplateBig :~: 'MapSignature Bool Bool
forall k (a :: k). a :~: a
Refl

_MyStoreTemplateBigMyStoreTemplate3 ::
  GetUStore "store3" MyStoreTemplateBig :~: 'MapSignature Natural MyNatural
_MyStoreTemplateBigMyStoreTemplate3 :: GetUStore "store3" MyStoreTemplateBig
:~: 'MapSignature Natural MyNatural
_MyStoreTemplateBigMyStoreTemplate3 = GetUStore "store3" MyStoreTemplateBig
:~: 'MapSignature Natural MyNatural
forall k (a :: k). a :~: a
Refl

type MyStoreBig = UStore MyStoreTemplateBig

_sample4 :: Integer : MyStoreBig : s :-> MyStoreBig : s
_sample4 :: (Integer : MyStoreBig : s) :-> (MyStoreBig : s)
_sample4 = Label "ints2"
-> (GetUStoreKey MyStoreTemplateBig "ints2" : MyStoreBig : s)
   :-> (MyStoreBig : s)
forall store (name :: Symbol) (s :: [*]).
KeyAccessC store name =>
Label name
-> (GetUStoreKey store name : UStore store : s)
   :-> (UStore store : s)
ustoreDelete IsLabel "ints2" (Label "ints2")
Label "ints2"
#ints2

_sample5 :: ByteString : MyStoreBig : s :-> Bool : s
_sample5 :: (ByteString : MyStoreBig : s) :-> (Bool : s)
_sample5 = Label "bytes"
-> (GetUStoreKey MyStoreTemplateBig "bytes" : MyStoreBig : s)
   :-> (Bool : s)
forall store (name :: Symbol) (s :: [*]).
KeyAccessC store name =>
Label name
-> (GetUStoreKey store name : UStore store : s) :-> (Bool : s)
ustoreMem IsLabel "bytes" (Label "bytes")
Label "bytes"
#bytes

_sample6 :: Natural : MyNatural : MyStoreBig : s :-> MyStoreBig : s
_sample6 :: (Natural : MyNatural : MyStoreBig : s) :-> (MyStoreBig : s)
_sample6 = Label "store3"
-> (GetUStoreKey MyStoreTemplateBig "store3"
      : GetUStoreValue MyStoreTemplateBig "store3" : MyStoreBig : s)
   :-> (MyStoreBig : s)
forall store (name :: Symbol) (s :: [*]).
(KeyAccessC store name, ValueAccessC store name) =>
Label name
-> (GetUStoreKey store name
      : GetUStoreValue store name : UStore store : s)
   :-> (UStore store : s)
ustoreInsert IsLabel "store3" (Label "store3")
Label "store3"
#store3

-- | When you want to express a constraint like
-- "given big store contains all elements present in given small concrete store",
-- you can use 'HasUStoreForAllIn'.
--
-- Here @store@ is a big store, and we expect it to contain 'MyStoreTemplate'
-- entirely.
_sample7
  :: HasUStoreForAllIn MyStoreTemplate store
  => UStore store : s :-> Bool : Maybe ByteString : s
_sample7 :: (UStore store : s) :-> (Bool : Maybe ByteString : s)
_sample7 = Label "flag"
-> (UStore store : s)
   :-> (GetUStoreField store "flag" : UStore store : s)
forall store (name :: Symbol) (s :: [*]).
FieldAccessC store name =>
Label name
-> (UStore store : s)
   :-> (GetUStoreField store name : UStore store : s)
ustoreGetField IsLabel "flag" (Label "flag")
Label "flag"
#flag ((UStore store : s) :-> (Bool : UStore store : s))
-> ((Bool : UStore store : s) :-> (Bool : Maybe ByteString : s))
-> (UStore store : s) :-> (Bool : Maybe ByteString : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((UStore store : s) :-> (Maybe ByteString : s))
-> (Bool : UStore store : s) :-> (Bool : Maybe ByteString : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (ByteString
-> (UStore store : s) :-> (ByteString & (UStore store : s))
forall t (s :: [*]). NiceConstant t => t -> s :-> (t & s)
push "x" ((UStore store : s) :-> (ByteString & (UStore store : s)))
-> ((ByteString & (UStore store : s)) :-> (Maybe ByteString : s))
-> (UStore store : s) :-> (Maybe ByteString : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label "bytes"
-> (GetUStoreKey store "bytes" : UStore store : s)
   :-> (Maybe (GetUStoreValue store "bytes") : s)
forall store (name :: Symbol) (s :: [*]).
(KeyAccessC store name, ValueAccessC store name) =>
Label name
-> (GetUStoreKey store name : UStore store : s)
   :-> (Maybe (GetUStoreValue store name) : s)
ustoreGet IsLabel "bytes" (Label "bytes")
Label "bytes"
#bytes)

-- | '_sample7' with @store@ instantiated to 'MyStoreTemplateBig'.
_sample7' :: UStore MyStoreTemplateBig : s :-> Bool : Maybe ByteString : s
_sample7' :: (MyStoreBig : s) :-> (Bool : Maybe ByteString : s)
_sample7' = (MyStoreBig : s) :-> (Bool : Maybe ByteString : s)
forall store (s :: [*]).
HasUStoreForAllIn MyStoreTemplate store =>
(UStore store : s) :-> (Bool : Maybe ByteString : s)
_sample7