@@ -246,6 +246,7 @@ data CekValue uni fun ann =
246
246
-- Check the docs of 'BuiltinRuntime' for details.
247
247
-- | A constructor value, including fully computed arguments and the tag.
248
248
| VConstr {- # UNPACK #-} !Word64 ! (ArgStack uni fun ann )
249
+ | VBlackHole ! Text ! Word64
249
250
250
251
deriving stock instance (GShow uni , Everywhere uni Show , Show fun , Show ann , Closed uni )
251
252
=> Show (CekValue uni fun ann )
@@ -508,7 +509,10 @@ dischargeCekValEnv valEnv = go 0
508
509
-- var is free, leave it alone
509
510
var
510
511
-- var is in the env, discharge its value
511
- dischargeCekValue
512
+ (\ case
513
+ VBlackHole recName recLamCnt ->
514
+ Var () (NamedDeBruijn recName . coerce $ lamCnt - recLamCnt)
515
+ val -> dischargeCekValue val)
512
516
-- index relative to (as seen from the point of view of) the environment
513
517
(Env. indexOne valEnv $ idx - lamCnt)
514
518
Apply ann fun arg -> Apply ann (go lamCnt fun) $ go lamCnt arg
@@ -537,6 +541,7 @@ dischargeCekValue = \case
537
541
stack2list = go []
538
542
go acc EmptyStack = acc
539
543
go acc (ConsStack arg rest) = go (arg : acc) rest
544
+ VBlackHole _ _ -> error " can't happen"
540
545
541
546
instance (PrettyUni uni , Pretty fun ) => PrettyBy PrettyConfigPlc (CekValue uni fun ann ) where
542
547
prettyBy cfg = prettyBy cfg . dischargeCekValue
@@ -571,7 +576,7 @@ data Context uni fun ann
571
576
-- ^ @(constr i V0 ... Vj-1 _ Nj ... Nn)@
572
577
| FrameCases ! (CekValEnv uni fun ann ) ! (V. Vector (NTerm uni fun ann )) ! (Context uni fun ann )
573
578
-- ^ @(case _ C0 .. Cn)@
574
- | FrameFix ! (Context uni fun ann )
579
+ | FrameFix {- # UNPACK # -} ! Word64 ! (Context uni fun ann )
575
580
| NoFrame
576
581
577
582
deriving stock instance (GShow uni , Everywhere uni Show , Show fun , Show ann , Closed uni )
@@ -580,11 +585,12 @@ deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Clo
580
585
-- See Note [ExMemoryUsage instances for non-constants].
581
586
instance (Closed uni , uni `Everywhere ` ExMemoryUsage ) => ExMemoryUsage (CekValue uni fun ann ) where
582
587
memoryUsage = \ case
583
- VCon c -> memoryUsage c
584
- VDelay {} -> singletonRose 1
585
- VLamAbs {} -> singletonRose 1
586
- VBuiltin {} -> singletonRose 1
587
- VConstr {} -> singletonRose 1
588
+ VCon c -> memoryUsage c
589
+ VDelay {} -> singletonRose 1
590
+ VLamAbs {} -> singletonRose 1
591
+ VBuiltin {} -> singletonRose 1
592
+ VConstr {} -> singletonRose 1
593
+ VBlackHole {} -> singletonRose 1
588
594
{-# INLINE memoryUsage #-}
589
595
590
596
{- Note [ArgStack vs Spine]
@@ -703,9 +709,10 @@ enterComputeCek = computeCek
703
709
computeCek ! ctx ! env (Case _ scrut cs) = do
704
710
stepAndMaybeSpend BCase
705
711
computeCek (FrameCases env cs ctx) env scrut
706
- computeCek ! ctx ! env (Fix _ _ body) = do
712
+ computeCek ! ctx ! env (Fix _ rec body) = do
707
713
stepAndMaybeSpend BFix
708
- computeCek (FrameFix ctx) env body
714
+ let ! len' = Env. length env + 1
715
+ computeCek (FrameFix len' ctx) (Env. cons (VBlackHole (ndbnString rec ) len') env) body
709
716
-- s ; ρ ▻ error ↦ <> A
710
717
computeCek ! _ ! _ (Error _) =
711
718
throwing_ _EvaluationFailure
@@ -759,12 +766,12 @@ enterComputeCek = computeCek
759
766
Just t -> computeCek (transferArgStack args ctx) env t
760
767
Nothing -> throwingDischarged _MachineError (MissingCaseBranch i) e
761
768
_ -> throwingDischarged _MachineError NonConstrScrutinized e
762
- returnCek (FrameFix ctx) bodyV =
769
+ returnCek (FrameFix recIx ctx) bodyV =
763
770
case bodyV of
764
- VLamAbs nameArg bodyLam env ->
765
- let env' = Env. cons bodyV' env
771
+ VLamAbs nameArg bodyLam env -> do
772
+ let env' = Env. contUpdateZero ( \ _ -> bodyV') env ( Env. length env - recIx)
766
773
bodyV' = VLamAbs nameArg bodyLam env'
767
- in returnCek ctx bodyV'
774
+ returnCek ctx bodyV'
768
775
_ -> throwingDischarged _MachineError NonLambdaFixedMachineError bodyV
769
776
770
777
-- | Evaluate a 'HeadSpine' by pushing the arguments (if any) onto the stack and proceeding with
0 commit comments