From 8dbee63de391e27dd7d2e32e24470973b41bad10 Mon Sep 17 00:00:00 2001 From: Ramsay Taylor Date: Tue, 6 Aug 2024 11:54:56 +0100 Subject: [PATCH] Clarified some comments. --- .../src/VerifiedCompilation/UForceDelay.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md index 9e7c4689c3b..650f2684dd1 100644 --- a/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md @@ -164,6 +164,7 @@ isForceDelay? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (Translation (FD isFD? : {X : Set} {{_ : DecEq X}} → (n nₐ : ℕ) → Binary.Decidable (FD n nₐ {X}) isFD? n nₐ ast ast' with isForce? isTerm? ast + -- If it doesn't start with force then it isn't going to match this translation, unless we have some delays left isFD? zero nₐ ast ast' | no ¬force = no λ { (forcefd .zero .nₐ x .ast' xx) → ¬force (isforce (isterm x)) ; (multiappliedfd .zero .nₐ x y x' y' x₁ xx) → ¬force (isforce (isterm (x · y))) ; (multiabstractfd .zero nₐ x x' xx) → ¬force (isforce (isterm (ƛ x))) } isFD? (suc n) nₐ ast ast' | no ¬force with (isDelay? isTerm? ast) @@ -192,8 +193,7 @@ isFD? n (suc nₐ ) ast ast' | yes (isforce (isterm t)) | no ¬isApp | yes (isla -- If we have zero in the application counter then we can't descend further isFD? n zero ast ast' | yes (isforce (isterm t)) | no ¬isApp | yes (islambda (isterm t₂)) = no λ { (forcefd .n .zero .(ƛ t₂) .ast' ()) } --- If we have matched none of the patterns then we need to consider nesting, which requires the --- sub-term to start with force +-- If we have matched none of the patterns then we need to consider nesting. isFD? n nₐ ast ast' | yes (isforce (isterm t)) | no ¬isApp | no ¬ƛ with isFD? (suc n) nₐ t ast' ... | yes p = yes (forcefd n nₐ t ast' p) ... | no ¬p = no λ { (forcefd .n .nₐ .t .ast' x) → ¬p x ; (multiappliedfd .n .nₐ x y x' y' x₁ x₂) → ¬isApp (isapp (isterm x) (isterm y)) ; (multiabstractfd .n nₐ x x' x₁) → ¬ƛ (islambda (isterm x)) }