From 4fe0d147fa7249c54b454f56cbbe2cb59379f441 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 13 Apr 2024 13:39:15 -0700
Subject: [PATCH] Adjust 'Program' to have a graph and basic blocks

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language.agda | 64 +++++++++++++++++++++++++++++++++------------------
 Utils.agda    |  6 +++++
 2 files changed, 47 insertions(+), 23 deletions(-)

diff --git a/Language.agda b/Language.agda
index f643de8..66fbcf9 100644
--- a/Language.agda
+++ b/Language.agda
@@ -5,10 +5,11 @@ 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₁; 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 ∈ˡ-++⁺ʳ)
@@ -19,11 +20,12 @@ open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁; inject≤; _↑
 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
@@ -104,6 +106,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)
 
@@ -471,7 +480,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'
@@ -487,13 +496,29 @@ private
 
 -- For now, just represent the program and CFG as one type, without branching.
 record Program : Set where
+    open Graphs
+
     field
-        length : ℕ
-        stmts : Vec Stmt length
+        prog : Stmt
+
+    private
+        buildResult = Construction.buildCfg prog 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 prog
 
     vars : List String
     vars = to-Listˢ vars-Set
@@ -501,20 +526,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 = lookup stmts
+    code : State → List BasicStmt
+    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}
@@ -522,14 +544,10 @@ record Program : Set where
     _≟_ : IsDecidable (_≡_ {_} {State})
     _≟_ = _≟ᶠ_
 
-    -- Computations for incoming and outgoing edges will have to change too
-    -- when we support branching etc.
+    _≟ᵉ_ : IsDecidable (_≡_ {_} {Graph.Edge graph})
+    _≟ᵉ_ = ≡-dec _≟_ _≟_
+
+    open import Data.List.Membership.DecPropositional _≟ᵉ_ using () renaming (_∈?_ to _∈ˡ?_)
 
     incoming : State → List State
-    incoming
-        with length
-    ...   | 0 = (λ ())
-    ...   | suc n' = (λ
-            { zero → []
-            ; (suc f') → (inject₁ f') ∷ []
-            })
+    incoming idx = filterᶠ (λ idx' → (idx' , idx) ∈ˡ? (Graph.edges graph)) states
diff --git a/Utils.agda b/Utils.agda
index e719af8..d37da9f 100644
--- a/Utils.agda
+++ b/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