Try using index-based comparisons

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Language.agda

@@ -6,18 +6,20 @@ 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; _∷_; []; _++_; cast)
-open import Data.Vec.Properties using (++-assoc; ++-identityʳ)
+open import Data.Vec.Properties using (++-assoc; ++-identityʳ; lookup-++ˡ)
 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.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.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any as RelAny using ()
+open import Data.List.Relation.Unary.Any.Properties using (++⁺ʳ)
 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 (subst; cong; _≡_; sym; refl)
+open import Relation.Binary.PropositionalEquality as Eq using (subst; cong; _≡_; sym; trans; refl)
 open import Relation.Nullary using (¬_)
 open import Function using (_∘_)
+open Eq.≡-Reasoning using (begin_; step-≡; _∎)
 
 open import Lattice
 open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs; _⊗_; _,_)
@@ -101,47 +103,29 @@ module Graphs where
             nodes : Vec (List BasicStmt) size
             edges : List Edge
 
-    Graph-build-≡ : ∀ (g₁ g₂ : Graph) (p : Graph.size g₁ ≡ Graph.size g₂) →
+    ↑ˡ-Edge : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n +ⁿ m) × Fin (n +ⁿ m))
-                      (cast p (Graph.nodes g₁) ≡ Graph.nodes g₂) →
-                      (subst (λ s → List (Fin s × Fin s)) p (Graph.edges g₁) ≡ Graph.edges g₂) →
-                    g₁ ≡ g₂
-    Graph-build-≡ g₁ g₂ refl cns₁≡ns₂ refl
-        rewrite cast-is-id refl (Graph.nodes g₁)
-        rewrite cns₁≡ns₂ = refl
-
-
-    ↑ˡ-Edge : ∀ {n} → Fin n × Fin n → ∀ m → Fin (n +ⁿ m) × Fin (n +ⁿ m)
     ↑ˡ-Edge (idx₁ , idx₂) m = (idx₁ ↑ˡ m , idx₂ ↑ˡ m)
 
-    ↑ʳ-Edge : ∀ {n} m → Fin n × Fin n → Fin (m +ⁿ n) × Fin (m +ⁿ n)
+    _[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
-    ↑ʳ-Edge m (idx₁ , idx₂) = (m ↑ʳ idx₁ , m ↑ʳ idx₂)
+    _[_] g idx = lookup (Graph.nodes g) idx
 
-    _∙_ : Graph → Graph → Graph
+    record _⊆_ (g₁ g₂ : Graph) : Set where
-    _∙_ (MkGraph s₁ ns₁ es₁) (MkGraph s₂ ns₂ es₂) = MkGraph
+        constructor Mk-⊆
-        (s₁ +ⁿ s₂)
+        field
-        (ns₁ ++ ns₂)
+            n : ℕ
-        (
+            sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ +ⁿ n
-            let
+            g₁[]≡g₂[] : ∀ (idx : Graph.Index g₁) →
-                edges₁ = mapˡ (λ e → ↑ˡ-Edge e s₂) es₁
+                        lookup (Graph.nodes g₁) idx ≡
-                edges₂ = mapˡ (↑ʳ-Edge s₁) es₂
+                        lookup (cast sg₂≡sg₁+n (Graph.nodes g₂)) (idx ↑ˡ n)
-            in
+            e∈g₁⇒e∈g₂ : ∀ (e : Graph.Edge g₁) →
-                edges₁ ++ˡ edges₂
+                        e ∈ˡ (Graph.edges g₁) →
-        )
+                        (↑ˡ-Edge e n) ∈ˡ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂))
-
-    ∙-assoc : ∀ (g₁ g₂ g₃ : Graph) → g₁ ∙ (g₂ ∙ g₃) ≡ (g₁ ∙ g₂) ∙ g₃
-    ∙-assoc = {!!}
-
-    ∙-zero : ∀ (g : Graph) → g ∙ (MkGraph 0 [] []) ≡ g
-    ∙-zero (MkGraph s ns es) = Graph-build-≡ _ _ (+-comm s 0) (++-identityʳ (+-comm s 0) ns) {!!}
-
-    _⊆_ : Graph → Graph → Set
-    _⊆_ g₁ g₂ = Σ Graph (λ g' → g₁ ∙ g' ≡ g₂)
-
-    ⊆-refl : ∀ (g : Graph) → g ⊆ g
-    ⊆-refl g = (MkGraph 0 [] [] , ∙-zero g)
 
     ⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃
-    ⊆-trans {g₁} {g₂} {g₃} (g₁₂ , refl) (g₂₃ , refl) = ((g₁₂ ∙ g₂₃) , ∙-assoc g₁ g₁₂ g₂₃)
+    ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃} (Mk-⊆ n₁ p₁@refl g₁[]≡g₂[] e∈g₁⇒e∈g₂) (Mk-⊆ n₂ p₂@refl g₂[]≡g₃[] e∈g₂⇒e∈g₃) = record
+        { n = n₁ +ⁿ n₂
+        ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂
+        }
 
     record Relaxable (T : Graph → Set) : Set where
         field relax : ∀ {g₁ g₂ : Graph} → g₁ ⊆ g₂ → T g₁ → T g₂
@@ -149,7 +133,7 @@ module Graphs where
     instance
         IndexRelaxable : Relaxable Graph.Index
         IndexRelaxable = record
-            { relax = λ { (g' , refl) idx → idx ↑ˡ (Graph.size g') }
+            { relax = λ { (Mk-⊆ n refl _ _) idx → idx ↑ˡ n }
             }
 
         EdgeRelaxable : Relaxable Graph.Edge
@@ -199,19 +183,36 @@ module Graphs where
 
     module Construction where
         pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
-        pushBasicBlock bss g₁ =
+        pushBasicBlock bss g =
-            let
+            ( record
-                g' : Graph
+                { size = Graph.size g +ⁿ 1
-                g' = record
+                ; nodes = Graph.nodes g ++ (bss ∷ [])
-                    { size = 1
+                ; edges = mapˡ (λ e → ↑ˡ-Edge e 1) (Graph.edges g)
-                    ; nodes = bss ∷ []
+                }
-                    ; edges = []
+            , ( Graph.size g ↑ʳ zero
-                    }
+              , record
-            in
+                  { n = 1
-                (g₁ ∙ g' , (Graph.size g₁ ↑ʳ zero , (g' , refl)))
+                  ; sg₂≡sg₁+n = refl
+                  ; g₁[]≡g₂[] = λ idx → trans (sym (lookup-++ˡ (Graph.nodes g) (bss ∷ []) idx)) (sym (cong (λ vec → lookup vec (idx ↑ˡ 1)) (cast-is-id refl (Graph.nodes g ++ (bss ∷ [])))))
+                  ; e∈g₁⇒e∈g₂ = λ e e∈g₁ → x∈xs⇒fx∈fxs (λ e' → ↑ˡ-Edge e' 1) e∈g₁
+                  }
+              )
+            )
 
         addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
-        addEdges g es = {!!}
+        addEdges g es =
+            ( record
+                { size = Graph.size g
+                ; nodes = Graph.nodes g
+                ; edges = es ++ˡ Graph.edges g
+                }
+            , record
+                { n = 0
+                ; sg₂≡sg₁+n = +-comm 0 (Graph.size g)
+                ; g₁[]≡g₂[] = {!!}
+                ; e∈g₁⇒e∈g₂ = {!!}
+                }
+            )
 
         pushEmptyBlock : MonotonicGraphFunction Graph.Index
         pushEmptyBlock = pushBasicBlock []