Skip to content

Commit

Permalink
Make frames strict and have them include their own tail. (IntersectMB…
Browse files Browse the repository at this point in the history 
…O#3432)

This lets us match once on a known, tagged context value
instead of matching on an unknown list and then an unknown frame.
  • Loading branch information
@michaelpj
michaelpj authored Jun 25, 2021
1 parent ee30190 commit 0c66016
Showing 1 changed file with 33 additions and 28 deletions.
61 changes: 33 additions & 28 deletions plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -515,13 +515,18 @@ instance AsConstant (CekValue uni fun) where
asConstant (VCon val) = pure val
asConstant term = throwNotAConstant term

data Frame uni fun
= FrameApplyFun (CekValue uni fun) -- ^ @[V _]@
| FrameApplyArg (CekValEnv uni fun) (Term Name uni fun ()) -- ^ @[_ N]@
| FrameForce -- ^ @(force _)@
deriving (Show)
{-|
The context in which the machine operates.
type Context uni fun = [Frame uni fun]
Morally, this is a stack of frames, but we use the "intrusive list" representation so that
we can match on context and the top frame in a single, strict pattern match.
-}
data Context uni fun
= FrameApplyFun (CekValue uni fun) !(Context uni fun) -- ^ @[V _]@
| FrameApplyArg (CekValEnv uni fun) (Term Name uni fun ()) !(Context uni fun) -- ^ @[_ N]@
| FrameForce !(Context uni fun) -- ^ @(force _)@
| NoFrame
deriving (Show)

toExMemory :: (Closed uni, uni `Everywhere` ExMemoryUsage) => CekValue uni fun -> ExMemory
toExMemory = \case
Expand Down Expand Up @@ -614,36 +619,36 @@ enterComputeCek = computeCek (toWordArray 0) where
-> Term Name uni fun ()
-> CekM uni fun s (Term Name uni fun ())
-- s ; ρ ▻ {L A} ↦ s , {_ A} ; ρ ▻ L
computeCek !unbudgetedSteps ctx env (Var _ varName) = do
computeCek !unbudgetedSteps !ctx env (Var _ varName) = do
!unbudgetedSteps' <- stepAndMaybeSpend BVar unbudgetedSteps
val <- lookupVarName varName env
returnCek unbudgetedSteps' ctx val
computeCek !unbudgetedSteps ctx _ (Constant _ val) = do
computeCek !unbudgetedSteps !ctx _ (Constant _ val) = do
!unbudgetedSteps' <- stepAndMaybeSpend BConst unbudgetedSteps
returnCek unbudgetedSteps' ctx (VCon val)
computeCek !unbudgetedSteps ctx env (LamAbs _ name body) = do
computeCek !unbudgetedSteps !ctx env (LamAbs _ name body) = do
!unbudgetedSteps' <- stepAndMaybeSpend BLamAbs unbudgetedSteps
returnCek unbudgetedSteps' ctx (VLamAbs name body env)
computeCek !unbudgetedSteps ctx env (Delay _ body) = do
computeCek !unbudgetedSteps !ctx env (Delay _ body) = do
!unbudgetedSteps' <- stepAndMaybeSpend BDelay unbudgetedSteps
returnCek unbudgetedSteps' ctx (VDelay body env)
-- s ; ρ ▻ lam x L ↦ s ◅ lam x (L , ρ)
computeCek !unbudgetedSteps ctx env (Force _ body) = do
computeCek !unbudgetedSteps !ctx env (Force _ body) = do
!unbudgetedSteps' <- stepAndMaybeSpend BForce unbudgetedSteps
computeCek unbudgetedSteps' (FrameForce : ctx) env body
computeCek unbudgetedSteps' (FrameForce ctx) env body
-- s ; ρ ▻ [L M] ↦ s , [_ (M,ρ)] ; ρ ▻ L
computeCek !unbudgetedSteps ctx env (Apply _ fun arg) = do
computeCek !unbudgetedSteps !ctx env (Apply _ fun arg) = do
!unbudgetedSteps' <- stepAndMaybeSpend BApply unbudgetedSteps
computeCek unbudgetedSteps' (FrameApplyArg env arg : ctx) env fun
computeCek unbudgetedSteps' (FrameApplyArg env arg ctx) env fun
-- s ; ρ ▻ abs α L ↦ s ◅ abs α (L , ρ)
-- s ; ρ ▻ con c ↦ s ◅ con c
-- s ; ρ ▻ builtin bn ↦ s ◅ builtin bn arity arity [] [] ρ
computeCek !unbudgetedSteps ctx env term@(Builtin _ bn) = do
computeCek !unbudgetedSteps !ctx env term@(Builtin _ bn) = do
!unbudgetedSteps' <- stepAndMaybeSpend BBuiltin unbudgetedSteps
meaning <- lookupBuiltin bn ?cekRuntime
returnCek unbudgetedSteps' ctx (VBuiltin bn term env meaning)
-- s ; ρ ▻ error A ↦ <> A
computeCek !_ _ _ (Error _) =
computeCek !_ !_ _ (Error _) =
throwing_ _EvaluationFailure

{- | The returning phase of the CEK machine.
Expand All @@ -658,17 +663,17 @@ enterComputeCek = computeCek (toWordArray 0) where
returnCek :: WordArray -> Context uni fun -> CekValue uni fun -> CekM uni fun s (Term Name uni fun ())
--- Instantiate all the free variable of the resulting term in case there are any.
-- . ◅ V ↦ [] V
returnCek !unbudgetedSteps [] val = do
returnCek !unbudgetedSteps NoFrame val = do
spendAccumulatedBudget unbudgetedSteps
pure $ dischargeCekValue val
-- s , {_ A} ◅ abs α M ↦ s ; ρ ▻ M [ α / A ]*
returnCek !unbudgetedSteps (FrameForce : ctx) fun = forceEvaluate unbudgetedSteps ctx fun
returnCek !unbudgetedSteps (FrameForce ctx) fun = forceEvaluate unbudgetedSteps ctx fun
-- s , [_ (M,ρ)] ◅ V ↦ s , [V _] ; ρ ▻ M
returnCek !unbudgetedSteps (FrameApplyArg argVarEnv arg : ctx) fun =
computeCek unbudgetedSteps (FrameApplyFun fun : ctx) argVarEnv arg
returnCek !unbudgetedSteps (FrameApplyArg argVarEnv arg ctx) fun =
computeCek unbudgetedSteps (FrameApplyFun fun ctx) argVarEnv arg
-- s , [(lam x (M,ρ)) _] ◅ V ↦ s ; ρ [ x ↦ V ] ▻ M
-- FIXME: add rule for VBuiltin once it's in the specification.
returnCek !unbudgetedSteps (FrameApplyFun fun : ctx) arg =
returnCek !unbudgetedSteps (FrameApplyFun fun ctx) arg =
applyEvaluate unbudgetedSteps ctx fun arg

-- | @force@ a term and proceed.
Expand All @@ -682,8 +687,8 @@ enterComputeCek = computeCek (toWordArray 0) where
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term Name uni fun ())
forceEvaluate !unbudgetedSteps ctx (VDelay body env) = computeCek unbudgetedSteps ctx env body
forceEvaluate !unbudgetedSteps ctx (VBuiltin fun term env (BuiltinRuntime sch f exF)) = do
forceEvaluate !unbudgetedSteps !ctx (VDelay body env) = computeCek unbudgetedSteps ctx env body
forceEvaluate !unbudgetedSteps !ctx (VBuiltin fun term env (BuiltinRuntime sch f exF)) = do
let term' = Force () term
case sch of
-- It's only possible to force a builtin application if the builtin expects a type
Expand All @@ -697,7 +702,7 @@ enterComputeCek = computeCek (toWordArray 0) where
returnCek unbudgetedSteps ctx res
_ ->
throwingWithCause _MachineError BuiltinTermArgumentExpectedMachineError (Just term')
forceEvaluate !_ _ val =
forceEvaluate !_ !_ val =
throwingDischarged _MachineError NonPolymorphicInstantiationMachineError val

-- | Apply a function to an argument and proceed.
Expand All @@ -713,11 +718,11 @@ enterComputeCek = computeCek (toWordArray 0) where
-> CekValue uni fun -- lhs of application
-> CekValue uni fun -- rhs of application
-> CekM uni fun s (Term Name uni fun ())
applyEvaluate !unbudgetedSteps ctx (VLamAbs name body env) arg =
applyEvaluate !unbudgetedSteps !ctx (VLamAbs name body env) arg =
computeCek unbudgetedSteps ctx (extendEnv name arg env) body
-- Annotating @f@ and @exF@ with bangs gave us some speed-up, but only until we added a bang to
-- 'VCon'. After that the bangs here were making things a tiny bit slower and so we removed them.
applyEvaluate !unbudgetedSteps ctx (VBuiltin fun term env (BuiltinRuntime sch f exF)) arg = do
applyEvaluate !unbudgetedSteps !ctx (VBuiltin fun term env (BuiltinRuntime sch f exF)) arg = do
let term' = Apply () term $ dischargeCekValue arg
case sch of
-- It's only possible to apply a builtin application if the builtin expects a term
Expand All @@ -734,7 +739,7 @@ enterComputeCek = computeCek (toWordArray 0) where
returnCek unbudgetedSteps ctx res
_ ->
throwingWithCause _MachineError UnexpectedBuiltinTermArgumentMachineError (Just term')
applyEvaluate !_ _ val _ =
applyEvaluate !_ !_ val _ =
throwingDischarged _MachineError NonFunctionalApplicationMachineError val

-- | Spend the budget that has been accumulated for a number of machine steps.
Expand Down Expand Up @@ -773,4 +778,4 @@ runCek
runCek params mode emitting term =
runCekM params mode emitting $ do
spendBudgetCek BStartup (cekStartupCost ?cekCosts)
enterComputeCek [] mempty term
enterComputeCek NoFrame mempty term

0 comments on commit 0c66016

Please sign in to comment.