DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Use foldl in multi-statement evaluation

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-08 21:50:38 -07:00
parent dd8cdcd10c
commit 1b8bea8957
1 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Analysis/Forward.agda
View File

@ -11,13 +11,13 @@ open import Data.Empty using (⊥-elim)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Data.Nat using (suc) open import Data.Nat using (suc)
open import Data.Product using (_×_; proj₁; _,_) 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.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
open import Data.List.Relation.Unary.Any as Any using () open import Data.List.Relation.Unary.Any as Any using ()
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Unit using (⊤) open import Data.Unit using (⊤)
open import Function using (_∘_) open import Function using (_∘_; flip)
open import Utils using (Pairwise) open import Utils using (Pairwise)
import Lattice.FiniteValueMap import Lattice.FiniteValueMap
@ -164,7 +164,7 @@ module WithProg (prog : Program) where
bss = code s bss = code s
(vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv) (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
in in
foldr updateVariablesFromStmt vs bss foldl (flip updateVariablesFromStmt) vs bss
updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s) updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ = 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₂ , 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₂ vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂
in in
foldr-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss foldl-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
updateVariablesFromStmt updateVariablesFromStmt-Monoʳ (flip updateVariablesFromStmt) updateVariablesFromStmt-Monoʳ
vs₁≼vs₂ vs₁≼vs₂
open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states