@@ -244,6 +244,7 @@ data CekValue uni fun ann =
244
244
-- Check the docs of 'BuiltinRuntime' for details.
245
245
-- | A constructor value, including fully computed arguments and the tag.
246
246
| VConstr {- # UNPACK #-} !Word64 ! (ArgStack uni fun ann )
247
+ | VBlackHole ! Text ! Word64
247
248
248
249
deriving stock instance (GShow uni , Everywhere uni Show , Show fun , Show ann , Closed uni )
249
250
=> Show (CekValue uni fun ann )
@@ -492,7 +493,10 @@ dischargeCekValEnv valEnv = go 0
492
493
-- var is free, leave it alone
493
494
var
494
495
-- var is in the env, discharge its value
495
- dischargeCekValue
496
+ (\ case
497
+ VBlackHole recName recLamCnt ->
498
+ Var () (NamedDeBruijn recName . coerce $ lamCnt - recLamCnt)
499
+ val -> dischargeCekValue val)
496
500
-- index relative to (as seen from the point of view of) the environment
497
501
(Env. indexOne valEnv $ idx - lamCnt)
498
502
Apply ann fun arg -> Apply ann (go lamCnt fun) $ go lamCnt arg
@@ -521,6 +525,7 @@ dischargeCekValue = \case
521
525
stack2list = go []
522
526
go acc EmptyStack = acc
523
527
go acc (ConsStack arg rest) = go (arg : acc) rest
528
+ VBlackHole _ _ -> error " can't happen"
524
529
525
530
instance (PrettyUni uni , Pretty fun ) => PrettyBy PrettyConfigPlc (CekValue uni fun ann ) where
526
531
prettyBy cfg = prettyBy cfg . dischargeCekValue
@@ -555,7 +560,7 @@ data Context uni fun ann
555
560
-- ^ @(constr i V0 ... Vj-1 _ Nj ... Nn)@
556
561
| FrameCases ! (CekValEnv uni fun ann ) ! (V. Vector (NTerm uni fun ann )) ! (Context uni fun ann )
557
562
-- ^ @(case _ C0 .. Cn)@
558
- | FrameFix ! (Context uni fun ann )
563
+ | FrameFix {- # UNPACK # -} ! Word64 ! (Context uni fun ann )
559
564
| NoFrame
560
565
561
566
deriving stock instance (GShow uni , Everywhere uni Show , Show fun , Show ann , Closed uni )
@@ -564,11 +569,12 @@ deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Clo
564
569
-- See Note [ExMemoryUsage instances for non-constants].
565
570
instance (Closed uni , uni `Everywhere ` ExMemoryUsage ) => ExMemoryUsage (CekValue uni fun ann ) where
566
571
memoryUsage = \ case
567
- VCon c -> memoryUsage c
568
- VDelay {} -> singletonRose 1
569
- VLamAbs {} -> singletonRose 1
570
- VBuiltin {} -> singletonRose 1
571
- VConstr {} -> singletonRose 1
572
+ VCon c -> memoryUsage c
573
+ VDelay {} -> singletonRose 1
574
+ VLamAbs {} -> singletonRose 1
575
+ VBuiltin {} -> singletonRose 1
576
+ VConstr {} -> singletonRose 1
577
+ VBlackHole {} -> singletonRose 1
572
578
{-# INLINE memoryUsage #-}
573
579
574
580
{- Note [ArgStack vs Spine]
@@ -687,9 +693,10 @@ enterComputeCek = computeCek
687
693
computeCek ! ctx ! env (Case _ scrut cs) = do
688
694
stepAndMaybeSpend BCase
689
695
computeCek (FrameCases env cs ctx) env scrut
690
- computeCek ! ctx ! env (Fix _ _ body) = do
696
+ computeCek ! ctx ! env (Fix _ rec body) = do
691
697
stepAndMaybeSpend BFix
692
- computeCek (FrameFix ctx) env body
698
+ let ! len' = Env. length env + 1
699
+ computeCek (FrameFix len' ctx) (Env. cons (VBlackHole (ndbnString rec ) len') env) body
693
700
-- s ; ρ ▻ error ↦ <> A
694
701
computeCek ! _ ! _ (Error _) =
695
702
throwing_ _EvaluationFailure
@@ -743,12 +750,12 @@ enterComputeCek = computeCek
743
750
Just t -> computeCek (transferArgStack args ctx) env t
744
751
Nothing -> throwingDischarged _MachineError (MissingCaseBranch i) e
745
752
_ -> throwingDischarged _MachineError NonConstrScrutinized e
746
- returnCek (FrameFix ctx) bodyV =
753
+ returnCek (FrameFix recIx ctx) bodyV =
747
754
case bodyV of
748
- VLamAbs nameArg bodyLam env ->
749
- let env' = Env. cons bodyV' env
755
+ VLamAbs nameArg bodyLam env -> do
756
+ let env' = Env. contUpdateZero ( \ _ -> bodyV') env ( Env. length env - recIx)
750
757
bodyV' = VLamAbs nameArg bodyLam env'
751
- in returnCek ctx bodyV'
758
+ returnCek ctx bodyV'
752
759
_ -> throwingDischarged _MachineError NonLambdaFixedMachineError bodyV
753
760
754
761
-- | Evaluate a 'HeadSpine' by pushing the arguments (if any) onto the stack and proceeding with
0 commit comments