| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
UntypedPlutusCore.Evaluation.Machine.SteppableCek.Internal
Description
The CEK machine.
The CEK machine relies on variables having non-equal Uniques whenever they have non-equal
string names. I.e. Uniques are used instead of string names. This is for efficiency reasons.
The CEK machines handles name capture by design.
Synopsis
- data CekState (uni :: Type -> Type) fun ann
- data Context (uni :: Type -> Type) fun ann
- = FrameAwaitArg ann !(CekValue uni fun ann) !(Context uni fun ann)
- | FrameAwaitFunTerm ann !(CekValEnv uni fun ann) !(NTerm uni fun ann) !(Context uni fun ann)
- | FrameAwaitFunConN ann !(Spine (Some (ValueOf uni))) !(Context uni fun ann)
- | FrameAwaitFunValueN ann !(ArgStackNonEmpty uni fun ann) !(Context uni fun ann)
- | FrameForce ann !(Context uni fun ann)
- | FrameConstr ann !(CekValEnv uni fun ann) !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
- | FrameCases ann !(CekValEnv uni fun ann) !(Vector (NTerm uni fun ann)) !(Context uni fun ann)
- | NoFrame
- contextAnn :: forall (uni :: Type -> Type) fun ann. Context uni fun ann -> Maybe ann
- liftCek :: forall m s (uni :: Type -> Type) fun a. (PrimMonad m, PrimState m ~ s) => CekM uni fun s a -> m a
- class Monad m => PrimMonad (m :: Type -> Type) where
- lenContext :: forall (uni :: Type -> Type) fun ann. Context uni fun ann -> Word
- cekStateContext :: forall (uni :: Type -> Type) fun ann f. Applicative f => (Context uni fun ann -> f (Context uni fun ann)) -> CekState uni fun ann -> f (CekState uni fun ann)
- cekStateAnn :: forall (uni :: Type -> Type) fun ann. CekState uni fun ann -> Maybe ann
- runCekDeBruijn :: forall (uni :: Type -> Type) fun ann cost. ThrowableBuiltins uni fun => MachineParameters CekMachineCosts fun (CekValue uni fun ann) -> ExBudgetMode cost uni fun -> EmitterMode uni fun -> NTerm uni fun ann -> CekReport cost NamedDeBruijn uni fun
- computeCek :: forall (uni :: Type -> Type) fun ann s. (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) => Context uni fun ann -> CekValEnv uni fun ann -> NTerm uni fun ann -> CekM uni fun s (CekState uni fun ann)
- returnCek :: forall (uni :: Type -> Type) fun ann s. (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) => Context uni fun ann -> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann)
- mkCekTrans :: forall cost (uni :: Type -> Type) fun ann m s. (ThrowableBuiltins uni fun, PrimMonad m, s ~ PrimState m) => MachineParameters CekMachineCosts fun (CekValue uni fun ann) -> ExBudgetMode cost uni fun -> EmitterMode uni fun -> Slippage -> m (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s)
- type CekTrans (uni :: Type -> Type) fun ann s = Trans (CekM uni fun s) (CekState uni fun ann)
- nilSlippage :: Slippage
- data EvaluationResult a
- data EvaluationError structural operational
- = StructuralError !structural
- | OperationalError !operational
- data ErrorWithCause err cause = ErrorWithCause {}
- splitStructuralOperational :: Either (EvaluationException structural operational term) a -> Either (ErrorWithCause structural term) (EvaluationResult a)
- unsafeSplitStructuralOperational :: (PrettyPlc structural, PrettyPlc term, Typeable structural, Typeable term) => Either (EvaluationException structural operational term) a -> EvaluationResult a
- type ThrowableBuiltins (uni :: Type -> Type) fun = (PrettyUni uni, Pretty fun, Typeable uni, Typeable fun)
- data CekUserError
- type CekEvaluationException name (uni :: Type -> Type) fun = EvaluationException (MachineError fun) CekUserError (Term name uni fun ())
- data ExBudgetCategory fun
- = BStep StepKind
- | BBuiltinApp fun
- | BStartup
- newtype CekBudgetSpender (uni :: Type -> Type) fun s = CekBudgetSpender {
- unCekBudgetSpender :: ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
- newtype ExBudgetMode cost (uni :: Type -> Type) fun = ExBudgetMode {
- unExBudgetMode :: forall s. ST s (ExBudgetInfo cost uni fun s)
- data StepKind
- data CekResult name (uni :: Type -> Type) fun
- = CekFailure (CekEvaluationException name uni fun)
- | CekSuccessConstant (Some (ValueOf uni))
- | CekSuccessNonConstant (Term name uni fun ())
- data CekReport cost name (uni :: Type -> Type) fun = CekReport {
- _cekReportResult :: CekResult name uni fun
- _cekReportCost :: cost
- _cekReportLogs :: [Text]
- cekResultToEither :: forall name (uni :: Type -> Type) fun. CekResult name uni fun -> Either (CekEvaluationException name uni fun) (Term name uni fun ())
- data CekValue (uni :: Type -> Type) fun ann
- data DischargeResult (uni :: Type -> Type) fun
- = DischargeConstant (Some (ValueOf uni))
- | DischargeNonConstant (NTerm uni fun ())
- dischargeResultToTerm :: forall (uni :: Type -> Type) fun. DischargeResult uni fun -> NTerm uni fun ()
- newtype EmitterMode (uni :: Type -> Type) fun = EmitterMode {
- unEmitterMode :: forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
- mapTermCekResult :: forall name (uni :: Type -> Type) fun name'. (Term name uni fun () -> Term name' uni fun ()) -> CekResult name uni fun -> CekResult name' uni fun
- data ArgStack (uni :: Type -> Type) fun ann
- data EmptyOrMultiStack (uni :: Type -> Type) fun ann
- = EmptyStack
- | MultiStack !(ArgStackNonEmpty uni fun ann)
- data ArgStackNonEmpty (uni :: Type -> Type) fun ann
- = LastStackNonEmpty !(CekValue uni fun ann)
- | ConsStackNonEmpty !(CekValue uni fun ann) !(ArgStackNonEmpty uni fun ann)
- data ExBudgetInfo cost (uni :: Type -> Type) fun s = ExBudgetInfo {
- _exBudgetModeSpender :: !(CekBudgetSpender uni fun s)
- _exBudgetModeGetFinal :: !(ST s cost)
- _exBudgetModeGetCumulative :: !(ST s ExBudget)
- type CekEmitter (uni :: Type -> Type) fun s = DList Text -> CekM uni fun s ()
- data CekEmitterInfo (uni :: Type -> Type) fun s = CekEmitterInfo {
- _cekEmitterInfoEmit :: !(CekEmitter uni fun s)
- _cekEmitterInfoGetFinal :: !(ST s [Text])
- newtype CekM (uni :: Type -> Type) fun s a = CekM {}
- dischargeCekValue :: forall (uni :: Type -> Type) fun ann. CekValue uni fun ann -> DischargeResult uni fun
- type CekValEnv (uni :: Type -> Type) fun ann = RAList (CekValue uni fun ann)
- type GivenCekReqs (uni :: Type -> Type) fun ann s = (GivenCekRuntime uni fun ann, GivenCekCaserBuiltin uni, GivenCekEmitter uni fun s, GivenCekSpender uni fun s, GivenCekSlippage, GivenCekStepCounter s, GivenCekCosts)
- type GivenCekSpender (uni :: Type -> Type) fun s = ?cekBudgetSpender :: CekBudgetSpender uni fun s
- data StepCounter (n :: Nat) s
- type NumberOfStepCounters = CountConstructorsEnum (Rep StepKind)
- type CounterSize = NumberOfStepCounters + 1
- type TotalCountIndex = NumberOfStepCounters
- type Slippage = Word8
- defaultSlippage :: Slippage
- type NTerm (uni :: Type -> Type) fun = Term NamedDeBruijn uni fun
- runCekM :: forall cost (uni :: Type -> Type) fun ann. ThrowableBuiltins uni fun => MachineParameters CekMachineCosts fun (CekValue uni fun ann) -> ExBudgetMode cost uni fun -> EmitterMode uni fun -> (forall s. GivenCekReqs uni fun ann s => CekM uni fun s (DischargeResult uni fun)) -> CekReport cost NamedDeBruijn uni fun
Documentation
data Context (uni :: Type -> Type) fun ann Source #
Similar to Context, but augmented with an ann
Constructors
| FrameAwaitArg ann !(CekValue uni fun ann) !(Context uni fun ann) | [V _] |
| FrameAwaitFunTerm ann !(CekValEnv uni fun ann) !(NTerm uni fun ann) !(Context uni fun ann) | [_ N] |
| FrameAwaitFunConN ann !(Spine (Some (ValueOf uni))) !(Context uni fun ann) | |
| FrameAwaitFunValueN ann !(ArgStackNonEmpty uni fun ann) !(Context uni fun ann) | |
| FrameForce ann !(Context uni fun ann) | (force _) |
| FrameConstr ann !(CekValEnv uni fun ann) !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann) | |
| FrameCases ann !(CekValEnv uni fun ann) !(Vector (NTerm uni fun ann)) !(Context uni fun ann) | |
| NoFrame |
liftCek :: forall m s (uni :: Type -> Type) fun a. (PrimMonad m, PrimState m ~ s) => CekM uni fun s a -> m a Source #
Lift a CEK computation to a primitive.PrimMonad m
class Monad m => PrimMonad (m :: Type -> Type) where #
Instances
cekStateContext :: forall (uni :: Type -> Type) fun ann f. Applicative f => (Context uni fun ann -> f (Context uni fun ann)) -> CekState uni fun ann -> f (CekState uni fun ann) Source #
runCekDeBruijn :: forall (uni :: Type -> Type) fun ann cost. ThrowableBuiltins uni fun => MachineParameters CekMachineCosts fun (CekValue uni fun ann) -> ExBudgetMode cost uni fun -> EmitterMode uni fun -> NTerm uni fun ann -> CekReport cost NamedDeBruijn uni fun Source #
computeCek :: forall (uni :: Type -> Type) fun ann s. (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) => Context uni fun ann -> CekValEnv uni fun ann -> NTerm uni fun ann -> CekM uni fun s (CekState uni fun ann) Source #
returnCek :: forall (uni :: Type -> Type) fun ann s. (ThrowableBuiltins uni fun, GivenCekReqs uni fun ann s) => Context uni fun ann -> CekValue uni fun ann -> CekM uni fun s (CekState uni fun ann) Source #
mkCekTrans :: forall cost (uni :: Type -> Type) fun ann m s. (ThrowableBuiltins uni fun, PrimMonad m, s ~ PrimState m) => MachineParameters CekMachineCosts fun (CekValue uni fun ann) -> ExBudgetMode cost uni fun -> EmitterMode uni fun -> Slippage -> m (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s) Source #
Based on the supplied arguments, initialize the CEK environment and construct a state transition function. Returns the constructed transition function paired with the methods to live access the running budget.
type CekTrans (uni :: Type -> Type) fun ann s = Trans (CekM uni fun s) (CekState uni fun ann) Source #
nilSlippage :: Slippage Source #
A CEK parameter that turns the slippage optimization *off*.
This is needed in the case of the debugger, where the accounting/budgeting costs must be *live* updated.
data EvaluationResult a Source #
The parameterized type of results various evaluation engines return.
Constructors
| EvaluationSuccess !a | |
| EvaluationFailure |
Instances
| MonadFail EvaluationResult Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods fail :: String -> EvaluationResult a Source # | |||||
| Foldable EvaluationResult Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods fold :: Monoid m => EvaluationResult m -> m Source # foldMap :: Monoid m => (a -> m) -> EvaluationResult a -> m Source # foldMap' :: Monoid m => (a -> m) -> EvaluationResult a -> m Source # foldr :: (a -> b -> b) -> b -> EvaluationResult a -> b Source # foldr' :: (a -> b -> b) -> b -> EvaluationResult a -> b Source # foldl :: (b -> a -> b) -> b -> EvaluationResult a -> b Source # foldl' :: (b -> a -> b) -> b -> EvaluationResult a -> b Source # foldr1 :: (a -> a -> a) -> EvaluationResult a -> a Source # foldl1 :: (a -> a -> a) -> EvaluationResult a -> a Source # toList :: EvaluationResult a -> [a] Source # null :: EvaluationResult a -> Bool Source # length :: EvaluationResult a -> Int Source # elem :: Eq a => a -> EvaluationResult a -> Bool Source # maximum :: Ord a => EvaluationResult a -> a Source # minimum :: Ord a => EvaluationResult a -> a Source # sum :: Num a => EvaluationResult a -> a Source # product :: Num a => EvaluationResult a -> a Source # | |||||
| Traversable EvaluationResult Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods traverse :: Applicative f => (a -> f b) -> EvaluationResult a -> f (EvaluationResult b) Source # sequenceA :: Applicative f => EvaluationResult (f a) -> f (EvaluationResult a) Source # mapM :: Monad m => (a -> m b) -> EvaluationResult a -> m (EvaluationResult b) Source # sequence :: Monad m => EvaluationResult (m a) -> m (EvaluationResult a) Source # | |||||
| Alternative EvaluationResult Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods empty :: EvaluationResult a Source # (<|>) :: EvaluationResult a -> EvaluationResult a -> EvaluationResult a Source # some :: EvaluationResult a -> EvaluationResult [a] Source # many :: EvaluationResult a -> EvaluationResult [a] Source # | |||||
| Applicative EvaluationResult Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods pure :: a -> EvaluationResult a Source # (<*>) :: EvaluationResult (a -> b) -> EvaluationResult a -> EvaluationResult b Source # liftA2 :: (a -> b -> c) -> EvaluationResult a -> EvaluationResult b -> EvaluationResult c Source # (*>) :: EvaluationResult a -> EvaluationResult b -> EvaluationResult b Source # (<*) :: EvaluationResult a -> EvaluationResult b -> EvaluationResult a Source # | |||||
| Functor EvaluationResult Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods fmap :: (a -> b) -> EvaluationResult a -> EvaluationResult b Source # (<$) :: a -> EvaluationResult b -> EvaluationResult a Source # | |||||
| Monad EvaluationResult Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods (>>=) :: EvaluationResult a -> (a -> EvaluationResult b) -> EvaluationResult b Source # (>>) :: EvaluationResult a -> EvaluationResult b -> EvaluationResult b Source # return :: a -> EvaluationResult a Source # | |||||
| MonadError () EvaluationResult Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods throwError :: () -> EvaluationResult a Source # catchError :: EvaluationResult a -> (() -> EvaluationResult a) -> EvaluationResult a Source # | |||||
| KnownTypeAst tyname uni a => KnownTypeAst tyname uni (EvaluationResult a :: Type) Source # | |||||
Defined in PlutusCore.Builtin.KnownTypeAst Associated Types
| |||||
| (TypeError ('Text "Use \8216BuiltinResult\8217 instead of \8216EvaluationResult\8217") :: Constraint, uni ~ UniOf val) => MakeKnownIn uni val (EvaluationResult a) Source # | |||||
Defined in PlutusCore.Builtin.KnownType Methods makeKnown :: EvaluationResult a -> BuiltinResult val Source # | |||||
| (TypeError ('Text "Use \8216BuiltinResult\8217 instead of \8216EvaluationResult\8217") :: Constraint, uni ~ UniOf val) => ReadKnownIn uni val (EvaluationResult a) Source # | |||||
Defined in PlutusCore.Builtin.KnownType Methods readKnown :: val -> ReadKnownM (EvaluationResult a) Source # | |||||
| PrettyBy config a => PrettyBy config (EvaluationResult a) Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods prettyBy :: config -> EvaluationResult a -> Doc ann # prettyListBy :: config -> [EvaluationResult a] -> Doc ann # | |||||
| Generic (EvaluationResult a) Source # | |||||
Defined in PlutusCore.Evaluation.Result Associated Types
Methods from :: EvaluationResult a -> Rep (EvaluationResult a) x Source # to :: Rep (EvaluationResult a) x -> EvaluationResult a Source # | |||||
| Show a => Show (EvaluationResult a) Source # | |||||
Defined in PlutusCore.Evaluation.Result | |||||
| NFData a => NFData (EvaluationResult a) Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods rnf :: EvaluationResult a -> () Source # | |||||
| Eq a => Eq (EvaluationResult a) Source # | |||||
Defined in PlutusCore.Evaluation.Result Methods (==) :: EvaluationResult a -> EvaluationResult a -> Bool Source # (/=) :: EvaluationResult a -> EvaluationResult a -> Bool Source # | |||||
| PrettyClassic a => Pretty (EvaluationResult a) Source # | |||||
Defined in PlutusCore.Evaluation.Result | |||||
| type ToBinds uni acc (EvaluationResult a :: Type) Source # | |||||
Defined in PlutusCore.Builtin.KnownTypeAst | |||||
| type ToHoles uni _1 (EvaluationResult a :: Type) Source # | |||||
Defined in PlutusCore.Builtin.KnownTypeAst | |||||
| type IsBuiltin uni (EvaluationResult a :: Type) Source # | |||||
Defined in PlutusCore.Builtin.KnownTypeAst | |||||
| type Rep (EvaluationResult a) Source # | |||||
Defined in PlutusCore.Evaluation.Result type Rep (EvaluationResult a) = D1 ('MetaData "EvaluationResult" "PlutusCore.Evaluation.Result" "plutus-core-1.60.0.0-LXFqBsoUlXsJIEqLytHte7" 'False) (C1 ('MetaCons "EvaluationSuccess" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)) :+: C1 ('MetaCons "EvaluationFailure" 'PrefixI 'False) (U1 :: Type -> Type)) | |||||
data EvaluationError structural operational Source #
The type of errors that can occur during evaluation. There are two kinds of errors:
- Structural ones -- these are errors that are indicative of the _structure_ of the program being
wrong. For example, a free variable was encountered during evaluation, a non-function was
applied to an argument or
tailListwas applied to a non-list. - Operational ones -- these are errors that are indicative of the _logic_ of the program being
wrong. For example,
errorwas executed,tailListwas applied to an empty list or evaluation ran out of gas.
On the chain both of these are just regular failures and we don't distinguish between them there: if a script fails, it fails, it doesn't matter what the reason was. However in the tests it does matter why the failure occurred: a structural error may indicate that the test was written incorrectly while an operational error may be entirely expected.
In other words, structural errors are "runtime type errors" and operational errors are regular runtime errors. Which means that evaluating an (erased) well-typed program should never produce a structural error, only an operational one. This creates a sort of "runtime type system" for UPLC and it would be great to stick to it and enforce in tests etc, but we currently don't.
Constructors
| StructuralError !structural | |
| OperationalError !operational |
Instances
| Bifoldable EvaluationError Source # | |||||
Defined in PlutusCore.Evaluation.Error Methods bifold :: Monoid m => EvaluationError m m -> m Source # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> EvaluationError a b -> m Source # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> EvaluationError a b -> c Source # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> EvaluationError a b -> c Source # | |||||
| Bifunctor EvaluationError Source # | |||||
Defined in PlutusCore.Evaluation.Error Methods bimap :: (a -> b) -> (c -> d) -> EvaluationError a c -> EvaluationError b d Source # first :: (a -> b) -> EvaluationError a c -> EvaluationError b c Source # second :: (b -> c) -> EvaluationError a b -> EvaluationError a c Source # | |||||
| Bitraversable EvaluationError Source # | |||||
Defined in PlutusCore.Evaluation.Error Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> EvaluationError a b -> f (EvaluationError c d) Source # | |||||
| (HasPrettyDefaults config ~ 'True, PrettyBy config structural, Pretty operational) => PrettyBy config (EvaluationError structural operational) Source # | |||||
Defined in PlutusCore.Evaluation.Error Methods prettyBy :: config -> EvaluationError structural operational -> Doc ann # prettyListBy :: config -> [EvaluationError structural operational] -> Doc ann # | |||||
| Functor (EvaluationError structural) Source # | |||||
Defined in PlutusCore.Evaluation.Error Methods fmap :: (a -> b) -> EvaluationError structural a -> EvaluationError structural b Source # (<$) :: a -> EvaluationError structural b -> EvaluationError structural a Source # | |||||
| Generic (EvaluationError structural operational) Source # | |||||
Defined in PlutusCore.Evaluation.Error Associated Types
Methods from :: EvaluationError structural operational -> Rep (EvaluationError structural operational) x Source # to :: Rep (EvaluationError structural operational) x -> EvaluationError structural operational Source # | |||||
| (Show structural, Show operational) => Show (EvaluationError structural operational) Source # | |||||
Defined in PlutusCore.Evaluation.Error | |||||
| (NFData structural, NFData operational) => NFData (EvaluationError structural operational) Source # | |||||
Defined in PlutusCore.Evaluation.Error Methods rnf :: EvaluationError structural operational -> () Source # | |||||
| (Eq structural, Eq operational) => Eq (EvaluationError structural operational) Source # | |||||
Defined in PlutusCore.Evaluation.Error Methods (==) :: EvaluationError structural operational -> EvaluationError structural operational -> Bool Source # (/=) :: EvaluationError structural operational -> EvaluationError structural operational -> Bool Source # | |||||
| (Pretty structural, Pretty operational) => Pretty (EvaluationError structural operational) Source # | |||||
Defined in PlutusCore.Evaluation.Error Methods pretty :: EvaluationError structural operational -> Doc ann # prettyList :: [EvaluationError structural operational] -> Doc ann # | |||||
| ThrowableBuiltins 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 # | |||||
| type Rep (EvaluationError structural operational) Source # | |||||
Defined in PlutusCore.Evaluation.Error type Rep (EvaluationError structural operational) = D1 ('MetaData "EvaluationError" "PlutusCore.Evaluation.Error" "plutus-core-1.60.0.0-LXFqBsoUlXsJIEqLytHte7" 'False) (C1 ('MetaCons "StructuralError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 structural)) :+: C1 ('MetaCons "OperationalError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 operational))) | |||||
data ErrorWithCause err cause Source #
An error and (optionally) what caused it.
Constructors
| ErrorWithCause | |
Instances
| Bifunctor ErrorWithCause Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause Methods bimap :: (a -> b) -> (c -> d) -> ErrorWithCause a c -> ErrorWithCause b d Source # first :: (a -> b) -> ErrorWithCause a c -> ErrorWithCause b c Source # second :: (b -> c) -> ErrorWithCause a b -> ErrorWithCause a c Source # | |||||
| (PrettyBy config cause, PrettyBy config err) => PrettyBy config (ErrorWithCause err cause) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause Methods prettyBy :: config -> ErrorWithCause err cause -> Doc ann # prettyListBy :: config -> [ErrorWithCause err cause] -> Doc ann # | |||||
| Foldable (ErrorWithCause err) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause Methods fold :: Monoid m => ErrorWithCause err m -> m Source # foldMap :: Monoid m => (a -> m) -> ErrorWithCause err a -> m Source # foldMap' :: Monoid m => (a -> m) -> ErrorWithCause err a -> m Source # foldr :: (a -> b -> b) -> b -> ErrorWithCause err a -> b Source # foldr' :: (a -> b -> b) -> b -> ErrorWithCause err a -> b Source # foldl :: (b -> a -> b) -> b -> ErrorWithCause err a -> b Source # foldl' :: (b -> a -> b) -> b -> ErrorWithCause err a -> b Source # foldr1 :: (a -> a -> a) -> ErrorWithCause err a -> a Source # foldl1 :: (a -> a -> a) -> ErrorWithCause err a -> a Source # toList :: ErrorWithCause err a -> [a] Source # null :: ErrorWithCause err a -> Bool Source # length :: ErrorWithCause err a -> Int Source # elem :: Eq a => a -> ErrorWithCause err a -> Bool Source # maximum :: Ord a => ErrorWithCause err a -> a Source # minimum :: Ord a => ErrorWithCause err a -> a Source # sum :: Num a => ErrorWithCause err a -> a Source # product :: Num a => ErrorWithCause err a -> a Source # | |||||
| Traversable (ErrorWithCause err) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause Methods traverse :: Applicative f => (a -> f b) -> ErrorWithCause err a -> f (ErrorWithCause err b) Source # sequenceA :: Applicative f => ErrorWithCause err (f a) -> f (ErrorWithCause err a) Source # mapM :: Monad m => (a -> m b) -> ErrorWithCause err a -> m (ErrorWithCause err b) Source # sequence :: Monad m => ErrorWithCause err (m a) -> m (ErrorWithCause err a) Source # | |||||
| Functor (ErrorWithCause err) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause Methods fmap :: (a -> b) -> ErrorWithCause err a -> ErrorWithCause err b Source # (<$) :: a -> ErrorWithCause err b -> ErrorWithCause err a Source # | |||||
| (PrettyPlc cause, PrettyPlc err, Typeable cause, Typeable err) => Exception (ErrorWithCause err cause) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause Methods toException :: ErrorWithCause err cause -> SomeException Source # fromException :: SomeException -> Maybe (ErrorWithCause err cause) Source # displayException :: ErrorWithCause err cause -> String Source # | |||||
| Generic (ErrorWithCause err cause) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause Associated Types
Methods from :: ErrorWithCause err cause -> Rep (ErrorWithCause err cause) x Source # to :: Rep (ErrorWithCause err cause) x -> ErrorWithCause err cause Source # | |||||
| (PrettyPlc cause, PrettyPlc err) => Show (ErrorWithCause err cause) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause | |||||
| (NFData err, NFData cause) => NFData (ErrorWithCause err cause) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause Methods rnf :: ErrorWithCause err cause -> () Source # | |||||
| (Eq err, Eq cause) => Eq (ErrorWithCause err cause) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause Methods (==) :: ErrorWithCause err cause -> ErrorWithCause err cause -> Bool Source # (/=) :: ErrorWithCause err cause -> ErrorWithCause err cause -> Bool Source # | |||||
| (Pretty err, Pretty cause) => Pretty (ErrorWithCause err cause) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause Methods pretty :: ErrorWithCause err cause -> Doc ann # prettyList :: [ErrorWithCause err cause] -> Doc ann # | |||||
| ThrowableBuiltins 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 # | |||||
| type Rep (ErrorWithCause err cause) Source # | |||||
Defined in PlutusCore.Evaluation.ErrorWithCause type Rep (ErrorWithCause err cause) = D1 ('MetaData "ErrorWithCause" "PlutusCore.Evaluation.ErrorWithCause" "plutus-core-1.60.0.0-LXFqBsoUlXsJIEqLytHte7" 'False) (C1 ('MetaCons "ErrorWithCause" 'PrefixI 'True) (S1 ('MetaSel ('Just "_ewcError") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 err) :*: S1 ('MetaSel ('Just "_ewcCause") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe cause)))) | |||||
splitStructuralOperational :: Either (EvaluationException structural operational term) a -> Either (ErrorWithCause structural term) (EvaluationResult a) Source #
Preserve the contents of an StructuralError as a Left and turn an
OperationalError into a Right EvaluationFailure (thus erasing the content of the
error in the latter case).
unsafeSplitStructuralOperational :: (PrettyPlc structural, PrettyPlc term, Typeable structural, Typeable term) => Either (EvaluationException structural operational term) a -> EvaluationResult a Source #
Throw on a StructuralError and turn an OperationalError into an
EvaluationFailure (thus erasing the content of the error in the latter case).
type ThrowableBuiltins (uni :: Type -> Type) fun = (PrettyUni uni, Pretty fun, Typeable uni, Typeable fun) Source #
The set of constraints we need to be able to throw exceptions with things with built-in types and functions in them.
data CekUserError Source #
Constructors
| CekCaseBuiltinError Text |
|
| CekOutOfExError !ExRestrictingBudget | The final overspent (i.e. negative) budget. |
| CekEvaluationFailure | Error has been called or a builtin application has failed |
Instances
| Generic CekUserError Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Associated Types
Methods from :: CekUserError -> Rep CekUserError x Source # to :: Rep CekUserError x -> CekUserError Source # | |||||
| Show CekUserError Source # | |||||
| NFData CekUserError Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods rnf :: CekUserError -> () Source # | |||||
| Eq CekUserError Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods (==) :: CekUserError -> CekUserError -> Bool Source # (/=) :: CekUserError -> CekUserError -> Bool Source # | |||||
| Pretty CekUserError Source # | |||||
| BuiltinErrorToEvaluationError (MachineError fun) CekUserError Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods builtinErrorToEvaluationError :: BuiltinError -> EvaluationError (MachineError fun) CekUserError Source # | |||||
| ThrowableBuiltins 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 # | |||||
| type Rep CekUserError Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal type Rep CekUserError = D1 ('MetaData "CekUserError" "UntypedPlutusCore.Evaluation.Machine.Cek.Internal" "plutus-core-1.60.0.0-LXFqBsoUlXsJIEqLytHte7" 'False) (C1 ('MetaCons "CekCaseBuiltinError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: (C1 ('MetaCons "CekOutOfExError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ExRestrictingBudget)) :+: C1 ('MetaCons "CekEvaluationFailure" 'PrefixI 'False) (U1 :: Type -> Type))) | |||||
type CekEvaluationException name (uni :: Type -> Type) fun = EvaluationException (MachineError fun) CekUserError (Term name uni fun ()) Source #
The CEK machine-specific EvaluationException.
data ExBudgetCategory fun Source #
Constructors
| BStep StepKind | |
| BBuiltinApp fun | |
| BStartup |
Instances
| ExBudgetBuiltin fun (ExBudgetCategory fun) Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods exBudgetBuiltin :: fun -> ExBudgetCategory fun Source # | |||||
| Generic (ExBudgetCategory fun) Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Associated Types
Methods from :: ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x Source # to :: Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun Source # | |||||
| Show fun => Show (ExBudgetCategory fun) Source # | |||||
| NFData fun => NFData (ExBudgetCategory fun) Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods rnf :: ExBudgetCategory fun -> () Source # | |||||
| Eq fun => Eq (ExBudgetCategory fun) Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods (==) :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool Source # (/=) :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool Source # | |||||
| Ord fun => Ord (ExBudgetCategory fun) Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods compare :: ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering Source # (<) :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool Source # (<=) :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool Source # (>) :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool Source # (>=) :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool Source # max :: ExBudgetCategory fun -> ExBudgetCategory fun -> ExBudgetCategory fun Source # min :: ExBudgetCategory fun -> ExBudgetCategory fun -> ExBudgetCategory fun Source # | |||||
| Hashable fun => Hashable (ExBudgetCategory fun) Source # | |||||
| Show fun => Pretty (ExBudgetCategory fun) Source # | |||||
| type Rep (ExBudgetCategory fun) Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal type Rep (ExBudgetCategory fun) = D1 ('MetaData "ExBudgetCategory" "UntypedPlutusCore.Evaluation.Machine.Cek.Internal" "plutus-core-1.60.0.0-LXFqBsoUlXsJIEqLytHte7" 'False) (C1 ('MetaCons "BStep" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 StepKind)) :+: (C1 ('MetaCons "BBuiltinApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 fun)) :+: C1 ('MetaCons "BStartup" 'PrefixI 'False) (U1 :: Type -> Type))) | |||||
newtype CekBudgetSpender (uni :: Type -> Type) 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
| |
newtype ExBudgetMode cost (uni :: Type -> Type) fun Source #
A budgeting mode to execute the CEK machine in.
Constructors
| ExBudgetMode | |
Fields
| |
Instances
| Bounded StepKind Source # | |||||
| Enum StepKind Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods succ :: StepKind -> StepKind Source # pred :: StepKind -> StepKind Source # toEnum :: Int -> StepKind Source # fromEnum :: StepKind -> Int Source # enumFrom :: StepKind -> [StepKind] Source # enumFromThen :: StepKind -> StepKind -> [StepKind] Source # enumFromTo :: StepKind -> StepKind -> [StepKind] Source # enumFromThenTo :: StepKind -> StepKind -> StepKind -> [StepKind] Source # | |||||
| Generic StepKind Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Associated Types
| |||||
| Show StepKind Source # | |||||
| NFData StepKind Source # | |||||
| Eq StepKind Source # | |||||
| Ord StepKind Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal | |||||
| Hashable StepKind Source # | |||||
| type Rep StepKind Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal type Rep StepKind = D1 ('MetaData "StepKind" "UntypedPlutusCore.Evaluation.Machine.Cek.Internal" "plutus-core-1.60.0.0-LXFqBsoUlXsJIEqLytHte7" 'False) (((C1 ('MetaCons "BConst" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BVar" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BLamAbs" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BApply" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BDelay" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BForce" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BBuiltin" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BConstr" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BCase" 'PrefixI 'False) (U1 :: Type -> Type))))) | |||||
data CekResult name (uni :: Type -> Type) fun Source #
The result of evaluating a term with the CEK machine.
Constructors
| CekFailure (CekEvaluationException name uni fun) | |
| CekSuccessConstant (Some (ValueOf uni)) | |
| CekSuccessNonConstant (Term name uni fun ()) |
data CekReport cost name (uni :: Type -> Type) fun Source #
All info produced by a CEK machine run.
Constructors
| CekReport | |
Fields
| |
cekResultToEither :: forall name (uni :: Type -> Type) fun. CekResult name uni fun -> Either (CekEvaluationException name uni fun) (Term name uni fun ()) Source #
data CekValue (uni :: Type -> Type) fun ann Source #
Constructors
| VCon !(Some (ValueOf uni)) | |
| VDelay !(NTerm uni fun ann) !(CekValEnv uni fun ann) | |
| VLamAbs !NamedDeBruijn !(NTerm uni fun ann) !(CekValEnv uni fun ann) | |
| VBuiltin | A partial builtin application, accumulating arguments for eventual full application.
We don't need a |
Fields
| |
| VConstr !Word64 !(EmptyOrMultiStack uni fun ann) | |
Instances
| (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun ann) Source # | |
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods prettyBy :: PrettyConfigPlc -> CekValue uni fun ann -> Doc ann0 # prettyListBy :: PrettyConfigPlc -> [CekValue uni fun ann] -> Doc ann0 # | |
| Show (BuiltinRuntime (CekValue uni fun ann)) Source # | |
| (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni) => Show (CekValue uni fun ann) Source # | |
| HasConstant (CekValue uni fun ann) Source # | |
| (Closed uni, Everywhere uni ExMemoryUsage) => ExMemoryUsage (CekValue uni fun ann) Source # | |
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods memoryUsage :: CekValue uni fun ann -> CostRose Source # | |
| type UniOf (CekValue uni fun ann) Source # | |
data DischargeResult (uni :: Type -> Type) fun Source #
The result of dischargeCekValue.
Constructors
| DischargeConstant (Some (ValueOf uni)) | |
| DischargeNonConstant (NTerm uni fun ()) |
Instances
| (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (DischargeResult uni fun) Source # | |
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods prettyBy :: PrettyConfigPlc -> DischargeResult uni fun -> Doc ann # prettyListBy :: PrettyConfigPlc -> [DischargeResult uni fun] -> Doc ann # | |
| (GShow uni, Everywhere uni Show, Show fun, Closed uni) => Show (DischargeResult uni fun) Source # | |
| (GEq uni, Everywhere uni Eq, Eq fun, Closed uni) => Eq (DischargeResult uni fun) Source # | |
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Methods (==) :: DischargeResult uni fun -> DischargeResult uni fun -> Bool Source # (/=) :: DischargeResult uni fun -> DischargeResult uni fun -> Bool Source # | |
dischargeResultToTerm :: forall (uni :: Type -> Type) fun. DischargeResult uni fun -> NTerm uni fun () Source #
newtype EmitterMode (uni :: Type -> Type) fun Source #
An emitting mode to execute the CEK machine in, similar to ExBudgetMode.
Constructors
| EmitterMode | |
Fields
| |
mapTermCekResult :: forall name (uni :: Type -> Type) fun name'. (Term name uni fun () -> Term name' uni fun ()) -> CekResult name uni fun -> CekResult name' uni fun Source #
data ArgStack (uni :: Type -> Type) fun ann Source #
A LIFO stack of CekValues, used to record multiple arguments that need to be pushed
onto the context in reverse order. Currently used by FrameConstr for collecting the
elements of a Constr as it is cheap to prepend new elements in ArgStack.
data EmptyOrMultiStack (uni :: Type -> Type) fun ann Source #
An alternative version of ArgStack that uses ArgNonEmptyStack when non-empty.
Used in VConstr. Once all evaluated elements of Constr is collecting to ArgStack
in FrameConstr, the collected elements gets reversed and put into VConstr as
EmptyOrMultiStack. VConstr using EmptyOrMultiStack is more efficient than ArgStack when casing,
since FrameAwaitFunValueN can be dispatched with a single pattern match.
Constructors
| EmptyStack | |
| MultiStack !(ArgStackNonEmpty uni fun ann) |
Instances
| (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni) => Show (EmptyOrMultiStack uni fun ann) Source # | |
data ArgStackNonEmpty (uni :: Type -> Type) fun ann Source #
A non-empty variant of ArgStack, used in FrameAwaitFunValueN to store arguments
that will be applied to a term. More efficient than ArgStack, since this saves one
evaluation cycle by ensuring there is no NilStack.
Constructors
| LastStackNonEmpty !(CekValue uni fun ann) | |
| ConsStackNonEmpty !(CekValue uni fun ann) !(ArgStackNonEmpty uni fun ann) |
Instances
| (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni) => Show (ArgStackNonEmpty uni fun ann) Source # | |
data ExBudgetInfo cost (uni :: Type -> Type) fun s Source #
Runtime budgeting info.
Constructors
| ExBudgetInfo | |
Fields
| |
type CekEmitter (uni :: Type -> Type) fun s = DList Text -> CekM uni fun s () Source #
The CEK machine is parameterized over an emitter function, similar to CekBudgetSpender.
data CekEmitterInfo (uni :: Type -> Type) fun s Source #
Runtime emitter info, similar to ExBudgetInfo.
Constructors
| CekEmitterInfo | |
Fields
| |
newtype CekM (uni :: Type -> Type) fun s a Source #
The monad the CEK machine runs in.
Instances
| 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 # | |||||
| Functor (CekM uni fun s) Source # | |||||
| Monad (CekM uni fun s) Source # | |||||
| PrimMonad (CekM uni fun s) Source # | |||||
Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal Associated Types
| |||||
| ThrowableBuiltins 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 # | |||||
| type PrimState (CekM uni fun s) Source # | |||||
dischargeCekValue :: forall (uni :: Type -> Type) fun ann. CekValue uni fun ann -> DischargeResult uni fun Source #
type GivenCekReqs (uni :: Type -> Type) fun ann s = (GivenCekRuntime uni fun ann, GivenCekCaserBuiltin uni, GivenCekEmitter uni fun s, GivenCekSpender uni fun s, GivenCekSlippage, GivenCekStepCounter s, GivenCekCosts) Source #
Constraint requiring all of the machine's implicit parameters.
type GivenCekSpender (uni :: Type -> Type) fun s = ?cekBudgetSpender :: CekBudgetSpender uni fun s Source #
Implicit parameter for budget spender.
data StepCounter (n :: Nat) s Source #
A set of Word8 counters that is used in the CEK machine
to count steps.
type NumberOfStepCounters = CountConstructorsEnum (Rep StepKind) Source #
The number of step counters that we need, should be the same as the number of constructors
of StepKind.
type CounterSize = NumberOfStepCounters + 1 Source #
The total number of counters that we need, one extra for the total counter. See Note [Structure of the step counter]
type TotalCountIndex = NumberOfStepCounters Source #
The index at which the total step counter is kept. See Note [Structure of the step counter]
defaultSlippage :: Slippage Source #
The default number of slippage (in machine steps) to allow.
type NTerm (uni :: Type -> Type) fun = Term NamedDeBruijn uni fun Source #
The Terms that CEK can execute must have DeBruijn binders
Name is not necessary but we leave it here for simplicity and debuggability.
runCekM :: forall cost (uni :: Type -> Type) fun ann. ThrowableBuiltins uni fun => MachineParameters CekMachineCosts fun (CekValue uni fun ann) -> ExBudgetMode cost uni fun -> EmitterMode uni fun -> (forall s. GivenCekReqs uni fun ann s => CekM uni fun s (DischargeResult uni fun)) -> CekReport cost NamedDeBruijn uni fun Source #