plutus-core-1.30.0.0: Language library for Plutus Core
Safe HaskellSafe-Inferred
LanguageHaskell2010

PlutusCore.Builtin.Meaning

Synopsis

Documentation

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 [(), Bool] Integer
FoldArgs [(), Bool] Integer :: *
= () -> Bool -> Integer

Equations

FoldArgs '[] res = res 
FoldArgs (arg ': args) res = arg → FoldArgs args res 

data BuiltinMeaning val cost Source #

The meaning of a built-in function consists of its type represented as a TypeScheme, its Haskell denotation and its uninstantiated runtime denotation.

The TypeScheme of a built-in function is used for example for

  1. computing the PLC type of the function to be used during type checking
  2. getting arity information
  3. generating arbitrary values to apply the function to in tests

The denotation is lazy, so that we don't need to worry about a builtin being bottom (happens in tests). The production path is not affected by that, since only runtime denotations are used for evaluation.

Constructors

∀ args res. BuiltinMeaning (TypeScheme val args res) ~(FoldArgs args res) (cost → BuiltinRuntime val) 

type HasMeaningIn uni val = (Typeable val, ExMemoryUsage val, HasConstantIn uni val) Source #

Constraints available when defining a built-in function.

class (Typeable uni, Typeable fun, Bounded fun, Enum fun, Ix fun, Default (BuiltinSemanticsVariant fun)) ⇒ ToBuiltinMeaning uni fun where Source #

A type class for "each function from a set of built-in functions has a BuiltinMeaning".

Associated Types

type CostingPart uni fun Source #

The cost part of BuiltinMeaning.

data BuiltinSemanticsVariant fun Source #

See Note [Builtin semantics variants]

Methods

toBuiltinMeaningHasMeaningIn uni val ⇒ BuiltinSemanticsVariant fun → fun → BuiltinMeaning val (CostingPart uni fun) Source #

Get the BuiltinMeaning of a built-in function.

typeOfBuiltinFunction ∷ ∀ uni fun. ToBuiltinMeaning uni fun ⇒ BuiltinSemanticsVariant fun → fun → Type TyName uni () Source #

Get the type of a built-in function.

type family GetArgs a where ... Source #

Chop a function type to get a list of its argument types.

Equations

GetArgs (a → b) = a ': GetArgs b 
GetArgs _ = '[] 

class KnownMonotype val args res where Source #

A class that allows us to derive a monotype for a builtin. We could've computed the runtime denotation from the TypeScheme and the denotation of the builtin, but not statically (due to unfolding not working for recursive functions and TypeScheme being recursive, i.e. requiring the conversion function to be recursive), and so it would cause us to retain a lot of evaluation-irrelevant stuff in the constructors of BuiltinRuntime, which has to make evaluation slower (we didn't check) and certainly makes the generated Core much harder to read. Technically speaking, we could get a RuntimeScheme from the TypeScheme and the denotation 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.

Methods

knownMonotypeTypeScheme val args res Source #

toMonoFReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream) → BuiltinRuntime val Source #

Convert the denotation of a builtin to its runtime counterpart . 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

Instances details
(Typeable res, KnownTypeAst TyName (UniOf val) res, MakeKnown val res) ⇒ KnownMonotype val ('[] ∷ [Type]) res Source #

Once we've run out of term-level arguments, we return a TypeSchemeResult/RuntimeSchemeResult.

Instance details

Defined in PlutusCore.Builtin.Meaning

(Typeable arg, KnownTypeAst TyName (UniOf val) arg, MakeKnown val arg, ReadKnown val arg, KnownMonotype val args res) ⇒ KnownMonotype val (arg ': args) res Source #

Every term-level argument becomes a TypeSchemeArrow/RuntimeSchemeArrow.

Instance details

Defined in PlutusCore.Builtin.Meaning

Methods

knownMonotypeTypeScheme val (arg ': args) res Source #

toMonoFReadKnownM (FoldArgs (arg ': args) res, FoldArgs (arg ': args) ExBudgetStream) → BuiltinRuntime val Source #

class KnownMonotype val args res ⇒ KnownPolytype (binds ∷ [Some TyNameRep]) val args res where Source #

A class that allows us to derive a polytype for a builtin.

Methods

knownPolytypeTypeScheme val args res Source #

toPolyFReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream) → BuiltinRuntime val Source #

Convert the denotation of a builtin to its runtime counterpart. The argument is in ReadKnownM, because that's what we need to do: passing the action returning the builtin application around until full saturation, which is when the action actually gets run.

Instances

Instances details
KnownMonotype val args res ⇒ KnownPolytype ('[] ∷ [Some TyNameRep]) val args res Source #

Once we've run out of type-level arguments, we start handling term-level ones.

Instance details

Defined in PlutusCore.Builtin.Meaning

(KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res) ⇒ KnownPolytype ('Some ('TyNameRep name uniq ∷ TyNameRep kind) ': binds) val args res Source #

Every type-level argument becomes a TypeSchemeAll.

Instance details

Defined in PlutusCore.Builtin.Meaning

type family ThrowOnBothEmpty binds args isBuiltin a where ... Source #

Ensure a built-in function is not nullary and throw a nice error otherwise.

Equations

ThrowOnBothEmpty '[] '[] 'True a = TypeError (('Text "A built-in function must take at least one type or term argument" ':$$: ((('Text "\8216" ':<>: 'ShowType a) ':<>: 'Text "\8217 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 \8216()\8217 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 \8216()\8217 argument") 
ThrowOnBothEmpty _ _ _ _ = () 

class MakeBuiltinMeaning a val where Source #

A function turned into a type class with exactly one fully general instance. We can't package up the constraints of makeBuiltinMeaning (see the instance) into a type or class synonym, because they contain a bunch of variables defined by ~ or determined via functional dependencies and neither class nor type definitions can handle that (see https://gitlab.haskell.org/ghc/ghc/-/issues/7100). Inlining three lines of constraints whenever we need to call makeBuiltinMeaning over a non-concrete type is a bad option and this abstraction is free anyway, hence its existence.

The a type variable goes first, because makeBuiltinMeaning @A is a common pattern.

Methods

makeBuiltinMeaning ∷ a → (cost → FoldArgs (GetArgs a) ExBudgetStream) → BuiltinMeaning val cost Source #

Construct the meaning for a built-in function by automatically deriving its TypeScheme, given

  1. the denotation of the builtin
  2. an uninstantiated costing function

Instances

Instances details
(uni ~ UniOf val, binds ~ ToBinds uni ('[] ∷ [Some TyNameRep]) 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 Source # 
Instance details

Defined in PlutusCore.Builtin.Meaning

Methods

makeBuiltinMeaning ∷ a → (cost → FoldArgs (GetArgs a) ExBudgetStream) → BuiltinMeaning val cost Source #

toBuiltinRuntime ∷ cost → BuiltinMeaning val cost → BuiltinRuntime val Source #

Convert a BuiltinMeaning to a BuiltinRuntime given a cost model.

toBuiltinsRuntime ∷ (cost ~ CostingPart uni fun, ToBuiltinMeaning uni fun, HasMeaningIn uni val) ⇒ BuiltinSemanticsVariant fun → cost → BuiltinsRuntime fun val Source #

Calculate runtime info for all built-in functions given meanings of builtins (as a constraint), the semantics variant of the set of builtins and a cost model.