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

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

-- | Composability helper for 'UStore'.
module Lorentz.UStore.Lift
  ( liftUStore
  , unliftUStore

    -- * Internals
  , UStoreFieldsAreUnique
  ) where

import qualified Data.Kind as Kind
import GHC.Generics (type (:+:), type (:*:))
import qualified GHC.Generics as G
import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)

import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Instr
import Lorentz.UStore.Types
import Michelson.Typed.Haskell
import Util.Label (Label)
import Util.Type

-- | Get all fields names accessible in given 'UStore' template.
type UStoreFields (template :: Kind.Type) = GUStoreFields (G.Rep template)

type family GUStoreFields (x :: Kind.Type -> Kind.Type) :: [Symbol] where
  -- We are not oblidged to fail in case of bad template - this will be handled
  -- in other operations with 'UStore' anyway.
  GUStoreFields (G.D1 _ x) = GUStoreFields x
  GUStoreFields (_ :+: _) = '[]
  GUStoreFields G.V1 = '[]
  GUStoreFields (G.C1 _ x) = GUStoreFields x
  GUStoreFields (x :*: y) = GUStoreFields x ++ GUStoreFields y
  GUStoreFields (G.S1 ('G.MetaSel ('Just fieldName) _ _ _) (G.Rec0 (_ |~> _))) =
    '[fieldName]
  GUStoreFields (G.S1 ('G.MetaSel ('Just fieldName) _ _ _) (G.Rec0 (UStoreFieldExt _ _))) =
    '[fieldName]
  GUStoreFields (G.S1 _ (G.Rec0 a)) =
    UStoreFields a

type UStoreFieldsAreUnique template = AllUnique (UStoreFields template)

type family RequireAllUniqueFields (template :: Kind.Type) :: Constraint where
  RequireAllUniqueFields template =
    If (UStoreFieldsAreUnique template)
       (() :: Constraint)
       (TypeError ('Text "Some field in template is duplicated"))
      -- TODO: if this ever fires for you and it's not clear which exact field
      -- is duplicated, please create a ticket to implement the corresponding
      -- logic.

-- | Lift an 'UStore' to another 'UStore' which contains all the entries
-- of the former under given field.
--
-- This function is not intended for use in migrations, only in normal
-- entry points.
--
-- Note that this function ensures that template of resulting store
-- does not contain inner nested templates with duplicated fields,
-- otherwise 'UStore' invariants could get broken.
liftUStore
  :: (Generic template, RequireAllUniqueFields template)
  => Label name
  -> UStore (GetFieldType template name) : s :-> UStore template : s
liftUStore :: Label name
-> (UStore (GetFieldType template name) : s)
   :-> (UStore template : s)
liftUStore _ = (UStore (GetFieldType template name) : s) :-> (UStore template : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a & s) :-> (b & s)
forcedCoerce_

-- | Unlift an 'UStore' to a smaller 'UStore' which is part of the former.
--
-- This function is not intended for use in migrations, only in normal
-- entry points.
--
-- Surprisingly, despite smaller 'UStore' may have extra entries,
-- this function is safe when used in contract code.
-- Truly, all getters and setters are still safe to use.
-- Also, there is no way for the resulting small @UStore@ to leak outside
-- of the contract since the only place where 'big_map' can appear
-- is contract storage, so this small @UStore@ can be either dropped
-- or lifted back via 'liftUStore' to appear as part of the new contract's state.
--
-- When this function is run as part of standalone instructions sequence,
-- not as part of contract code (e.g. in tests), you may get an @UStore@
-- with entries not inherent to it.
unliftUStore
  :: (Generic template)
  => Label name
  -> UStore template : s :-> UStore (GetFieldType template name) : s
unliftUStore :: Label name
-> (UStore template : s)
   :-> (UStore (GetFieldType template name) : s)
unliftUStore _ = (UStore template : s) :-> (UStore (GetFieldType template name) : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a & s) :-> (b & s)
forcedCoerce_

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

data MyStoreTemplate = MyStoreTemplate
  { MyStoreTemplate -> Integer |~> Integer
ints :: Integer |~> 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

data MyStoreTemplateBig = MyStoreTemplateBig
  { MyStoreTemplateBig -> UStoreField Bool
bool :: UStoreField Bool
  , MyStoreTemplateBig -> MyStoreTemplate
substore :: MyStoreTemplate
  } 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

-- | This example demostrates a way to run an instruction, operating on small
-- 'UStore', so that it works on a larger 'UStore'.
_sampleWithMyStore
  :: ('[param, UStore MyStoreTemplate] :-> '[UStore MyStoreTemplate])
  -> ('[param, UStore MyStoreTemplateBig] :-> '[UStore MyStoreTemplateBig])
_sampleWithMyStore :: ('[param, UStore MyStoreTemplate] :-> '[UStore MyStoreTemplate])
-> '[param, UStore MyStoreTemplateBig]
   :-> '[UStore MyStoreTemplateBig]
_sampleWithMyStore instr :: '[param, UStore MyStoreTemplate] :-> '[UStore MyStoreTemplate]
instr =
  ('[UStore MyStoreTemplateBig] :-> '[UStore MyStoreTemplate])
-> '[param, UStore MyStoreTemplateBig]
   :-> '[param, UStore MyStoreTemplate]
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (Label "substore"
-> '[UStore MyStoreTemplateBig]
   :-> '[UStore (GetFieldType MyStoreTemplateBig "substore")]
forall template (name :: Symbol) (s :: [*]).
Generic template =>
Label name
-> (UStore template : s)
   :-> (UStore (GetFieldType template name) : s)
unliftUStore IsLabel "substore" (Label "substore")
Label "substore"
#substore) ('[param, UStore MyStoreTemplateBig]
 :-> '[param, UStore MyStoreTemplate])
-> ('[param, UStore MyStoreTemplate] :-> '[UStore MyStoreTemplate])
-> '[param, UStore MyStoreTemplateBig]
   :-> '[UStore MyStoreTemplate]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# '[param, UStore MyStoreTemplate] :-> '[UStore MyStoreTemplate]
instr ('[param, UStore MyStoreTemplateBig] :-> '[UStore MyStoreTemplate])
-> ('[UStore MyStoreTemplate] :-> '[UStore MyStoreTemplateBig])
-> '[param, UStore MyStoreTemplateBig]
   :-> '[UStore MyStoreTemplateBig]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label "substore"
-> '[UStore (GetFieldType MyStoreTemplateBig "substore")]
   :-> '[UStore MyStoreTemplateBig]
forall template (name :: Symbol) (s :: [*]).
(Generic template, RequireAllUniqueFields template) =>
Label name
-> (UStore (GetFieldType template name) : s)
   :-> (UStore template : s)
liftUStore IsLabel "substore" (Label "substore")
Label "substore"
#substore