Skip to content

Commit

Permalink
Add a second new type of frame
Browse files Browse the repository at this point in the history
  • Loading branch information
kwxm committed Jun 26, 2022
1 parent 6ec5a87 commit d5fbf8d
Showing 1 changed file with 3 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -525,6 +525,7 @@ data Context uni fun
| FrameApplyArg !(CekValEnv uni fun) !(Term NamedDeBruijn uni fun ()) !(Context uni fun) -- ^ @[_ N]@
| FrameForce !(Context uni fun) -- ^ @(force _)@
| FrameExtra1 !(Context uni fun)
| FrameExtra2 !(Context uni fun)
| NoFrame
deriving stock (Show)

Expand Down Expand Up @@ -680,6 +681,8 @@ enterComputeCek = computeCek (toWordArray 0) where
-- FIXME: add rule for VBuiltin once it's in the specification.
returnCek !unbudgetedSteps (FrameExtra1 ctx) fun = forceEvaluate unbudgetedSteps ctx fun
-- s , [_ (M,ρ)] ◅ V ↦ s , [V _] ; ρ ▻ M
returnCek !unbudgetedSteps (FrameExtra2 ctx) fun = forceEvaluate unbudgetedSteps ctx fun
-- s , [_ (M,ρ)] ◅ V ↦ s , [V _] ; ρ ▻ M
returnCek !unbudgetedSteps (FrameApplyFun fun ctx) arg =
applyEvaluate unbudgetedSteps ctx fun arg

Expand Down

0 comments on commit d5fbf8d

Please sign in to comment.