Skip to content

Commit

Permalink
Fix the Steppable CEK machine to correctly "pause/step" in case of SO…
Browse files Browse the repository at this point in the history
…Ps. (#6790)

Co-authored-by: Nikolaos Bezirgiannis <[email protected]>
  • Loading branch information
bezirg and bezirg authored Jan 15, 2025
1 parent 5266419 commit 23c0e64
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 4 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
### Fixed

- Fix the Steppable CEK machine to correctly "pause/step" in case of SOPs.
Original file line number Diff line number Diff line change
Expand Up @@ -157,13 +157,13 @@ computeCek !ctx !_ (Builtin _ bn) = do
-- s ; ρ ▻ constr I T0 .. Tn ↦ s , constr I _ (T1 ... Tn, ρ) ; ρ ▻ T0
computeCek !ctx !env (Constr ann i es) = do
stepAndMaybeSpend BConstr
case es of
(t : rest) -> computeCek (FrameConstr ann env i rest EmptyStack ctx) env t
[] -> returnCek ctx $ VConstr i EmptyStack
pure $ case es of
(t : rest) -> Computing (FrameConstr ann env i rest EmptyStack ctx) env t
[] -> Returning ctx $ VConstr i EmptyStack
-- s ; ρ ▻ case S C0 ... Cn ↦ s , case _ (C0 ... Cn, ρ) ; ρ ▻ S
computeCek !ctx !env (Case ann scrut cs) = do
stepAndMaybeSpend BCase
computeCek (FrameCases ann env cs ctx) env scrut
pure $ Computing (FrameCases ann env cs ctx) env scrut
-- s ; ρ ▻ error A ↦ <> A
computeCek !_ !_ (Error _) =
throwing_ _EvaluationFailure
Expand Down

0 comments on commit 23c0e64

Please sign in to comment.