{-# LANGUAGE UndecidableSuperClasses #-}
module Lorentz.Entrypoints.Core
( CanHaveEntrypoints
, EntrypointsDerivation (..)
, EpConstructionRes (..)
, EpCallingDesc (..)
, EpCallingStep (..)
, RequireAllUniqueEntrypoints
, ParameterHasEntrypoints (..)
, ParameterDeclaresEntrypoints
, GetParameterEpDerivation
, pepNotes
, pepCall
, pepDescs
, pepDescsWithDef
, AllParameterEntrypoints
, LookupParameterEntrypoint
, parameterEntrypointsToNotes
, GetEntrypointArg
, parameterEntrypointCall
, GetDefaultEntrypointArg
, parameterEntrypointCallDefault
, ForbidExplicitDefaultEntrypoint
, NoExplicitDefaultEntrypoint
, sepcCallRootChecked
, EntrypointRef (..)
, NiceEntrypointName
, eprName
, GetEntrypointArgCustom
, TrustEpName (..)
, HasEntrypointArg (..)
, HasDefEntrypointArg
, HasEntrypointOfType
, ParameterContainsEntrypoints
, parameterEntrypointCallCustom
, EpdNone
, (:>)
, RequireAllUniqueEntrypoints'
) where
import Data.Default (Default(..))
import Data.Type.Bool (type (&&))
import Data.Type.Equality ((:~:)(..))
import Data.Typeable (typeRep)
import Data.Vinyl (Rec(..))
import Fcf (Eval, Exp)
import Fcf qualified
import Fcf.Utils qualified as Fcf
import Fmt (pretty)
import GHC.TypeLits (CharToNat, ConsSymbol, NatToChar, UnconsSymbol, type (-), type (<=?))
import Type.Errors (DelayError, IfStuck)
import Unsafe.Coerce (unsafeCoerce)
import Morley.Michelson.Typed
import Morley.Michelson.Untyped qualified as U
import Morley.Util.Label
import Morley.Util.Type
import Morley.Util.TypeLits
import Lorentz.Annotation (FollowEntrypointFlag(..), HasAnnotation, getAnnotation)
import Lorentz.Constraints.Scopes
import Lorentz.Entrypoints.Helpers
class EntrypointsDerivation deriv cp where
type EpdAllEntrypoints deriv cp :: [(Symbol, Type)]
type EpdLookupEntrypoint deriv cp :: Symbol -> Exp (Maybe Type)
epdNotes :: (Notes (ToT cp), U.RootAnn)
epdCall
:: ParameterScope (ToT cp)
=> Label name
-> EpConstructionRes (ToT cp) (Eval (EpdLookupEntrypoint deriv cp name))
epdDescs :: Rec EpCallingDesc (EpdAllEntrypoints deriv cp)
type RequireAllUniqueEntrypoints' deriv cp =
RequireAllUnique
"entrypoint name"
(Eval (Fcf.Map Fcf.Fst $ EpdAllEntrypoints deriv cp))
type RequireAllUniqueEntrypoints cp =
RequireAllUniqueEntrypoints' (ParameterEntrypointsDerivation cp) cp
data EpConstructionRes (param :: T) (marg :: Maybe Type) where
EpConstructed
:: ParameterScope (ToT arg)
=> EpLiftSequence (ToT arg) param -> EpConstructionRes param ('Just arg)
EpConstructionFailed
:: EpConstructionRes param 'Nothing
data EpCallingDesc (info :: (Symbol, Type)) where
EpCallingDesc ::
{ forall name (name :: Symbol).
EpCallingDesc '(name, name) -> Proxy name
epcdArg :: Proxy (arg :: Type)
, forall name (name :: Symbol). EpCallingDesc '(name, name) -> EpName
epcdEntrypoint :: EpName
, forall name (name :: Symbol).
EpCallingDesc '(name, name) -> [EpCallingStep]
epcdSteps :: [EpCallingStep]
} -> EpCallingDesc '(name, arg)
deriving stock instance Show (EpCallingDesc info)
data EpCallingStep
= EpsWrapIn Text
deriving stock (Int -> EpCallingStep -> ShowS
[EpCallingStep] -> ShowS
EpCallingStep -> String
(Int -> EpCallingStep -> ShowS)
-> (EpCallingStep -> String)
-> ([EpCallingStep] -> ShowS)
-> Show EpCallingStep
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EpCallingStep -> ShowS
showsPrec :: Int -> EpCallingStep -> ShowS
$cshow :: EpCallingStep -> String
show :: EpCallingStep -> String
$cshowList :: [EpCallingStep] -> ShowS
showList :: [EpCallingStep] -> ShowS
Show, EpCallingStep -> EpCallingStep -> Bool
(EpCallingStep -> EpCallingStep -> Bool)
-> (EpCallingStep -> EpCallingStep -> Bool) -> Eq EpCallingStep
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EpCallingStep -> EpCallingStep -> Bool
== :: EpCallingStep -> EpCallingStep -> Bool
$c/= :: EpCallingStep -> EpCallingStep -> Bool
/= :: EpCallingStep -> EpCallingStep -> Bool
Eq)
class ( EntrypointsDerivation (ParameterEntrypointsDerivation cp) cp
, RequireAllUniqueEntrypoints cp
) =>
ParameterHasEntrypoints cp where
type ParameterEntrypointsDerivation cp :: Type
type ParameterDeclaresEntrypoints cp =
( If (CanHaveEntrypoints cp)
(ParameterHasEntrypoints cp)
(() :: Constraint)
, NiceParameter cp
, EntrypointsDerivation (GetParameterEpDerivation cp) cp
)
type GetParameterEpDerivation cp =
If (CanHaveEntrypoints cp)
(ParameterEntrypointsDerivation cp)
EpdNone
pepNotes :: forall cp. ParameterDeclaresEntrypoints cp => (Notes (ToT cp), U.RootAnn)
pepNotes :: forall cp.
ParameterDeclaresEntrypoints cp =>
(Notes (ToT cp), RootAnn)
pepNotes = forall {k} (deriv :: k) cp.
EntrypointsDerivation deriv cp =>
(Notes (ToT cp), RootAnn)
forall deriv cp.
EntrypointsDerivation deriv cp =>
(Notes (ToT cp), RootAnn)
epdNotes @(GetParameterEpDerivation cp) @cp
pepCall
:: forall cp name.
(ParameterDeclaresEntrypoints cp)
=> Label name
-> EpConstructionRes (ToT cp) (Eval (LookupParameterEntrypoint cp name))
pepCall :: forall cp (name :: Symbol).
ParameterDeclaresEntrypoints cp =>
Label name
-> EpConstructionRes
(ToT cp) (Eval (LookupParameterEntrypoint cp name))
pepCall = forall {k} (deriv :: k) cp (name :: Symbol).
(EntrypointsDerivation deriv cp, ParameterScope (ToT cp)) =>
Label name
-> EpConstructionRes
(ToT cp) (Eval (EpdLookupEntrypoint deriv cp name))
forall deriv cp (name :: Symbol).
(EntrypointsDerivation deriv cp, ParameterScope (ToT cp)) =>
Label name
-> EpConstructionRes
(ToT cp) (Eval (EpdLookupEntrypoint deriv cp name))
epdCall @(GetParameterEpDerivation cp) @cp
pepDescs
:: forall cp.
(ParameterDeclaresEntrypoints cp)
=> Rec EpCallingDesc (AllParameterEntrypoints cp)
pepDescs :: forall cp.
ParameterDeclaresEntrypoints cp =>
Rec EpCallingDesc (AllParameterEntrypoints cp)
pepDescs = forall {k} (deriv :: k) cp.
EntrypointsDerivation deriv cp =>
Rec EpCallingDesc (EpdAllEntrypoints deriv cp)
forall deriv cp.
EntrypointsDerivation deriv cp =>
Rec EpCallingDesc (EpdAllEntrypoints deriv cp)
epdDescs @(GetParameterEpDerivation cp) @cp
pepDescsWithDef
:: forall cp.
(ParameterDeclaresEntrypoints cp)
=> [Some1 EpCallingDesc]
pepDescsWithDef :: forall cp. ParameterDeclaresEntrypoints cp => [Some1 EpCallingDesc]
pepDescsWithDef = Rec
EpCallingDesc
(EpdAllEntrypoints
(If
(CanHaveEntrypoints cp)
(ParameterEntrypointsDerivation cp)
EpdNone)
cp)
-> [Some1 EpCallingDesc]
addDefaultIfImplicit (Rec
EpCallingDesc
(EpdAllEntrypoints
(If
(CanHaveEntrypoints cp)
(ParameterEntrypointsDerivation cp)
EpdNone)
cp)
-> [Some1 EpCallingDesc])
-> Rec
EpCallingDesc
(EpdAllEntrypoints
(If
(CanHaveEntrypoints cp)
(ParameterEntrypointsDerivation cp)
EpdNone)
cp)
-> [Some1 EpCallingDesc]
forall a b. (a -> b) -> a -> b
$ forall cp.
ParameterDeclaresEntrypoints cp =>
Rec EpCallingDesc (AllParameterEntrypoints cp)
pepDescs @cp
where
addDefaultIfImplicit :: Rec
EpCallingDesc
(EpdAllEntrypoints
(If
(CanHaveEntrypoints cp)
(ParameterEntrypointsDerivation cp)
EpdNone)
cp)
-> [Some1 EpCallingDesc]
addDefaultIfImplicit Rec
EpCallingDesc
(EpdAllEntrypoints
(If
(CanHaveEntrypoints cp)
(ParameterEntrypointsDerivation cp)
EpdNone)
cp)
descsRec =
let descs :: [Some1 EpCallingDesc]
descs = Rec
EpCallingDesc
(EpdAllEntrypoints
(If
(CanHaveEntrypoints cp)
(ParameterEntrypointsDerivation cp)
EpdNone)
cp)
-> [Some1 EpCallingDesc]
forall {k} (f :: k -> *) (l :: [k]). Rec f l -> [Some1 f]
recordToSomeList Rec
EpCallingDesc
(EpdAllEntrypoints
(If
(CanHaveEntrypoints cp)
(ParameterEntrypointsDerivation cp)
EpdNone)
cp)
descsRec
hasDef :: Bool
hasDef =
(Element [Some1 EpCallingDesc] -> Bool)
-> [Some1 EpCallingDesc] -> Bool
forall c b.
(Container c, BooleanMonoid b) =>
(Element c -> b) -> c -> b
any (\(Some1 EpCallingDesc{[EpCallingStep]
Proxy arg
EpName
epcdArg :: forall name (name :: Symbol).
EpCallingDesc '(name, name) -> Proxy name
epcdEntrypoint :: forall name (name :: Symbol). EpCallingDesc '(name, name) -> EpName
epcdSteps :: forall name (name :: Symbol).
EpCallingDesc '(name, name) -> [EpCallingStep]
epcdArg :: Proxy arg
epcdEntrypoint :: EpName
epcdSteps :: [EpCallingStep]
..}) -> EpName
epcdEntrypoint EpName -> EpName -> Bool
forall a. Eq a => a -> a -> Bool
== EpName
DefEpName) [Some1 EpCallingDesc]
descs
in if Bool
hasDef
then [Some1 EpCallingDesc]
descs
else EpCallingDesc '(Any, cp) -> Some1 EpCallingDesc
forall k (f :: k -> *) (a :: k). f a -> Some1 f
Some1 EpCallingDesc
{ epcdArg :: Proxy cp
epcdArg = forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @cp
, epcdEntrypoint :: EpName
epcdEntrypoint = EpName
DefEpName
, epcdSteps :: [EpCallingStep]
epcdSteps = []
} Some1 EpCallingDesc
-> [Some1 EpCallingDesc] -> [Some1 EpCallingDesc]
forall a. a -> [a] -> [a]
: [Some1 EpCallingDesc]
descs
type family AllParameterEntrypoints (cp :: Type)
:: [(Symbol, Type)] where
AllParameterEntrypoints cp =
EpdAllEntrypoints (GetParameterEpDerivation cp) cp
type family LookupParameterEntrypoint (cp :: Type)
:: Symbol -> Exp (Maybe Type) where
LookupParameterEntrypoint cp =
EpdLookupEntrypoint (GetParameterEpDerivation cp) cp
parameterEntrypointsToNotes
:: forall cp. ParameterDeclaresEntrypoints cp
=> ParamNotes (ToT cp)
parameterEntrypointsToNotes :: forall cp. ParameterDeclaresEntrypoints cp => ParamNotes (ToT cp)
parameterEntrypointsToNotes =
let (Notes (ToT cp)
notes, RootAnn
ra) = forall cp.
ParameterDeclaresEntrypoints cp =>
(Notes (ToT cp), RootAnn)
pepNotes @cp
in case Notes (ToT cp)
-> RootAnn -> Either ParamEpError (ParamNotes (ToT cp))
forall (t :: T).
Notes t -> RootAnn -> Either ParamEpError (ParamNotes t)
mkParamNotes Notes (ToT cp)
notes RootAnn
ra of
Right ParamNotes (ToT cp)
n -> ParamNotes (ToT cp)
n
Left ParamEpError
e -> Text -> ParamNotes (ToT cp)
forall a. HasCallStack => Text -> a
error (Text -> ParamNotes (ToT cp)) -> Text -> ParamNotes (ToT cp)
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
[ Text
"Lorentz unexpectedly compiled into contract with \
\illegal parameter declaration.\n"
, Text
"Parameter: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> TypeRep -> Text
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Proxy cp -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @cp)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n"
, Text
"Derived annotations: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Notes (ToT cp) -> Text
forall a b. (Buildable a, FromDoc b) => a -> b
pretty Notes (ToT cp)
notes Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n"
, Text
"Failure reason: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> ParamEpError -> Text
forall a b. (Buildable a, FromDoc b) => a -> b
pretty ParamEpError
e
]
parameterEntrypointCall
:: forall cp name.
ParameterDeclaresEntrypoints cp
=> Label name
-> EntrypointCall cp (GetEntrypointArg cp name)
parameterEntrypointCall :: forall cp (name :: Symbol).
ParameterDeclaresEntrypoints cp =>
Label name -> EntrypointCall cp (GetEntrypointArg cp name)
parameterEntrypointCall label :: Label name
label@Label name
Label =
case forall cp (name :: Symbol).
ParameterDeclaresEntrypoints cp =>
Label name
-> EpConstructionRes
(ToT cp) (Eval (LookupParameterEntrypoint cp name))
pepCall @cp Label name
label of
EpConstructed EpLiftSequence (ToT arg) (ToT cp)
liftSeq -> EntrypointCall
{ epcName :: EpName
epcName = forall (ctor :: Symbol). (KnownSymbol ctor, HasCallStack) => EpName
ctorNameToEp @name
, epcParamProxy :: Proxy (ToT cp)
epcParamProxy = Proxy (ToT cp)
forall {k} (t :: k). Proxy t
Proxy
, epcLiftSequence :: EpLiftSequence (ToT arg) (ToT cp)
epcLiftSequence = EpLiftSequence (ToT arg) (ToT cp)
liftSeq
}
EpConstructionRes
(ToT cp) (Eval (LookupParameterEntrypoint cp name))
EpConstructionFailed ->
Text -> EntrypointCallT (ToT cp) (ToT (TypeError ...))
forall a. HasCallStack => Text -> a
error Text
"impossible"
type GetEntrypointArg cp name = Eval
( Fcf.LiftM2
Fcf.FromMaybe
(Fcf.TError ('Text "Entrypoint not found: " ':<>: 'ShowType name ':$$:
'Text "In contract parameter `" ':<>: 'ShowType cp ':<>: 'Text "`"))
(LookupParameterEntrypoint cp name)
)
type DefaultEpName = "Default"
parameterEntrypointCallDefault
:: forall cp.
(ParameterDeclaresEntrypoints cp)
=> EntrypointCall cp (GetDefaultEntrypointArg cp)
parameterEntrypointCallDefault :: forall cp.
ParameterDeclaresEntrypoints cp =>
EntrypointCall cp (GetDefaultEntrypointArg cp)
parameterEntrypointCallDefault =
case forall cp (name :: Symbol).
ParameterDeclaresEntrypoints cp =>
Label name
-> EpConstructionRes
(ToT cp) (Eval (LookupParameterEntrypoint cp name))
pepCall @cp (forall (x :: Symbol) a. IsLabel x a => a
fromLabel @DefaultEpName) of
EpConstructed EpLiftSequence (ToT arg) (ToT cp)
liftSeq -> EntrypointCall
{ epcName :: EpName
epcName = EpName
DefEpName
, epcParamProxy :: Proxy (ToT cp)
epcParamProxy = Proxy (ToT cp)
forall {k} (t :: k). Proxy t
Proxy
, epcLiftSequence :: EpLiftSequence (ToT arg) (ToT cp)
epcLiftSequence = EpLiftSequence (ToT arg) (ToT cp)
liftSeq
}
EpConstructionRes
(ToT cp) (Eval (LookupParameterEntrypoint cp DefaultEpName))
EpConstructionFailed ->
EntrypointCall
{ epcName :: EpName
epcName = EpName
DefEpName
, epcParamProxy :: Proxy (ToT cp)
epcParamProxy = Proxy (ToT cp)
forall {k} (t :: k). Proxy t
Proxy
, epcLiftSequence :: EpLiftSequence (ToT cp) (ToT cp)
epcLiftSequence = EpLiftSequence (ToT cp) (ToT cp)
forall (arg :: T). EpLiftSequence arg arg
EplArgHere
}
type GetDefaultEntrypointArg cp = Eval
( Fcf.LiftM2
Fcf.FromMaybe
(Fcf.Pure cp)
(LookupParameterEntrypoint cp DefaultEpName)
)
type ForbidExplicitDefaultEntrypoint cp = Eval
(Fcf.LiftM3
Fcf.UnMaybe
(Fcf.Pure (Fcf.Pure (() :: Constraint)))
(Fcf.TError
('Text "Parameter used here must have no explicit \"default\" entrypoint" ':$$:
'Text "In parameter type `" ':<>: 'ShowType cp ':<>: 'Text "`"
)
)
(LookupParameterEntrypoint cp DefaultEpName)
)
type NoExplicitDefaultEntrypoint cp =
Eval (LookupParameterEntrypoint cp DefaultEpName) ~ 'Nothing
sepcCallRootChecked
:: forall cp.
(NiceParameter cp, ForbidExplicitDefaultEntrypoint cp)
=> SomeEntrypointCall cp
sepcCallRootChecked :: forall cp.
(NiceParameter cp, ForbidExplicitDefaultEntrypoint cp) =>
SomeEntrypointCall cp
sepcCallRootChecked = SomeEntrypointCallT (ToT cp)
forall (param :: T).
ParameterScope param =>
SomeEntrypointCallT param
unsafeSepcCallRoot
where
_validUsage :: Dict (ForbidExplicitDefaultEntrypoint cp)
_validUsage = forall (a :: Constraint). a => Dict a
Dict @(ForbidExplicitDefaultEntrypoint cp)
data EntrypointRef (mname :: Maybe Symbol) where
CallDefault :: EntrypointRef 'Nothing
Call :: NiceEntrypointName name => EntrypointRef ('Just name)
type UppercaseFirstChar :: Symbol -> Symbol
type family UppercaseFirstChar s where
UppercaseFirstChar s = TryUppercase (UnconsSymbol s)
type TryUppercase :: Maybe (Char, Symbol) -> Symbol
type family TryUppercase mb where
TryUppercase 'Nothing = ""
TryUppercase ('Just '(c, s)) = UppercaseChar c `ConsSymbol` s
type UppercaseChar :: Char -> Char
type family UppercaseChar c where
UppercaseChar c =
If ('a' <=? c && c <=? 'z')
(NatToChar (CharToNat c - 0x20))
c
instance (NiceEntrypointName (UppercaseFirstChar name), mname ~ 'Just (UppercaseFirstChar name))
=> IsLabel name (EntrypointRef mname) where
fromLabel :: EntrypointRef mname
fromLabel = EntrypointRef mname
EntrypointRef ('Just (TryUppercase (UnconsSymbol name)))
forall (name :: Symbol).
NiceEntrypointName name =>
EntrypointRef ('Just name)
Call
instance mname ~ 'Nothing => Default (EntrypointRef mname) where
def :: EntrypointRef mname
def = EntrypointRef mname
EntrypointRef 'Nothing
CallDefault
type NiceEntrypointName name = (KnownSymbol name, ForbidDefaultName name)
type family ForbidDefaultName (name :: Symbol) :: Constraint where
ForbidDefaultName "Default" =
TypeError ('Text "Calling `Default` entrypoint is not allowed here")
ForbidDefaultName _ = ()
eprName :: forall mname. EntrypointRef mname -> EpName
eprName :: forall (mname :: Maybe Symbol). EntrypointRef mname -> EpName
eprName = \case
EntrypointRef mname
CallDefault -> EpName
DefEpName
EntrypointRef mname
Call | (Proxy ('Just name)
_ :: Proxy ('Just name)) <- forall (t :: Maybe Symbol). Proxy t
forall {k} (t :: k). Proxy t
Proxy @mname ->
RootAnn -> Maybe EpName
epNameFromParamAnn (forall (ctor :: Symbol).
(KnownSymbol ctor, HasCallStack) =>
RootAnn
ctorNameToAnn @name)
Maybe EpName -> EpName -> EpName
forall a. Maybe a -> a -> a
?: Text -> EpName
forall a. HasCallStack => Text -> a
error Text
"Empty constructor-entrypoint name"
parameterEntrypointCallCustom
:: forall cp mname.
(ParameterDeclaresEntrypoints cp)
=> EntrypointRef mname
-> EntrypointCall cp (GetEntrypointArgCustom cp mname)
parameterEntrypointCallCustom :: forall cp (mname :: Maybe Symbol).
ParameterDeclaresEntrypoints cp =>
EntrypointRef mname
-> EntrypointCall cp (GetEntrypointArgCustom cp mname)
parameterEntrypointCallCustom = \case
EntrypointRef mname
CallDefault ->
forall cp.
ParameterDeclaresEntrypoints cp =>
EntrypointCall cp (GetDefaultEntrypointArg cp)
parameterEntrypointCallDefault @cp
EntrypointRef mname
Call | (Proxy ('Just name)
_ :: Proxy ('Just name)) <- forall (t :: Maybe Symbol). Proxy t
forall {k} (t :: k). Proxy t
Proxy @mname ->
forall cp (name :: Symbol).
ParameterDeclaresEntrypoints cp =>
Label name -> EntrypointCall cp (GetEntrypointArg cp name)
parameterEntrypointCall @cp (forall (x :: Symbol) a. IsLabel x a => a
fromLabel @name)
type family GetEntrypointArgCustom cp mname :: Type where
GetEntrypointArgCustom cp 'Nothing = GetDefaultEntrypointArg cp
GetEntrypointArgCustom cp ('Just name) = GetEntrypointArg cp name
class HasEntrypointArg cp name arg where
useHasEntrypointArg :: name -> (Dict (ParameterScope (ToT arg)), EpName)
type HasDefEntrypointArg cp defEpName defArg =
( defEpName ~ EntrypointRef 'Nothing
, HasEntrypointArg cp defEpName defArg
)
type StuckEpErrorTemplate cp constraint =
'Text "Can not look up entrypoints in type" ':$$:
'Text " " ':<>: 'ShowType cp ':$$:
'Text "The most likely reason it is ambiguous, or you need" ':$$:
'Text " " ':<>: 'ShowType constraint ':$$:
'Text "constraint"
type CheckStuckEp cp mname arg =
IfStuck (GetEntrypointArgCustom cp mname)
(DelayError (StuckEpErrorTemplate cp
(HasEntrypointArg cp (EntrypointRef mname) arg)
))
(Fcf.Pure (GetEntrypointArgCustom cp mname ~ arg))
instance
( CheckStuckEp cp mname arg
, ParameterDeclaresEntrypoints cp) =>
HasEntrypointArg cp (EntrypointRef mname) arg where
useHasEntrypointArg :: EntrypointRef mname -> (Dict (ParameterScope (ToT arg)), EpName)
useHasEntrypointArg EntrypointRef mname
epRef
| GetEntrypointArgCustom cp mname :~: arg
Refl :: GetEntrypointArgCustom cp mname :~: arg <- (Any :~: Any) -> GetEntrypointArgCustom cp mname :~: arg
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl =
case forall cp (mname :: Maybe Symbol).
ParameterDeclaresEntrypoints cp =>
EntrypointRef mname
-> EntrypointCall cp (GetEntrypointArgCustom cp mname)
parameterEntrypointCallCustom @cp EntrypointRef mname
epRef of
EntrypointCall{} -> (Dict (ParameterScope (ToT arg))
forall (a :: Constraint). a => Dict a
Dict, EntrypointRef mname -> EpName
forall (mname :: Maybe Symbol). EntrypointRef mname -> EpName
eprName EntrypointRef mname
epRef)
newtype TrustEpName = TrustEpName EpName
instance (NiceParameter arg) =>
HasEntrypointArg cp TrustEpName arg where
useHasEntrypointArg :: TrustEpName -> (Dict (ParameterScope (ToT arg)), EpName)
useHasEntrypointArg (TrustEpName EpName
epName) = (Dict (ParameterScope (ToT arg))
forall (a :: Constraint). a => Dict a
Dict, EpName
epName)
type HasEntrypointOfType param con exp
= (GetEntrypointArgCustom param ('Just con) ~ exp, ParameterDeclaresEntrypoints param)
data NamedEp = NamedEp Symbol Type
type n :> ty = 'NamedEp n ty
infixr 0 :>
type family
ParameterContainsEntrypoints param (fields :: [NamedEp]) :: Constraint
where
ParameterContainsEntrypoints _ '[] = ()
ParameterContainsEntrypoints param ((n :> ty) ': rest) =
(HasEntrypointOfType param n ty, ParameterContainsEntrypoints param rest)
data EpdNone
instance (HasAnnotation cp) => EntrypointsDerivation EpdNone cp where
type EpdAllEntrypoints EpdNone cp = '[]
type EpdLookupEntrypoint EpdNone cp = Fcf.ConstFn 'Nothing
epdNotes :: (Notes (ToT cp), RootAnn)
epdNotes = (forall a. HasAnnotation a => FollowEntrypointFlag -> Notes (ToT a)
getAnnotation @cp FollowEntrypointFlag
FollowEntrypoint, RootAnn
forall {k} (a :: k). Annotation a
U.noAnn)
epdCall :: forall (name :: Symbol).
ParameterScope (ToT cp) =>
Label name
-> EpConstructionRes
(ToT cp) (Eval (EpdLookupEntrypoint EpdNone cp name))
epdCall Label name
_ = EpConstructionRes (ToT cp) 'Nothing
EpConstructionRes
(ToT cp) (Eval (EpdLookupEntrypoint EpdNone cp name))
forall (param :: T). EpConstructionRes param 'Nothing
EpConstructionFailed
epdDescs :: Rec EpCallingDesc (EpdAllEntrypoints EpdNone cp)
epdDescs = Rec EpCallingDesc '[]
Rec EpCallingDesc (EpdAllEntrypoints EpdNone cp)
forall {u} (a :: u -> *). Rec a '[]
RNil