From 734e82ff6d54ef3f7142a7a0d888b09df1fee69e Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 9 May 2024 21:08:32 -0700
Subject: [PATCH] Wrap generated graphs to ensure entry and exit nodes have no
 extra edges

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language.agda            |  6 +++---
 Language/Graphs.agda     |  3 +++
 Language/Properties.agda | 23 ++++++++---------------
 3 files changed, 14 insertions(+), 18 deletions(-)

diff --git a/Language.agda b/Language.agda
index 2042c76..a8d1c3f 100644
--- a/Language.agda
+++ b/Language.agda
@@ -55,16 +55,16 @@ record Program : Set where
         rootStmt : Stmt
 
     graph : Graph
-    graph = buildCfg rootStmt
+    graph = wrap (buildCfg rootStmt)
 
     State : Set
     State = Graph.Index graph
 
     initialState : State
-    initialState = proj₁ (buildCfg-input rootStmt)
+    initialState = proj₁ (wrap-input (buildCfg rootStmt))
 
     finalState : State
-    finalState = proj₁ (buildCfg-output rootStmt)
+    finalState = proj₁ (wrap-output (buildCfg rootStmt))
 
     private
         vars-Set : StringSet
diff --git a/Language/Graphs.agda b/Language/Graphs.agda
index d4f8bfd..0976fe3 100644
--- a/Language/Graphs.agda
+++ b/Language/Graphs.agda
@@ -112,6 +112,9 @@ singleton bss = record
     ; outputs = zero ∷ []
     }
 
+wrap : Graph → Graph
+wrap g = singleton [] ↦ g ↦ singleton []
+
 buildCfg : Stmt → Graph
 buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ [])
 buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
diff --git a/Language/Properties.agda b/Language/Properties.agda
index ca82ec7..b1309a8 100644
--- a/Language/Properties.agda
+++ b/Language/Properties.agda
@@ -18,22 +18,11 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
 
 open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct; concat-∈)
 
+wrap-input : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.inputs (wrap g) ≡ idx ∷ [])
+wrap-input g = (_ , refl)
 
-buildCfg-input : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.inputs g ≡ idx ∷ [])
-buildCfg-input ⟨ bs₁ ⟩ = (zero , refl)
-buildCfg-input (s₁ then s₂)
-    with (idx , p) ← buildCfg-input s₁ rewrite p = (_ , refl)
-buildCfg-input (if _ then s₁ else s₂) = (zero , refl)
-buildCfg-input (while _ repeat s)
-    with (idx , p) ← buildCfg-input s rewrite p = (_ , refl)
-
-buildCfg-output : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.outputs g ≡ idx ∷ [])
-buildCfg-output ⟨ bs₁ ⟩ = (zero , refl)
-buildCfg-output (s₁ then s₂)
-    with (idx , p) ← buildCfg-output s₂ rewrite p = (_ , refl)
-buildCfg-output (if _ then s₁ else s₂) = (_ , refl)
-buildCfg-output (while _ repeat s)
-    with (idx , p) ← buildCfg-output s rewrite p = (_ , refl)
+wrap-output : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.outputs (wrap g) ≡ idx ∷ [])
+wrap-output g = (_ , refl)
 
 Trace-∙ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} →
            Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →
@@ -224,6 +213,10 @@ EndToEndTrace-singleton ρ₁⇒ρ₂ = record
 EndToEndTrace-singleton[] : ∀ (ρ : Env) → EndToEndTrace {singleton []} ρ ρ
 EndToEndTrace-singleton[] env = EndToEndTrace-singleton []
 
+EndToEndTrace-wrap : ∀ {g : Graph} {ρ₁ ρ₂ : Env} →
+                     EndToEndTrace {g} ρ₁ ρ₂ → EndToEndTrace {wrap g} ρ₁ ρ₂
+EndToEndTrace-wrap {g} {ρ₁} {ρ₂} etr = EndToEndTrace-singleton[] ρ₁ ++ etr ++ EndToEndTrace-singleton[] ρ₂
+
 buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ →
                       EndToEndTrace {buildCfg s} ρ₁ ρ₂
 buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) =