{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StrictData #-}
module PlutusCore.Builtin.Meaning where
import PlutusPrelude
import PlutusCore.Builtin.Elaborate
import PlutusCore.Builtin.HasConstant
import PlutusCore.Builtin.KnownKind
import PlutusCore.Builtin.KnownType
import PlutusCore.Builtin.KnownTypeAst
import PlutusCore.Builtin.Runtime
import PlutusCore.Builtin.TypeScheme
import PlutusCore.Core
import PlutusCore.Evaluation.Machine.ExBudgetStream
import PlutusCore.Evaluation.Machine.ExMemoryUsage
import PlutusCore.Name.Unique
import Data.Array
import Data.Kind qualified as GHC
import Data.Proxy
import Data.Some.GADT
import GHC.Exts (inline, lazy, oneShot)
import GHC.TypeLits
type family FoldArgs args res where
FoldArgs '[] res = res
FoldArgs (arg ': args) res = arg -> FoldArgs args res
data BuiltinMeaning val cost =
forall args res. BuiltinMeaning
(TypeScheme val args res)
~(FoldArgs args res)
(cost -> BuiltinRuntime val)
type HasMeaningIn uni val = (Typeable val, ExMemoryUsage val, HasConstantIn uni val)
class
( Typeable uni
, Typeable fun
, Bounded fun
, Enum fun
, Ix fun
, Default (BuiltinSemanticsVariant fun)
) => ToBuiltinMeaning uni fun where
type CostingPart uni fun
data BuiltinSemanticsVariant fun
toBuiltinMeaning
:: HasMeaningIn uni val
=> BuiltinSemanticsVariant fun
-> fun
-> BuiltinMeaning val (CostingPart uni fun)
withTypeSchemeOfBuiltinFunction
:: forall val fun r.
(ToBuiltinMeaning (UniOf val) fun, ExMemoryUsage val, Typeable val, HasConstant val)
=> BuiltinSemanticsVariant fun
-> fun
-> (forall args res. TypeScheme val args res -> r)
-> r
withTypeSchemeOfBuiltinFunction :: forall val fun r.
(ToBuiltinMeaning (UniOf val) fun, ExMemoryUsage val, Typeable val,
HasConstant val) =>
BuiltinSemanticsVariant fun
-> fun
-> (forall (args :: [*]) res. TypeScheme val args res -> r)
-> r
withTypeSchemeOfBuiltinFunction BuiltinSemanticsVariant fun
semVar fun
fun forall (args :: [*]) res. TypeScheme val args res -> r
k =
case BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart (UniOf val) fun)
forall val.
HasMeaningIn (UniOf val) val =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart (UniOf val) fun)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning BuiltinSemanticsVariant fun
semVar fun
fun of
BuiltinMeaning TypeScheme val args res
sch FoldArgs args res
_ CostingPart (UniOf val) fun -> BuiltinRuntime val
_ -> TypeScheme val args res -> r
forall (args :: [*]) res. TypeScheme val args res -> r
k TypeScheme val args res
sch
typeOfBuiltinFunction
:: forall uni fun. ToBuiltinMeaning uni fun
=> BuiltinSemanticsVariant fun
-> fun
-> Type TyName uni ()
typeOfBuiltinFunction :: forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> fun -> Type TyName uni ()
typeOfBuiltinFunction BuiltinSemanticsVariant fun
semVar fun
fun =
forall val fun r.
(ToBuiltinMeaning (UniOf val) fun, ExMemoryUsage val, Typeable val,
HasConstant val) =>
BuiltinSemanticsVariant fun
-> fun
-> (forall (args :: [*]) res. TypeScheme val args res -> r)
-> r
withTypeSchemeOfBuiltinFunction @(Term TyName Name uni fun ()) BuiltinSemanticsVariant fun
semVar fun
fun TypeScheme (Term TyName Name uni fun ()) args res
-> Type TyName uni ()
TypeScheme (Term TyName Name uni fun ()) args res
-> Type TyName (UniOf (Term TyName Name uni fun ())) ()
forall (args :: [*]) res.
TypeScheme (Term TyName Name uni fun ()) args res
-> Type TyName uni ()
forall val (args :: [*]) res.
TypeScheme val args res -> Type TyName (UniOf val) ()
typeSchemeToType
type GetArgs :: GHC.Type -> [GHC.Type]
type family GetArgs a where
GetArgs (a -> b) = a ': GetArgs b
GetArgs _ = '[]
class KnownMonotype val args res where
knownMonotype :: TypeScheme val args res
toMonoF
:: ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
instance (Typeable res, KnownTypeAst TyName (UniOf val) res, MakeKnown val res) =>
KnownMonotype val '[] res where
knownMonotype :: TypeScheme val '[] res
knownMonotype = TypeScheme val '[] res
forall res val.
(Typeable res, KnownTypeAst TyName (UniOf val) res,
MakeKnown val res) =>
TypeScheme val '[] res
TypeSchemeResult
toMonoF :: ReadKnownM (FoldArgs '[] res, FoldArgs '[] ExBudgetStream)
-> BuiltinRuntime val
toMonoF =
(BuiltinError -> BuiltinRuntime val)
-> ((res, ExBudgetStream) -> BuiltinRuntime val)
-> Either BuiltinError (res, ExBudgetStream)
-> BuiltinRuntime val
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
BuiltinError -> BuiltinRuntime val
forall val. BuiltinError -> BuiltinRuntime val
builtinRuntimeFailure
(\(res
x, ExBudgetStream
cost) -> ExBudgetStream
-> BuiltinResult (HeadSpine val) -> BuiltinRuntime val
forall val.
ExBudgetStream
-> BuiltinResult (HeadSpine val) -> BuiltinRuntime val
BuiltinCostedResult ExBudgetStream
cost (BuiltinResult (HeadSpine val) -> BuiltinRuntime val)
-> BuiltinResult (HeadSpine val) -> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
$ res -> BuiltinResult (HeadSpine val)
forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> BuiltinResult (HeadSpine val)
makeKnown res
x)
{-# INLINE toMonoF #-}
instance
( Typeable arg, KnownTypeAst TyName (UniOf val) arg, MakeKnown val arg, ReadKnown val arg
, KnownMonotype val args res
) => KnownMonotype val (arg ': args) res where
knownMonotype :: TypeScheme val (arg : args) res
knownMonotype = TypeScheme val args res -> TypeScheme val (arg : args) res
forall arg val (args1 :: [*]) res.
(Typeable arg, KnownTypeAst TyName (UniOf val) arg,
MakeKnown val arg, ReadKnown val arg) =>
TypeScheme val args1 res -> TypeScheme val (arg : args1) res
TypeSchemeArrow TypeScheme val args res
forall val (args :: [*]) res.
KnownMonotype val args res =>
TypeScheme val args res
knownMonotype
toMonoF :: ReadKnownM
(FoldArgs (arg : args) res, FoldArgs (arg : args) ExBudgetStream)
-> BuiltinRuntime val
toMonoF ReadKnownM
(FoldArgs (arg : args) res, FoldArgs (arg : args) ExBudgetStream)
getBoth = (val -> BuiltinRuntime val) -> BuiltinRuntime val
forall val. (val -> BuiltinRuntime val) -> BuiltinRuntime val
BuiltinExpectArgument ((val -> BuiltinRuntime val) -> BuiltinRuntime val)
-> ((val -> BuiltinRuntime val) -> val -> BuiltinRuntime val)
-> (val -> BuiltinRuntime val)
-> BuiltinRuntime val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (val -> BuiltinRuntime val) -> val -> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
oneShot ((val -> BuiltinRuntime val) -> BuiltinRuntime val)
-> (val -> BuiltinRuntime val) -> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
$ \val
arg ->
forall val (args :: [*]) res.
KnownMonotype val args res =>
ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toMonoF @val @args @res (ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val)
-> ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
$! do
(arg -> FoldArgs args res
f, arg -> FoldArgs args ExBudgetStream
exF) <- ReadKnownM
(FoldArgs (arg : args) res, FoldArgs (arg : args) ExBudgetStream)
Either
BuiltinError
(arg -> FoldArgs args res, arg -> FoldArgs args ExBudgetStream)
getBoth
arg
x <- val -> ReadKnownM arg
forall (uni :: * -> *) val a.
ReadKnownIn uni val a =>
val -> ReadKnownM a
readKnown val
arg
let !exY :: FoldArgs args ExBudgetStream
exY = arg -> FoldArgs args ExBudgetStream
exF arg
x
(FoldArgs args res, FoldArgs args ExBudgetStream)
-> ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (arg -> FoldArgs args res
f arg
x, FoldArgs args ExBudgetStream
exY)
{-# INLINE toMonoF #-}
class KnownMonotype val args res => KnownPolytype (binds :: [Some TyNameRep]) val args res where
knownPolytype :: TypeScheme val args res
toPolyF
:: ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
instance KnownMonotype val args res => KnownPolytype '[] val args res where
knownPolytype :: TypeScheme val args res
knownPolytype = TypeScheme val args res
forall val (args :: [*]) res.
KnownMonotype val args res =>
TypeScheme val args res
knownMonotype
toPolyF :: ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toPolyF = forall val (args :: [*]) res.
KnownMonotype val args res =>
ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toMonoF @val @args @res
{-# INLINE toPolyF #-}
instance (KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res) =>
KnownPolytype ('Some ('TyNameRep @kind name uniq) ': binds) val args res where
knownPolytype :: TypeScheme val args res
knownPolytype = forall (text :: Symbol) (uniq :: Nat) kind val (args :: [*]) res.
(KnownSymbol text, KnownNat uniq, KnownKind kind) =>
Proxy '(text, uniq, kind)
-> TypeScheme val args res -> TypeScheme val args res
TypeSchemeAll @name @uniq @kind Proxy '(name, uniq, kind)
forall {k} (t :: k). Proxy t
Proxy (TypeScheme val args res -> TypeScheme val args res)
-> TypeScheme val args res -> TypeScheme val args res
forall a b. (a -> b) -> a -> b
$ forall (binds :: [Some TyNameRep]) val (args :: [*]) res.
KnownPolytype binds val args res =>
TypeScheme val args res
knownPolytype @binds
toPolyF :: ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toPolyF = BuiltinRuntime val -> BuiltinRuntime val
forall val. BuiltinRuntime val -> BuiltinRuntime val
BuiltinExpectForce (BuiltinRuntime val -> BuiltinRuntime val)
-> (ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val)
-> ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (binds :: [Some TyNameRep]) val (args :: [*]) res.
KnownPolytype binds val args res =>
ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toPolyF @binds @val @args @res
{-# INLINE toPolyF #-}
type ThrowOnBothEmpty :: [Some TyNameRep] -> [GHC.Type] -> Bool -> GHC.Type -> GHC.Constraint
type family ThrowOnBothEmpty binds args isBuiltin a where
ThrowOnBothEmpty '[] '[] 'True a =
TypeError (
'Text "A built-in function must take at least one type or term argument" ':$$:
'Text "‘" ':<>: 'ShowType a ':<>: 'Text "’ is a built-in type" ':<>:
'Text " so you can embed any of its values as a constant" ':$$:
'Text "If you still want a built-in function, add a dummy ‘()’ argument"
)
ThrowOnBothEmpty '[] '[] 'False a =
TypeError (
'Text "A built-in function must take at least one type or term argument" ':$$:
'Text "To fix this error add a dummy ‘()’ argument"
)
ThrowOnBothEmpty _ _ _ _ = ()
class MakeBuiltinMeaning a val where
makeBuiltinMeaning
:: a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
instance
( uni ~ UniOf val, binds ~ ToBinds uni '[] a, args ~ GetArgs a, a ~ FoldArgs args res
, ThrowOnBothEmpty binds args (IsBuiltin uni a) a
, ElaborateFromTo uni 0 j val a, KnownPolytype binds val args res
) => MakeBuiltinMeaning a val where
makeBuiltinMeaning :: forall cost.
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning a
f cost -> FoldArgs (GetArgs a) ExBudgetStream
toExF =
TypeScheme val args res
-> FoldArgs args res
-> (cost -> BuiltinRuntime val)
-> BuiltinMeaning val cost
forall val cost (args :: [*]) res.
TypeScheme val args res
-> FoldArgs args res
-> (cost -> BuiltinRuntime val)
-> BuiltinMeaning val cost
BuiltinMeaning (forall (binds :: [Some TyNameRep]) val (args :: [*]) res.
KnownPolytype binds val args res =>
TypeScheme val args res
knownPolytype @binds @val @args @res) a
FoldArgs args res
f ((cost -> BuiltinRuntime val) -> BuiltinMeaning val cost)
-> (cost -> BuiltinRuntime val) -> BuiltinMeaning val cost
forall a b. (a -> b) -> a -> b
$ \cost
cost ->
BuiltinRuntime val -> BuiltinRuntime val
forall a. a -> a
lazy (BuiltinRuntime val -> BuiltinRuntime val)
-> BuiltinRuntime val -> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
$ case cost -> FoldArgs (GetArgs a) ExBudgetStream
toExF cost
cost of
!FoldArgs (GetArgs a) ExBudgetStream
exF -> forall (binds :: [Some TyNameRep]) val (args :: [*]) res.
KnownPolytype binds val args res =>
ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toPolyF @binds @val @args @res (ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val)
-> ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
$ (a, FoldArgs args ExBudgetStream)
-> Either BuiltinError (a, FoldArgs args ExBudgetStream)
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
f, FoldArgs args ExBudgetStream
FoldArgs (GetArgs a) ExBudgetStream
exF)
{-# INLINE makeBuiltinMeaning #-}
toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
toBuiltinRuntime :: forall cost val.
cost -> BuiltinMeaning val cost -> BuiltinRuntime val
toBuiltinRuntime cost
cost (BuiltinMeaning TypeScheme val args res
_ FoldArgs args res
_ cost -> BuiltinRuntime val
denot) = cost -> BuiltinRuntime val
denot cost
cost
{-# INLINE toBuiltinRuntime #-}
toBuiltinsRuntime
:: (cost ~ CostingPart uni fun, ToBuiltinMeaning uni fun, HasMeaningIn uni val)
=> BuiltinSemanticsVariant fun
-> cost
-> BuiltinsRuntime fun val
toBuiltinsRuntime :: forall cost (uni :: * -> *) fun val.
(cost ~ CostingPart uni fun, ToBuiltinMeaning uni fun,
HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun -> cost -> BuiltinsRuntime fun val
toBuiltinsRuntime BuiltinSemanticsVariant fun
semvar cost
cost =
BuiltinsRuntime fun val -> BuiltinsRuntime fun val
forall a. a -> a
lazy (BuiltinsRuntime fun val -> BuiltinsRuntime fun val)
-> ((fun -> BuiltinRuntime val) -> BuiltinsRuntime fun val)
-> (fun -> BuiltinRuntime val)
-> BuiltinsRuntime fun val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fun -> BuiltinRuntime val) -> BuiltinsRuntime fun val
forall fun val.
(fun -> BuiltinRuntime val) -> BuiltinsRuntime fun val
BuiltinsRuntime ((fun -> BuiltinRuntime val) -> BuiltinsRuntime fun val)
-> (fun -> BuiltinRuntime val) -> BuiltinsRuntime fun val
forall a b. (a -> b) -> a -> b
$ cost -> BuiltinMeaning val cost -> BuiltinRuntime val
forall cost val.
cost -> BuiltinMeaning val cost -> BuiltinRuntime val
toBuiltinRuntime cost
cost (BuiltinMeaning val cost -> BuiltinRuntime val)
-> (fun -> BuiltinMeaning val cost) -> fun -> BuiltinRuntime val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BuiltinSemanticsVariant fun -> fun -> BuiltinMeaning val cost)
-> BuiltinSemanticsVariant fun -> fun -> BuiltinMeaning val cost
forall a. a -> a
inline BuiltinSemanticsVariant fun -> fun -> BuiltinMeaning val cost
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
forall val.
HasMeaningIn uni val =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning BuiltinSemanticsVariant fun
semvar
{-# INLINE toBuiltinsRuntime #-}