Skip to content

Instantly share code, notes, and snippets.

@louisswarren

louisswarren/Graph.agda

Last active Nov 27, 2019
Embed
What would you like to do?
Graphs in agda
module Graph where
open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)
data Fin : Set where
zero : {n} Fin (suc n)
suc : {n} Fin n Fin (suc n)
len : {A : Set} List A
len [] = zero
len (_ ∷ xs) = suc (len xs)
Index : {A : Set} List A Set
Index xs = Fin (len xs)
_!_ : {A : Set} (xs : List A) Index xs A
(x ∷ xs) ! zero = x
(x ∷ xs) ! suc n = xs ! n
record Graph : Set where
constructor graph
field
∣V∣ :
E : Fin ∣V∣ Fin ∣V∣ List ℕ
V : Set
V = Fin ∣V∣
open Graph renaming (∣V∣ to ∣V_∣ ; E to w[_]_⇒_) public
_∋_⇒_ : (G : Graph) V(G) V(G) Set
G ∋ u ⇒ v = Index (w[ G ] u ⇒ v)
data Walk (G : Graph) : V(G) V(G) Set where
[_] : (u : V(G)) Walk G u u
_⟨_⟩_ : {v w} (u : V(G)) G ∋ u ⇒ v Walk G v w Walk G u w
infixr 10 _⟨_⟩_
walk∣_∣ : {G : Graph} {u v : V(G)} Walk G u v
walk∣ [ u ] ∣ = zero
walk∣_∣ {G} (_⟨_⟩_ {v} u n wlk) = (w[ G ] u ⇒ v) ! n + walk∣ wlk ∣
module example where
pattern f0 = zero
pattern f1 = suc f0
pattern f2 = suc f1
pattern f3 = suc f2
pattern f4 = suc f3
pattern f5 = suc f4
G : Graph
∣V G ∣ = 4
w[ G ] f0 ⇒ f1 = 2 ∷ []
w[ G ] f0 ⇒ f2 = 3 ∷ []
w[ G ] f2 ⇒ f1 = 1 ∷ []
w[ G ] f2 ⇒ f3 = 24 ∷ []
w[ G ] f3 ⇒ f2 = 2 ∷ []
w[ G ] _ ⇒ _ = []
w₁ w₂ : Walk G f0 f1
-- w₁ = f0 ∷ [ f1 ]
-- w₂ = f0 ∷ f2 ∷ f3 ∷ f2 ∷ [ f1 ]
w₁ = f0 ⟨ f0 ⟩ [ f1 ]
w₂ = f0 ⟨ f0 ⟩ f2 ⟨ f0 ⟩ f3 ⟨ f0 ⟩ f2 ⟨ f0 ⟩ [ f1 ]
-- w₂ = f0 ∷ f2 ∷ f3 ∷ f2 ∷ [ f1 ]
len-w₁ len-w₂ :
len-w₁ = walk∣ w₁ ∣
len-w₂ = walk∣ w₂ ∣
open example using (len-w₁ ; len-w₂) public
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.