{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Lorentz.UStore.Lift
( liftUStore
, unliftUStore
, UStoreFieldsAreUnique
) where
import Data.Vinyl.Derived (Label)
import Data.Type.Bool (If)
import qualified Data.Kind as Kind
import GHC.TypeLits (Symbol, TypeError, ErrorMessage (..))
import Data.Vinyl.TypeLevel (type (++))
import GHC.Generics (type (:+:), type (:*:))
import qualified GHC.Generics as G
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Instr
import Lorentz.UStore.Types
import Michelson.Typed.Haskell
import Util.Type
type UStoreFields (template :: Kind.Type) = GUStoreFields (G.Rep template)
type family GUStoreFields (x :: Kind.Type -> Kind.Type) :: [Symbol] where
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"))
liftUStore
:: (Generic template, RequireAllUniqueFields template)
=> Label name
-> UStore (GetFieldType template name) : s :-> UStore template : s
liftUStore _ = forcedCoerce_
unliftUStore
:: (Generic template)
=> Label name
-> UStore template : s :-> UStore (GetFieldType template name) : s
unliftUStore _ = forcedCoerce_
data MyStoreTemplate = MyStoreTemplate
{ ints :: Integer |~> Integer
} deriving stock Generic
data MyStoreTemplateBig = MyStoreTemplateBig
{ bool :: UStoreField Bool
, substore :: MyStoreTemplate
} deriving stock Generic
_sampleWithMyStore
:: ('[param, UStore MyStoreTemplate] :-> '[UStore MyStoreTemplate])
-> ('[param, UStore MyStoreTemplateBig] :-> '[UStore MyStoreTemplateBig])
_sampleWithMyStore instr =
dip (unliftUStore #substore) # instr # liftUStore #substore