| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
UntypedPlutusCore.Evaluation.Machine.Cek.Internal
Description
The CEK machine.
The CEK machine relies on variables having non-equal
Unique
s whenever they have non-equal
string names. I.e.
Unique
s are used instead of string names. This is for efficiency reasons.
The CEK machines handles name capture by design.
Synopsis
- data EvaluationResult a
-
data
CekValue
uni fun
- = VCon !( Some ( ValueOf uni))
- | VDelay ( Term NamedDeBruijn uni fun ()) !(CekValEnv uni fun)
- | VLamAbs NamedDeBruijn ( Term NamedDeBruijn uni fun ()) !(CekValEnv uni fun)
- | VBuiltin !fun ( Term NamedDeBruijn uni fun ()) (CekValEnv uni fun) !( BuiltinRuntime ( CekValue uni fun))
- data CekUserError
- type CekEvaluationException name uni fun = EvaluationException CekUserError ( MachineError fun) ( Term name uni fun ())
-
newtype
CekBudgetSpender
uni fun s =
CekBudgetSpender
{
- unCekBudgetSpender :: ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
-
data
ExBudgetInfo
cost uni fun s =
ExBudgetInfo
{
- _exBudgetModeSpender :: !( CekBudgetSpender uni fun s)
- _exBudgetModeGetFinal :: !( ST s cost)
- _exBudgetModeGetCumulative :: !( ST s ExBudget )
-
newtype
ExBudgetMode
cost uni fun =
ExBudgetMode
{
- unExBudgetMode :: forall s. ST s ( ExBudgetInfo cost uni fun s)
- type CekEmitter uni fun s = DList Text -> CekM uni fun s ()
-
data
CekEmitterInfo
uni fun s =
CekEmitterInfo
{
- _cekEmitterInfoEmit :: CekEmitter uni fun s
- _cekEmitterInfoGetFinal :: ST s [ Text ]
-
newtype
EmitterMode
uni fun =
EmitterMode
{
- unEmitterMode :: forall s. ST s ExBudget -> ST s ( CekEmitterInfo uni fun s)
- newtype CekM uni fun s a = CekM { }
- data ErrorWithCause err cause = ErrorWithCause { }
-
data
EvaluationError
user internal
- = InternalEvaluationError internal
- | UserEvaluationError user
-
data
ExBudgetCategory
fun
- = BStep StepKind
- | BBuiltinApp fun
- | BStartup
- data StepKind
- type PrettyUni uni fun = ( GShow uni, Closed uni, Pretty fun, Typeable uni, Typeable fun, Everywhere uni PrettyConst )
- extractEvaluationResult :: Either ( EvaluationException user internal term) a -> Either ( ErrorWithCause internal term) ( EvaluationResult a)
- runCekDeBruijn :: (uni `Everywhere` ExMemoryUsage , Ix fun, PrettyUni uni fun) => MachineParameters CekMachineCosts CekValue uni fun -> ExBudgetMode cost uni fun -> EmitterMode uni fun -> Term NamedDeBruijn uni fun () -> ( Either ( CekEvaluationException NamedDeBruijn uni fun) ( Term NamedDeBruijn uni fun ()), cost, [ Text ])
- dischargeCekValue :: CekValue uni fun -> Term NamedDeBruijn uni fun ()
Documentation
data EvaluationResult a Source #
The parameterized type of results various evaluation engines return.
On the PLC side this becomes (via
makeKnown
) either a call to
Error
or
a value of the PLC counterpart of type
a
.
Constructors
| EvaluationSuccess a | |
| EvaluationFailure |
Instances
data CekValue uni fun Source #
Constructors
| VCon !( Some ( ValueOf uni)) | |
| VDelay ( Term NamedDeBruijn uni fun ()) !(CekValEnv uni fun) | |
| VLamAbs NamedDeBruijn ( Term NamedDeBruijn uni fun ()) !(CekValEnv uni fun) | |
| VBuiltin !fun ( Term NamedDeBruijn uni fun ()) (CekValEnv uni fun) !( BuiltinRuntime ( CekValue uni fun)) |
Instances
| ( Closed uni, GShow uni, Everywhere uni PrettyConst , Pretty fun) => PrettyBy PrettyConfigPlc ( CekValue uni fun) Source # | |
|
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods prettyBy :: PrettyConfigPlc -> CekValue uni fun -> Doc ann Source # prettyListBy :: PrettyConfigPlc -> [ CekValue uni fun] -> Doc ann Source # |
|
| Show ( BuiltinRuntime ( CekValue uni fun)) Source # | |
| ( Everywhere uni Show , GShow uni, Closed uni, Show fun) => Show ( CekValue uni fun) Source # | |
| HasConstant ( CekValue uni fun) Source # | |
|
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods asConstant :: AsUnliftingError err => Maybe cause -> CekValue uni fun -> Either ( ErrorWithCause err cause) ( Some ( ValueOf ( UniOf ( CekValue uni fun)))) Source # fromConstant :: Some ( ValueOf ( UniOf ( CekValue uni fun))) -> CekValue uni fun Source # |
|
| type UniOf ( CekValue uni fun) Source # | |
data CekUserError Source #
Constructors
| CekOutOfExError ExRestrictingBudget |
The final overspent (i.e. negative) budget. |
| CekEvaluationFailure |
Error has been called or a builtin application has failed |
Instances
type CekEvaluationException name uni fun = EvaluationException CekUserError ( MachineError fun) ( Term name uni fun ()) Source #
The CEK machine-specific
EvaluationException
.
newtype CekBudgetSpender uni fun s Source #
The CEK machine is parameterized over a
spendBudget
function. This makes the budgeting machinery extensible
and allows us to separate budgeting logic from evaluation logic and avoid branching on the union
of all possible budgeting state types during evaluation.
Constructors
| CekBudgetSpender | |
|
Fields
|
|
data ExBudgetInfo cost uni fun s Source #
Runtime budgeting info.
Constructors
| ExBudgetInfo | |
|
Fields
|
|
newtype ExBudgetMode cost uni fun Source #
A budgeting mode to execute the CEK machine in.
Constructors
| ExBudgetMode | |
|
Fields
|
|
type CekEmitter uni fun s = DList Text -> CekM uni fun s () Source #
The CEK machine is parameterized over an emitter function, similar to
CekBudgetSpender
.
data CekEmitterInfo uni fun s Source #
Runtime emitter info, similar to
ExBudgetInfo
.
Constructors
| CekEmitterInfo | |
|
Fields
|
|
newtype EmitterMode uni fun Source #
An emitting mode to execute the CEK machine in, similar to
ExBudgetMode
.
Constructors
| EmitterMode | |
|
Fields
|
|
newtype CekM uni fun s a Source #
The monad the CEK machine runs in.
Instances
| Monad ( CekM uni fun s) Source # | |
| Functor ( CekM uni fun s) Source # | |
| Applicative ( CekM uni fun s) Source # | |
|
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods pure :: a -> CekM uni fun s a Source # (<*>) :: CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b Source # liftA2 :: (a -> b -> c) -> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c Source # (*>) :: CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b Source # (<*) :: CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a Source # |
|
| PrettyUni uni fun => MonadError ( CekEvaluationException NamedDeBruijn uni fun) ( CekM uni fun s) Source # | |
|
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods throwError :: CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a Source # catchError :: CekM uni fun s a -> ( CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a) -> CekM uni fun s a Source # |
|
data ErrorWithCause err cause Source #
An error and (optionally) what caused it.
Constructors
| ErrorWithCause | |
Instances
data EvaluationError user internal Source #
The type of errors (all of them) which can occur during evaluation (some are used-caused, some are internal).
Constructors
| InternalEvaluationError internal |
Indicates bugs. |
| UserEvaluationError user |
Indicates user errors. |
Instances
data ExBudgetCategory fun Source #
Constructors
| BStep StepKind | |
| BBuiltinApp fun | |
| BStartup |
Instances
Instances
type PrettyUni uni fun = ( GShow uni, Closed uni, Pretty fun, Typeable uni, Typeable fun, Everywhere uni PrettyConst ) Source #
The set of constraints we need to be able to print things in universes, which we need in order to throw exceptions.
extractEvaluationResult :: Either ( EvaluationException user internal term) a -> Either ( ErrorWithCause internal term) ( EvaluationResult a) Source #
Turn any
UserEvaluationError
into an
EvaluationFailure
.
runCekDeBruijn :: (uni `Everywhere` ExMemoryUsage , Ix fun, PrettyUni uni fun) => MachineParameters CekMachineCosts CekValue uni fun -> ExBudgetMode cost uni fun -> EmitterMode uni fun -> Term NamedDeBruijn uni fun () -> ( Either ( CekEvaluationException NamedDeBruijn uni fun) ( Term NamedDeBruijn uni fun ()), cost, [ Text ]) Source #
Evaluate a term using the CEK machine and keep track of costing, logging is optional.
dischargeCekValue :: CekValue uni fun -> Term NamedDeBruijn uni fun () Source #