From 1b8bea89572c46ea3ab34d49cc3fd09bd0906636 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 8 May 2024 21:50:38 -0700 Subject: [PATCH] Use foldl in multi-statement evaluation Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 4de15fb..9983432 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -11,13 +11,13 @@ open import Data.Empty using (⊥-elim) open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.Nat using (suc) open import Data.Product using (_×_; proj₁; _,_) -open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith) +open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) open import Data.List.Relation.Unary.Any as Any using () open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst) open import Relation.Nullary using (¬_; Dec; yes; no) open import Data.Unit using (⊤) -open import Function using (_∘_) +open import Function using (_∘_; flip) open import Utils using (Pairwise) import Lattice.FiniteValueMap @@ -164,7 +164,7 @@ module WithProg (prog : Program) where bss = code s (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv) in - foldr updateVariablesFromStmt vs bss + foldl (flip updateVariablesFromStmt) vs bss updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s) updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ = @@ -174,8 +174,8 @@ module WithProg (prog : Program) where (vs₂ , s,vs₂∈sv₂) = locateᵐ {s} {sv₂} (states-in-Map s sv₂) vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂ in - foldr-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss - updateVariablesFromStmt updateVariablesFromStmt-Monoʳ + foldl-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss + (flip updateVariablesFromStmt) updateVariablesFromStmt-Monoʳ vs₁≼vs₂ open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states