Graphs in agda

Graph.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 = 2 ∷ 4 ∷ []
  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