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

-- | Common implementations of entrypoints.
module Lorentz.Entrypoints.Impl
  ( -- * Ways to implement 'ParameterHasEntrypoints'
    EpdPlain
  , EpdRecursive
  , EpdDelegate
  , EpdWithRoot

  -- * Implementation details
  , 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, ann, noAnn)
import Util.Fcf (type (<|>), Over2, TyEqSing)
import Util.Type

import Lorentz.Annotation
import Lorentz.Entrypoints.Core
import Lorentz.Entrypoints.Helpers

-- | Implementation of 'ParameterHasEntrypoints' which fits for case when
-- your contract exposes multiple entrypoints via having sum type as its
-- parameter.
--
-- In particular, each constructor would produce a homonymous entrypoint with
-- argument type equal to type of constructor field (each constructor should
-- have only one field).
-- Constructor called 'Default' will designate the default entrypoint.
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), RootAnn)
epdNotes = ((PlainEntrypointsC EpdPlain cp, HasCallStack) => Notes (ToT cp)
forall mode cp.
(PlainEntrypointsC mode cp, HasCallStack) =>
Notes (ToT cp)
plainEpdNotesExt @EpdPlain @cp, RootAnn
forall k (a :: k). Annotation a
noAnn)
  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

-- | Extension of 'EpdPlain' on parameters being defined as several nested
-- datatypes.
--
-- In particular, this will traverse sum types recursively, stopping at
-- Michelson primitives (like 'Natural') and constructors with number of
-- fields different from one.
--
-- It does not assign names to intermediate nodes of 'Or' tree, only to the very
-- leaves.
--
-- If some entrypoint arguments have custom 'IsoValue' instance, this
-- derivation way will not work. As a workaround, you can wrap your
-- argument into some primitive (e.g. ':!').
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), RootAnn)
epdNotes = ((PlainEntrypointsC EpdRecursive cp, HasCallStack) => Notes (ToT cp)
forall mode cp.
(PlainEntrypointsC mode cp, HasCallStack) =>
Notes (ToT cp)
plainEpdNotesExt @EpdRecursive @cp, RootAnn
forall k (a :: k). Annotation a
noAnn)
  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

-- | Extension of 'EpdPlain' on parameters being defined as several nested
-- datatypes.
--
-- In particular, it will traverse the immediate sum type, and require another
-- 'ParameterHasEntrypoints' for the inner complex datatypes. Only those
-- inner types are considered which are the only fields in their respective
-- constructors.
-- Inner types should not themselves declare default entrypoint, we enforce
-- this for better modularity.
-- Each top-level constructor will be treated as entrypoint even if it contains
-- a complex datatype within, in such case that would be an entrypoint
-- corresponding to intermediate node in @or@ tree.
--
-- Comparing to 'EpdRecursive' this gives you more control over where and how
-- entrypoints will be derived.
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), RootAnn)
epdNotes = ((PlainEntrypointsC EpdDelegate cp, HasCallStack) => Notes (ToT cp)
forall mode cp.
(PlainEntrypointsC mode cp, HasCallStack) =>
Notes (ToT cp)
plainEpdNotesExt @EpdDelegate @cp, RootAnn
forall k (a :: k). Annotation a
noAnn)
  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

-- | Extension of 'EpdPlain', 'EpdRecursive', and 'EpdDelegate' which allow specifying root annotation
-- for the parameters.
data EpdWithRoot (r :: Symbol) epd
instance (KnownSymbol r, PlainEntrypointsC deriv cp) => EntrypointsDerivation (EpdWithRoot r deriv) cp where
  type EpdAllEntrypoints (EpdWithRoot r deriv) cp =
    '(r, cp) ': PlainAllEntrypointsExt deriv cp
  type EpdLookupEntrypoint (EpdWithRoot r deriv) cp =
    Fcf.Case
      '[ Fcf.Is (TyEqSing r) ('Just cp)
       , Fcf.Else (PlainLookupEntrypointExt deriv cp)
       ]
  epdNotes :: (Notes (ToT cp), RootAnn)
epdNotes = ((PlainEntrypointsC deriv cp, HasCallStack) => Notes (ToT cp)
forall mode cp.
(PlainEntrypointsC mode cp, HasCallStack) =>
Notes (ToT cp)
plainEpdNotesExt @deriv @cp, Text -> RootAnn
forall k (a :: k). HasCallStack => Text -> Annotation a
ann (KnownSymbol r => Text
forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @r))
  epdCall :: Label name
-> EpConstructionRes
     (ToT cp) (Eval (EpdLookupEntrypoint (EpdWithRoot r deriv) cp name))
epdCall label :: Label name
label@(Label name
Label :: Label name) = case SingI r => Sing r
forall k (a :: k). SingI a => Sing a
sing @r Sing r -> Sing name -> Sing (r == 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 cp) (GValueType (Rep cp))
-> EpConstructionRes (GValueType (Rep cp)) ('Just cp)
forall arg (param :: T).
ParameterScope (ToT arg) =>
EpLiftSequence (ToT arg) param
-> EpConstructionRes param ('Just arg)
EpConstructed EpLiftSequence (ToT cp) (GValueType (Rep cp))
forall (arg :: T). EpLiftSequence arg arg
EplArgHere
      SFalse -> Label name
-> EpConstructionRes
     (ToT cp)
     (Eval (LookupEntrypoint deriv (BuildEPTree deriv cp) cp name))
forall mode cp (name :: Symbol).
(PlainEntrypointsC mode cp, ParameterScope (ToT cp)) =>
Label name
-> EpConstructionRes
     (ToT cp)
     (Eval (LookupEntrypoint mode (BuildEPTree mode cp) cp name))
plainEpdCallExt @deriv @cp Label name
label
  epdDescs :: Rec EpCallingDesc (EpdAllEntrypoints (EpdWithRoot r deriv) cp)
epdDescs =
    (forall (eps :: [(Symbol, *)]).
KnownSymbol r =>
Rec EpCallingDesc eps -> Rec EpCallingDesc eps
forall (ctor :: Symbol) (eps :: [(Symbol, *)]).
KnownSymbol ctor =>
Rec EpCallingDesc eps -> Rec EpCallingDesc eps
addDescStep @r (Rec EpCallingDesc '[ '(r, cp)] -> Rec EpCallingDesc '[ '(r, cp)])
-> Rec EpCallingDesc '[ '(r, cp)] -> Rec EpCallingDesc '[ '(r, cp)]
forall a b. (a -> b) -> a -> b
$
      $WEpCallingDesc :: forall arg (name :: Symbol).
Proxy arg
-> EpName -> [EpCallingStep] -> EpCallingDesc '(name, arg)
EpCallingDesc
        { epcdArg :: Proxy cp
epcdArg = Proxy cp
forall k (t :: k). Proxy t
Proxy
        , epcdEntrypoint :: EpName
epcdEntrypoint = (KnownSymbol r, HasCallStack) => EpName
forall (ctor :: Symbol). (KnownSymbol ctor, HasCallStack) => EpName
ctorNameToEp @r
        , epcdSteps :: [EpCallingStep]
epcdSteps = []
        } EpCallingDesc '(r, cp)
-> Rec EpCallingDesc '[] -> Rec EpCallingDesc '[ '(r, cp)]
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
    ) Rec EpCallingDesc '[ '(r, cp)]
-> Rec
     EpCallingDesc
     (GAllEntrypoints deriv (BuildEPTree deriv cp) (Rep cp))
-> Rec
     EpCallingDesc
     ('[ '(r, cp)]
      ++ GAllEntrypoints deriv (BuildEPTree deriv cp) (Rep cp))
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> PlainEntrypointsC deriv cp =>
Rec
  EpCallingDesc
  (GAllEntrypoints deriv (BuildEPTree deriv cp) (Rep cp))
forall mode cp.
PlainEntrypointsC mode cp =>
Rec EpCallingDesc (PlainAllEntrypointsExt mode cp)
plainEpdDescsExt @deriv @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
  )

-- | Entrypoints tree - skeleton on 'TOr' tree later used to distinguish
-- between constructors-entrypoints and constructors which consolidate
-- a whole pack of entrypoints.
data EPTree
  = EPNode EPTree EPTree
    -- ^ We are in the intermediate node and need to go deeper.
  | EPLeaf
    -- ^ We reached entrypoint argument.
  | EPDelegate
    -- ^ We reached complex parameter part and will need to ask how to process it.

-- | Build 'EPTree' by parameter type.
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)

-- | Traverses sum type and constructs 'Notes' which report
-- constructor names via field annotations.
type EntrypointsNotes mode ep a = (Generic a, GEntrypointsNotes mode ep (G.Rep a))

-- | Makes up notes with proper field annotations for given parameter.
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)

-- | Makes up a way to lift entrypoint argument to full parameter.
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)

-- | Makes up descriptions of entrypoints calling.
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)

-- | Fetches information about all entrypoints - leaves of 'Or' tree.
type AllEntrypoints mode ep a = GAllEntrypoints mode ep (G.Rep a)

-- | Fetches information about all entrypoints - leaves of 'Or' tree.
type LookupEntrypoint mode ep a = GLookupEntrypoint mode ep (G.Rep a)

-- | Generic traversal for 'EntrypointsNotes'.
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)

  {- | Returns:
    1. Notes corresponding to this level;
    2. Field annotation for this level (and which should be used one level above).
  -}
  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 ( GHasAnnotation 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 =
    ((Notes (GValueType x), FieldAnn)
-> Notes (GValueType (C1 ('MetaCons ctor _1 _2) x))
forall a b. (a, b) -> a
fst ((Notes (GValueType x), FieldAnn)
 -> Notes (GValueType (C1 ('MetaCons ctor _1 _2) x)))
-> (Notes (GValueType x), FieldAnn)
-> Notes (GValueType (C1 ('MetaCons ctor _1 _2) x))
forall a b. (a -> b) -> a -> b
$ FollowEntrypointFlag
-> GenerateFieldAnnFlag -> (Notes (GValueType x), FieldAnn)
forall (a :: * -> *).
GHasAnnotation a =>
FollowEntrypointFlag
-> GenerateFieldAnnFlag -> (Notes (GValueType a), FieldAnn)
gGetAnnotation @x FollowEntrypointFlag
FollowEntrypoint GenerateFieldAnnFlag
NotGenerateFieldAnn, (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 = ((Notes (ToT a), RootAnn) -> Notes (ToT a)
forall a b. (a, b) -> a
fst (ParameterDeclaresEntrypoints a => (Notes (ToT a), RootAnn)
forall cp.
ParameterDeclaresEntrypoints cp =>
(Notes (ToT cp), RootAnn)
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

-- Return 'Just' iff given entries of type @k1@ are equal.
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
       ]

-- Get field type under 'G.C1'.
type family GExtractField (x :: Kind.Type -> Kind.Type) where
  GExtractField (G.S1 _ x) = GExtractField x
  GExtractField (G.Rec0 a) = a
  GExtractField 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, .. }