Safe Haskell | None |
---|---|
Language | Haskell2010 |
Reexports from modules from the Builtin
folder.
Synopsis
- data TypeScheme val (args :: [Type]) res where
- TypeSchemeResult :: (KnownTypeAst (UniOf val) res, MakeKnown val res) => TypeScheme val '[] res
- TypeSchemeArrow :: (KnownTypeAst (UniOf val) arg, MakeKnown val arg, ReadKnown val arg) => TypeScheme val args res -> TypeScheme val (arg ': args) res
- TypeSchemeAll :: (KnownSymbol text, KnownNat uniq, KnownKind kind) => Proxy '(text, uniq, kind) -> TypeScheme val args res -> TypeScheme val args res
- argProxy :: TypeScheme val (arg ': args) res -> Proxy arg
- typeSchemeToType :: TypeScheme val args res -> Type TyName (UniOf val) ()
- class (uni `Everywhere` ImplementedKnownTypeAst uni, uni `Everywhere` ImplementedReadKnownIn uni, uni `Everywhere` ImplementedMakeKnownIn uni) => TestTypesFromTheUniverseAreAllKnown uni
- data Peano
- data RuntimeScheme n where
- RuntimeSchemeResult :: RuntimeScheme 'Z
- RuntimeSchemeArrow :: RuntimeScheme n -> RuntimeScheme ('S n)
- RuntimeSchemeAll :: RuntimeScheme n -> RuntimeScheme n
- type family ToRuntimeDenotationType val n where ...
- type family ToCostingType n where ...
- data BuiltinRuntime val = forall n. BuiltinRuntime (RuntimeScheme n) ~(ToRuntimeDenotationType val n) (ToCostingType n)
- noThunksInCosting :: Context -> ToCostingType n -> RuntimeScheme n -> IO (Maybe ThunkInfo)
- data UnliftingMode
- data BuiltinRuntimeOptions n val cost = BuiltinRuntimeOptions {
- _broRuntimeScheme :: RuntimeScheme n
- _broImmediateF :: ToRuntimeDenotationType val n
- _broDeferredF :: ToRuntimeDenotationType val n
- _broToExF :: cost -> ToCostingType n
- fromBuiltinRuntimeOptions :: UnliftingMode -> cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val
- newtype BuiltinsRuntime fun val = BuiltinsRuntime {
- unBuiltinRuntime :: Array fun (BuiltinRuntime val)
- lookupBuiltin :: (MonadError (ErrorWithCause err cause) m, AsMachineError err fun, Ix fun) => fun -> BuiltinsRuntime fun val -> m (BuiltinRuntime val)
- newtype Opaque val (rep :: Type) = Opaque {
- unOpaque :: val
- newtype SomeConstant uni (rep :: Type) = SomeConstant {
- unSomeConstant :: Some (ValueOf uni)
- data TyNameRep (kind :: Type) = TyNameRep Symbol Nat
- data family TyVarRep (name :: TyNameRep kind) :: kind
- data family TyAppRep (fun :: dom -> cod) (arg :: dom) :: cod
- data family TyForallRep (name :: TyNameRep kind) (a :: Type) :: Type
- type family FoldArgs args res where ...
- data BuiltinMeaning val cost = forall args res. BuiltinMeaning (TypeScheme val args res) (FoldArgs args res) (BuiltinRuntimeOptions (Length args) val cost)
- class (Bounded fun, Enum fun, Ix fun) => ToBuiltinMeaning uni fun where
- type CostingPart uni fun
- toBuiltinMeaning :: HasConstantIn uni val => fun -> BuiltinMeaning val (CostingPart uni fun)
- typeOfBuiltinFunction :: ToBuiltinMeaning uni fun => fun -> Type TyName uni ()
- type family Length xs where ...
- type family GetArgs a where ...
- class KnownMonotype val args res a | args res -> a, a -> res where
- knownMonotype :: TypeScheme val args res
- knownMonoruntime :: RuntimeScheme (Length args)
- toImmediateF :: FoldArgs args res -> ToRuntimeDenotationType val (Length args)
- toDeferredF :: ReadKnownM () (FoldArgs args res) -> ToRuntimeDenotationType val (Length args)
- class KnownMonotype val args res a => KnownPolytype (binds :: [Some TyNameRep]) val args res a | args res -> a, a -> res where
- knownPolytype :: TypeScheme val args res
- knownPolyruntime :: RuntimeScheme (Length args)
- makeBuiltinMeaning :: forall a val cost binds args res j. (binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res, ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) => a -> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
- toBuiltinRuntime :: UnliftingMode -> cost -> BuiltinMeaning val cost -> BuiltinRuntime val
- toBuiltinsRuntime :: (cost ~ CostingPart uni fun, HasConstantIn uni val, ToBuiltinMeaning uni fun) => UnliftingMode -> cost -> BuiltinsRuntime fun val
- data TyNameRep (kind :: Type) = TyNameRep Symbol Nat
- data family TyVarRep (name :: TyNameRep kind) :: kind
- data family TyAppRep (fun :: dom -> cod) (arg :: dom) :: cod
- data family TyForallRep (name :: TyNameRep kind) (a :: Type) :: Type
- data Hole
- data family RepHole x
- data family TypeHole a
- type KnownBuiltinTypeAst uni a = KnownTypeAst uni (ElaborateBuiltin a)
- class KnownTypeAst uni x where
- type family Merge xs ys :: [a] where ...
- data KnownTypeError
- throwKnownTypeErrorWithCause :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err, AsEvaluationFailure err) => ErrorWithCause KnownTypeError cause -> m void
- type KnownBuiltinTypeIn uni val a = (HasConstantIn uni val, GShow uni, GEq uni, uni `Contains` a)
- type KnownBuiltinType val a = KnownBuiltinTypeIn (UniOf val) val a
- type MakeKnownM cause = ExceptT (ErrorWithCause KnownTypeError cause) Emitter
- type ReadKnownM cause = Either (ErrorWithCause KnownTypeError cause)
- readKnownConstant :: forall val a cause. KnownBuiltinType val a => Maybe cause -> val -> ReadKnownM cause a
- class uni ~ UniOf val => MakeKnownIn uni val a where
- makeKnown :: Maybe cause -> a -> MakeKnownM cause val
- type MakeKnown val = MakeKnownIn (UniOf val) val
- class uni ~ UniOf val => ReadKnownIn uni val a where
- readKnown :: Maybe cause -> val -> ReadKnownM cause a
- type ReadKnown val = ReadKnownIn (UniOf val) val
- makeKnownRun :: MakeKnownIn uni val a => Maybe cause -> a -> (ReadKnownM cause val, DList Text)
- makeKnownOrFail :: MakeKnownIn uni val a => a -> EvaluationResult val
- readKnownSelf :: (ReadKnown val a, AsUnliftingError err, AsEvaluationFailure err) => val -> Either (ErrorWithCause err val) a
- data SingKind k where
- class KnownKind k where
- class ToKind (uni :: Type -> Type) where
- toSingKind :: uni (Esc (a :: k)) -> SingKind k
- demoteKind :: SingKind k -> Kind ()
- kindOfBuiltinType :: ToKind uni => uni (Esc a) -> Kind ()
- throwNotAConstant :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err) => Maybe cause -> m r
- class HasConstant term where
- asConstant :: AsUnliftingError err => Maybe cause -> term -> Either (ErrorWithCause err cause) (Some (ValueOf (UniOf term)))
- fromConstant :: Some (ValueOf (UniOf term)) -> term
- type HasConstantIn uni term = (UniOf term ~ uni, HasConstant term)
- module PlutusCore.Builtin.Emitter
Documentation
data TypeScheme val (args :: [Type]) res where Source #
Type schemes of primitive operations.
as
is a list of types of arguments, r
is the resulting type.
E.g. Text -> Bool -> Integer
is encoded as TypeScheme val [Text, Bool] Integer
.
TypeSchemeResult :: (KnownTypeAst (UniOf val) res, MakeKnown val res) => TypeScheme val '[] res | |
TypeSchemeArrow :: (KnownTypeAst (UniOf val) arg, MakeKnown val arg, ReadKnown val arg) => TypeScheme val args res -> TypeScheme val (arg ': args) res infixr 9 | |
TypeSchemeAll :: (KnownSymbol text, KnownNat uniq, KnownKind kind) => Proxy '(text, uniq, kind) -> TypeScheme val args res -> TypeScheme val args res |
argProxy :: TypeScheme val (arg ': args) res -> Proxy arg Source #
typeSchemeToType :: TypeScheme val args res -> Type TyName (UniOf val) () Source #
Convert a TypeScheme
to the corresponding Type
.
Basically, a map from the PHOAS representation to the FOAS one.
class (uni `Everywhere` ImplementedKnownTypeAst uni, uni `Everywhere` ImplementedReadKnownIn uni, uni `Everywhere` ImplementedMakeKnownIn uni) => TestTypesFromTheUniverseAreAllKnown uni Source #
An instance of this class not having any constraints ensures that every type (according to
Everywhere
) from the universe has 'KnownTypeAst, ReadKnownIn
and MakeKnownIn
instances.
Instances
Peano numbers. Normally called Nat
, but that is already reserved by base
.
data RuntimeScheme n where Source #
Same as TypeScheme
except this one doesn't contain any evaluation-irrelevant types stuff.
n
represents the number of term-level arguments that a builtin takes.
RuntimeSchemeResult :: RuntimeScheme 'Z | |
RuntimeSchemeArrow :: RuntimeScheme n -> RuntimeScheme ('S n) | |
RuntimeSchemeAll :: RuntimeScheme n -> RuntimeScheme n |
Instances
Eq (RuntimeScheme n) Source # | |
Defined in PlutusCore.Builtin.Runtime (==) :: RuntimeScheme n -> RuntimeScheme n -> Bool Source # (/=) :: RuntimeScheme n -> RuntimeScheme n -> Bool Source # | |
Show (RuntimeScheme n) Source # | |
Defined in PlutusCore.Builtin.Runtime | |
NFData (RuntimeScheme n) Source # | |
Defined in PlutusCore.Builtin.Runtime rnf :: RuntimeScheme n -> () Source # | |
NoThunks (RuntimeScheme n) Source # | |
Defined in PlutusCore.Builtin.Runtime noThunks :: Context -> RuntimeScheme n -> IO (Maybe ThunkInfo) wNoThunks :: Context -> RuntimeScheme n -> IO (Maybe ThunkInfo) showTypeOf :: Proxy (RuntimeScheme n) -> String |
type family ToRuntimeDenotationType val n where ... Source #
Compute the runtime denotation type of a builtin given the type of values and the number of
arguments that the builtin takes. A "runtime denotation type" is different from a regular
denotation type in that a regular one can have any ReadKnownIn
type as an argument and can
return any MakeKnownIn
type, while in a runtime one only val
can appear as the type of an
argument, as well as in the result type. This is what we get by calling readKnown
over each
argument of the denotation and calling makeKnown
over its result.
ToRuntimeDenotationType val 'Z = MakeKnownM () val | |
ToRuntimeDenotationType val ('S n) = val -> ReadKnownM () (ToRuntimeDenotationType val n) |
type family ToCostingType n where ... Source #
Compute the costing type for a builtin given the number of arguments that the builtin takes.
ToCostingType 'Z = ExBudget | |
ToCostingType ('S n) = ExMemory -> ToCostingType n |
data BuiltinRuntime val Source #
A BuiltinRuntime
represents a possibly partial builtin application.
We get an initial BuiltinRuntime
representing an empty builtin application (i.e. just the
builtin with no arguments) by instantiating (via fromBuiltinRuntimeOptions
) a
BuiltinRuntimeOptions
.
A BuiltinRuntime
contains info that is used during evaluation:
- the
RuntimeScheme
of the uninstantiated part of the builtin. I.e. initially it's the runtime scheme of the whole builtin, but applying or type-instantiating the builtin peels off the corresponding constructor from the runtime scheme - the (possibly partially instantiated) runtime denotation
- the (possibly partially instantiated) costing function
All the three are in sync in terms of partial instantiatedness due to RuntimeScheme
being a
GADT and ToRuntimeDenotationType
and ToCostingType
operating on the index of that GADT.
forall n. BuiltinRuntime (RuntimeScheme n) ~(ToRuntimeDenotationType val n) (ToCostingType n) |
Instances
Show (BuiltinRuntime (CkValue uni fun)) Source # | |
Defined in PlutusCore.Evaluation.Machine.Ck | |
Show (BuiltinRuntime (CekValue uni fun)) Source # | |
NFData (BuiltinRuntime val) Source # | |
Defined in PlutusCore.Builtin.Runtime rnf :: BuiltinRuntime val -> () Source # | |
NoThunks (BuiltinRuntime val) Source # | |
Defined in PlutusCore.Builtin.Runtime noThunks :: Context -> BuiltinRuntime val -> IO (Maybe ThunkInfo) wNoThunks :: Context -> BuiltinRuntime val -> IO (Maybe ThunkInfo) showTypeOf :: Proxy (BuiltinRuntime val) -> String |
noThunksInCosting :: Context -> ToCostingType n -> RuntimeScheme n -> IO (Maybe ThunkInfo) Source #
Check whether the given `ToCostingType n` contains thunks. The `RuntimeScheme n` is used to
refine n
.
data UnliftingMode Source #
Determines how to unlift arguments. The difference is that with UnliftingImmediate
unlifting
is performed immediately after a builtin gets the argument and so can fail immediately too, while
with deferred unlifting all arguments are unlifted upon full saturation, hence no failure can
occur until that. The former makes it much harder to specify the behaviour of builtins and
so UnliftingDeferred
is the preferred mode.
data BuiltinRuntimeOptions n val cost Source #
A BuiltinRuntimeOptions
is a precursor to BuiltinRuntime
. One gets the latter from the
former by choosing the runtime denotation of the builtin (either _broImmediateF
for immediate
unlifting or _broDeferredF
for deferred unlifting, see UnliftingMode
for details) and by
instantiating _broToExF
with a cost model to get the costing function for the builtin.
BuiltinRuntimeOptions | |
|
fromBuiltinRuntimeOptions :: UnliftingMode -> cost -> BuiltinRuntimeOptions n val cost -> BuiltinRuntime val Source #
Convert a BuiltinRuntimeOptions
to a BuiltinRuntime
given an UnliftingMode
and a cost
model.
newtype BuiltinsRuntime fun val Source #
A BuiltinRuntime
for each builtin from a set of builtins.
BuiltinsRuntime | |
|
Instances
NFData fun => NFData (BuiltinsRuntime fun val) Source # | |
Defined in PlutusCore.Builtin.Runtime rnf :: BuiltinsRuntime fun val -> () Source # | |
NoThunks (BuiltinsRuntime fun val) Source # | |
Defined in PlutusCore.Builtin.Runtime noThunks :: Context -> BuiltinsRuntime fun val -> IO (Maybe ThunkInfo) wNoThunks :: Context -> BuiltinsRuntime fun val -> IO (Maybe ThunkInfo) showTypeOf :: Proxy (BuiltinsRuntime fun val) -> String |
lookupBuiltin :: (MonadError (ErrorWithCause err cause) m, AsMachineError err fun, Ix fun) => fun -> BuiltinsRuntime fun val -> m (BuiltinRuntime val) Source #
Look up the runtime info of a built-in function during evaluation.
newtype Opaque val (rep :: Type) Source #
The denotation of a term whose PLC type is encoded in rep
(for example a type variable or
an application of a type variable). I.e. the denotation of such a term is the term itself.
This is because we have parametricity in Haskell, so we can't inspect a value whose
type is, say, a bound variable, so we never need to convert such a term from Plutus Core to
Haskell and back and instead can keep it intact.
Instances
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => Bitraversable Opaque Source # | |
Defined in PlutusCore.Builtin.Polymorphism bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Opaque a b -> f (Opaque c d) Source # | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => Bifoldable Opaque Source # | |
Defined in PlutusCore.Builtin.Polymorphism | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => Bifunctor Opaque Source # | |
uni ~ UniOf val => ReadKnownIn uni val (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.KnownType | |
uni ~ UniOf val => MakeKnownIn uni val (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.KnownType | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => Monad (Opaque val) Source # | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => Functor (Opaque val) Source # | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => MonadFail (Opaque val) Source # | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => Applicative (Opaque val) Source # | |
Defined in PlutusCore.Builtin.Polymorphism pure :: a -> Opaque val a Source # (<*>) :: Opaque val (a -> b) -> Opaque val a -> Opaque val b Source # liftA2 :: (a -> b -> c) -> Opaque val a -> Opaque val b -> Opaque val c Source # (*>) :: Opaque val a -> Opaque val b -> Opaque val b Source # (<*) :: Opaque val a -> Opaque val b -> Opaque val a Source # | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => Foldable (Opaque val) Source # | |
Defined in PlutusCore.Builtin.Polymorphism fold :: Monoid m => Opaque val m -> m Source # foldMap :: Monoid m => (a -> m) -> Opaque val a -> m Source # foldMap' :: Monoid m => (a -> m) -> Opaque val a -> m Source # foldr :: (a -> b -> b) -> b -> Opaque val a -> b Source # foldr' :: (a -> b -> b) -> b -> Opaque val a -> b Source # foldl :: (b -> a -> b) -> b -> Opaque val a -> b Source # foldl' :: (b -> a -> b) -> b -> Opaque val a -> b Source # foldr1 :: (a -> a -> a) -> Opaque val a -> a Source # foldl1 :: (a -> a -> a) -> Opaque val a -> a Source # toList :: Opaque val a -> [a] Source # null :: Opaque val a -> Bool Source # length :: Opaque val a -> Int Source # elem :: Eq a => a -> Opaque val a -> Bool Source # maximum :: Ord a => Opaque val a -> a Source # minimum :: Ord a => Opaque val a -> a Source # | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => Traversable (Opaque val) Source # | |
Defined in PlutusCore.Builtin.Polymorphism traverse :: Applicative f => (a -> f b) -> Opaque val a -> f (Opaque val b) Source # sequenceA :: Applicative f => Opaque val (f a) -> f (Opaque val a) Source # mapM :: Monad m => (a -> m b) -> Opaque val a -> m (Opaque val b) Source # sequence :: Monad m => Opaque val (m a) -> m (Opaque val a) Source # | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => MonadIO (Opaque val) Source # | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => Alternative (Opaque val) Source # | |
(TypeError NoRegularlyAppliedHkVarsMsg :: Constraint) => MonadPlus (Opaque val) Source # | |
KnownTypeAst uni rep => KnownTypeAst uni (Opaque val rep :: Type) Source # | |
(TypeError NoConstraintsErrMsg :: Constraint) => Bounded (Opaque val rep) Source # | |
(TypeError NoConstraintsErrMsg :: Constraint) => Enum (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism succ :: Opaque val rep -> Opaque val rep Source # pred :: Opaque val rep -> Opaque val rep Source # toEnum :: Int -> Opaque val rep Source # fromEnum :: Opaque val rep -> Int Source # enumFrom :: Opaque val rep -> [Opaque val rep] Source # enumFromThen :: Opaque val rep -> Opaque val rep -> [Opaque val rep] Source # enumFromTo :: Opaque val rep -> Opaque val rep -> [Opaque val rep] Source # enumFromThenTo :: Opaque val rep -> Opaque val rep -> Opaque val rep -> [Opaque val rep] Source # | |
(TypeError NoConstraintsErrMsg :: Constraint) => Eq (Opaque val rep) Source # | |
(TypeError NoConstraintsErrMsg :: Constraint) => Integral (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism quot :: Opaque val rep -> Opaque val rep -> Opaque val rep Source # rem :: Opaque val rep -> Opaque val rep -> Opaque val rep Source # div :: Opaque val rep -> Opaque val rep -> Opaque val rep Source # mod :: Opaque val rep -> Opaque val rep -> Opaque val rep Source # quotRem :: Opaque val rep -> Opaque val rep -> (Opaque val rep, Opaque val rep) Source # divMod :: Opaque val rep -> Opaque val rep -> (Opaque val rep, Opaque val rep) Source # | |
(TypeError NoConstraintsErrMsg :: Constraint) => Num (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism (+) :: Opaque val rep -> Opaque val rep -> Opaque val rep Source # (-) :: Opaque val rep -> Opaque val rep -> Opaque val rep Source # (*) :: Opaque val rep -> Opaque val rep -> Opaque val rep Source # negate :: Opaque val rep -> Opaque val rep Source # abs :: Opaque val rep -> Opaque val rep Source # signum :: Opaque val rep -> Opaque val rep Source # fromInteger :: Integer -> Opaque val rep Source # | |
(TypeError NoConstraintsErrMsg :: Constraint) => Ord (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism compare :: Opaque val rep -> Opaque val rep -> Ordering Source # (<) :: Opaque val rep -> Opaque val rep -> Bool Source # (<=) :: Opaque val rep -> Opaque val rep -> Bool Source # (>) :: Opaque val rep -> Opaque val rep -> Bool Source # (>=) :: Opaque val rep -> Opaque val rep -> Bool Source # max :: Opaque val rep -> Opaque val rep -> Opaque val rep Source # min :: Opaque val rep -> Opaque val rep -> Opaque val rep Source # | |
(TypeError NoConstraintsErrMsg :: Constraint) => Real (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism toRational :: Opaque val rep -> Rational Source # | |
(TypeError NoConstraintsErrMsg :: Constraint) => Ix (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism range :: (Opaque val rep, Opaque val rep) -> [Opaque val rep] Source # index :: (Opaque val rep, Opaque val rep) -> Opaque val rep -> Int Source # unsafeIndex :: (Opaque val rep, Opaque val rep) -> Opaque val rep -> Int Source # inRange :: (Opaque val rep, Opaque val rep) -> Opaque val rep -> Bool Source # rangeSize :: (Opaque val rep, Opaque val rep) -> Int Source # unsafeRangeSize :: (Opaque val rep, Opaque val rep) -> Int Source # | |
(TypeError NoConstraintsErrMsg :: Constraint) => Semigroup (Opaque val rep) Source # | |
(TypeError NoConstraintsErrMsg :: Constraint) => Monoid (Opaque val rep) Source # | |
Pretty val => Pretty (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism | |
HasConstant val => HasConstant (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism asConstant :: AsUnliftingError err => Maybe cause -> Opaque val rep -> Either (ErrorWithCause err cause) (Some (ValueOf (UniOf (Opaque val rep)))) Source # fromConstant :: Some (ValueOf (UniOf (Opaque val rep))) -> Opaque val rep Source # | |
type ToHoles (Opaque val rep :: Type) Source # | |
type ToBinds (Opaque val rep :: Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
type UniOf (Opaque val rep) Source # | |
Defined in PlutusCore.Builtin.Polymorphism |
newtype SomeConstant uni (rep :: Type) Source #
For unlifting from the Constant
constructor when the stored value is of a monomorphic
built-in type
The rep
parameter specifies how the type looks on the PLC side (i.e. just like with
Opaque val rep
).
SomeConstant | |
|
Instances
HasConstantIn uni val => ReadKnownIn uni val (SomeConstant uni rep) Source # | |
Defined in PlutusCore.Builtin.KnownType readKnown :: Maybe cause -> val -> ReadKnownM cause (SomeConstant uni rep) Source # | |
HasConstantIn uni val => MakeKnownIn uni val (SomeConstant uni rep) Source # | |
Defined in PlutusCore.Builtin.KnownType makeKnown :: Maybe cause -> SomeConstant uni rep -> MakeKnownM cause val Source # | |
KnownTypeAst uni rep => KnownTypeAst uni (SomeConstant uni rep :: Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst type ToHoles (SomeConstant uni rep) :: [Hole] Source # type ToBinds (SomeConstant uni rep) :: [Some TyNameRep] Source # | |
type ToHoles (SomeConstant uni rep :: Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
type ToBinds (SomeConstant uni rep :: Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst |
data TyNameRep (kind :: Type) Source #
Representation of a type variable: its name and unique and an implicit kind.
Instances
KnownMonotype val args res a => KnownPolytype ('[] :: [Some TyNameRep]) val args res (a :: k) Source # | Once we've run out of type-level arguments, we start handling term-level ones. |
Defined in PlutusCore.Builtin.Meaning knownPolytype :: TypeScheme val args res Source # knownPolyruntime :: RuntimeScheme (Length args) Source # | |
(KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res a) => KnownPolytype ('Some ('TyNameRep name uniq :: TyNameRep kind) ': binds) val args res (a :: k) Source # | Every type-level argument becomes a |
Defined in PlutusCore.Builtin.Meaning knownPolytype :: TypeScheme val args res Source # knownPolyruntime :: RuntimeScheme (Length args) Source # | |
(TypeError NoStandalonePolymorphicDataErrMsg :: Constraint) => Contains uni (TyVarRep :: TyNameRep kind -> kind) Source # | |
data family TyVarRep (name :: TyNameRep kind) :: kind Source #
Representation of an intrinsically-kinded type variable: a name.
Instances
(name ~ ('TyNameRep text uniq :: TyNameRep a), KnownSymbol text, KnownNat uniq) => KnownTypeAst uni (TyVarRep name :: a) Source # | |
(TypeError NoStandalonePolymorphicDataErrMsg :: Constraint) => Contains uni (TyVarRep :: TyNameRep kind -> kind) Source # | |
type ToHoles (TyVarRep name :: a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
type ToBinds (TyVarRep name :: a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst |
data family TyAppRep (fun :: dom -> cod) (arg :: dom) :: cod Source #
Representation of an intrinsically-kinded type application: a function and an argument.
Instances
(KnownTypeAst uni fun, KnownTypeAst uni arg) => KnownTypeAst uni (TyAppRep fun arg :: a) Source # | |
type ToHoles (TyAppRep fun arg :: a) Source # | |
type ToBinds (TyAppRep fun arg :: a) Source # | |
data family TyForallRep (name :: TyNameRep kind) (a :: Type) :: Type Source #
Representation of of an intrinsically-kinded universal quantifier: a bound name and a body.
Instances
(name ~ ('TyNameRep text uniq :: TyNameRep kind), KnownSymbol text, KnownNat uniq, KnownKind kind, KnownTypeAst uni a) => KnownTypeAst uni (TyForallRep name a :: Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst type ToHoles (TyForallRep name a) :: [Hole] Source # type ToBinds (TyForallRep name a) :: [Some TyNameRep] Source # | |
type ToHoles (TyForallRep name a :: Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
type ToBinds (TyForallRep name a :: Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst |
type family FoldArgs args res where ... Source #
Turn a list of Haskell types args
into a functional type ending in res
.
>>>
:set -XDataKinds
>>>
:kind! FoldArgs [Text, Bool] Integer
FoldArgs [Text, Bool] Integer :: * = Text -> Bool -> Integer
data BuiltinMeaning val cost Source #
The meaning of a built-in function consists of its type represented as a TypeScheme
,
its Haskell denotation and a costing function (both in uninstantiated form).
The TypeScheme
of a built-in function is used for
- computing the PLC type of the function to be used during type checking
- checking equality of the expected type of an argument of a builtin and the actual one during evaluation, so that we can avoid unsafe-coercing
A costing function for a built-in function is computed from a cost model for all built-in
functions from a certain set, hence the cost
parameter.
forall args res. BuiltinMeaning (TypeScheme val args res) (FoldArgs args res) (BuiltinRuntimeOptions (Length args) val cost) |
class (Bounded fun, Enum fun, Ix fun) => ToBuiltinMeaning uni fun where Source #
A type class for "each function from a set of built-in functions has a BuiltinMeaning
".
type CostingPart uni fun Source #
The cost
part of BuiltinMeaning
.
toBuiltinMeaning :: HasConstantIn uni val => fun -> BuiltinMeaning val (CostingPart uni fun) Source #
Get the BuiltinMeaning
of a built-in function.
Instances
uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun Source # | |
Defined in PlutusCore.Default.Builtins type CostingPart uni DefaultFun Source # toBuiltinMeaning :: HasConstantIn uni val => DefaultFun -> BuiltinMeaning val (CostingPart uni DefaultFun) Source # | |
uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun Source # | |
Defined in PlutusCore.Examples.Builtins type CostingPart uni ExtensionFun Source # toBuiltinMeaning :: HasConstantIn uni val => ExtensionFun -> BuiltinMeaning val (CostingPart uni ExtensionFun) Source # | |
(ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2) => ToBuiltinMeaning uni (Either fun1 fun2) Source # | |
Defined in PlutusCore.Examples.Builtins type CostingPart uni (Either fun1 fun2) Source # toBuiltinMeaning :: HasConstantIn uni val => Either fun1 fun2 -> BuiltinMeaning val (CostingPart uni (Either fun1 fun2)) Source # |
typeOfBuiltinFunction :: ToBuiltinMeaning uni fun => fun -> Type TyName uni () Source #
Get the type of a built-in function.
class KnownMonotype val args res a | args res -> a, a -> res where Source #
A class that allows us to derive a monotype for a builtin.
We could've easily computed a RuntimeScheme
from a TypeScheme
but not statically (due to
unfolding not working for recursive functions and TypeScheme
is recursive, i.e. the conversion
can only be a recursive function), and so it would cause us to retain a lot of
evaluation-irrelevant stuff in the constructors of TypeScheme
, which makes it much harder to
read the Core. Technically speaking, we could convert a TypeScheme
to a RuntimeScheme
statically if we changed the definition of TypeScheme
and made it a singleton, but then the
conversion function would have to become a class anyway and we'd just replicate what we have here,
except in a much more complicated way.
It's also more efficient to generate RuntimeScheme
s directly, but that shouldn't really matter, -- given that they computed only once and cached afterwards.
Similarly, we could've computed toImmediateF
and toDeferredF
from a TypeScheme
but not
statically again, and that would break inlining and basically all the optimization.
knownMonotype :: TypeScheme val args res Source #
knownMonoruntime :: RuntimeScheme (Length args) Source #
toImmediateF :: FoldArgs args res -> ToRuntimeDenotationType val (Length args) Source #
Convert the denotation of a builtin to its runtime counterpart with immediate unlifting.
toDeferredF :: ReadKnownM () (FoldArgs args res) -> ToRuntimeDenotationType val (Length args) Source #
Convert the denotation of a builtin to its runtime counterpart with deferred unlifting.
The argument is in ReadKnownM
, because that's what deferred unlifting amounts to:
passing the action returning the builtin application around until full saturation, which is
when the action actually gets run.
Instances
class KnownMonotype val args res a => KnownPolytype (binds :: [Some TyNameRep]) val args res a | args res -> a, a -> res where Source #
A class that allows us to derive a polytype for a builtin.
knownPolytype :: TypeScheme val args res Source #
knownPolyruntime :: RuntimeScheme (Length args) Source #
Instances
KnownMonotype val args res a => KnownPolytype ('[] :: [Some TyNameRep]) val args res (a :: k) Source # | Once we've run out of type-level arguments, we start handling term-level ones. |
Defined in PlutusCore.Builtin.Meaning knownPolytype :: TypeScheme val args res Source # knownPolyruntime :: RuntimeScheme (Length args) Source # | |
(KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res a) => KnownPolytype ('Some ('TyNameRep name uniq :: TyNameRep kind) ': binds) val args res (a :: k) Source # | Every type-level argument becomes a |
Defined in PlutusCore.Builtin.Meaning knownPolytype :: TypeScheme val args res Source # knownPolyruntime :: RuntimeScheme (Length args) Source # |
makeBuiltinMeaning :: forall a val cost binds args res j. (binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res, ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) => a -> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost Source #
Construct the meaning for a built-in function by automatically deriving its
TypeScheme
, given
- the denotation of the builtin
- an uninstantiated costing function
toBuiltinRuntime :: UnliftingMode -> cost -> BuiltinMeaning val cost -> BuiltinRuntime val Source #
Convert a BuiltinMeaning
to a BuiltinRuntime
given an UnliftingMode
and a cost model.
toBuiltinsRuntime :: (cost ~ CostingPart uni fun, HasConstantIn uni val, ToBuiltinMeaning uni fun) => UnliftingMode -> cost -> BuiltinsRuntime fun val Source #
Calculate runtime info for all built-in functions given denotations of builtins and a cost model.
data TyNameRep (kind :: Type) Source #
Representation of a type variable: its name and unique and an implicit kind.
Instances
KnownMonotype val args res a => KnownPolytype ('[] :: [Some TyNameRep]) val args res (a :: k) Source # | Once we've run out of type-level arguments, we start handling term-level ones. |
Defined in PlutusCore.Builtin.Meaning knownPolytype :: TypeScheme val args res Source # knownPolyruntime :: RuntimeScheme (Length args) Source # | |
(KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res a) => KnownPolytype ('Some ('TyNameRep name uniq :: TyNameRep kind) ': binds) val args res (a :: k) Source # | Every type-level argument becomes a |
Defined in PlutusCore.Builtin.Meaning knownPolytype :: TypeScheme val args res Source # knownPolyruntime :: RuntimeScheme (Length args) Source # | |
(TypeError NoStandalonePolymorphicDataErrMsg :: Constraint) => Contains uni (TyVarRep :: TyNameRep kind -> kind) Source # | |
data family TyVarRep (name :: TyNameRep kind) :: kind Source #
Representation of an intrinsically-kinded type variable: a name.
Instances
(name ~ ('TyNameRep text uniq :: TyNameRep a), KnownSymbol text, KnownNat uniq) => KnownTypeAst uni (TyVarRep name :: a) Source # | |
(TypeError NoStandalonePolymorphicDataErrMsg :: Constraint) => Contains uni (TyVarRep :: TyNameRep kind -> kind) Source # | |
type ToHoles (TyVarRep name :: a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
type ToBinds (TyVarRep name :: a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst |
data family TyAppRep (fun :: dom -> cod) (arg :: dom) :: cod Source #
Representation of an intrinsically-kinded type application: a function and an argument.
Instances
(KnownTypeAst uni fun, KnownTypeAst uni arg) => KnownTypeAst uni (TyAppRep fun arg :: a) Source # | |
type ToHoles (TyAppRep fun arg :: a) Source # | |
type ToBinds (TyAppRep fun arg :: a) Source # | |
data family TyForallRep (name :: TyNameRep kind) (a :: Type) :: Type Source #
Representation of of an intrinsically-kinded universal quantifier: a bound name and a body.
Instances
(name ~ ('TyNameRep text uniq :: TyNameRep kind), KnownSymbol text, KnownNat uniq, KnownKind kind, KnownTypeAst uni a) => KnownTypeAst uni (TyForallRep name a :: Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst type ToHoles (TyForallRep name a) :: [Hole] Source # type ToBinds (TyForallRep name a) :: [Some TyNameRep] Source # | |
type ToHoles (TyForallRep name a :: Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
type ToBinds (TyForallRep name a :: Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst |
type KnownBuiltinTypeAst uni a = KnownTypeAst uni (ElaborateBuiltin a) Source #
A constraint for "a
is a KnownTypeAst
by means of being included in uni
".
class KnownTypeAst uni x where Source #
Nothing
type ToHoles x :: [Hole] Source #
Return every part of the type that can be a to-be-instantiated type variable.
For example, in Integer
there's no such types and in (a, b)
it's the two arguments
(a
and b
) and the same applies to a -> b
(to mention a type that is not built-in).
type ToBinds x :: [Some TyNameRep] Source #
Collect all unique variables (a variable consists of a textual name, a unique and a kind)
in an a
.
Instances
type family Merge xs ys :: [a] where ... Source #
Delete all elements appearing in the first list from the second one and concatenate the lists.
data KnownTypeError Source #
Instances
Eq KnownTypeError Source # | |
Defined in PlutusCore.Builtin.KnownType (==) :: KnownTypeError -> KnownTypeError -> Bool Source # (/=) :: KnownTypeError -> KnownTypeError -> Bool Source # | |
AsEvaluationFailure KnownTypeError Source # | |
Defined in PlutusCore.Builtin.KnownType _EvaluationFailure :: Prism' KnownTypeError () Source # | |
AsUnliftingError KnownTypeError Source # | |
Defined in PlutusCore.Builtin.KnownType _UnliftingError :: Prism' KnownTypeError UnliftingError Source # _UnliftingErrorE :: Prism' KnownTypeError Text Source # |
throwKnownTypeErrorWithCause :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err, AsEvaluationFailure err) => ErrorWithCause KnownTypeError cause -> m void Source #
Throw a ErrorWithCause KnownTypeError cause
.
type KnownBuiltinTypeIn uni val a = (HasConstantIn uni val, GShow uni, GEq uni, uni `Contains` a) Source #
A constraint for "a
is a ReadKnownIn
and MakeKnownIn
by means of being included
in uni
".
type KnownBuiltinType val a = KnownBuiltinTypeIn (UniOf val) val a Source #
A constraint for "a
is a ReadKnownIn
and MakeKnownIn
by means of being included
in UniOf term
".
type MakeKnownM cause = ExceptT (ErrorWithCause KnownTypeError cause) Emitter Source #
The monad that makeKnown
runs in.
type ReadKnownM cause = Either (ErrorWithCause KnownTypeError cause) Source #
The monad that readKnown
runs in.
readKnownConstant :: forall val a cause. KnownBuiltinType val a => Maybe cause -> val -> ReadKnownM cause a Source #
Convert a constant embedded into a PLC term to the corresponding Haskell value.
class uni ~ UniOf val => MakeKnownIn uni val a where Source #
Nothing
makeKnown :: Maybe cause -> a -> MakeKnownM cause val Source #
Convert a Haskell value to the corresponding PLC val.
The inverse of readKnown
.
default makeKnown :: KnownBuiltinType val a => Maybe cause -> a -> MakeKnownM cause val Source #
Instances
type MakeKnown val = MakeKnownIn (UniOf val) val Source #
class uni ~ UniOf val => ReadKnownIn uni val a where Source #
Nothing
readKnown :: Maybe cause -> val -> ReadKnownM cause a Source #
Convert a PLC val to the corresponding Haskell value.
The inverse of makeKnown
.
default readKnown :: KnownBuiltinType val a => Maybe cause -> val -> ReadKnownM cause a Source #
Instances
type ReadKnown val = ReadKnownIn (UniOf val) val Source #
makeKnownRun :: MakeKnownIn uni val a => Maybe cause -> a -> (ReadKnownM cause val, DList Text) Source #
makeKnownOrFail :: MakeKnownIn uni val a => a -> EvaluationResult val Source #
Same as makeKnown
, but allows for neither emitting nor storing the cause of a failure.
readKnownSelf :: (ReadKnown val a, AsUnliftingError err, AsEvaluationFailure err) => val -> Either (ErrorWithCause err val) a Source #
Same as readKnown
, but the cause of a potential failure is the provided term itself.
class KnownKind k where Source #
For reifying Haskell kinds representing Plutus kinds at the term level.
class ToKind (uni :: Type -> Type) where Source #
For computing the Plutus kind of a built-in type. See kindOfBuiltinType
.
toSingKind :: uni (Esc (a :: k)) -> SingKind k Source #
Reify the kind of a type from the universe at the term level.
Instances
ToKind DefaultUni Source # | |
Defined in PlutusCore.Default.Universe toSingKind :: forall k (a :: k). DefaultUni (Esc a) -> SingKind k Source # |
demoteKind :: SingKind k -> Kind () Source #
Convert a reified Haskell kind to a Plutus kind.
kindOfBuiltinType :: ToKind uni => uni (Esc a) -> Kind () Source #
Compute the kind of a type from a universe.
throwNotAConstant :: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err) => Maybe cause -> m r Source #
Throw an UnliftingError
saying that the received argument is not a constant.
class HasConstant term where Source #
Ensures that term
has a Constant
-like constructor to lift values to and unlift values from.
asConstant :: AsUnliftingError err => Maybe cause -> term -> Either (ErrorWithCause err cause) (Some (ValueOf (UniOf term))) Source #
Unlift from the Constant
constructor throwing an UnliftingError
if the provided term
is not a Constant
.
fromConstant :: Some (ValueOf (UniOf term)) -> term Source #
Wrap a Haskell value as a term
.
Instances
type HasConstantIn uni term = (UniOf term ~ uni, HasConstant term) Source #
Ensures that term
has a Constant
-like constructor to lift values to and unlift values from
and connects term
and its uni
.
module PlutusCore.Builtin.Emitter