From fc27b045d37565639542691d7a0c0b7ad53dcb83 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 13 Apr 2024 19:33:58 -0700
Subject: [PATCH] Remove nested module from Graphs

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language.agda        |   2 +-
 Language/Graphs.agda | 109 +++++++++++++++++++++----------------------
 2 files changed, 55 insertions(+), 56 deletions(-)

diff --git a/Language.agda b/Language.agda
index 7bc21b6..725c4f2 100644
--- a/Language.agda
+++ b/Language.agda
@@ -52,7 +52,7 @@ record Program : Set where
         rootStmt : Stmt
 
     private
-        buildResult = Construction.buildCfg rootStmt empty
+        buildResult = buildCfg rootStmt empty
 
     graph : Graph
     graph = proj₁ buildResult
diff --git a/Language/Graphs.agda b/Language/Graphs.agda
index 8bb07f0..33f6c1e 100644
--- a/Language/Graphs.agda
+++ b/Language/Graphs.agda
@@ -220,61 +220,60 @@ always P m = ∀ g₁ → let (g₂ , t , _) = m g₁ in P g₂ t
     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 =
-        ( record
-            { size = Graph.size g Nat.+ 1
-            ; nodes = Graph.nodes g ++ (bss ∷ [])
-            ; edges = List.map (λ e → ↑ˡ-Edge e 1) (Graph.edges g)
-            }
-        , ( Graph.size g ↑ʳ zero
-          , record
-              { n = 1
-              ; sg₂≡sg₁+n = refl
-              ; newNodes = (bss ∷ [])
-              ; nsg₂≡nsg₁++newNodes = cast-is-id refl _
-              ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e → ↑ˡ-Edge e 1) e∈g₁
-              }
-          )
-        )
+pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
+pushBasicBlock bss g =
+    ( record
+        { size = Graph.size g Nat.+ 1
+        ; nodes = Graph.nodes g ++ (bss ∷ [])
+        ; edges = List.map (λ e → ↑ˡ-Edge e 1) (Graph.edges g)
+        }
+    , ( Graph.size g ↑ʳ zero
+      , record
+          { n = 1
+          ; sg₂≡sg₁+n = refl
+          ; newNodes = (bss ∷ [])
+          ; nsg₂≡nsg₁++newNodes = cast-is-id refl _
+          ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e → ↑ˡ-Edge e 1) e∈g₁
+          }
+      )
+    )
 
-    addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
-    addEdges (MkGraph s ns es) es' =
-        ( record
-            { size = s
-            ; nodes = ns
-            ; edges = es' List.++ es
-            }
-        , record
-            { n = 0
-            ; sg₂≡sg₁+n = +-comm 0 s
-            ; newNodes = []
-            ; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns)
-            ; e∈g₁⇒e∈g₂ = λ {e} e∈es →
-                cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _
-                             (subst (λ e' → e' ListMem.∈ _)
-                                    (↑ˡ-Edge-identityʳ e (+-comm s 0))
-                                    (ListMemProp.∈-++⁺ʳ es' e∈es))
-            }
-        )
+addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
+addEdges (MkGraph s ns es) es' =
+    ( record
+        { size = s
+        ; nodes = ns
+        ; edges = es' List.++ es
+        }
+    , record
+        { n = 0
+        ; sg₂≡sg₁+n = +-comm 0 s
+        ; newNodes = []
+        ; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns)
+        ; e∈g₁⇒e∈g₂ = λ {e} e∈es →
+            cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _
+                         (subst (λ e' → e' ListMem.∈ _)
+                                (↑ˡ-Edge-identityʳ e (+-comm s 0))
+                                (ListMemProp.∈-++⁺ʳ es' e∈es))
+        }
+    )
 
-    pushEmptyBlock : MonotonicGraphFunction Graph.Index
-    pushEmptyBlock = pushBasicBlock []
+pushEmptyBlock : MonotonicGraphFunction Graph.Index
+pushEmptyBlock = pushBasicBlock []
 
-    buildCfg : Stmt → MonotonicGraphFunction (Graph.Index ⊗ Graph.Index)
-    buildCfg ⟨ bs₁ ⟩ = pushBasicBlock (bs₁ ∷ []) map (λ g idx → (idx , idx))
-    buildCfg (s₁ then s₂) =
-        (buildCfg s₁ ⟨⊗⟩ buildCfg s₂)
-        update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → addEdges g ((idx₂ , idx₃) ∷ []) })
-        map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → (idx₁ , idx₄) })
-    buildCfg (if _ then s₁ else s₂) =
-        (buildCfg s₁ ⟨⊗⟩ buildCfg s₂ ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
-        update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') →
-                  addEdges g ((idx , idx₁) ∷ (idx , idx₃) ∷ (idx₂ , idx') ∷ (idx₄ , idx') ∷ []) })
-        map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → (idx , idx') })
-    buildCfg (while _ repeat s) =
-        (buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
-        update (λ { g ((idx₁ , idx₂) , idx , idx') →
-                  addEdges g ((idx , idx') ∷ (idx , idx₁) ∷ (idx₂ , idx) ∷ []) })
-        map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') })
+buildCfg : Stmt → MonotonicGraphFunction (Graph.Index ⊗ Graph.Index)
+buildCfg ⟨ bs₁ ⟩ = pushBasicBlock (bs₁ ∷ []) map (λ g idx → (idx , idx))
+buildCfg (s₁ then s₂) =
+    (buildCfg s₁ ⟨⊗⟩ buildCfg s₂)
+    update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → addEdges g ((idx₂ , idx₃) ∷ []) })
+    map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → (idx₁ , idx₄) })
+buildCfg (if _ then s₁ else s₂) =
+    (buildCfg s₁ ⟨⊗⟩ buildCfg s₂ ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
+    update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') →
+              addEdges g ((idx , idx₁) ∷ (idx , idx₃) ∷ (idx₂ , idx') ∷ (idx₄ , idx') ∷ []) })
+    map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → (idx , idx') })
+buildCfg (while _ repeat s) =
+    (buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock)
+    update (λ { g ((idx₁ , idx₂) , idx , idx') →
+              addEdges g ((idx , idx') ∷ (idx , idx₁) ∷ (idx₂ , idx) ∷ []) })
+    map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') })