Extend API

src/API.agda

@@ -27,11 +27,36 @@ connects = foldr connect empty
 vertices : ∀ {A} -> List A -> Graph A
 vertices = overlays ∘ map vertex
 
-clique : ∀ {A} -> List A -> Graph A
-clique = connects ∘ map vertex
-
 edges : ∀ {A} -> List (A × A) -> Graph A
 edges = overlays ∘ map (uncurry edge)
 
 graph : ∀ {A} -> List A -> List (A × A) -> Graph A
 graph vs es = overlay (vertices vs) (edges es)
+
+foldg : ∀ {A} {B : Set} -> B -> (A -> B) -> (B -> B -> B) -> (B -> B -> B) -> Graph A -> B
+foldg {A} {B} e w o c = go
+  where
+    go : Graph A -> B
+    go ε       = e
+    go (v x)   = w x
+    go (x + y) = o (go x) (go y)
+    go (x * y) = c (go x) (go y)
+
+path : ∀ {A} -> List A -> Graph A
+path []        = empty
+path (x :: []) = vertex x
+path (x :: xs) = edges (zip (x :: xs) xs)
+
+circuit : ∀ {A} -> List A -> Graph A
+circuit []        = empty
+circuit (x :: xs) = path ([ x ] ++ xs ++ [ x ])
+
+clique : ∀ {A} -> List A -> Graph A
+clique = connects ∘ map vertex
+
+biclique : ∀ {A} -> List A -> List A -> Graph A
+biclique xs ys = connect (vertices xs) (vertices ys)
+
+star : ∀ {A} -> A -> List A -> Graph A
+star x ys = connect (vertex x) (vertices ys)
+

src/API/Theorems.agda

@@ -7,7 +7,7 @@ open import Prelude
 open import Reasoning
 
 -- vertices [x] == vertex x
-vertices-vertex : ∀ {A} {x : A} -> vertices (x :: []) ≡ vertex x
+vertices-vertex : ∀ {A} {x : A} -> vertices [ x ] ≡ vertex x
 vertices-vertex = +identity >> reflexivity
 
 -- vertices xs ⊆ clique xs

src/Prelude.agda

@@ -17,6 +17,10 @@ data List (A : Set) : Set where
   _::_ : A -> List A -> List A
 
 infixr 20 _::_
+infixr 15 _++_
+
+[_] : ∀ {A} -> A -> List A
+[ x ] = x :: []
 
 _++_ : ∀ {A} -> List A -> List A -> List A
 [] ++ l = l
@@ -29,3 +33,8 @@ foldr f b (x :: xs) = f x (foldr f b xs)
 map : ∀ {A B} -> (A -> B) -> List A -> List B
 map f [] = []
 map f (x :: xs) = f x :: map f xs
+
+zip : ∀ {A B} -> List A -> List B -> List (A × B)
+zip [] _                = []
+zip _  []               = []
+zip (x :: xs) (y :: ys) = (x , y) :: zip xs ys