Add a new 'properties' module

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-20 20:25:40 -07:00
parent 54b11d21b0
commit 6e3f06ca5d
3 changed files with 62 additions and 47 deletions

View File

@ -3,6 +3,7 @@ module Language where
open import Language.Base public
open import Language.Semantics public
open import Language.Graphs public
open import Language.Properties public
open import Data.Fin using (Fin; suc; zero)
open import Data.Fin.Properties as FinProp using (suc-injective)

View File

@ -1,7 +1,6 @@
module Language.Graphs where
open import Language.Base
open import Language.Semantics
open import Data.Fin as Fin using (Fin; suc; zero; _↑ˡ_; _↑ʳ_)
open import Data.Fin.Properties as FinProp using (suc-injective)
@ -57,38 +56,39 @@ record _⊆_ (g₁ g₂ : Graph) : Set where
e ListMem.∈ (Graph.edges g₁)
(↑ˡ-Edge e n) ListMem.∈ (subst (λ m List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂))
castᵉ : {n m : } .(p : n m) (Fin n × Fin n) (Fin m × Fin m)
castᵉ p (idx₁ , idx₂) = (Fin.cast p idx₁ , Fin.cast p idx₂)
private
castᵉ : {n m : } .(p : n m) (Fin n × Fin n) (Fin m × Fin m)
castᵉ p (idx₁ , idx₂) = (Fin.cast p idx₁ , Fin.cast p idx₂)
↑ˡ-assoc : {s n₁ n₂} (f : Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) s Nat.+ n₁ Nat.+ n₂)
f ↑ˡ n₁ ↑ˡ n₂ Fin.cast p (f ↑ˡ (n₁ Nat.+ n₂))
↑ˡ-assoc zero p = refl
↑ˡ-assoc {suc s'} {n₁} {n₂} (suc f') p rewrite ↑ˡ-assoc f' (sym (+-assoc s' n₁ n₂)) = refl
↑ˡ-assoc : {s n₁ n₂} (f : Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) s Nat.+ n₁ Nat.+ n₂)
f ↑ˡ n₁ ↑ˡ n₂ Fin.cast p (f ↑ˡ (n₁ Nat.+ n₂))
↑ˡ-assoc zero p = refl
↑ˡ-assoc {suc s'} {n₁} {n₂} (suc f') p rewrite ↑ˡ-assoc f' (sym (+-assoc s' n₁ n₂)) = refl
↑ˡ-Edge-assoc : {s n₁ n₂} (e : Fin s × Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) s Nat.+ n₁ Nat.+ n₂)
↑ˡ-Edge (↑ˡ-Edge e n₁) n₂ castᵉ p (↑ˡ-Edge e (n₁ Nat.+ n₂))
↑ˡ-Edge-assoc (idx₁ , idx₂) p
rewrite ↑ˡ-assoc idx₁ p
rewrite ↑ˡ-assoc idx₂ p = refl
↑ˡ-Edge-assoc : {s n₁ n₂} (e : Fin s × Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) s Nat.+ n₁ Nat.+ n₂)
↑ˡ-Edge (↑ˡ-Edge e n₁) n₂ castᵉ p (↑ˡ-Edge e (n₁ Nat.+ n₂))
↑ˡ-Edge-assoc (idx₁ , idx₂) p
rewrite ↑ˡ-assoc idx₁ p
rewrite ↑ˡ-assoc idx₂ p = refl
↑ˡ-identityʳ : {s} (f : Fin s) (p : s Nat.+ 0 s)
f Fin.cast p (f ↑ˡ 0)
↑ˡ-identityʳ zero p = refl
↑ˡ-identityʳ {suc s'} (suc f') p rewrite sym (↑ˡ-identityʳ f' (+-comm s' 0)) = refl
↑ˡ-identityʳ : {s} (f : Fin s) (p : s Nat.+ 0 s)
f Fin.cast p (f ↑ˡ 0)
↑ˡ-identityʳ zero p = refl
↑ˡ-identityʳ {suc s'} (suc f') p rewrite sym (↑ˡ-identityʳ f' (+-comm s' 0)) = refl
↑ˡ-Edge-identityʳ : {s} (e : Fin s × Fin s) (p : s Nat.+ 0 s)
e castᵉ p (↑ˡ-Edge e 0)
↑ˡ-Edge-identityʳ (idx₁ , idx₂) p
rewrite sym (↑ˡ-identityʳ idx₁ p)
rewrite sym (↑ˡ-identityʳ idx₂ p) = refl
↑ˡ-Edge-identityʳ : {s} (e : Fin s × Fin s) (p : s Nat.+ 0 s)
e castᵉ p (↑ˡ-Edge e 0)
↑ˡ-Edge-identityʳ (idx₁ , idx₂) p
rewrite sym (↑ˡ-identityʳ idx₁ p)
rewrite sym (↑ˡ-identityʳ idx₂ p) = refl
cast∈⇒∈subst : {n m : } (p : n m) (q : m n)
(e : Fin n × Fin n) (es : List (Fin m × Fin m))
castᵉ p e ListMem.∈ es
e ListMem.∈ subst (λ m List (Fin m × Fin m)) q es
cast∈⇒∈subst refl refl (idx₁ , idx₂) es e∈es
rewrite FinProp.cast-is-id refl idx₁
rewrite FinProp.cast-is-id refl idx₂ = e∈es
cast∈⇒∈subst : {n m : } (p : n m) (q : m n)
(e : Fin n × Fin n) (es : List (Fin m × Fin m))
castᵉ p e ListMem.∈ es
e ListMem.∈ subst (λ m List (Fin m × Fin m)) q es
cast∈⇒∈subst refl refl (idx₁ , idx₂) es e∈es
rewrite FinProp.cast-is-id refl idx₁
rewrite FinProp.cast-is-id refl idx₂ = e∈es
⊆-trans : {g₁ g₂ g₃ : Graph} g₁ g₂ g₂ g₃ g₁ g₃
⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃}
@ -128,20 +128,6 @@ instance
open Relaxable {{...}}
relax-preserves-[]≡ : (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ g₂) (idx : Graph.Index g₁)
g₁ [ idx ] g₂ [ relax g₁⊆g₂ idx ]
relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl newNodes nsg₂≡nsg₁++newNodes _) idx
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
@ -160,8 +146,8 @@ 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)
pushEmptyBlock : MonotonicGraphFunction Graph.Index
pushEmptyBlock = pushBasicBlock []
addEdges : (g : Graph) List (Graph.Edge g) Σ Graph (λ g' g g')
addEdges (MkGraph s ns es) es' =
@ -183,9 +169,6 @@ addEdges (MkGraph s ns es) 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₂) =

31
Language/Properties.agda Normal file
View File

@ -0,0 +1,31 @@
module Language.Properties where
open import Language.Base
open import Language.Semantics
open import Language.Graphs
open import MonotonicState _⊆_ ⊆-trans renaming (MonotonicState to MonotonicGraphFunction)
open Relaxable {{...}}
open import Data.Fin using (zero)
open import Data.List using (List)
open import Data.Vec using (_∷_; [])
open import Data.Vec.Properties using (cast-is-id; lookup-++ˡ; lookup-++ʳ)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans)
relax-preserves-[]≡ : (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ g₂) (idx : Graph.Index g₁)
g₁ [ idx ] g₂ [ relax g₁⊆g₂ idx ]
relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl newNodes nsg₂≡nsg₁++newNodes _) idx
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-works : (bss : List BasicStmt) Always (λ g idx g [ idx ] bss) (pushBasicBlock bss)
pushBasicBlock-works bss = MkAlways (λ g lookup-++ʳ (Graph.nodes g) (bss []) zero)