117 lines
5.7 KiB
Agda
117 lines
5.7 KiB
Agda
module Lattice.Builder where
|
||
|
||
open import Lattice
|
||
open import Equivalence
|
||
open import Utils using (fins; fins-complete)
|
||
open import Data.Nat as Nat using (ℕ)
|
||
open import Data.Fin as Fin using (Fin; suc; zero; _≟_)
|
||
open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
|
||
open import Data.Maybe.Properties using (just-injective)
|
||
open import Data.Unit using (⊤; tt)
|
||
open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_)
|
||
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_; mapWith∈ to mapWith∈ˡ)
|
||
open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ)
|
||
open import Data.List.Relation.Unary.Any using (Any; here; there)
|
||
open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
|
||
open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr) renaming (_++_ to _++ˡ_)
|
||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||
open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂)
|
||
open import Data.Empty using (⊥; ⊥-elim)
|
||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
|
||
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
|
||
|
||
record Graph : Set where
|
||
constructor mkGraph
|
||
field
|
||
size : ℕ
|
||
|
||
Node : Set
|
||
Node = Fin size
|
||
|
||
nodes = fins size
|
||
|
||
nodes-complete = fins-complete size
|
||
|
||
Edge : Set
|
||
Edge = Node × Node
|
||
|
||
field
|
||
edges : List Edge
|
||
|
||
data Path : Node → Node → Set where
|
||
done : ∀ {n : Node} → Path n n
|
||
step : ∀ {n₁ n₂ n₃ : Node} → (n₁ , n₂) ∈ˡ edges → Path n₂ n₃ → Path n₁ n₃
|
||
|
||
_++_ : ∀ {n₁ n₂ n₃} → Path n₁ n₂ → Path n₂ n₃ → Path n₁ n₃
|
||
done ++ p = p
|
||
(step e p₁) ++ p₂ = step e (p₁ ++ p₂)
|
||
|
||
interior : ∀ {n₁ n₂} → Path n₁ n₂ → List Node
|
||
interior done = []
|
||
interior (step _ done) = []
|
||
interior (step {n₂ = n₂} _ p) = n₂ ∷ interior p
|
||
|
||
Adjacency : Set
|
||
Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂)
|
||
|
||
Adjacency-update : ∀ (n₁ n₂ : Node) → (List (Path n₁ n₂) → List (Path n₁ n₂)) → Adjacency → Adjacency
|
||
Adjacency-update n₁ n₂ f adj n₁' n₂'
|
||
with n₁ ≟ n₁' | n₂ ≟ n₂'
|
||
... | yes refl | yes refl = f (adj n₁ n₂)
|
||
... | _ | _ = adj n₁' n₂'
|
||
|
||
Adjacency-merge : Adjacency → Adjacency → Adjacency
|
||
Adjacency-merge adj₁ adj₂ n₁ n₂ = adj₁ n₁ n₂ ++ˡ adj₂ n₁ n₂
|
||
|
||
adj⁰ : Adjacency
|
||
adj⁰ n₁ n₂
|
||
with n₁ ≟ n₂
|
||
... | yes refl = done ∷ []
|
||
... | no _ = []
|
||
|
||
seedWithEdges : ∀ (es : List Edge) → (∀ {e} → e ∈ˡ es → e ∈ˡ edges) → Adjacency → Adjacency
|
||
seedWithEdges es e∈es⇒e∈edges adj = foldr (λ ((n₁ , n₂) , n₁n₂∈edges) → Adjacency-update n₁ n₂ ((step n₁n₂∈edges done) ∷_)) adj (mapWith∈ˡ es (λ {e} e∈es → (e , e∈es⇒e∈edges e∈es)))
|
||
|
||
e∈seedWithEdges : ∀ {n₁ n₂ es adj} → (e∈es⇒e∈edges : ∀ {e} → e ∈ˡ es → e ∈ˡ edges) → ∀ (n₁n₂∈es : (n₁ , n₂) ∈ˡ es) → (step (e∈es⇒e∈edges n₁n₂∈es) done) ∈ˡ seedWithEdges es e∈es⇒e∈edges adj n₁ n₂
|
||
e∈seedWithEdges {es = []} e∈es⇒e∈edges ()
|
||
e∈seedWithEdges {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (here refl)
|
||
with n₁' ≟ n₁' | n₂' ≟ n₂'
|
||
... | yes refl | yes refl = here refl
|
||
... | no n₁'≢n₁' | _ = ⊥-elim (n₁'≢n₁' refl)
|
||
... | _ | no n₂'≢n₂' = ⊥-elim (n₂'≢n₂' refl)
|
||
e∈seedWithEdges {n₁} {n₂} {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (there n₁n₂∈es)
|
||
with n₁' ≟ n₁ | n₂' ≟ n₂
|
||
... | yes refl | yes refl = there (e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es)
|
||
... | no _ | no _ = e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
|
||
... | no _ | yes _ = e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
|
||
... | yes refl | no _ = e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es
|
||
|
||
adj¹ : Adjacency
|
||
adj¹ = seedWithEdges edges (λ x → x) adj⁰
|
||
|
||
edge∈adj¹ : ∀ {n₁ n₂} (n₁n₂∈edges : (n₁ , n₂) ∈ˡ edges) → (step n₁n₂∈edges done) ∈ˡ adj¹ n₁ n₂
|
||
edge∈adj¹ = e∈seedWithEdges (λ x → x)
|
||
|
||
through : Node → Adjacency → Adjacency
|
||
through n adj n₁ n₂ = cartesianProductWith _++_ (adj n₁ n) (adj n n₂) ++ˡ adj n₁ n₂
|
||
|
||
through-monotonic : ∀ adj n {n₁ n₂ p} → p ∈ˡ adj n₁ n₂ → p ∈ˡ (through n adj) n₁ n₂
|
||
through-monotonic adj n p∈adjn₁n₂ = ∈ˡ-++⁺ʳ _ p∈adjn₁n₂
|
||
|
||
throughAll : List Node → Adjacency
|
||
throughAll = foldr through adj¹
|
||
|
||
throughAll-adj₁ : ∀ {n₁ n₂ p} ns → p ∈ˡ adj¹ n₁ n₂ → p ∈ˡ throughAll ns n₁ n₂
|
||
throughAll-adj₁ [] p∈adj¹ = p∈adj¹
|
||
throughAll-adj₁ (n ∷ ns) p∈adj¹ = through-monotonic (throughAll ns) n (throughAll-adj₁ ns p∈adj¹)
|
||
|
||
-- paths-throughAll : ∀ {n₁ n₂ : Node} (p : Path n₁ n₂) (ns : List Node) → All (λ n → n ∈ˡ ns) (interior p) → p ∈ˡ throughAll ns n₁ n₂
|
||
-- paths-throughAll (last n₁n₂∈edges) ns _ = throughAll-adj₁ ns (edge∈adj¹ n₁n₂∈edges)
|
||
|
||
adj : Adjacency
|
||
adj = throughAll (proj₁ nodes)
|
||
|
||
NoCycles : Set
|
||
NoCycles = ∀ (n : Node) → All (_≡ done) (adj n n)
|