Get forward analysis working again

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Analysis/Forward.agda

@@ -145,25 +145,33 @@ module WithProg (prog : Program) where
         -- also monotonically; we derive the for-each-state update from
         -- the Exercise 4.26 again.
 
+        updateVariablesFromStmt : BasicStmt → VariableValues → VariableValues
+        updateVariablesFromStmt (k ← e) vs = updateVariablesFromExpression k e vs
+        updateVariablesFromStmt noop vs = vs
+
+        updateVariablesFromStmt-Monoʳ : ∀ (bs : BasicStmt) → Monotonic _≼ᵛ_ _≼ᵛ_ (updateVariablesFromStmt bs)
+        updateVariablesFromStmt-Monoʳ (k ← e) {vs₁} {vs₂} vs₁≼vs₂ = updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂
+        updateVariablesFromStmt-Monoʳ noop vs₁≼vs₂ = vs₁≼vs₂
+
         updateVariablesForState : State → StateVariables → VariableValues
-        updateVariablesForState s sv
+        updateVariablesForState s sv =
-            with code s
+            let
-        ...   | k ← e =
+                bss = code s
-                let
+                (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
-                    updateVariablesFromExpression k e vs
 
         updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
-        updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂
+        updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ =
-            with code s
+            let
-        ...   | k ← e =
+                bss = code s
-                let
+                (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₂ , 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
-                    updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂
+                            updateVariablesFromStmt updateVariablesFromStmt-Monoʳ
+                            vs₁≼vs₂
 
         open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
             renaming

Language.agda

@@ -499,10 +499,10 @@ record Program : Set where
     open Graphs
 
     field
-        prog : Stmt
+        rootStmt : Stmt
 
     private
-        buildResult = Construction.buildCfg prog empty
+        buildResult = Construction.buildCfg rootStmt empty
 
     graph : Graph
     graph = proj₁ buildResult
@@ -518,7 +518,7 @@ record Program : Set where
 
     private
         vars-Set : StringSet
-        vars-Set = Stmt-vars prog
+        vars-Set = Stmt-vars rootStmt
 
     vars : List String
     vars = to-Listˢ vars-Set

Lattice.agda

@@ -150,6 +150,21 @@ module _ {a b} {A : Set a} {B : Set b}
         ≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
                  (f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))
 
+module _ {a b} {A : Set a} {B : Set b}
+         {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
+         (lB : IsSemilattice B _≈₂_ _⊔₂_) where
+
+    open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
+
+    open import Data.List as List using (List; foldr; _∷_)
+    open import Utils using (Pairwise; _∷_)
+
+    foldr-Mono' : ∀ (l : List A) (f : A → B → B) →
+                  (∀ a → Monotonic _≼₂_ _≼₂_ (f a)) →
+                  Monotonic _≼₂_ _≼₂_ (λ b → foldr f b l)
+    foldr-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
+    foldr-Mono' (x ∷ xs) f f-Mono₂ b₁≼b₂ = f-Mono₂ x (foldr-Mono' xs f f-Mono₂ b₁≼b₂)
+
 record IsLattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A)