From c00c8e3e858d4576924b9526fc1e26d23d714479 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 25 Apr 2024 23:10:41 -0700 Subject: [PATCH] Use different graph operations to implement construction Signed-off-by: Danila Fedorin --- Language.agda | 9 +- Language/Graphs.agda | 357 +++++++++++++++++++++++---------------- Language/Properties.agda | 60 ++----- Utils.agda | 10 +- 4 files changed, 239 insertions(+), 197 deletions(-) diff --git a/Language.agda b/Language.agda index 99a7737..971a2c5 100644 --- a/Language.agda +++ b/Language.agda @@ -52,20 +52,17 @@ record Program : Set where field rootStmt : Stmt - private - buildResult = buildCfg rootStmt empty - graph : Graph - graph = proj₁ buildResult + graph = buildCfg rootStmt State : Set State = Graph.Index graph initialState : State - initialState = Utils.proj₁ (proj₁ (proj₂ buildResult)) + initialState = proj₁ (buildCfg-input rootStmt) finalState : State - finalState = Utils.proj₂ (proj₁ (proj₂ buildResult)) + finalState = proj₁ (buildCfg-output rootStmt) private vars-Set : StringSet diff --git a/Language/Graphs.agda b/Language/Graphs.agda index 022eaba..dfd1580 100644 --- a/Language/Graphs.agda +++ b/Language/Graphs.agda @@ -1,8 +1,8 @@ module Language.Graphs where -open import Language.Base +open import Language.Base using (Expr; Stmt; BasicStmt; ⟨_⟩; _then_; if_then_else_; while_repeat_) -open import Data.Fin as Fin using (Fin; suc; zero; _↑ˡ_; _↑ʳ_) +open import Data.Fin as Fin using (Fin; suc; zero) open import Data.Fin.Properties as FinProp using (suc-injective) open import Data.List as List using (List; []; _∷_) open import Data.List.Membership.Propositional as ListMem using () @@ -15,7 +15,7 @@ open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-s open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans) open import Lattice -open import Utils using (x∈xs⇒fx∈fxs; _⊗_; _,_) +open import Utils using (x∈xs⇒fx∈fxs; _⊗_; _,_; ∈-cartesianProduct) record Graph : Set where constructor MkGraph @@ -31,157 +31,218 @@ record Graph : Set where field nodes : Vec (List BasicStmt) size edges : List Edge + inputs : List Index + outputs : List Index -empty : Graph -empty = record - { size = 0 - ; nodes = [] - ; edges = [] +_↑ˡ_ : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n Nat.+ m) × Fin (n Nat.+ m)) +_↑ˡ_ (idx₁ , idx₂) m = (idx₁ Fin.↑ˡ m , idx₂ Fin.↑ˡ m) + +_↑ʳ_ : ∀ {m} n → (Fin m × Fin m) → Fin (n Nat.+ m) × Fin (n Nat.+ m) +_↑ʳ_ n (idx₁ , idx₂) = (n Fin.↑ʳ idx₁ , n Fin.↑ʳ idx₂) + +_↑ˡⁱ_ : ∀ {n} → List (Fin n) → ∀ m → List (Fin (n Nat.+ m)) +_↑ˡⁱ_ l m = List.map (Fin._↑ˡ m) l + +_↑ʳⁱ_ : ∀ {m} n → List (Fin m) → List (Fin (n Nat.+ m)) +_↑ʳⁱ_ n l = List.map (n Fin.↑ʳ_) l + +_↑ˡᵉ_ : ∀ {n} → List (Fin n × Fin n) → ∀ m → List (Fin (n Nat.+ m) × Fin (n Nat.+ m)) +_↑ˡᵉ_ l m = List.map (_↑ˡ m) l + +_↑ʳᵉ_ : ∀ {m} n → List (Fin m × Fin m) → List (Fin (n Nat.+ m) × Fin (n Nat.+ m)) +_↑ʳᵉ_ n l = List.map (n ↑ʳ_) l + +infixl 5 _∙_ +_∙_ : Graph → Graph → Graph +_∙_ g₁ g₂ = record + { size = Graph.size g₁ Nat.+ Graph.size g₂ + ; nodes = Graph.nodes g₁ ++ Graph.nodes g₂ + ; edges = (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) List.++ + (Graph.size g₁ ↑ʳᵉ Graph.edges g₂) + ; inputs = (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂) List.++ + (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂) + ; outputs = (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂) List.++ + (Graph.size g₁ ↑ʳⁱ Graph.outputs g₂) } -↑ˡ-Edge : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n Nat.+ m) × Fin (n Nat.+ m)) -↑ˡ-Edge (idx₁ , idx₂) m = (idx₁ ↑ˡ m , idx₂ ↑ˡ m) +infixl 5 _↦_ +_↦_ : Graph → Graph → Graph +_↦_ g₁ g₂ = record + { size = Graph.size g₁ Nat.+ Graph.size g₂ + ; nodes = Graph.nodes g₁ ++ Graph.nodes g₂ + ; edges = (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) List.++ + (Graph.size g₁ ↑ʳᵉ Graph.edges g₂) List.++ + (List.cartesianProduct (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂) + (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂)) + ; inputs = Graph.inputs g₁ ↑ˡⁱ Graph.size g₂ + ; outputs = Graph.size g₁ ↑ʳⁱ Graph.outputs g₂ + } + +loop : Graph → Graph +loop g = record + { size = Graph.size g + ; nodes = Graph.nodes g + ; edges = Graph.edges g List.++ + List.cartesianProduct (Graph.outputs g) (Graph.inputs g) + ; inputs = Graph.inputs g + ; outputs = Graph.outputs g + } _[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt _[_] g idx = lookup (Graph.nodes g) idx -record _⊆_ (g₁ g₂ : Graph) : Set where - constructor Mk-⊆ - field - n : ℕ - sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ Nat.+ n - newNodes : Vec (List BasicStmt) n - nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes - e∈g₁⇒e∈g₂ : ∀ {e : Graph.Edge g₁} → - e ListMem.∈ (Graph.edges g₁) → - (↑ˡ-Edge e n) ListMem.∈ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂)) +singleton : List BasicStmt → Graph +singleton bss = record + { size = 1 + ; nodes = bss ∷ [] + ; edges = [] + ; inputs = zero ∷ [] + ; outputs = zero ∷ [] + } -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₂) +buildCfg : Stmt → Graph +buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ []) +buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂ +buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton [] +buildCfg (while _ repeat s) = loop (buildCfg s ↦ singleton []) - ↑ˡ-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 - - ↑ˡ-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 - - 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₃} - (Mk-⊆ n₁ p₁@refl newNodes₁ nsg₂≡nsg₁++newNodes₁ e∈g₁⇒e∈g₂) - (Mk-⊆ n₂ p₂@refl newNodes₂ nsg₃≡nsg₂++newNodes₂ e∈g₂⇒e∈g₃) - rewrite cast-is-id refl ns₂ - rewrite cast-is-id refl ns₃ - with refl ← nsg₂≡nsg₁++newNodes₁ - with refl ← nsg₃≡nsg₂++newNodes₂ = - record - { n = n₁ Nat.+ n₂ - ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂ - ; newNodes = newNodes₁ ++ newNodes₂ - ; nsg₂≡nsg₁++newNodes = ++-assoc (+-assoc s₁ n₁ n₂) ns₁ newNodes₁ newNodes₂ - ; e∈g₁⇒e∈g₂ = λ {e} e∈g₁ → - cast∈⇒∈subst (sym (+-assoc s₁ n₁ n₂)) (+-assoc s₁ n₁ n₂) _ _ - (subst (λ e' → e' ListMem.∈ es₃) - (↑ˡ-Edge-assoc e (sym (+-assoc s₁ n₁ n₂))) - (e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁))) - } - -open import MonotonicState _⊆_ ⊆-trans renaming (MonotonicState to MonotonicGraphFunction) - -instance - IndexRelaxable : Relaxable Graph.Index - IndexRelaxable = record - { relax = λ { (Mk-⊆ n refl _ _ _) idx → idx ↑ˡ n } - } - - EdgeRelaxable : Relaxable Graph.Edge - EdgeRelaxable = record - { relax = λ g₁⊆g₂ (idx₁ , idx₂) → - ( Relaxable.relax IndexRelaxable g₁⊆g₂ idx₁ - , Relaxable.relax IndexRelaxable g₁⊆g₂ idx₂ - ) - } - -open Relaxable {{...}} - -pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index -pushBasicBlock bss g = - ( record - { size = Graph.size g Nat.+ 1 - ; nodes = Graph.nodes g ++ (bss ∷ []) - ; edges = List.map (λ e → ↑ˡ-Edge e 1) (Graph.edges g) - } - , ( Graph.size g ↑ʳ zero - , record - { n = 1 - ; sg₂≡sg₁+n = refl - ; newNodes = (bss ∷ []) - ; nsg₂≡nsg₁++newNodes = cast-is-id refl _ - ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e → ↑ˡ-Edge e 1) e∈g₁ - } - ) - ) - -pushEmptyBlock : MonotonicGraphFunction Graph.Index -pushEmptyBlock = pushBasicBlock [] - -addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g') -addEdges (MkGraph s ns es) es' = - ( record - { size = s - ; nodes = ns - ; edges = es' List.++ es - } - , record - { n = 0 - ; sg₂≡sg₁+n = +-comm 0 s - ; newNodes = [] - ; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns) - ; e∈g₁⇒e∈g₂ = λ {e} e∈es → - cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _ - (subst (λ e' → e' ListMem.∈ _) - (↑ˡ-Edge-identityʳ e (+-comm s 0)) - (ListMemProp.∈-++⁺ʳ es' e∈es)) - } - ) - -buildCfg : Stmt → MonotonicGraphFunction (Graph.Index ⊗ Graph.Index) -buildCfg ⟨ bs₁ ⟩ = pushBasicBlock (bs₁ ∷ []) map (λ g idx → (idx , idx)) -buildCfg (s₁ then s₂) = - (buildCfg s₁ ⟨⊗⟩ buildCfg s₂) - update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → addEdges g ((idx₂ , idx₃) ∷ []) }) - map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → (idx₁ , idx₄) }) -buildCfg (if _ then s₁ else s₂) = - (buildCfg s₁ ⟨⊗⟩ buildCfg s₂ ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock) - update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → - addEdges g ((idx , idx₁) ∷ (idx , idx₃) ∷ (idx₂ , idx') ∷ (idx₄ , idx') ∷ []) }) - map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → (idx , idx') }) -buildCfg (while _ repeat s) = - (buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock) - update (λ { g ((idx₁ , idx₂) , idx , idx') → - addEdges g ((idx , idx') ∷ (idx , idx₁) ∷ (idx₂ , idx) ∷ []) }) - map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') }) +-- record _⊆_ (g₁ g₂ : Graph) : Set where +-- constructor Mk-⊆ +-- field +-- n : ℕ +-- sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ Nat.+ n +-- newNodes : Vec (List BasicStmt) n +-- nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes +-- e∈g₁⇒e∈g₂ : ∀ {e : Graph.Edge g₁} → +-- e ListMem.∈ (Graph.edges g₁) → +-- (↑ˡ-Edge e n) ListMem.∈ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂)) +-- +-- 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 +-- +-- ↑ˡ-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 +-- +-- ↑ˡ-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 +-- +-- ⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃ +-- ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃} +-- (Mk-⊆ n₁ p₁@refl newNodes₁ nsg₂≡nsg₁++newNodes₁ e∈g₁⇒e∈g₂) +-- (Mk-⊆ n₂ p₂@refl newNodes₂ nsg₃≡nsg₂++newNodes₂ e∈g₂⇒e∈g₃) +-- rewrite cast-is-id refl ns₂ +-- rewrite cast-is-id refl ns₃ +-- with refl ← nsg₂≡nsg₁++newNodes₁ +-- with refl ← nsg₃≡nsg₂++newNodes₂ = +-- record +-- { n = n₁ Nat.+ n₂ +-- ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂ +-- ; newNodes = newNodes₁ ++ newNodes₂ +-- ; nsg₂≡nsg₁++newNodes = ++-assoc (+-assoc s₁ n₁ n₂) ns₁ newNodes₁ newNodes₂ +-- ; e∈g₁⇒e∈g₂ = λ {e} e∈g₁ → +-- cast∈⇒∈subst (sym (+-assoc s₁ n₁ n₂)) (+-assoc s₁ n₁ n₂) _ _ +-- (subst (λ e' → e' ListMem.∈ es₃) +-- (↑ˡ-Edge-assoc e (sym (+-assoc s₁ n₁ n₂))) +-- (e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁))) +-- } +-- +-- open import MonotonicState _⊆_ ⊆-trans renaming (MonotonicState to MonotonicGraphFunction) +-- +-- instance +-- IndexRelaxable : Relaxable Graph.Index +-- IndexRelaxable = record +-- { relax = λ { (Mk-⊆ n refl _ _ _) idx → idx ↑ˡ n } +-- } +-- +-- EdgeRelaxable : Relaxable Graph.Edge +-- EdgeRelaxable = record +-- { relax = λ g₁⊆g₂ (idx₁ , idx₂) → +-- ( Relaxable.relax IndexRelaxable g₁⊆g₂ idx₁ +-- , Relaxable.relax IndexRelaxable g₁⊆g₂ idx₂ +-- ) +-- } +-- +-- open Relaxable {{...}} +-- +-- pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index +-- pushBasicBlock bss g = +-- ( record +-- { size = Graph.size g Nat.+ 1 +-- ; nodes = Graph.nodes g ++ (bss ∷ []) +-- ; edges = List.map (λ e → ↑ˡ-Edge e 1) (Graph.edges g) +-- } +-- , ( Graph.size g ↑ʳ zero +-- , record +-- { n = 1 +-- ; sg₂≡sg₁+n = refl +-- ; newNodes = (bss ∷ []) +-- ; nsg₂≡nsg₁++newNodes = cast-is-id refl _ +-- ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e → ↑ˡ-Edge e 1) e∈g₁ +-- } +-- ) +-- ) +-- +-- pushEmptyBlock : MonotonicGraphFunction Graph.Index +-- pushEmptyBlock = pushBasicBlock [] +-- +-- addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g') +-- addEdges (MkGraph s ns es) es' = +-- ( record +-- { size = s +-- ; nodes = ns +-- ; edges = es' List.++ es +-- } +-- , record +-- { n = 0 +-- ; sg₂≡sg₁+n = +-comm 0 s +-- ; newNodes = [] +-- ; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns) +-- ; e∈g₁⇒e∈g₂ = λ {e} e∈es → +-- cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _ +-- (subst (λ e' → e' ListMem.∈ _) +-- (↑ˡ-Edge-identityʳ e (+-comm s 0)) +-- (ListMemProp.∈-++⁺ʳ es' e∈es)) +-- } +-- ) +-- +-- buildCfg : Stmt → MonotonicGraphFunction (Graph.Index ⊗ Graph.Index) +-- buildCfg ⟨ bs₁ ⟩ = pushBasicBlock (bs₁ ∷ []) map (λ g idx → (idx , idx)) +-- buildCfg (s₁ then s₂) = +-- (buildCfg s₁ ⟨⊗⟩ buildCfg s₂) +-- update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → addEdges g ((idx₂ , idx₃) ∷ []) }) +-- map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄)) → (idx₁ , idx₄) }) +-- buildCfg (if _ then s₁ else s₂) = +-- (buildCfg s₁ ⟨⊗⟩ buildCfg s₂ ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock) +-- update (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → +-- addEdges g ((idx , idx₁) ∷ (idx , idx₃) ∷ (idx₂ , idx') ∷ (idx₄ , idx') ∷ []) }) +-- map (λ { g ((idx₁ , idx₂) , (idx₃ , idx₄) , idx , idx') → (idx , idx') }) +-- buildCfg (while _ repeat s) = +-- (buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock) +-- update (λ { g ((idx₁ , idx₂) , idx , idx') → +-- addEdges g ((idx , idx') ∷ (idx , idx₁) ∷ (idx₂ , idx) ∷ []) }) +-- map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') }) diff --git a/Language/Properties.agda b/Language/Properties.agda index e3138a4..15b11ab 100644 --- a/Language/Properties.agda +++ b/Language/Properties.agda @@ -5,48 +5,24 @@ open import Language.Semantics open import Language.Graphs open import Language.Traces -open import MonotonicState _⊆_ ⊆-trans renaming (MonotonicState to MonotonicGraphFunction) -open import Utils using (_⊗_; _,_) -open Relaxable {{...}} +open import Data.Fin as Fin using (zero) +open import Data.List using (_∷_; []) +open import Data.Product using (Σ; _,_) -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; subst) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) -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₁) _ _) +buildCfg-input : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.inputs g ≡ idx ∷ []) +buildCfg-input ⟨ bs₁ ⟩ = (zero , refl) +buildCfg-input (s₁ then s₂) + with (idx , p) ← buildCfg-input s₁ rewrite p = (_ , refl) +buildCfg-input (if _ then s₁ else s₂) = (zero , refl) +buildCfg-input (while _ repeat s) + with (idx , p) ← buildCfg-input s rewrite p = (_ , refl) -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) - -TransformsEnv : ∀ (ρ₁ ρ₂ : Env) → DependentPredicate (Graph.Index ⊗ Graph.Index) -TransformsEnv ρ₁ ρ₂ g (idx₁ , idx₂) = Trace {g} idx₁ idx₂ ρ₁ ρ₂ - -instance - TransformsEnvMonotonic : ∀ {ρ₁ ρ₂ : Env} → MonotonicPredicate (TransformsEnv ρ₁ ρ₂) - TransformsEnvMonotonic = {!!} - -buildCfg-sufficient : ∀ {ρ₁ ρ₂ : Env} {s : Stmt} → ρ₁ , s ⇒ˢ ρ₂ → Always (TransformsEnv ρ₁ ρ₂) (buildCfg s) -buildCfg-sufficient {ρ₁} {ρ₂} {⟨ bs ⟩} (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) = - pushBasicBlock-works (bs ∷ []) - map-reason - (λ g idx g[idx]≡[bs] → Trace-single (subst (ρ₁ ,_⇒ᵇˢ ρ₂) - (sym g[idx]≡[bs]) - (ρ₁,bs⇒ρ₂ ∷ []))) -buildCfg-sufficient {ρ₁} {ρ₂} {s₁ then s₂} (⇒ˢ-then ρ₁ ρ ρ₂ s₁ s₂ ρ₁,s₁⇒ρ₂ ρ₂,s₂⇒ρ₃) = - (buildCfg-sufficient ρ₁,s₁⇒ρ₂ ⟨⊗⟩-reason buildCfg-sufficient ρ₂,s₂⇒ρ₃) - update-reason {!!} - map-reason {!!} +buildCfg-output : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.outputs g ≡ idx ∷ []) +buildCfg-output ⟨ bs₁ ⟩ = (zero , refl) +buildCfg-output (s₁ then s₂) + with (idx , p) ← buildCfg-output s₂ rewrite p = (_ , refl) +buildCfg-output (if _ then s₁ else s₂) = (_ , refl) +buildCfg-output (while _ repeat s) + with (idx , p) ← buildCfg-output s rewrite p = (_ , refl) diff --git a/Utils.agda b/Utils.agda index d37da9f..d1c7c09 100644 --- a/Utils.agda +++ b/Utils.agda @@ -1,9 +1,11 @@ module Utils where open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_) +open import Data.Product as Prod using () open import Data.Nat using (ℕ; suc) -open import Data.List using (List; []; _∷_; _++_) renaming (map to mapˡ) +open import Data.List using (List; cartesianProduct; []; _∷_; _++_) renaming (map to mapˡ) open import Data.List.Membership.Propositional using (_∈_) +open import Data.List.Membership.Propositional.Properties as ListMemProp using () open import Data.List.Relation.Unary.All using (All; []; _∷_; map) open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map open import Function.Definitions using (Injective) @@ -78,3 +80,9 @@ proj₁ (v , _) = v proj₂ : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {a : A} → (P ⊗ Q) a → Q a proj₂ (_ , v) = v + +∈-cartesianProduct : ∀ {a b} {A : Set a} {B : Set b} + {x : A} {xs : List A} {y : B} {ys : List B} → + x ∈ xs → y ∈ ys → (x Prod., y) ∈ cartesianProduct xs ys +∈-cartesianProduct {x = x} (here refl) y∈ys = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (x Prod.,_) y∈ys) +∈-cartesianProduct {x = x} {xs = x' ∷ _} {ys = ys} (there x∈rest) y∈ys = ListMemProp.∈-++⁺ʳ (mapˡ (x' Prod.,_) ys) (∈-cartesianProduct x∈rest y∈ys)