@@ -714,7 +714,7 @@ data Context uni fun ann
714
714
| FrameCases ! (CekValEnv uni fun ann ) ! (V. Vector (NTerm uni fun ann )) ! (Context uni fun ann )
715
715
-- ^ @(case _ C0 .. Cn)@
716
716
| FrameAwaitLetBinds ! (CekValEnv uni fun ann ) ! (NTerm uni fun ann ) ! [NTerm uni fun ann ] ! [CekValue uni fun ann ] ! (Context uni fun ann )
717
- | FrameMine ! [CekValue uni fun ann ] ! (Context uni fun ann )
717
+ | FrameAwaitLet ! [CekValue uni fun ann ] ! (Context uni fun ann )
718
718
| NoFrame
719
719
720
720
deriving stock instance (GShow uni , Everywhere uni Show , Show fun , Show ann , Closed uni )
@@ -892,9 +892,10 @@ enterComputeCek = computeCek
892
892
SpineLast arg -> applyEvaluate ctx fun (VCon arg)
893
893
SpineCons arg rest -> applyEvaluate (FrameAwaitFunConN rest ctx) fun (VCon arg)
894
894
-- s , [_ V1 .. Vn] ◅ lam x (M,ρ) ↦ s , [_ V2 .. Vn]; ρ [ x ↦ V1 ] ▻ M
895
- returnCek (FrameMine args ctx) l =
895
+ returnCek (FrameAwaitLet args ctx) l =
896
896
case l of
897
- VLet _ body env -> computeCek ctx (foldr Env. cons env args) body
897
+ VLet names body env
898
+ | length names == length args -> computeCek ctx (foldr Env. cons env args) body
898
899
_ -> error " no"
899
900
900
901
returnCek (FrameAwaitFunValueN args ctx) fun =
@@ -938,7 +939,7 @@ enterComputeCek = computeCek
938
939
returnCek (FrameAwaitLetBinds env l todo done ctx) e =
939
940
case todo of
940
941
(next : todo') -> computeCek (FrameAwaitLetBinds env l todo' (e : done) ctx) env next
941
- [] -> computeCek (FrameMine (e : done) ctx) env l
942
+ [] -> computeCek (FrameAwaitLet (e : done) ctx) env l
942
943
943
944
-- | @force@ a term and proceed.
944
945
-- If v is a delay then compute the body of v;
0 commit comments