From b505063771976a10fc276730a95db296da282e6b Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 4 Apr 2024 20:34:08 -0700
Subject: [PATCH] Start working on proofs of Graph-related things

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language.agda | 99 ++++++++++++++++++++++++++++++++++++++++++++++++---
 Utils.agda    |  3 ++
 2 files changed, 97 insertions(+), 5 deletions(-)

diff --git a/Language.agda b/Language.agda
index ceb9b8a..7afa2f6 100644
--- a/Language.agda
+++ b/Language.agda
@@ -1,22 +1,23 @@
 module Language where
 
-open import Data.Nat using (ℕ; suc; pred)
+open import Data.Nat using (ℕ; suc; pred; _≤_) renaming (_+_ to _+ⁿ_)
+open import Data.Nat.Properties using (m≤n⇒m≤n+o; ≤-reflexive)
 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.Vec using (Vec; foldr; lookup; _∷_)
+open import Data.Vec using (Vec; foldr; lookup; _∷_; []; _++_)
 open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
 open import Data.List.Membership.Propositional as MemProp 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.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_)
+open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁; inject≤; _↑ʳ_) renaming (_≟_ to _≟ᶠ_)
 open import Data.Fin.Properties using (suc-injective)
-open import Relation.Binary.PropositionalEquality using (cong; _≡_; refl)
+open import Relation.Binary.PropositionalEquality using (subst; cong; _≡_; refl)
 open import Relation.Nullary using (¬_)
 open import Function using (_∘_)
 
 open import Lattice
-open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs)
+open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs; _⊗_; _,_)
 
 data Expr : Set where
     _+_ : Expr → Expr → Expr
@@ -79,6 +80,94 @@ module Semantics where
             ρ , e ⇒ᵉ (↑ᶻ (+ 0)) →
             ρ , (while e repeat s) ⇒ˢ ρ
 
+module Graphs where
+    open Semantics
+
+    record Graph : Set where
+        field
+            size : ℕ
+
+        Index : Set
+        Index = Fin size
+
+        Edge : Set
+        Edge = Index × Index
+
+        field
+            nodes : Vec (List BasicStmt) size
+            edges : List Edge
+
+    _[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
+    _[_] g idx = lookup (Graph.nodes g) idx
+
+    _⊆_ : Graph → Graph → Set
+    _⊆_ g₁ g₂ =
+        Σ (Graph.size g₁ ≤ Graph.size g₂) (λ n₁≤n₂ →
+            ( ∀ (idx : Graph.Index g₁) → g₁ [ idx ] ≡ g₂ [ inject≤ idx n₁≤n₂ ]
+            × ∀ (idx₁ idx₂ : Graph.Index g₁) → (idx₁ , idx₂) ∈ˡ (Graph.edges g₁) →
+                (inject≤ idx₁ n₁≤n₂ , inject≤ idx₂ n₁≤n₂) ∈ˡ (Graph.edges g₂)
+            ))
+
+    -- Note: inject≤ doesn't seem to work as nicely with vector lookups.
+    --       The ↑ˡ and ↑ʳ operators are way nicer. Can we reformulate the
+    --       ⊆ property to use them?
+
+    n≤n+m : ∀ (n m : ℕ) → n ≤ n +ⁿ m
+    n≤n+m n m = m≤n⇒m≤n+o m (≤-reflexive (refl {x = n}))
+
+    lookup-++ˡ : ∀ {a} {A : Set a} {n m : ℕ} (xs : Vec A n) (ys : Vec A m)
+                   (idx : Fin n) → lookup xs idx ≡ lookup (xs ++ ys) (inject≤ idx (n≤n+m n m))
+    lookup-++ˡ = {!!}
+
+    pushBasicBlock : List BasicStmt → (g₁ : Graph) → Σ Graph (λ g₂ → Graph.Index g₂ × g₁ ⊆ g₂)
+    pushBasicBlock bss g₁ =
+        let
+            size' = Graph.size g₁ +ⁿ 1
+            size≤size' = n≤n+m (Graph.size g₁) 1
+            inject-Edge = λ (idx₁ , idx₂) → (inject≤ idx₁ size≤size' , inject≤ idx₂ size≤size')
+        in
+            ( record
+                { size = size'
+                ; nodes = Graph.nodes g₁ ++ (bss ∷ [])
+                ; edges = mapˡ inject-Edge (Graph.edges g₁)
+                }
+            , ( (Graph.size g₁) ↑ʳ zero
+              , ( size≤size'
+                , λ idx → lookup-++ˡ (Graph.nodes g₁) (bss ∷ []) idx
+                , λ idx₁ idx₂ e∈es → x∈xs⇒fx∈fxs inject-Edge e∈es
+                )
+              )
+            )
+
+    record Relaxable (T : Graph → Set) : Set where
+        field relax : ∀ {g₁ g₂ : Graph} → g₁ ⊆ g₂ → T g₁ → T g₂
+
+    instance
+        IndexRelaxable : Relaxable Graph.Index
+        IndexRelaxable = record
+            { relax = λ g₁⊆g₂ idx → inject≤ idx (proj₁ g₁⊆g₂)
+            }
+
+        EdgeRelaxable : Relaxable Graph.Edge
+        EdgeRelaxable = record
+            { relax = λ {g₁} {g₂} g₁⊆g₂ (idx₁ , idx₂) →
+                ( Relaxable.relax IndexRelaxable {g₁} {g₂} g₁⊆g₂ idx₁
+                , Relaxable.relax IndexRelaxable {g₁} {g₂} g₁⊆g₂ idx₂
+                )
+            }
+
+        ProdRelaxable : ∀ {P : Graph → Set} {Q : Graph → Set} →
+                        {{ PRelaxable : Relaxable P }} → {{ QRelaxable : Relaxable Q }} →
+                        Relaxable (P ⊗ Q)
+        ProdRelaxable {{pr}} {{qr}} = record
+            { relax = (λ { g₁⊆g₂ (p , q) →
+                ( Relaxable.relax pr g₁⊆g₂ p
+                , Relaxable.relax qr g₁⊆g₂ q) }
+                )
+            }
+
+    open Relaxable {{...}} public
+
 open import Lattice.MapSet _≟ˢ_
     renaming
         ( MapSet to StringSet
diff --git a/Utils.agda b/Utils.agda
index 825975b..4d9cc8d 100644
--- a/Utils.agda
+++ b/Utils.agda
@@ -68,3 +68,6 @@ data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List
     _∷_ : ∀ {x : A} {y : B} {xs : List A} {ys : List B} →
           P x y → Pairwise P xs ys →
           Pairwise P (x ∷ xs) (y ∷ ys)
+
+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