From 54b11d21b05710253fb726be51ac95353595b612 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 20 Apr 2024 19:31:47 -0700 Subject: [PATCH] Start working on proving facts about graph construction Signed-off-by: Danila Fedorin --- Language/Graphs.agda | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/Language/Graphs.agda b/Language/Graphs.agda index 73be572..a594740 100644 --- a/Language/Graphs.agda +++ b/Language/Graphs.agda @@ -12,8 +12,8 @@ open import Data.Nat as Nat using (ℕ; suc) open import Data.Nat.Properties using (+-assoc; +-comm) open import Data.Product using (_×_; Σ; _,_) open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_) -open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ) -open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst) +open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans) open import Lattice open import Utils using (x∈xs⇒fx∈fxs; _⊗_; _,_) @@ -134,6 +134,14 @@ relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl newNodes nsg₂≡nsg₁++newNode rewrite cast-is-id refl (Graph.nodes g₂) with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes g₁) _ _) +instance + NodeEqualsMonotonic : ∀ {bss : List BasicStmt} → + MonotonicPredicate (λ g n → g [ n ] ≡ bss) + NodeEqualsMonotonic = record + { relaxPredicate = λ g₁ g₂ idx g₁⊆g₂ g₁[idx]≡bss → + trans (sym (relax-preserves-[]≡ g₁ g₂ g₁⊆g₂ idx)) g₁[idx]≡bss + } + pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index pushBasicBlock bss g = ( record @@ -152,6 +160,9 @@ pushBasicBlock bss g = ) ) +pushBasicBlock-works : ∀ (bss : List BasicStmt) → Always (λ g idx → g [ idx ] ≡ bss) (pushBasicBlock bss) +pushBasicBlock-works bss = MkAlways (λ g → lookup-++ʳ (Graph.nodes g) (bss ∷ []) zero) + addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g') addEdges (MkGraph s ns es) es' = ( record