Intermediate commit. Switch to *-based definition of <=.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
b505063771
commit
d4b0796715
127
Language.agda
127
Language.agda
|
|
@ -1,18 +1,21 @@
|
|||
module Language where
|
||||
|
||||
open import Data.Nat using (ℕ; suc; pred; _≤_) renaming (_+_ to _+ⁿ_)
|
||||
open import Data.Nat.Properties using (m≤n⇒m≤n+o; ≤-reflexive)
|
||||
open import Data.Nat.Properties using (m≤n⇒m≤n+o; ≤-reflexive; +-assoc; +-comm)
|
||||
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.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
|
||||
open import Data.Vec using (Vec; foldr; lookup; _∷_; []; _++_; cast)
|
||||
open import Data.Vec.Properties using (++-assoc; ++-identityʳ)
|
||||
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.Fin using (Fin; suc; zero; fromℕ; inject₁; 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 (subst; cong; _≡_; refl)
|
||||
open import Relation.Binary.PropositionalEquality using (subst; cong; _≡_; sym; refl)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Function using (_∘_)
|
||||
|
||||
|
|
@ -84,6 +87,7 @@ module Graphs where
|
|||
open Semantics
|
||||
|
||||
record Graph : Set where
|
||||
constructor MkGraph
|
||||
field
|
||||
size : ℕ
|
||||
|
||||
|
|
@ -97,47 +101,47 @@ module Graphs where
|
|||
nodes : Vec (List BasicStmt) size
|
||||
edges : List Edge
|
||||
|
||||
_[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
|
||||
_[_] g idx = lookup (Graph.nodes g) idx
|
||||
Graph-build-≡ : ∀ (g₁ g₂ : Graph) (p : Graph.size g₁ ≡ Graph.size g₂) →
|
||||
(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)
|
||||
↑ʳ-Edge m (idx₁ , idx₂) = (m ↑ʳ idx₁ , m ↑ʳ idx₂)
|
||||
|
||||
_∙_ : Graph → Graph → Graph
|
||||
_∙_ (MkGraph s₁ ns₁ es₁) (MkGraph s₂ ns₂ es₂) = MkGraph
|
||||
(s₁ +ⁿ s₂)
|
||||
(ns₁ ++ ns₂)
|
||||
(
|
||||
let
|
||||
edges₁ = mapˡ (λ e → ↑ˡ-Edge e s₂) es₁
|
||||
edges₂ = mapˡ (↑ʳ-Edge s₁) es₂
|
||||
in
|
||||
edges₁ ++ˡ edges₂
|
||||
)
|
||||
|
||||
∙-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.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₂)
|
||||
))
|
||||
_⊆_ g₁ g₂ = Σ Graph (λ g' → g₁ ∙ g' ≡ 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?
|
||||
⊆-refl : ∀ (g : Graph) → g ⊆ g
|
||||
⊆-refl g = (MkGraph 0 [] [] , ∙-zero g)
|
||||
|
||||
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
|
||||
)
|
||||
)
|
||||
)
|
||||
⊆-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₂₃)
|
||||
|
||||
record Relaxable (T : Graph → Set) : Set where
|
||||
field relax : ∀ {g₁ g₂ : Graph} → g₁ ⊆ g₂ → T g₁ → T g₂
|
||||
|
|
@ -145,14 +149,14 @@ module Graphs where
|
|||
instance
|
||||
IndexRelaxable : Relaxable Graph.Index
|
||||
IndexRelaxable = record
|
||||
{ relax = λ g₁⊆g₂ idx → inject≤ idx (proj₁ g₁⊆g₂)
|
||||
{ relax = λ { (g' , refl) idx → idx ↑ˡ (Graph.size 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₂
|
||||
{ relax = λ g₁⊆g₂ (idx₁ , idx₂) →
|
||||
( Relaxable.relax IndexRelaxable g₁⊆g₂ idx₁
|
||||
, Relaxable.relax IndexRelaxable g₁⊆g₂ idx₂
|
||||
)
|
||||
}
|
||||
|
||||
|
|
@ -166,7 +170,36 @@ module Graphs where
|
|||
)
|
||||
}
|
||||
|
||||
open Relaxable {{...}} public
|
||||
MonotonicGraphFunction : (Graph → Set) → Set
|
||||
MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂)
|
||||
|
||||
infixr 2 _⟨⊗⟩_
|
||||
_⟨⊗⟩_ : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }} →
|
||||
MonotonicGraphFunction T₁ → MonotonicGraphFunction T₂ →
|
||||
MonotonicGraphFunction (T₁ ⊗ T₂)
|
||||
_⟨⊗⟩_ {{r}} f₁ f₂ g
|
||||
with (g' , (t₁ , g⊆g')) ← f₁ g
|
||||
with (g'' , (t₂ , g'⊆g'')) ← f₂ g' =
|
||||
(g'' , ((Relaxable.relax r g'⊆g'' t₁ , t₂) , ⊆-trans g⊆g' g'⊆g''))
|
||||
|
||||
|
||||
module Construction where
|
||||
pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
|
||||
pushBasicBlock bss g₁ =
|
||||
let
|
||||
g' : Graph
|
||||
g' = record
|
||||
{ size = 1
|
||||
; nodes = bss ∷ []
|
||||
; edges = []
|
||||
}
|
||||
in
|
||||
(g₁ ∙ g' , (Graph.size g₁ ↑ʳ zero , (g' , refl)))
|
||||
|
||||
pushEmptyBlock : MonotonicGraphFunction Graph.Index
|
||||
pushEmptyBlock = pushBasicBlock []
|
||||
|
||||
-- open Relaxable {{...}} public
|
||||
|
||||
open import Lattice.MapSet _≟ˢ_
|
||||
renaming
|
||||
|
|
|
|||
|
|
@ -69,5 +69,6 @@ data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List
|
|||
P x y → Pairwise P xs ys →
|
||||
Pairwise P (x ∷ xs) (y ∷ ys)
|
||||
|
||||
infixr 2 _⊗_
|
||||
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
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user