module Lorentz.EntryPoints.Impl
( EpdPlain
, EpdRecursive
) where
import qualified Data.Kind as Kind
import Data.Singletons (SingI (..))
import Data.Singletons.Prelude (Sing (STrue, SFalse))
import Data.Singletons.Prelude.Eq ((%==))
import Data.Type.Bool (If)
import qualified GHC.Generics as G
import Util.TypeLits
import Fcf (Exp, Eval)
import qualified Fcf
import Michelson.Typed
import Michelson.Typed.Haskell.Instr.Sum (IsPrimitiveValue)
import Michelson.Typed.Haskell.Value (GValueType, GenericIsoValue)
import Michelson.Untyped (FieldAnn, noAnn)
import Lorentz.Value
import Util.Type
import Util.Fcf (Over2, type (<|>), TyEqSing)
import Lorentz.EntryPoints.Helpers
import Lorentz.EntryPoints.Core
import Lorentz.TypeAnns
data EpdPlain
instance PlainEntryPointsC 'False cp => EntryPointsDerivation EpdPlain cp where
type EpdAllEntryPoints EpdPlain cp = PlainAllEntryPointsExt 'False cp
type EpdLookupEntryPoint EpdPlain cp = PlainLookupEntryPointExt 'False cp
epdNotes = plainEpdNotesExt @'False @cp
epdCall = plainEpdCallExt @'False @cp
data EpdRecursive
instance PlainEntryPointsC 'True cp => EntryPointsDerivation EpdRecursive cp where
type EpdAllEntryPoints EpdRecursive cp = PlainAllEntryPointsExt 'True cp
type EpdLookupEntryPoint EpdRecursive cp = PlainLookupEntryPointExt 'True cp
epdNotes = plainEpdNotesExt @'True @cp
epdCall = plainEpdCallExt @'True @cp
type PlainAllEntryPointsExt deep cp = AllEntryPoints deep (BuildEPTree deep cp) cp
type PlainLookupEntryPointExt deep cp = LookupEntryPoint deep (BuildEPTree deep cp) cp
plainEpdNotesExt
:: forall deep cp.
(PlainEntryPointsC deep cp, HasCallStack)
=> Notes (ToT cp)
plainEpdNotesExt = mkEntryPointsNotes @deep @(BuildEPTree deep cp) @cp
plainEpdCallExt
:: forall deep cp name.
(PlainEntryPointsC deep cp, ParameterScope (ToT cp), KnownSymbol name)
=> Label name
-> EpConstructionRes (ToT cp) (Eval (LookupEntryPoint deep (BuildEPTree deep cp) cp name))
plainEpdCallExt = mkEpLiftSequence @deep @(BuildEPTree deep cp) @cp
type PlainEntryPointsC deep cp =
( GenericIsoValue cp
, EntryPointsNotes deep (BuildEPTree deep cp) cp
, RequireSumType cp
)
data EPTree
= EPNode EPTree EPTree
| EPLeaf
type BuildEPTree deep a = GBuildEntryPointsTree deep (G.Rep a)
type family GBuildEntryPointsTree (deep :: Bool) (x :: Kind.Type -> Kind.Type)
:: EPTree where
GBuildEntryPointsTree deep (G.D1 _ x) =
GBuildEntryPointsTree deep x
GBuildEntryPointsTree deep (x G.:+: y) =
'EPNode (GBuildEntryPointsTree deep x) (GBuildEntryPointsTree deep y)
GBuildEntryPointsTree 'False (G.C1 _ _) =
'EPLeaf
GBuildEntryPointsTree 'True (G.C1 _ x) =
GBuildEntryPointsTree 'True x
GBuildEntryPointsTree deep (G.S1 _ x) =
GBuildEntryPointsTree deep x
GBuildEntryPointsTree _ G.U1 =
'EPLeaf
GBuildEntryPointsTree _ (_ G.:*: _) =
'EPLeaf
GBuildEntryPointsTree deep (G.Rec0 a) =
If (IsPrimitiveValue a)
'EPLeaf
(BuildEPTree deep a)
type EntryPointsNotes deep ep a = (Generic a, GEntryPointsNotes deep ep (G.Rep a))
mkEntryPointsNotes
:: forall deep ep a.
(EntryPointsNotes deep ep a, GenericIsoValue a, HasCallStack)
=> Notes (ToT a)
mkEntryPointsNotes = fst $ gMkEntryPointsNotes @deep @ep @(G.Rep a)
mkEpLiftSequence
:: forall deep ep a name.
( EntryPointsNotes deep ep a, ParameterScope (ToT a)
, GenericIsoValue a, KnownSymbol name
)
=> Label name
-> EpConstructionRes (ToT a) (Eval (LookupEntryPoint deep ep a name))
mkEpLiftSequence = gMkEpLiftSequence @deep @ep @(G.Rep a)
type AllEntryPoints deep ep a = GAllEntryPoints deep ep (G.Rep a)
type LookupEntryPoint deep ep a = GLookupEntryPoint deep ep (G.Rep a)
class GEntryPointsNotes (deep :: Bool) (ep :: EPTree) (x :: Kind.Type -> Kind.Type) where
type GAllEntryPoints deep ep x :: [(Symbol, Kind.Type)]
type GLookupEntryPoint deep ep x :: Symbol -> Exp (Maybe Kind.Type)
gMkEntryPointsNotes :: HasCallStack => (Notes (GValueType x), FieldAnn)
gMkEpLiftSequence
:: (KnownSymbol name, ParameterScope (GValueType x))
=> Label name
-> EpConstructionRes (GValueType x) (Eval (GLookupEntryPoint deep ep x name))
instance GEntryPointsNotes deep ep x => GEntryPointsNotes deep ep (G.D1 i x) where
type GAllEntryPoints deep ep (G.D1 i x) = GAllEntryPoints deep ep x
type GLookupEntryPoint deep ep (G.D1 i x) = GLookupEntryPoint deep ep x
gMkEntryPointsNotes = gMkEntryPointsNotes @deep @ep @x
gMkEpLiftSequence = gMkEpLiftSequence @deep @ep @x
instance (GEntryPointsNotes deep epx x, GEntryPointsNotes deep epy y) =>
GEntryPointsNotes deep ('EPNode epx epy) (x G.:+: y) where
type GAllEntryPoints deep ('EPNode epx epy) (x G.:+: y) =
GAllEntryPoints deep epx x ++ GAllEntryPoints deep epy y
type GLookupEntryPoint deep ('EPNode epx epy) (x G.:+: y) =
Over2 (<|>) (GLookupEntryPoint deep epx x) (GLookupEntryPoint deep epy y)
gMkEntryPointsNotes =
let (xnotes, xann) = gMkEntryPointsNotes @deep @epx @x
(ynotes, yann) = gMkEntryPointsNotes @deep @epy @y
in (NTOr noAnn xann yann xnotes ynotes, noAnn)
gMkEpLiftSequence label =
case sing @(GValueType (x G.:+: y)) of
STOr sl _ -> case (checkOpPresence sl, checkNestedBigMapsPresence sl) of
(OpAbsent, NestedBigMapsAbsent) ->
case gMkEpLiftSequence @deep @epx @x label of
EpConstructed liftSeq -> EpConstructed (EplWrapLeft liftSeq)
EpConstructionFailed ->
case gMkEpLiftSequence @deep @epy @y label of
EpConstructed liftSeq -> EpConstructed (EplWrapRight liftSeq)
EpConstructionFailed -> EpConstructionFailed
instance ( GHasTypeAnn x, KnownSymbol ctor
, ToT (GExtractField x) ~ GValueType x
) =>
GEntryPointsNotes 'False ep (G.C1 ('G.MetaCons ctor _1 _2) x) where
type GAllEntryPoints 'False ep (G.C1 ('G.MetaCons ctor _1 _2) x) =
'[ '(ctor, GExtractField x) ]
type GLookupEntryPoint 'False ep (G.C1 ('G.MetaCons ctor _1 _2) x) =
JustOnEq ctor (GExtractField x)
gMkEntryPointsNotes =
(gGetTypeAnn @x, ctorNameToAnn @ctor)
gMkEpLiftSequence (_ :: Label name) =
case sing @ctor %== sing @name of
STrue -> EpConstructed EplArgHere
SFalse -> EpConstructionFailed
instance ( GHasTypeAnn x, KnownSymbol ctor
, ToT (GExtractField x) ~ GValueType x
) =>
GEntryPointsNotes 'True 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) where
type GAllEntryPoints 'True 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) =
'[ '(ctor, GExtractField x) ]
type GLookupEntryPoint 'True 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) =
JustOnEq ctor (GExtractField x)
gMkEntryPointsNotes =
(gGetTypeAnn @x, ctorNameToAnn @ctor)
gMkEpLiftSequence (_ :: Label name) =
case sing @ctor %== sing @name of
STrue -> EpConstructed EplArgHere
SFalse -> EpConstructionFailed
instance (ep ~ 'EPNode epx epy, GEntryPointsNotes 'True ep x) =>
GEntryPointsNotes 'True ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) where
type GAllEntryPoints 'True ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) =
GAllEntryPoints 'True ('EPNode epx epy) x
type GLookupEntryPoint 'True ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) =
GLookupEntryPoint 'True ('EPNode epx epy) x
gMkEntryPointsNotes = gMkEntryPointsNotes @'True @ep @x
gMkEpLiftSequence = gMkEpLiftSequence @'True @ep @x
instance GEntryPointsNotes deep ep x => GEntryPointsNotes deep ep (G.S1 i x) where
type GAllEntryPoints deep ep (G.S1 i x) = GAllEntryPoints deep ep x
type GLookupEntryPoint deep ep (G.S1 i x) = GLookupEntryPoint deep ep x
gMkEntryPointsNotes = gMkEntryPointsNotes @deep @ep @x
gMkEpLiftSequence = gMkEpLiftSequence @deep @ep @x
instance (EntryPointsNotes deep ep a, GenericIsoValue a) =>
GEntryPointsNotes deep ep (G.Rec0 a) where
type GAllEntryPoints deep ep (G.Rec0 a) = AllEntryPoints deep ep a
type GLookupEntryPoint deep ep (G.Rec0 a) = LookupEntryPoint deep ep a
gMkEntryPointsNotes = (mkEntryPointsNotes @deep @ep @a, noAnn)
gMkEpLiftSequence = mkEpLiftSequence @deep @ep @a
instance GEntryPointsNotes deep 'EPLeaf G.U1 where
type GAllEntryPoints deep 'EPLeaf G.U1 = '[]
type GLookupEntryPoint deep 'EPLeaf G.U1 = Fcf.ConstFn 'Nothing
gMkEntryPointsNotes = (starNotes, noAnn)
gMkEpLiftSequence _ = EpConstructionFailed
instance Each [Typeable, SingI] [GValueType x, GValueType y] =>
GEntryPointsNotes deep 'EPLeaf (x G.:*: y) where
type GAllEntryPoints deep 'EPLeaf (x G.:*: y) = '[]
type GLookupEntryPoint deep 'EPLeaf (x G.:*: y) = Fcf.ConstFn 'Nothing
gMkEntryPointsNotes = (starNotes, noAnn)
gMkEpLiftSequence _ = EpConstructionFailed
type family JustOnEq (a :: k1) (b :: k2) :: k1 -> Exp (Maybe k2) where
JustOnEq a b =
Fcf.Flip Fcf.Guarded
'[ TyEqSing a 'Fcf.:= Fcf.Pure ('Just b)
, Fcf.Otherwise 'Fcf.:= Fcf.Pure 'Nothing
]
type family GExtractField (x :: Kind.Type -> Kind.Type) where
GExtractField (G.S1 _ x) = GExtractField x
GExtractField (G.Rec0 a) = a
GExtractField G.U1 = ()