From 195537fe15292937dc7c6a21aa00f0e76f1b153f Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 7 Apr 2024 20:26:38 -0700
Subject: [PATCH] Implement graph construction using <*>, map, and update.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language.agda | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/Language.agda b/Language.agda
index 7d7e7eb..152ad8d 100644
--- a/Language.agda
+++ b/Language.agda
@@ -182,6 +182,20 @@ module Graphs where
         with (g'' , (t₂ , g'⊆g'')) ← f₂ g' =
         (g'' , ((Relaxable.relax r g'⊆g'' t₁ , t₂) , ⊆-trans g⊆g' g'⊆g''))
 
+    infixl 2 _update_
+    _update_ : ∀ {T : Graph → Set} {{ TRelaxable : Relaxable T }} →
+             MonotonicGraphFunction T → (∀ (g : Graph) → T g → Σ Graph (λ g' → g ⊆ g')) →
+             MonotonicGraphFunction T
+    _update_ {{r}} f mod g
+        with (g' , (t , g⊆g')) ← f g
+        with (g'' , g'⊆g'') ← mod g' t =
+        (g'' , ((Relaxable.relax r g'⊆g'' t , ⊆-trans g⊆g' g'⊆g'')))
+
+    infixl 2 _map_
+    _map_ : ∀ {T₁ T₂ : Graph → Set} →
+          MonotonicGraphFunction T₁ → (∀ (g : Graph) → T₁ g → T₂ g) →
+          MonotonicGraphFunction T₂
+    _map_ f fn g = let (g' , (t₁ , g⊆g')) = f g in (g' , (fn g' t₁ , g⊆g'))
 
     module Construction where
         pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
@@ -196,9 +210,29 @@ module Graphs where
             in
                 (g₁ ∙ g' , (Graph.size g₁ ↑ʳ zero , (g' , refl)))
 
+        addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
+        addEdges g es = {!!}
+
         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) ∷ []) })
+            map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') })
+
     -- open Relaxable {{...}} public
 
 open import Lattice.MapSet _≟ˢ_