module Lorentz.EntryPoints.Impl
(
EpdPlain
, EpdRecursive
, EpdDelegate
, PlainEntryPointsC
, EPTree (..)
, BuildEPTree
) where
import qualified Data.Kind as Kind
import Data.Singletons.Prelude (SBool(SFalse, STrue))
import Data.Singletons.Prelude.Eq ((%==))
import Data.Vinyl.Core (Rec(..), (<+>))
import Data.Vinyl.Recursive (rmap)
import Fcf (Eval, Exp)
import qualified Fcf
import qualified GHC.Generics as G
import Util.TypeLits
import Lorentz.Value
import Michelson.Typed
import Michelson.Typed.Haskell.Value (GValueType)
import Michelson.Untyped (FieldAnn, noAnn)
import Util.Fcf (type (<|>), Over2, TyEqSing)
import Util.Type
import Lorentz.EntryPoints.Core
import Lorentz.EntryPoints.Helpers
import Lorentz.TypeAnns
data EpdPlain
instance PlainEntryPointsC EpdPlain cp => EntryPointsDerivation EpdPlain cp where
type EpdAllEntryPoints EpdPlain cp = PlainAllEntryPointsExt EpdPlain cp
type EpdLookupEntryPoint EpdPlain cp = PlainLookupEntryPointExt EpdPlain cp
epdNotes :: Notes (ToT cp)
epdNotes = (PlainEntryPointsC EpdPlain cp, HasCallStack) => Notes (ToT cp)
forall mode cp.
(PlainEntryPointsC mode cp, HasCallStack) =>
Notes (ToT cp)
plainEpdNotesExt @EpdPlain @cp
epdCall :: Label name
-> EpConstructionRes
(ToT cp) (Eval (EpdLookupEntryPoint EpdPlain cp name))
epdCall = forall mode cp (name :: Symbol).
(PlainEntryPointsC mode cp, ParameterScope (ToT cp)) =>
Label name
-> EpConstructionRes
(ToT cp)
(Eval (LookupEntryPoint mode (BuildEPTree mode cp) cp name))
forall (name :: Symbol).
(PlainEntryPointsC EpdPlain cp, ParameterScope (ToT cp)) =>
Label name
-> EpConstructionRes
(ToT cp)
(Eval
(LookupEntryPoint EpdPlain (BuildEPTree EpdPlain cp) cp name))
plainEpdCallExt @EpdPlain @cp
epdDescs :: Rec EpCallingDesc (EpdAllEntryPoints EpdPlain cp)
epdDescs = PlainEntryPointsC EpdPlain cp =>
Rec EpCallingDesc (PlainAllEntryPointsExt EpdPlain cp)
forall mode cp.
PlainEntryPointsC mode cp =>
Rec EpCallingDesc (PlainAllEntryPointsExt mode cp)
plainEpdDescsExt @EpdPlain @cp
data EpdRecursive
instance PlainEntryPointsC EpdRecursive cp => EntryPointsDerivation EpdRecursive cp where
type EpdAllEntryPoints EpdRecursive cp = PlainAllEntryPointsExt EpdRecursive cp
type EpdLookupEntryPoint EpdRecursive cp = PlainLookupEntryPointExt EpdRecursive cp
epdNotes :: Notes (ToT cp)
epdNotes = (PlainEntryPointsC EpdRecursive cp, HasCallStack) => Notes (ToT cp)
forall mode cp.
(PlainEntryPointsC mode cp, HasCallStack) =>
Notes (ToT cp)
plainEpdNotesExt @EpdRecursive @cp
epdCall :: Label name
-> EpConstructionRes
(ToT cp) (Eval (EpdLookupEntryPoint EpdRecursive cp name))
epdCall = forall mode cp (name :: Symbol).
(PlainEntryPointsC mode cp, ParameterScope (ToT cp)) =>
Label name
-> EpConstructionRes
(ToT cp)
(Eval (LookupEntryPoint mode (BuildEPTree mode cp) cp name))
forall (name :: Symbol).
(PlainEntryPointsC EpdRecursive cp, ParameterScope (ToT cp)) =>
Label name
-> EpConstructionRes
(ToT cp)
(Eval
(LookupEntryPoint
EpdRecursive (BuildEPTree EpdRecursive cp) cp name))
plainEpdCallExt @EpdRecursive @cp
epdDescs :: Rec EpCallingDesc (EpdAllEntryPoints EpdRecursive cp)
epdDescs = PlainEntryPointsC EpdRecursive cp =>
Rec EpCallingDesc (PlainAllEntryPointsExt EpdRecursive cp)
forall mode cp.
PlainEntryPointsC mode cp =>
Rec EpCallingDesc (PlainAllEntryPointsExt mode cp)
plainEpdDescsExt @EpdRecursive @cp
data EpdDelegate
instance (PlainEntryPointsC EpdDelegate cp) => EntryPointsDerivation EpdDelegate cp where
type EpdAllEntryPoints EpdDelegate cp = PlainAllEntryPointsExt EpdDelegate cp
type EpdLookupEntryPoint EpdDelegate cp = PlainLookupEntryPointExt EpdDelegate cp
epdNotes :: Notes (ToT cp)
epdNotes = (PlainEntryPointsC EpdDelegate cp, HasCallStack) => Notes (ToT cp)
forall mode cp.
(PlainEntryPointsC mode cp, HasCallStack) =>
Notes (ToT cp)
plainEpdNotesExt @EpdDelegate @cp
epdCall :: Label name
-> EpConstructionRes
(ToT cp) (Eval (EpdLookupEntryPoint EpdDelegate cp name))
epdCall = forall mode cp (name :: Symbol).
(PlainEntryPointsC mode cp, ParameterScope (ToT cp)) =>
Label name
-> EpConstructionRes
(ToT cp)
(Eval (LookupEntryPoint mode (BuildEPTree mode cp) cp name))
forall (name :: Symbol).
(PlainEntryPointsC EpdDelegate cp, ParameterScope (ToT cp)) =>
Label name
-> EpConstructionRes
(ToT cp)
(Eval
(LookupEntryPoint
EpdDelegate (BuildEPTree EpdDelegate cp) cp name))
plainEpdCallExt @EpdDelegate @cp
epdDescs :: Rec EpCallingDesc (EpdAllEntryPoints EpdDelegate cp)
epdDescs = PlainEntryPointsC EpdDelegate cp =>
Rec EpCallingDesc (PlainAllEntryPointsExt EpdDelegate cp)
forall mode cp.
PlainEntryPointsC mode cp =>
Rec EpCallingDesc (PlainAllEntryPointsExt mode cp)
plainEpdDescsExt @EpdDelegate @cp
type PlainAllEntryPointsExt mode cp = AllEntryPoints mode (BuildEPTree mode cp) cp
type PlainLookupEntryPointExt mode cp = LookupEntryPoint mode (BuildEPTree mode cp) cp
plainEpdNotesExt
:: forall mode cp.
(PlainEntryPointsC mode cp, HasCallStack)
=> Notes (ToT cp)
plainEpdNotesExt :: Notes (ToT cp)
plainEpdNotesExt = (EntryPointsNotes mode (BuildEPTree mode cp) cp,
GenericIsoValue cp, HasCallStack) =>
Notes (ToT cp)
forall mode (ep :: EPTree) a.
(EntryPointsNotes mode ep a, GenericIsoValue a, HasCallStack) =>
Notes (ToT a)
mkEntryPointsNotes @mode @(BuildEPTree mode cp) @cp
plainEpdCallExt
:: forall mode cp name.
(PlainEntryPointsC mode cp, ParameterScope (ToT cp))
=> Label name
-> EpConstructionRes (ToT cp) (Eval (LookupEntryPoint mode (BuildEPTree mode cp) cp name))
plainEpdCallExt :: Label name
-> EpConstructionRes
(ToT cp)
(Eval (LookupEntryPoint mode (BuildEPTree mode cp) cp name))
plainEpdCallExt = forall mode (ep :: EPTree) a (name :: Symbol).
(EntryPointsNotes mode ep a, ParameterScope (ToT a),
GenericIsoValue a) =>
Label name
-> EpConstructionRes
(ToT a) (Eval (LookupEntryPoint mode ep a name))
forall (name :: Symbol).
(EntryPointsNotes mode (BuildEPTree mode cp) cp,
ParameterScope (ToT cp), GenericIsoValue cp) =>
Label name
-> EpConstructionRes
(ToT cp)
(Eval (LookupEntryPoint mode (BuildEPTree mode cp) cp name))
mkEpLiftSequence @mode @(BuildEPTree mode cp) @cp
plainEpdDescsExt
:: forall mode cp.
(PlainEntryPointsC mode cp)
=> Rec EpCallingDesc (PlainAllEntryPointsExt mode cp)
plainEpdDescsExt :: Rec EpCallingDesc (PlainAllEntryPointsExt mode cp)
plainEpdDescsExt = EntryPointsNotes mode (BuildEPTree mode cp) cp =>
Rec EpCallingDesc (PlainAllEntryPointsExt mode cp)
forall mode (ep :: EPTree) a.
EntryPointsNotes mode ep a =>
Rec EpCallingDesc (AllEntryPoints mode ep a)
mkEpDescs @mode @(BuildEPTree mode cp) @cp
type PlainEntryPointsC mode cp =
( GenericIsoValue cp
, EntryPointsNotes mode (BuildEPTree mode cp) cp
, RequireSumType cp
)
data EPTree
= EPNode EPTree EPTree
| EPLeaf
| EPDelegate
type BuildEPTree mode a = GBuildEntryPointsTree mode (G.Rep a)
type family GBuildEntryPointsTree (mode :: Kind.Type) (x :: Kind.Type -> Kind.Type)
:: EPTree where
GBuildEntryPointsTree mode (G.D1 _ x) =
GBuildEntryPointsTree mode x
GBuildEntryPointsTree mode (x G.:+: y) =
'EPNode (GBuildEntryPointsTree mode x) (GBuildEntryPointsTree mode y)
GBuildEntryPointsTree EpdPlain (G.C1 _ _) =
'EPLeaf
GBuildEntryPointsTree EpdRecursive (G.C1 _ x) =
GBuildEntryPointsTree EpdRecursive x
GBuildEntryPointsTree EpdDelegate (G.C1 _ (G.S1 _ (G.Rec0 _))) =
'EPDelegate
GBuildEntryPointsTree EpdDelegate (G.C1 _ _) =
'EPLeaf
GBuildEntryPointsTree mode (G.S1 _ x) =
GBuildEntryPointsTree mode x
GBuildEntryPointsTree _ G.U1 =
'EPLeaf
GBuildEntryPointsTree _ (_ G.:*: _) =
'EPLeaf
GBuildEntryPointsTree mode (G.Rec0 a) =
If (IsPrimitiveValue a)
'EPLeaf
(BuildEPTree mode a)
type EntryPointsNotes mode ep a = (Generic a, GEntryPointsNotes mode ep (G.Rep a))
mkEntryPointsNotes
:: forall mode ep a.
(EntryPointsNotes mode ep a, GenericIsoValue a, HasCallStack)
=> Notes (ToT a)
mkEntryPointsNotes :: Notes (ToT a)
mkEntryPointsNotes = (Notes (GValueType (Rep a)), FieldAnn) -> Notes (ToT a)
forall a b. (a, b) -> a
fst ((Notes (GValueType (Rep a)), FieldAnn) -> Notes (ToT a))
-> (Notes (GValueType (Rep a)), FieldAnn) -> Notes (ToT a)
forall a b. (a -> b) -> a -> b
$ (GEntryPointsNotes mode ep (Rep a), HasCallStack) =>
(Notes (GValueType (Rep a)), FieldAnn)
forall mode (ep :: EPTree) (x :: * -> *).
(GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
gMkEntryPointsNotes @mode @ep @(G.Rep a)
mkEpLiftSequence
:: forall mode ep a name.
( EntryPointsNotes mode ep a, ParameterScope (ToT a)
, GenericIsoValue a
)
=> Label name
-> EpConstructionRes (ToT a) (Eval (LookupEntryPoint mode ep a name))
mkEpLiftSequence :: Label name
-> EpConstructionRes
(ToT a) (Eval (LookupEntryPoint mode ep a name))
mkEpLiftSequence = forall (name :: Symbol).
(GEntryPointsNotes mode ep (Rep a),
ParameterScope (GValueType (Rep a))) =>
Label name
-> EpConstructionRes
(GValueType (Rep a))
(Eval (GLookupEntryPoint mode ep (Rep a) name))
forall mode (ep :: EPTree) (x :: * -> *) (name :: Symbol).
(GEntryPointsNotes mode ep x, ParameterScope (GValueType x)) =>
Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
gMkEpLiftSequence @mode @ep @(G.Rep a)
mkEpDescs
:: forall mode ep a.
(EntryPointsNotes mode ep a)
=> Rec EpCallingDesc (AllEntryPoints mode ep a)
mkEpDescs :: Rec EpCallingDesc (AllEntryPoints mode ep a)
mkEpDescs = GEntryPointsNotes mode ep (Rep a) =>
Rec EpCallingDesc (AllEntryPoints mode ep a)
forall mode (ep :: EPTree) (x :: * -> *).
GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
gMkDescs @mode @ep @(G.Rep a)
type AllEntryPoints mode ep a = GAllEntryPoints mode ep (G.Rep a)
type LookupEntryPoint mode ep a = GLookupEntryPoint mode ep (G.Rep a)
class GEntryPointsNotes (mode :: Kind.Type) (ep :: EPTree) (x :: Kind.Type -> Kind.Type) where
type GAllEntryPoints mode ep x :: [(Symbol, Kind.Type)]
type GLookupEntryPoint mode ep x :: Symbol -> Exp (Maybe Kind.Type)
gMkEntryPointsNotes :: HasCallStack => (Notes (GValueType x), FieldAnn)
gMkEpLiftSequence
:: ParameterScope (GValueType x)
=> Label name
-> EpConstructionRes (GValueType x) (Eval (GLookupEntryPoint mode ep x name))
gMkDescs
:: Rec EpCallingDesc (GAllEntryPoints mode ep x)
instance GEntryPointsNotes mode ep x => GEntryPointsNotes mode ep (G.D1 i x) where
type GAllEntryPoints mode ep (G.D1 i x) = GAllEntryPoints mode ep x
type GLookupEntryPoint mode ep (G.D1 i x) = GLookupEntryPoint mode ep x
gMkEntryPointsNotes :: (Notes (GValueType (D1 i x)), FieldAnn)
gMkEntryPointsNotes = (GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
forall mode (ep :: EPTree) (x :: * -> *).
(GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
gMkEntryPointsNotes @mode @ep @x
gMkEpLiftSequence :: Label name
-> EpConstructionRes
(GValueType (D1 i x))
(Eval (GLookupEntryPoint mode ep (D1 i x) name))
gMkEpLiftSequence = forall (name :: Symbol).
(GEntryPointsNotes mode ep x, ParameterScope (GValueType x)) =>
Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
forall mode (ep :: EPTree) (x :: * -> *) (name :: Symbol).
(GEntryPointsNotes mode ep x, ParameterScope (GValueType x)) =>
Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
gMkEpLiftSequence @mode @ep @x
gMkDescs :: Rec EpCallingDesc (GAllEntryPoints mode ep (D1 i x))
gMkDescs = GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
forall mode (ep :: EPTree) (x :: * -> *).
GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
gMkDescs @mode @ep @x
instance (GEntryPointsNotes mode epx x, GEntryPointsNotes mode epy y) =>
GEntryPointsNotes mode ('EPNode epx epy) (x G.:+: y) where
type GAllEntryPoints mode ('EPNode epx epy) (x G.:+: y) =
GAllEntryPoints mode epx x ++ GAllEntryPoints mode epy y
type GLookupEntryPoint mode ('EPNode epx epy) (x G.:+: y) =
Over2 (<|>) (GLookupEntryPoint mode epx x) (GLookupEntryPoint mode epy y)
gMkEntryPointsNotes :: (Notes (GValueType (x :+: y)), FieldAnn)
gMkEntryPointsNotes =
let (xnotes :: Notes (GValueType x)
xnotes, xann :: FieldAnn
xann) = (GEntryPointsNotes mode epx x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
forall mode (ep :: EPTree) (x :: * -> *).
(GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
gMkEntryPointsNotes @mode @epx @x
(ynotes :: Notes (GValueType y)
ynotes, yann :: FieldAnn
yann) = (GEntryPointsNotes mode epy y, HasCallStack) =>
(Notes (GValueType y), FieldAnn)
forall mode (ep :: EPTree) (x :: * -> *).
(GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
gMkEntryPointsNotes @mode @epy @y
in (TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes (GValueType x)
-> Notes (GValueType y)
-> Notes ('TOr (GValueType x) (GValueType y))
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
NTOr TypeAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
xann FieldAnn
yann Notes (GValueType x)
xnotes Notes (GValueType y)
ynotes, FieldAnn
forall k (a :: k). Annotation a
noAnn)
gMkEpLiftSequence :: Label name
-> EpConstructionRes
(GValueType (x :+: y))
(Eval (GLookupEntryPoint mode ('EPNode epx epy) (x :+: y) name))
gMkEpLiftSequence label :: Label name
label =
case SingI (GValueType (x :+: y)) => Sing (GValueType (x :+: y))
forall k (a :: k). SingI a => Sing a
sing @(GValueType (x G.:+: y)) of
STOr sl _ -> case (Sing (GValueType x) -> OpPresence (GValueType x)
forall (ty :: T). Sing ty -> OpPresence ty
checkOpPresence Sing a1
Sing (GValueType x)
sl, Sing (GValueType x) -> NestedBigMapsPresence (GValueType x)
forall (ty :: T). Sing ty -> NestedBigMapsPresence ty
checkNestedBigMapsPresence Sing a1
Sing (GValueType x)
sl) of
(OpAbsent, NestedBigMapsAbsent) ->
case Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode epx x name))
forall mode (ep :: EPTree) (x :: * -> *) (name :: Symbol).
(GEntryPointsNotes mode ep x, ParameterScope (GValueType x)) =>
Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
gMkEpLiftSequence @mode @epx @x Label name
label of
EpConstructed liftSeq :: EpLiftSequence (ToT arg) (GValueType x)
liftSeq -> EpLiftSequence (ToT arg) ('TOr (GValueType x) (GValueType y))
-> EpConstructionRes
('TOr (GValueType x) (GValueType y)) ('Just arg)
forall arg (param :: T).
ParameterScope (ToT arg) =>
EpLiftSequence (ToT arg) param
-> EpConstructionRes param ('Just arg)
EpConstructed (EpLiftSequence (ToT arg) (GValueType x)
-> EpLiftSequence (ToT arg) ('TOr (GValueType x) (GValueType y))
forall (subparam :: T) (r :: T) (arg :: T).
(KnownT subparam, KnownT r) =>
EpLiftSequence arg subparam -> EpLiftSequence arg ('TOr subparam r)
EplWrapLeft EpLiftSequence (ToT arg) (GValueType x)
liftSeq)
EpConstructionFailed ->
case Label name
-> EpConstructionRes
(GValueType y) (Eval (GLookupEntryPoint mode epy y name))
forall mode (ep :: EPTree) (x :: * -> *) (name :: Symbol).
(GEntryPointsNotes mode ep x, ParameterScope (GValueType x)) =>
Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
gMkEpLiftSequence @mode @epy @y Label name
label of
EpConstructed liftSeq :: EpLiftSequence (ToT arg) (GValueType y)
liftSeq -> EpLiftSequence (ToT arg) ('TOr (GValueType x) (GValueType y))
-> EpConstructionRes
('TOr (GValueType x) (GValueType y)) ('Just arg)
forall arg (param :: T).
ParameterScope (ToT arg) =>
EpLiftSequence (ToT arg) param
-> EpConstructionRes param ('Just arg)
EpConstructed (EpLiftSequence (ToT arg) (GValueType y)
-> EpLiftSequence (ToT arg) ('TOr (GValueType x) (GValueType y))
forall (l :: T) (subparam :: T) (arg :: T).
(KnownT l, KnownT subparam) =>
EpLiftSequence arg subparam -> EpLiftSequence arg ('TOr l subparam)
EplWrapRight EpLiftSequence (ToT arg) (GValueType y)
liftSeq)
EpConstructionFailed -> EpConstructionRes
(GValueType (x :+: y))
(Eval (GLookupEntryPoint mode ('EPNode epx epy) (x :+: y) name))
forall (param :: T). EpConstructionRes param 'Nothing
EpConstructionFailed
gMkDescs :: Rec
EpCallingDesc (GAllEntryPoints mode ('EPNode epx epy) (x :+: y))
gMkDescs =
GEntryPointsNotes mode epx x =>
Rec EpCallingDesc (GAllEntryPoints mode epx x)
forall mode (ep :: EPTree) (x :: * -> *).
GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
gMkDescs @mode @epx @x Rec EpCallingDesc (GAllEntryPoints mode epx x)
-> Rec EpCallingDesc (GAllEntryPoints mode epy y)
-> Rec
EpCallingDesc
(GAllEntryPoints mode epx x ++ GAllEntryPoints mode epy y)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> GEntryPointsNotes mode epy y =>
Rec EpCallingDesc (GAllEntryPoints mode epy y)
forall mode (ep :: EPTree) (x :: * -> *).
GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
gMkDescs @mode @epy @y
instance ( GHasTypeAnn x, KnownSymbol ctor
, ToT (GExtractField x) ~ GValueType x
) =>
GEntryPointsNotes mode 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) where
type GAllEntryPoints mode 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) =
'[ '(ctor, GExtractField x) ]
type GLookupEntryPoint mode 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) =
JustOnEq ctor (GExtractField x)
gMkEntryPointsNotes :: (Notes (GValueType (C1 ('MetaCons ctor _1 _2) x)), FieldAnn)
gMkEntryPointsNotes =
(GHasTypeAnn x => Notes (GValueType x)
forall (a :: * -> *). GHasTypeAnn a => Notes (GValueType a)
gGetTypeAnn @x, (KnownSymbol ctor, HasCallStack) => FieldAnn
forall (ctor :: Symbol).
(KnownSymbol ctor, HasCallStack) =>
FieldAnn
ctorNameToAnn @ctor)
gMkEpLiftSequence :: Label name
-> EpConstructionRes
(GValueType (C1 ('MetaCons ctor _1 _2) x))
(Eval
(GLookupEntryPoint
mode 'EPLeaf (C1 ('MetaCons ctor _1 _2) x) name))
gMkEpLiftSequence (Label name
Label :: Label name) =
case SingI ctor => Sing ctor
forall k (a :: k). SingI a => Sing a
sing @ctor Sing ctor -> Sing name -> Sing (ctor == name)
forall k (a :: k) (b :: k).
SEq k =>
Sing a -> Sing b -> Sing (a == b)
%== SingI name => Sing name
forall k (a :: k). SingI a => Sing a
sing @name of
STrue -> EpLiftSequence (ToT (GExtractField x)) (GValueType x)
-> EpConstructionRes (GValueType x) ('Just (GExtractField x))
forall arg (param :: T).
ParameterScope (ToT arg) =>
EpLiftSequence (ToT arg) param
-> EpConstructionRes param ('Just arg)
EpConstructed EpLiftSequence (ToT (GExtractField x)) (GValueType x)
forall (arg :: T). EpLiftSequence arg arg
EplArgHere
SFalse -> EpConstructionRes
(GValueType (C1 ('MetaCons ctor _1 _2) x))
(Eval
(GLookupEntryPoint
mode 'EPLeaf (C1 ('MetaCons ctor _1 _2) x) name))
forall (param :: T). EpConstructionRes param 'Nothing
EpConstructionFailed
gMkDescs :: Rec
EpCallingDesc
(GAllEntryPoints mode 'EPLeaf (C1 ('MetaCons ctor _1 _2) x))
gMkDescs = forall (eps :: [(Symbol, *)]).
KnownSymbol ctor =>
Rec EpCallingDesc eps -> Rec EpCallingDesc eps
forall (ctor :: Symbol) (eps :: [(Symbol, *)]).
KnownSymbol ctor =>
Rec EpCallingDesc eps -> Rec EpCallingDesc eps
addDescStep @ctor (Rec EpCallingDesc '[ '(ctor, GExtractField x)]
-> Rec
EpCallingDesc
(GAllEntryPoints mode 'EPLeaf (C1 ('MetaCons ctor _1 _2) x)))
-> Rec EpCallingDesc '[ '(ctor, GExtractField x)]
-> Rec
EpCallingDesc
(GAllEntryPoints mode 'EPLeaf (C1 ('MetaCons ctor _1 _2) x))
forall a b. (a -> b) -> a -> b
$
$WEpCallingDesc :: forall arg (name :: Symbol).
Proxy arg
-> EpName -> [EpCallingStep] -> EpCallingDesc '(name, arg)
EpCallingDesc
{ epcdArg :: Proxy (GExtractField x)
epcdArg = Proxy (GExtractField x)
forall k (t :: k). Proxy t
Proxy
, epcdEntrypoint :: EpName
epcdEntrypoint = (KnownSymbol ctor, HasCallStack) => EpName
forall (ctor :: Symbol). (KnownSymbol ctor, HasCallStack) => EpName
ctorNameToEp @ctor
, epcdSteps :: [EpCallingStep]
epcdSteps = []
} EpCallingDesc '(ctor, GExtractField x)
-> Rec EpCallingDesc '[]
-> Rec EpCallingDesc '[ '(ctor, GExtractField x)]
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec EpCallingDesc '[]
forall u (a :: u -> *). Rec a '[]
RNil
instance (ep ~ 'EPNode epx epy, GEntryPointsNotes mode ep x, KnownSymbol ctor) =>
GEntryPointsNotes mode ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) where
type GAllEntryPoints mode ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) =
GAllEntryPoints mode ('EPNode epx epy) x
type GLookupEntryPoint mode ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) =
GLookupEntryPoint mode ('EPNode epx epy) x
gMkEntryPointsNotes :: (Notes (GValueType (C1 ('MetaCons ctor _1 _2) x)), FieldAnn)
gMkEntryPointsNotes = (GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
forall mode (ep :: EPTree) (x :: * -> *).
(GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
gMkEntryPointsNotes @mode @ep @x
gMkEpLiftSequence :: Label name
-> EpConstructionRes
(GValueType (C1 ('MetaCons ctor _1 _2) x))
(Eval
(GLookupEntryPoint
mode ('EPNode epx epy) (C1 ('MetaCons ctor _1 _2) x) name))
gMkEpLiftSequence = forall (name :: Symbol).
(GEntryPointsNotes mode ep x, ParameterScope (GValueType x)) =>
Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
forall mode (ep :: EPTree) (x :: * -> *) (name :: Symbol).
(GEntryPointsNotes mode ep x, ParameterScope (GValueType x)) =>
Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
gMkEpLiftSequence @mode @ep @x
gMkDescs :: Rec
EpCallingDesc
(GAllEntryPoints
mode ('EPNode epx epy) (C1 ('MetaCons ctor _1 _2) x))
gMkDescs = forall (eps :: [(Symbol, *)]).
KnownSymbol ctor =>
Rec EpCallingDesc eps -> Rec EpCallingDesc eps
forall (ctor :: Symbol) (eps :: [(Symbol, *)]).
KnownSymbol ctor =>
Rec EpCallingDesc eps -> Rec EpCallingDesc eps
addDescStep @ctor (Rec EpCallingDesc (GAllEntryPoints mode ('EPNode epx epy) x)
-> Rec
EpCallingDesc
(GAllEntryPoints
mode ('EPNode epx epy) (C1 ('MetaCons ctor _1 _2) x)))
-> Rec EpCallingDesc (GAllEntryPoints mode ('EPNode epx epy) x)
-> Rec
EpCallingDesc
(GAllEntryPoints
mode ('EPNode epx epy) (C1 ('MetaCons ctor _1 _2) x))
forall a b. (a -> b) -> a -> b
$ GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
forall mode (ep :: EPTree) (x :: * -> *).
GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
gMkDescs @mode @ep @x
instance ( ep ~ 'EPDelegate, GEntryPointsNotes mode ep x
, KnownSymbol ctor, ToT (GExtractField x) ~ GValueType x
) =>
GEntryPointsNotes mode 'EPDelegate (G.C1 ('G.MetaCons ctor _1 _2) x) where
type GAllEntryPoints mode 'EPDelegate (G.C1 ('G.MetaCons ctor _1 _2) x) =
'(ctor, GExtractField x) ': GAllEntryPoints mode 'EPDelegate x
type GLookupEntryPoint mode 'EPDelegate (G.C1 ('G.MetaCons ctor _1 _2) x) =
Over2 (<|>) (JustOnEq ctor (GExtractField x)) (GLookupEntryPoint mode 'EPDelegate x)
gMkEntryPointsNotes :: (Notes (GValueType (C1 ('MetaCons ctor _1 _2) x)), FieldAnn)
gMkEntryPointsNotes =
let (notes :: Notes (GValueType x)
notes, _rootAnn :: FieldAnn
_rootAnn) = (GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
forall mode (ep :: EPTree) (x :: * -> *).
(GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
gMkEntryPointsNotes @mode @ep @x
in (Notes (GValueType x)
Notes (GValueType (C1 ('MetaCons ctor _1 _2) x))
notes, (KnownSymbol ctor, HasCallStack) => FieldAnn
forall (ctor :: Symbol).
(KnownSymbol ctor, HasCallStack) =>
FieldAnn
ctorNameToAnn @ctor)
gMkEpLiftSequence :: Label name
-> EpConstructionRes
(GValueType (C1 ('MetaCons ctor _1 _2) x))
(Eval
(GLookupEntryPoint
mode 'EPDelegate (C1 ('MetaCons ctor _1 _2) x) name))
gMkEpLiftSequence label :: Label name
label@(Label name
Label :: Label name) =
case SingI ctor => Sing ctor
forall k (a :: k). SingI a => Sing a
sing @ctor Sing ctor -> Sing name -> Sing (ctor == name)
forall k (a :: k) (b :: k).
SEq k =>
Sing a -> Sing b -> Sing (a == b)
%== SingI name => Sing name
forall k (a :: k). SingI a => Sing a
sing @name of
STrue -> EpLiftSequence (ToT (GExtractField x)) (GValueType x)
-> EpConstructionRes (GValueType x) ('Just (GExtractField x))
forall arg (param :: T).
ParameterScope (ToT arg) =>
EpLiftSequence (ToT arg) param
-> EpConstructionRes param ('Just arg)
EpConstructed EpLiftSequence (ToT (GExtractField x)) (GValueType x)
forall (arg :: T). EpLiftSequence arg arg
EplArgHere
SFalse -> Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
forall mode (ep :: EPTree) (x :: * -> *) (name :: Symbol).
(GEntryPointsNotes mode ep x, ParameterScope (GValueType x)) =>
Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
gMkEpLiftSequence @mode @ep @x Label name
label
gMkDescs :: Rec
EpCallingDesc
(GAllEntryPoints mode 'EPDelegate (C1 ('MetaCons ctor _1 _2) x))
gMkDescs = forall (eps :: [(Symbol, *)]).
KnownSymbol ctor =>
Rec EpCallingDesc eps -> Rec EpCallingDesc eps
forall (ctor :: Symbol) (eps :: [(Symbol, *)]).
KnownSymbol ctor =>
Rec EpCallingDesc eps -> Rec EpCallingDesc eps
addDescStep @ctor (Rec
EpCallingDesc
('(ctor, GExtractField x) : GAllEntryPoints mode 'EPDelegate x)
-> Rec
EpCallingDesc
(GAllEntryPoints mode 'EPDelegate (C1 ('MetaCons ctor _1 _2) x)))
-> Rec
EpCallingDesc
('(ctor, GExtractField x) : GAllEntryPoints mode 'EPDelegate x)
-> Rec
EpCallingDesc
(GAllEntryPoints mode 'EPDelegate (C1 ('MetaCons ctor _1 _2) x))
forall a b. (a -> b) -> a -> b
$
$WEpCallingDesc :: forall arg (name :: Symbol).
Proxy arg
-> EpName -> [EpCallingStep] -> EpCallingDesc '(name, arg)
EpCallingDesc
{ epcdArg :: Proxy (GExtractField x)
epcdArg = Proxy (GExtractField x)
forall k (t :: k). Proxy t
Proxy
, epcdEntrypoint :: EpName
epcdEntrypoint = (KnownSymbol ctor, HasCallStack) => EpName
forall (ctor :: Symbol). (KnownSymbol ctor, HasCallStack) => EpName
ctorNameToEp @ctor
, epcdSteps :: [EpCallingStep]
epcdSteps = []
} EpCallingDesc '(ctor, GExtractField x)
-> Rec EpCallingDesc (GAllEntryPoints mode 'EPDelegate x)
-> Rec
EpCallingDesc
('(ctor, GExtractField x) : GAllEntryPoints mode 'EPDelegate x)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
forall mode (ep :: EPTree) (x :: * -> *).
GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
gMkDescs @mode @ep @x
instance GEntryPointsNotes mode ep x => GEntryPointsNotes mode ep (G.S1 i x) where
type GAllEntryPoints mode ep (G.S1 i x) = GAllEntryPoints mode ep x
type GLookupEntryPoint mode ep (G.S1 i x) = GLookupEntryPoint mode ep x
gMkEntryPointsNotes :: (Notes (GValueType (S1 i x)), FieldAnn)
gMkEntryPointsNotes = (GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
forall mode (ep :: EPTree) (x :: * -> *).
(GEntryPointsNotes mode ep x, HasCallStack) =>
(Notes (GValueType x), FieldAnn)
gMkEntryPointsNotes @mode @ep @x
gMkEpLiftSequence :: Label name
-> EpConstructionRes
(GValueType (S1 i x))
(Eval (GLookupEntryPoint mode ep (S1 i x) name))
gMkEpLiftSequence = forall (name :: Symbol).
(GEntryPointsNotes mode ep x, ParameterScope (GValueType x)) =>
Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
forall mode (ep :: EPTree) (x :: * -> *) (name :: Symbol).
(GEntryPointsNotes mode ep x, ParameterScope (GValueType x)) =>
Label name
-> EpConstructionRes
(GValueType x) (Eval (GLookupEntryPoint mode ep x name))
gMkEpLiftSequence @mode @ep @x
gMkDescs :: Rec EpCallingDesc (GAllEntryPoints mode ep (S1 i x))
gMkDescs = GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
forall mode (ep :: EPTree) (x :: * -> *).
GEntryPointsNotes mode ep x =>
Rec EpCallingDesc (GAllEntryPoints mode ep x)
gMkDescs @mode @ep @x
instance (EntryPointsNotes EpdRecursive ep a, GenericIsoValue a) =>
GEntryPointsNotes EpdRecursive ep (G.Rec0 a) where
type GAllEntryPoints EpdRecursive ep (G.Rec0 a) = AllEntryPoints EpdRecursive ep a
type GLookupEntryPoint EpdRecursive ep (G.Rec0 a) = LookupEntryPoint EpdRecursive ep a
gMkEntryPointsNotes :: (Notes (GValueType (Rec0 a)), FieldAnn)
gMkEntryPointsNotes = ((EntryPointsNotes EpdRecursive ep a, GenericIsoValue a,
HasCallStack) =>
Notes (ToT a)
forall mode (ep :: EPTree) a.
(EntryPointsNotes mode ep a, GenericIsoValue a, HasCallStack) =>
Notes (ToT a)
mkEntryPointsNotes @EpdRecursive @ep @a, FieldAnn
forall k (a :: k). Annotation a
noAnn)
gMkEpLiftSequence :: Label name
-> EpConstructionRes
(GValueType (Rec0 a))
(Eval (GLookupEntryPoint EpdRecursive ep (Rec0 a) name))
gMkEpLiftSequence = forall mode (ep :: EPTree) a (name :: Symbol).
(EntryPointsNotes mode ep a, ParameterScope (ToT a),
GenericIsoValue a) =>
Label name
-> EpConstructionRes
(ToT a) (Eval (LookupEntryPoint mode ep a name))
forall (name :: Symbol).
(EntryPointsNotes EpdRecursive ep a, ParameterScope (ToT a),
GenericIsoValue a) =>
Label name
-> EpConstructionRes
(ToT a) (Eval (LookupEntryPoint EpdRecursive ep a name))
mkEpLiftSequence @EpdRecursive @ep @a
gMkDescs :: Rec EpCallingDesc (GAllEntryPoints EpdRecursive ep (Rec0 a))
gMkDescs = EntryPointsNotes EpdRecursive ep a =>
Rec EpCallingDesc (AllEntryPoints EpdRecursive ep a)
forall mode (ep :: EPTree) a.
EntryPointsNotes mode ep a =>
Rec EpCallingDesc (AllEntryPoints mode ep a)
mkEpDescs @EpdRecursive @ep @a
instance (ParameterDeclaresEntryPoints a) =>
GEntryPointsNotes EpdDelegate 'EPDelegate (G.Rec0 a) where
type GAllEntryPoints EpdDelegate 'EPDelegate (G.Rec0 a) = AllParameterEntryPoints a
type GLookupEntryPoint EpdDelegate 'EPDelegate (G.Rec0 a) = LookupParameterEntryPoint a
gMkEntryPointsNotes :: (Notes (GValueType (Rec0 a)), FieldAnn)
gMkEntryPointsNotes = (ParameterDeclaresEntryPoints a => Notes (ToT a)
forall cp. ParameterDeclaresEntryPoints cp => Notes (ToT cp)
pepNotes @a, FieldAnn
forall k (a :: k). Annotation a
noAnn)
gMkEpLiftSequence :: Label name
-> EpConstructionRes
(GValueType (Rec0 a))
(Eval (GLookupEntryPoint EpdDelegate 'EPDelegate (Rec0 a) name))
gMkEpLiftSequence = forall cp (name :: Symbol).
(ParameterDeclaresEntryPoints cp, ParameterScope (ToT cp)) =>
Label name
-> EpConstructionRes
(ToT cp) (Eval (LookupParameterEntryPoint cp name))
forall (name :: Symbol).
(ParameterDeclaresEntryPoints a, ParameterScope (ToT a)) =>
Label name
-> EpConstructionRes
(ToT a) (Eval (LookupParameterEntryPoint a name))
pepCall @a
gMkDescs :: Rec
EpCallingDesc (GAllEntryPoints EpdDelegate 'EPDelegate (Rec0 a))
gMkDescs = ParameterDeclaresEntryPoints a =>
Rec EpCallingDesc (AllParameterEntryPoints a)
forall cp.
ParameterDeclaresEntryPoints cp =>
Rec EpCallingDesc (AllParameterEntryPoints cp)
pepDescs @a
instance GEntryPointsNotes mode 'EPLeaf G.U1 where
type GAllEntryPoints mode 'EPLeaf G.U1 = '[]
type GLookupEntryPoint mode 'EPLeaf G.U1 = Fcf.ConstFn 'Nothing
gMkEntryPointsNotes :: (Notes (GValueType U1), FieldAnn)
gMkEntryPointsNotes = (Notes (GValueType U1)
forall (t :: T). SingI t => Notes t
starNotes, FieldAnn
forall k (a :: k). Annotation a
noAnn)
gMkEpLiftSequence :: Label name
-> EpConstructionRes
(GValueType U1) (Eval (GLookupEntryPoint mode 'EPLeaf U1 name))
gMkEpLiftSequence _ = EpConstructionRes
(GValueType U1) (Eval (GLookupEntryPoint mode 'EPLeaf U1 name))
forall (param :: T). EpConstructionRes param 'Nothing
EpConstructionFailed
gMkDescs :: Rec EpCallingDesc (GAllEntryPoints mode 'EPLeaf U1)
gMkDescs = Rec EpCallingDesc (GAllEntryPoints mode 'EPLeaf U1)
forall u (a :: u -> *). Rec a '[]
RNil
instance Each '[KnownT] [GValueType x, GValueType y] =>
GEntryPointsNotes mode 'EPLeaf (x G.:*: y) where
type GAllEntryPoints mode 'EPLeaf (x G.:*: y) = '[]
type GLookupEntryPoint mode 'EPLeaf (x G.:*: y) = Fcf.ConstFn 'Nothing
gMkEntryPointsNotes :: (Notes (GValueType (x :*: y)), FieldAnn)
gMkEntryPointsNotes = (Notes (GValueType (x :*: y))
forall (t :: T). SingI t => Notes t
starNotes, FieldAnn
forall k (a :: k). Annotation a
noAnn)
gMkEpLiftSequence :: Label name
-> EpConstructionRes
(GValueType (x :*: y))
(Eval (GLookupEntryPoint mode 'EPLeaf (x :*: y) name))
gMkEpLiftSequence _ = EpConstructionRes
(GValueType (x :*: y))
(Eval (GLookupEntryPoint mode 'EPLeaf (x :*: y) name))
forall (param :: T). EpConstructionRes param 'Nothing
EpConstructionFailed
gMkDescs :: Rec EpCallingDesc (GAllEntryPoints mode 'EPLeaf (x :*: y))
gMkDescs = Rec EpCallingDesc (GAllEntryPoints mode 'EPLeaf (x :*: y))
forall u (a :: u -> *). Rec a '[]
RNil
type family JustOnEq (a :: k1) (b :: k2) :: k1 -> Exp (Maybe k2) where
JustOnEq a b =
Fcf.Case
'[ Fcf.Is (TyEqSing a) ('Just b)
, Fcf.Any 'Nothing
]
type family (x :: Kind.Type -> Kind.Type) where
(G.S1 _ x) = GExtractField x
(G.Rec0 a) = a
G.U1 = ()
addDescStep
:: forall ctor eps.
KnownSymbol ctor
=> Rec EpCallingDesc eps -> Rec EpCallingDesc eps
addDescStep :: Rec EpCallingDesc eps -> Rec EpCallingDesc eps
addDescStep =
let step :: EpCallingStep
step = Text -> EpCallingStep
EpsWrapIn (Text -> EpCallingStep) -> Text -> EpCallingStep
forall a b. (a -> b) -> a -> b
$ KnownSymbol ctor => Text
forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @ctor
in (forall (x :: (Symbol, *)). EpCallingDesc x -> EpCallingDesc x)
-> Rec EpCallingDesc eps -> Rec EpCallingDesc eps
forall u (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap ((forall (x :: (Symbol, *)). EpCallingDesc x -> EpCallingDesc x)
-> Rec EpCallingDesc eps -> Rec EpCallingDesc eps)
-> (forall (x :: (Symbol, *)). EpCallingDesc x -> EpCallingDesc x)
-> Rec EpCallingDesc eps
-> Rec EpCallingDesc eps
forall a b. (a -> b) -> a -> b
$ \EpCallingDesc{..} ->
$WEpCallingDesc :: forall arg (name :: Symbol).
Proxy arg
-> EpName -> [EpCallingStep] -> EpCallingDesc '(name, arg)
EpCallingDesc{ epcdSteps :: [EpCallingStep]
epcdSteps = EpCallingStep
step EpCallingStep -> [EpCallingStep] -> [EpCallingStep]
forall a. a -> [a] -> [a]
: [EpCallingStep]
epcdSteps, .. }