From 20dc99ba1fb9c621bd280651ab461718dfea82ec Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 9 May 2024 16:57:03 -0700 Subject: [PATCH] Re-indent some code to take up less horizontal space Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index df88452..26d2e83 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -275,13 +275,17 @@ module WithProg (prog : Program) where updateVariablesFromStmt-fold-matches : ∀ {bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂ updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ = - updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁) + updateVariablesFromStmt-fold-matches + {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ + (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁) updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂ - updateVariablesForState-matches = updateVariablesFromStmt-fold-matches + updateVariablesForState-matches = + updateVariablesFromStmt-fold-matches updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂ - updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ rewrite variablesAt-updateAll s sv = + updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ + rewrite variablesAt-updateAll s sv = updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ @@ -289,12 +293,22 @@ module WithProg (prog : Program) where stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ = let -- I'd use rewrite, but Agda gets a memory overflow (?!). - ⟦joinAll-result⟧ρ₁ = subst (λ vs → ⟦ vs ⟧ᵛ ρ₁) (sym (variablesAt-joinAll s₁ result)) ⟦joinForKey-s₁⟧ρ₁ - ⟦analyze-result⟧ρ₂ = updateAll-matches {sv = joinAll result} ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁ - analyze-result≈result = ≈ᵐ-sym {result} {updateAll (joinAll result)} result≈analyze-result - analyze-s₁≈s₁ = variablesAt-≈ s₁ (updateAll (joinAll result)) result (analyze-result≈result) + ⟦joinAll-result⟧ρ₁ = + subst (λ vs → ⟦ vs ⟧ᵛ ρ₁) + (sym (variablesAt-joinAll s₁ result)) + ⟦joinForKey-s₁⟧ρ₁ + ⟦analyze-result⟧ρ₂ = + updateAll-matches {sv = joinAll result} + ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁ + analyze-result≈result = + ≈ᵐ-sym {result} {updateAll (joinAll result)} + result≈analyze-result + analyze-s₁≈s₁ = + variablesAt-≈ s₁ (updateAll (joinAll result)) + result (analyze-result≈result) in ⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ₂ walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂ - walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) = stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ + walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) = + stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂