Skip to content

Commit

Permalink
Remove FrameExtra2
Browse files Browse the repository at this point in the history
  • Loading branch information
kwxm committed Jun 26, 2022
1 parent d11fdb4 commit adb631c
Showing 1 changed file with 0 additions and 3 deletions.
Expand Up @@ -525,7 +525,6 @@ 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 @@ -681,8 +680,6 @@ 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 adb631c

Please sign in to comment.