From 82027ecd045882b951851e10b405270da2eac56e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 9 May 2024 21:26:32 -0700 Subject: [PATCH] Move predecessor computation into Graphs Signed-off-by: Danila Fedorin --- Language.agda | 32 ++++--------------------------- Language/Graphs.agda | 45 ++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 47 insertions(+), 30 deletions(-) diff --git a/Language.agda b/Language.agda index a8d1c3f..a35ee01 100644 --- a/Language.agda +++ b/Language.agda @@ -11,8 +11,6 @@ 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 () open import Data.List.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺) -open import Data.List.Relation.Unary.All using (All; []; _∷_) -open import Data.List.Relation.Unary.Any as RelAny using () open import Data.Nat using (ℕ; suc) open import Data.Product using (_,_; Σ; proj₁; proj₂) open import Data.Product.Properties as ProdProp using () @@ -28,28 +26,6 @@ open import Lattice.MapSet _≟ˢ_ using () ; to-List to to-Listˢ ) -private - z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f) - z≢sf f () - - z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs) - z≢mapsfs [] = [] - z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs' - - indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique - indices 0 = ([] , Utils.empty) - indices (suc n') = - let - (inds' , unids') = indices n' - in - ( zero ∷ List.map suc inds' - , push (z≢mapsfs inds') (Unique-map suc suc-injective unids') - ) - - indices-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (indices n)) - indices-complete (suc n') zero = RelAny.here refl - indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f')) - record Program : Set where field rootStmt : Stmt @@ -77,13 +53,13 @@ record Program : Set where vars-Unique = proj₂ vars-Set states : List State - states = proj₁ (indices (Graph.size graph)) + states = indices graph states-complete : ∀ (s : State) → s ListMem.∈ states - states-complete = indices-complete (Graph.size graph) + states-complete = indices-complete graph states-Unique : Unique states - states-Unique = proj₂ (indices (Graph.size graph)) + states-Unique = indices-Unique graph code : State → List BasicStmt code st = graph [ st ] @@ -100,7 +76,7 @@ record Program : Set where open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_) incoming : State → List State - incoming idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges graph)) states + incoming = predecessors graph edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) → s₁ ListMem.∈ (incoming s₂) diff --git a/Language/Graphs.agda b/Language/Graphs.agda index 0976fe3..bb5599f 100644 --- a/Language/Graphs.agda +++ b/Language/Graphs.agda @@ -7,15 +7,19 @@ 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 () open import Data.List.Membership.Propositional.Properties as ListMemProp using () +open import Data.List.Relation.Unary.All using (All; []; _∷_) +open import Data.List.Relation.Unary.Any as RelAny using () open import Data.Nat as Nat using (ℕ; suc) open import Data.Nat.Properties using (+-assoc; +-comm) -open import Data.Product using (_×_; Σ; _,_) +open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) +open import Data.Product.Properties as ProdProp using () open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_) 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 Relation.Nullary using (¬_) open import Lattice -open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct) +open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct) record Graph : Set where constructor MkGraph @@ -120,3 +124,40 @@ 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) + +private + z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f) + z≢sf f () + + z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs) + z≢mapsfs [] = [] + z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs' + + finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique + finValues 0 = ([] , Utils.empty) + finValues (suc n') = + let + (inds' , unids') = finValues n' + in + ( zero ∷ List.map suc inds' + , push (z≢mapsfs inds') (Unique-map suc suc-injective unids') + ) + + finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n)) + finValues-complete (suc n') zero = RelAny.here refl + finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f')) + +module _ (g : Graph) where + open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size g}) (FinProp._≟_ {Graph.size g})) using (_∈?_) + + indices : List (Graph.Index g) + indices = proj₁ (finValues (Graph.size g)) + + indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices + indices-complete = finValues-complete (Graph.size g) + + indices-Unique : Unique indices + indices-Unique = proj₂ (finValues (Graph.size g)) + + predecessors : (Graph.Index g) → List (Graph.Index g) + predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices