Get everything compiling

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

@@ -5,24 +5,27 @@ open import Data.Nat.Properties using (m≤n⇒m≤n+o; ≤-reflexive; +-assoc;
 open import Data.Integer using (ℤ; +_) renaming (_+_ to _+ᶻ_; _-_ to _-ᶻ_)
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
+open import Data.Product.Properties using (≡-dec)
 open import Data.Vec using (Vec; foldr; lookup; _∷_; []; _++_; cast)
-open import Data.Vec.Properties using (++-assoc; ++-identityʳ; lookup-++ˡ; lookup-cast₁)
+open import Data.Vec.Properties using (++-assoc; ++-identityʳ; lookup-++ˡ; lookup-cast₁; cast-sym)
 open import Data.Vec.Relation.Binary.Equality.Cast using (cast-is-id)
-open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ; _++_ to _++ˡ_)
+open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ; filter to filterᶠ; _++_ to _++ˡ_)
 open import Data.List.Properties using () renaming (++-assoc to ++ˡ-assoc; map-++ to mapˡ-++ˡ; ++-identityʳ to ++ˡ-identityʳ)
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
+open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any as RelAny using ()
 open import Data.List.Relation.Unary.Any.Properties using (++⁺ʳ)
 open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁; inject≤; _↑ʳ_; _↑ˡ_) renaming (_≟_ to _≟ᶠ_; cast to castᶠ)
-open import Data.Fin.Properties using (suc-injective)
+open import Data.Fin.Properties using (suc-injective) renaming (cast-is-id to castᶠ-is-id)
 open import Relation.Binary.PropositionalEquality as Eq using (subst; cong; _≡_; sym; trans; refl)
 open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Decidable.Core using (does)
 open import Function using (_∘_)
 open Eq.≡-Reasoning
 
 open import Lattice
-open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs; _⊗_; _,_)
+open import Utils using (Unique; Unique-map; push; x∈xs⇒fx∈fxs; _⊗_; _,_) renaming (empty to emptyᵘ; proj₁ to proj₁'; proj₂ to proj₂')
 
 data Expr : Set where
     _+_ : Expr → Expr → Expr
@@ -34,6 +37,7 @@ data BasicStmt : Set where
     _←_ : String → Expr → BasicStmt
     noop : BasicStmt
 
+infixr 2 _then_
 data Stmt : Set where
     ⟨_⟩ : BasicStmt → Stmt
     _then_ : Stmt → Stmt → Stmt
@@ -103,6 +107,13 @@ module Graphs where
             nodes : Vec (List BasicStmt) size
             edges : List Edge
 
+    empty : Graph
+    empty = record
+        { size = 0
+        ; nodes = []
+        ; edges = []
+        }
+
     ↑ˡ-Edge : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n +ⁿ m) × Fin (n +ⁿ m))
     ↑ˡ-Edge (idx₁ , idx₂) m = (idx₁ ↑ˡ m , idx₂ ↑ˡ m)
 
@@ -114,45 +125,64 @@ module Graphs where
         field
             n : ℕ
             sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ +ⁿ n
-            g₁[]≡g₂[] : ∀ (idx : Graph.Index g₁) →
+            newNodes : Vec (List BasicStmt) n
-                        lookup (Graph.nodes g₁) idx ≡
+            nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes
-                        lookup (cast sg₂≡sg₁+n (Graph.nodes g₂)) (idx ↑ˡ n)
             e∈g₁⇒e∈g₂ : ∀ {e : Graph.Edge g₁} →
                         e ∈ˡ (Graph.edges g₁) →
                         (↑ˡ-Edge e n) ∈ˡ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂))
 
+    castᵉ : ∀ {n m : ℕ} .(p : n ≡ m) → (Fin n × Fin n) → (Fin m × Fin m)
+    castᵉ p (idx₁ , idx₂) = (castᶠ p idx₁ , castᶠ p idx₂)
+
+    ↑ˡ-assoc : ∀ {s n₁ n₂} (f : Fin s) (p : s +ⁿ (n₁ +ⁿ n₂) ≡ s +ⁿ n₁ +ⁿ n₂) →
+               f ↑ˡ n₁ ↑ˡ n₂ ≡ castᶠ p (f ↑ˡ (n₁ +ⁿ n₂))
+    ↑ˡ-assoc zero p = refl
+    ↑ˡ-assoc {suc s'} {n₁} {n₂} (suc f') p rewrite ↑ˡ-assoc f' (sym (+-assoc s' n₁ n₂)) = refl
+
+    ↑ˡ-Edge-assoc : ∀ {s n₁ n₂} (e : Fin s × Fin s) (p : s +ⁿ (n₁ +ⁿ n₂) ≡ s +ⁿ n₁ +ⁿ n₂) →
+                    ↑ˡ-Edge (↑ˡ-Edge e n₁) n₂ ≡ castᵉ p (↑ˡ-Edge e (n₁ +ⁿ n₂))
+    ↑ˡ-Edge-assoc (idx₁ , idx₂) p
+        rewrite ↑ˡ-assoc idx₁ p
+        rewrite ↑ˡ-assoc idx₂ p = refl
+
+    ↑ˡ-identityʳ : ∀ {s} (f : Fin s) (p : s +ⁿ 0 ≡ s) →
+               f ≡ castᶠ p (f ↑ˡ 0)
+    ↑ˡ-identityʳ zero p = refl
+    ↑ˡ-identityʳ {suc s'} (suc f') p rewrite sym (↑ˡ-identityʳ f' (+-comm s' 0)) = refl
+
+    ↑ˡ-Edge-identityʳ : ∀ {s} (e : Fin s × Fin s) (p : s +ⁿ 0 ≡ s) →
+                        e ≡ castᵉ p (↑ˡ-Edge e 0)
+    ↑ˡ-Edge-identityʳ (idx₁ , idx₂) p
+        rewrite sym (↑ˡ-identityʳ idx₁ p)
+        rewrite sym (↑ˡ-identityʳ idx₂ p) = refl
+
+    cast∈⇒∈subst : ∀ {n m : ℕ} (p : n ≡ m) (q : m ≡ n)
+                   (e : Fin n × Fin n) (es : List (Fin m × Fin m)) →
+                   castᵉ p e ∈ˡ es →
+                   e ∈ˡ subst (λ m → List (Fin m × Fin m)) q es
+    cast∈⇒∈subst refl refl (idx₁ , idx₂) es e∈es
+        rewrite castᶠ-is-id refl idx₁
+        rewrite castᶠ-is-id refl idx₂ = e∈es
+
     ⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃
     ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃}
-            (Mk-⊆ n₁ p₁@refl g₁[]≡g₂[] e∈g₁⇒e∈g₂) (Mk-⊆ n₂ p₂@refl g₂[]≡g₃[] e∈g₂⇒e∈g₃) = record
+            (Mk-⊆ n₁ p₁@refl newNodes₁ nsg₂≡nsg₁++newNodes₁ e∈g₁⇒e∈g₂)
-        { n = n₁ +ⁿ n₂
+            (Mk-⊆ n₂ p₂@refl newNodes₂ nsg₃≡nsg₂++newNodes₂ e∈g₂⇒e∈g₃)
-        ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂
+        rewrite cast-is-id refl ns₂
-        ; g₁[]≡g₂[] = λ idx →
+        rewrite cast-is-id refl ns₃
-            begin
+        with refl ← nsg₂≡nsg₁++newNodes₁
-              lookup ns₁ idx
+        with refl ← nsg₃≡nsg₂++newNodes₂ =
-            ≡⟨ g₁[]≡g₂[] _ ⟩
+        record
-              lookup (cast p₁ ns₂) (idx ↑ˡ n₁)
+            { n = n₁ +ⁿ n₂
-            ≡⟨ lookup-cast₁ p₁ ns₂ _ ⟩
+            ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂
-              lookup ns₂ (castᶠ (sym p₁) (idx ↑ˡ n₁))
+            ; newNodes = newNodes₁ ++ newNodes₂
-            ≡⟨ g₂[]≡g₃[] _ ⟩
+            ; nsg₂≡nsg₁++newNodes = ++-assoc (+-assoc s₁ n₁ n₂) ns₁ newNodes₁ newNodes₂
-              lookup (cast p₂ ns₃) ((castᶠ (sym p₁) (idx ↑ˡ n₁)) ↑ˡ n₂)
+            ; e∈g₁⇒e∈g₂ = λ {e} e∈g₁ →
-            ≡⟨ lookup-cast₁ p₂ _ _ ⟩
+                cast∈⇒∈subst (sym (+-assoc s₁ n₁ n₂)) (+-assoc s₁ n₁ n₂) _ _
-              lookup ns₃ (castᶠ (sym p₂) (((castᶠ (sym p₁) (idx ↑ˡ n₁)) ↑ˡ n₂)))
+                             (subst (λ e' → e' ∈ˡ es₃)
-            ≡⟨ cong (lookup ns₃) (↑ˡ-assoc (sym p₂) (sym p₁) (sym (+-assoc s₁ n₁ n₂)) idx) ⟩
+                                    (↑ˡ-Edge-assoc e (sym (+-assoc s₁ n₁ n₂)))
-              lookup ns₃ (castᶠ (sym (+-assoc s₁ n₁ n₂)) (idx ↑ˡ (n₁ +ⁿ n₂)))
+                                    (e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁)))
-            ≡⟨ sym (lookup-cast₁ (+-assoc s₁ n₁ n₂) _ _) ⟩
+            }
-              lookup (cast (+-assoc s₁ n₁ n₂) ns₃) (idx ↑ˡ (n₁ +ⁿ n₂))
-            ∎
-        ; e∈g₁⇒e∈g₂ = {!!} -- λ e∈g₁ → e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁)
-        }
-        where
-            ↑ˡ-assoc : ∀ {s₁ s₂ s₃ n₁ n₂ : ℕ}
-                            (p : s₂ +ⁿ n₂ ≡ s₃) (q : s₁ +ⁿ n₁ ≡ s₂)
-                            (r : s₁ +ⁿ (n₁ +ⁿ n₂) ≡ s₃)
-                            (idx : Fin s₁) →
-                            castᶠ p ((castᶠ q (idx ↑ˡ n₁)) ↑ˡ n₂) ≡ castᶠ r (idx ↑ˡ (n₁ +ⁿ n₂))
-            ↑ˡ-assoc refl refl r zero = refl
-            ↑ˡ-assoc {(suc s₁)} {s₂} {s₃} {n₁} {n₂} refl refl r (suc idx')
-                rewrite ↑ˡ-assoc refl refl (sym (+-assoc s₁ n₁ n₂)) idx' = refl
 
     record Relaxable (T : Graph → Set) : Set where
         field relax : ∀ {g₁ g₂ : Graph} → g₁ ⊆ g₂ → T g₁ → T g₂
@@ -160,7 +190,7 @@ module Graphs where
     instance
         IndexRelaxable : Relaxable Graph.Index
         IndexRelaxable = record
-            { relax = λ { (Mk-⊆ n refl _ _) idx → idx ↑ˡ n }
+            { relax = λ { (Mk-⊆ n refl _ _ _) idx → idx ↑ˡ n }
             }
 
         EdgeRelaxable : Relaxable Graph.Edge
@@ -185,13 +215,20 @@ module Graphs where
 
     relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) →
                           g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ]
-    relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl g₁[]≡g₂[] _) idx =
+    relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl newNodes nsg₂≡nsg₁++newNodes _) idx
-        trans (g₁[]≡g₂[] idx) (cong (λ vec → lookup vec (idx ↑ˡ n))
+        rewrite cast-is-id refl (Graph.nodes g₂)
-                                    (cast-is-id refl (Graph.nodes g₂)))
+        with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes g₁) _ _)
+
+    -- Tools for graph construction. The most important is a 'monotonic function':
+    -- one that takes a graph, and produces another graph, such that the
+    -- new graph includes all the information from the old one.
 
     MonotonicGraphFunction : (Graph → Set) → Set
     MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂)
 
+    -- Now, define some operations on monotonic functions; these are useful
+    -- to save the work of threading intermediate graphs in and out of operations.
+
     infixr 2 _⟨⊗⟩_
     _⟨⊗⟩_ : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }} →
           MonotonicGraphFunction T₁ → MonotonicGraphFunction T₂ →
@@ -216,6 +253,47 @@ module Graphs where
           MonotonicGraphFunction T₂
     _map_ f fn g = let (g' , (t₁ , g⊆g')) = f g in (g' , (fn g' t₁ , g⊆g'))
 
+
+    -- To reason about monotonic functions and what we do, we need a way
+    -- to describe values they produce. A 'graph-value predicate' is
+    -- just a predicate for some (dependent) value.
+
+    GraphValuePredicate : (Graph → Set) → Set₁
+    GraphValuePredicate T = ∀ (g : Graph) → T g → Set
+
+    Both : {T₁ T₂ : Graph → Set} → GraphValuePredicate T₁ → GraphValuePredicate T₂ →
+           GraphValuePredicate (T₁ ⊗ T₂)
+    Both P Q = (λ { g (t₁ , t₂) → (P g t₁ × Q g t₂) })
+
+    -- Since monotnic functions keep adding on to a function, proofs of
+    -- graph-value predicates go stale fast (they describe old values of
+    -- the graph). To keep propagating them through, we need them to still
+    -- on 'bigger graphs'. We call such predicates monotonic as well, since
+    -- they respect the ordering of graphs.
+
+    MonotonicPredicate : ∀ {T : Graph → Set} {{ TRelaxable : Relaxable T }} →
+                         GraphValuePredicate T → Set
+    MonotonicPredicate {T} P = ∀ (g₁ g₂ : Graph) (t₁ : T g₁) (g₁⊆g₂ : g₁ ⊆ g₂) →
+                               P g₁ t₁ → P g₂ (relax g₁⊆g₂ t₁)
+
+
+    -- A 'map' has a certain property if its ouputs satisfy that property
+    -- for all inputs.
+
+    always : ∀ {T : Graph → Set} → GraphValuePredicate T → MonotonicGraphFunction T → Set
+    always P m = ∀ g₁ → let (g₂ , t , _) = m g₁ in P g₂ t
+
+    ⟨⊗⟩-reason : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }}
+                 {P : GraphValuePredicate T₁} {Q : GraphValuePredicate T₂}
+                 {P-Mono : MonotonicPredicate P}
+                 {m₁ : MonotonicGraphFunction T₁} {m₂ : MonotonicGraphFunction T₂} →
+                 always P m₁ → always Q m₂ → always (Both P Q) (m₁ ⟨⊗⟩ m₂)
+    ⟨⊗⟩-reason {P-Mono = P-Mono} {m₁ = m₁} {m₂ = m₂} aP aQ g
+        with p ← aP g
+        with (g' , (t₁ , g⊆g')) ← m₁ g
+        with q ← aQ g'
+        with (g'' , (t₂ , g'⊆g'')) ← m₂ g' = (P-Mono _ _ _ g'⊆g'' p , q)
+
     module Construction where
         pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
         pushBasicBlock bss g =
@@ -228,8 +306,9 @@ module Graphs where
               , record
                   { n = 1
                   ; sg₂≡sg₁+n = refl
-                  ; g₁[]≡g₂[] = {!!} -- λ idx → trans (sym (lookup-++ˡ (Graph.nodes g) (bss ∷ []) idx)) (sym (cong (λ vec → lookup vec (idx ↑ˡ 1)) (cast-is-id refl (Graph.nodes g ++ (bss ∷ [])))))
+                  ; newNodes = (bss ∷ [])
-                  ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e' → ↑ˡ-Edge e' 1) e∈g₁
+                  ; nsg₂≡nsg₁++newNodes = cast-is-id refl _
+                  ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e → ↑ˡ-Edge e 1) e∈g₁
                   }
               )
             )
@@ -244,23 +323,15 @@ module Graphs where
             , record
                 { n = 0
                 ; sg₂≡sg₁+n = +-comm 0 s
-                ; g₁[]≡g₂[] = λ idx →
+                ; newNodes = []
-                    begin
+                ; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns)
-                        lookup ns idx
+                ; e∈g₁⇒e∈g₂ = λ {e} e∈es →
-                    ≡⟨ cong (lookup ns) (↑ˡ-identityʳ (sym (+-comm 0 s)) idx) ⟩
+                    cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _
-                        lookup ns (castᶠ (sym (+-comm 0 s)) (idx ↑ˡ 0))
+                                 (subst (λ e' → e' ∈ˡ _)
-                    ≡⟨ sym (lookup-cast₁ (+-comm 0 s) _ _) ⟩
+                                        (↑ˡ-Edge-identityʳ e (+-comm s 0))
-                        lookup (cast (+-comm 0 s) ns) (idx ↑ˡ 0)
+                                        (∈ˡ-++⁺ʳ es' e∈es))
-                    ∎
-                ; e∈g₁⇒e∈g₂ = {!!}
                 }
             )
-            where
-                ↑ˡ-identityʳ : ∀ {s} (p : s +ⁿ 0 ≡ s) (idx : Fin s) →
-                           idx ≡ castᶠ p (idx ↑ˡ 0)
-                ↑ˡ-identityʳ p zero = refl
-                ↑ˡ-identityʳ {suc s'} p (suc f')
-                    rewrite sym (↑ˡ-identityʳ (+-comm s' 0) f') = refl
 
         pushEmptyBlock : MonotonicGraphFunction Graph.Index
         pushEmptyBlock = pushBasicBlock []
@@ -410,7 +481,7 @@ private
     z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
 
     indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
-    indices 0 = ([] , empty)
+    indices 0 = ([] , emptyᵘ)
     indices (suc n') =
         let
             (inds' , unids') = indices n'
@@ -423,54 +494,32 @@ private
     indices-complete (suc n') zero = RelAny.here refl
     indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f'))
 
-    -- Sketch, 'build control flow graph'
-
-    -- -- Create new block, mark it as the current insertion point.
-    -- emptyBlock : m Id
-
-    -- currentBlock : m Id
-
-    -- -- Create a new block, and insert the statement into it. Shold restore insertion pont.
-    -- createBlock : Stmt → m (Id × Id)
-
-    -- -- Note that the given ID is a successor / predecessor of the given
-    -- -- insertion point.
-    -- noteSuccessor : Id → m ()
-    -- notePredecessor : Id → m ()
-    -- noteEdge : Id → Id → m ()
-
-    -- -- Insert the given statment into the current insertion point.
-    -- buildCfg : Stmt → m Cfg
-    -- buildCfg { bs₁ } = push bs₁
-    -- buildCfg (s₁ ; s₂ ) = buildCfg s₁ >> buildCfg s₂
-    -- buildCfg (if _ then s₁ else s₂) = do
-    --     (b₁ , b₁') ← createBlock s₁
-    --     noteSuccessor b₁
-
-    --     (b₂ , b₂') ← createBlock s₂
-    --     noteSuccessor b₂
-
-    --     b ← emptyBlock
-    --     notePredecessor b₁'
-    --     notePredecessor b₂'
-    -- buildCfg (while e repeat s) = do
-    --     (b₁, b₁') ← createBlock s
-    --     noteSuccessor b₁
-    --     noteEdge b₁' b₁
-
-    --     b ← emptyBlock
-    --     notePredecessor b₁'
-
 
 -- For now, just represent the program and CFG as one type, without branching.
 record Program : Set where
+    open Graphs
+
     field
-        length : ℕ
+        rootStmt : Stmt
-        stmts : Vec Stmt length
+
+    private
+        buildResult = Construction.buildCfg rootStmt empty
+
+    graph : Graph
+    graph = proj₁ buildResult
+
+    State : Set
+    State = Graph.Index graph
+
+    initialState : State
+    initialState = proj₁' (proj₁ (proj₂ buildResult))
+
+    finalState : State
+    finalState = proj₂' (proj₁ (proj₂ buildResult))
 
     private
         vars-Set : StringSet
-        vars-Set = Stmts-vars stmts
+        vars-Set = Stmt-vars rootStmt
 
     vars : List String
     vars = to-Listˢ vars-Set
@@ -478,20 +527,17 @@ record Program : Set where
     vars-Unique : Unique vars
     vars-Unique = proj₂ vars-Set
 
-    State : Set
-    State = Fin length
-
     states : List State
-    states = proj₁ (indices length)
+    states = proj₁ (indices (Graph.size graph))
 
     states-complete : ∀ (s : State) → s ∈ˡ states
-    states-complete = indices-complete length
+    states-complete = indices-complete (Graph.size graph)
 
     states-Unique : Unique states
-    states-Unique = proj₂ (indices length)
+    states-Unique = proj₂ (indices (Graph.size graph))
 
-    code : State → Stmt
+    code : State → List BasicStmt
-    code = lookup stmts
+    code st = graph [ st ]
 
     -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ∈ˡ vars
     -- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}
@@ -499,14 +545,10 @@ record Program : Set where
     _≟_ : IsDecidable (_≡_ {_} {State})
     _≟_ = _≟ᶠ_
 
-    -- Computations for incoming and outgoing edges will have to change too
+    _≟ᵉ_ : IsDecidable (_≡_ {_} {Graph.Edge graph})
-    -- when we support branching etc.
+    _≟ᵉ_ = ≡-dec _≟_ _≟_
+
+    open import Data.List.Membership.DecPropositional _≟ᵉ_ using () renaming (_∈?_ to _∈ˡ?_)
 
     incoming : State → List State
-    incoming
+    incoming idx = filterᶠ (λ idx' → (idx' , idx) ∈ˡ? (Graph.edges graph)) states
-        with length
-    ...   | 0 = (λ ())
-    ...   | suc n' = (λ
-            { zero → []
-            ; (suc f') → (inject₁ f') ∷ []
-            })

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)

Main.agda

@@ -6,18 +6,16 @@ open import Data.Vec using (Vec; _∷_; [])
 open import IO
 open import Level using (0ℓ)
 
-testCode : Vec Stmt _
+testCode : Stmt
 testCode =
-    ("zero" ← (# 0)) ∷
+    ⟨ "zero" ← (# 0) ⟩ then
-    ("pos" ← ((` "zero") Expr.+ (# 1))) ∷
+    ⟨ "pos" ← ((` "zero") Expr.+ (# 1)) ⟩ then
-    ("neg" ← ((` "zero") Expr.- (# 1))) ∷
+    ⟨ "neg" ← ((` "zero") Expr.- (# 1)) ⟩ then
-    ("unknown" ← ((` "pos") Expr.+ (` "neg"))) ∷
+    ⟨ "unknown" ← ((` "pos") Expr.+ (` "neg")) ⟩
-    []
 
 testProgram : Program
 testProgram = record
-    { length = _
+    { rootStmt = testCode
-    ; stmts = testCode
     }
 
 open WithProg testProgram using (output)

Utils.agda

@@ -72,3 +72,9 @@ data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List
 infixr 2 _⊗_
 data _⊗_ {a p q} {A : Set a} (P : A → Set p) (Q : A → Set q) : A → Set (a ⊔ℓ p ⊔ℓ q) where
     _,_ : ∀ {val : A} → P val → Q val → (P ⊗ Q) val
+
+proj₁ : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {a : A} → (P ⊗ Q) a → P a
+proj₁ (v , _) = v
+
+proj₂ : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {a : A} → (P ⊗ Q) a → Q a
+proj₂ (_ , v) = v