Add unproven lemma about fold implication

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

Analysis/Forward.agda

@@ -80,6 +80,7 @@ module WithProg (prog : Program) where
         renaming
             ( FiniteMap to StateVariables
             ; isLattice to isLatticeᵐ
+            ; _≈_ to _≈ᵐ_
             ; _∈k_ to _∈kᵐ_
             ; locate to locateᵐ
             ; _≼_ to _≼ᵐ_
@@ -92,6 +93,11 @@ module WithProg (prog : Program) where
         renaming
             ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
             )
+    open IsFiniteHeightLattice isFiniteHeightLatticeᵐ
+        using ()
+        renaming
+            ( ≈-sym to ≈ᵐ-sym
+            )
 
     ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
     fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
@@ -107,6 +113,9 @@ module WithProg (prog : Program) where
     variablesAt : State → StateVariables → VariableValues
     variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
 
+    variablesAt-≈ : ∀ s sv₁ sv₂ → sv₁ ≈ᵐ sv₂ → variablesAt s sv₁ ≈ᵛ variablesAt s sv₂
+    variablesAt-≈ = {!!}
+
     -- build up the 'join' function, which follows from Exercise 4.26's
     --
     --    L₁ → (A → L₂)
@@ -238,6 +247,10 @@ module WithProg (prog : Program) where
                 in
                     ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
 
+            ⟦⟧ᵛ-foldr : ∀ {vs : VariableValues} {vss : List VariableValues} {ρ : Env} →
+                        ⟦ vs ⟧ᵛ ρ → vs ∈ˡ vss → ⟦ foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ
+            ⟦⟧ᵛ-foldr = {!!}
+
             InterpretationValid : Set
             InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
 
@@ -270,3 +283,18 @@ module WithProg (prog : Program) where
                 updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
                 updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ rewrite variablesAt-updateAll s sv =
                     updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
+
+
+                stepTrace : ∀ {s₁ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → ρ₁ , (code s₁) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s₁ result ⟧ᵛ ρ₂
+                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)
+                        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⇒ρ₂

Language.agda

@@ -2,6 +2,7 @@ module Language where
 
 open import Language.Base public
 open import Language.Semantics public
+open import Language.Traces public
 open import Language.Graphs public
 open import Language.Properties public
 

Main.agda

@@ -13,6 +13,25 @@ testCode =
     ⟨ "neg" ← ((` "zero") Expr.- (# 1)) ⟩ then
     ⟨ "unknown" ← ((` "pos") Expr.+ (` "neg")) ⟩
 
+testCodeCond₁ : Stmt
+testCodeCond₁ =
+    ⟨ "var" ← (# 1) ⟩ then
+    if (` "var") then (
+        ⟨ "var" ← ((` "var") Expr.+ (# 1)) ⟩
+    ) else (
+        ⟨ "var" ← ((` "var") Expr.- (# 1)) ⟩ then
+        ⟨ "var" ← (# 1) ⟩
+    )
+
+testCodeCond₂ : Stmt
+testCodeCond₂ =
+    ⟨ "var" ← (# 1) ⟩ then
+    if (` "var") then (
+        ⟨ "x" ← (# 1) ⟩
+    ) else (
+        ⟨ noop ⟩
+    )
+
 testProgram : Program
 testProgram = record
     { rootStmt = testCode