From d4b0796715bd982cd2f73d7decffd49916c6c16a Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 7 Apr 2024 19:51:59 -0700 Subject: [PATCH] Intermediate commit. Switch to *-based definition of <=. Signed-off-by: Danila Fedorin --- Language.agda | 127 +++++++++++++++++++++++++++++++------------------- Utils.agda | 1 + 2 files changed, 81 insertions(+), 47 deletions(-) diff --git a/Language.agda b/Language.agda index 7afa2f6..7d7e7eb 100644 --- a/Language.agda +++ b/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 diff --git a/Utils.agda b/Utils.agda index 4d9cc8d..e719af8 100644 --- a/Utils.agda +++ b/Utils.agda @@ -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