erwig.idr

module Graph

%default total

Node : Type
Node = Nat

Adj : Type -> Type
Adj a = List (a, Node)

Context : Type -> Type -> Type
Context a b = (Adj b, Node, a, Adj b)

data Graph a b = Empty | 
                 (&) (Context a b) (Graph a b)

infixr 10 & -- So we can do `context & graph` to construct graphs

isEmpty : Graph a b -> Bool
isEmpty Empty = True
isEmpty _ = False

gmap : (Context a b -> Context a b) -> Graph a b -> Graph a b
gmap fn Empty = Empty
gmap fn (co & gr) = (fn co) & (gmap fn gr)

grev : Graph a b -> Graph a b
grev = gmap swap where swap (p, v, l, s) = (s, v, l, p)

n1 : Node
n1 = 1

n2 : Node
n2 = 2

n3 : Node
n3 = 3

left : Adj String
left = [("left", 2)]

up : Adj String
up = [("up", 3)]

right : Adj String
right = [("right", 2)]

down : Adj String
down = [("down", 3)]

g : Graph String String
g = (left ++ up, n1, "a", right) & 
            ([], n2, "b", down)  & 
            ([], n3, "c", [])    & Empty
 

*Graph> g
([("left", 2), ("up", 3)], 1, "a", [("right", 2)]) &
([], 2, "b", [("down", 3)]) &
([], 3, "c", []) & Empty : Graph String String
*Graph> grev g
([("right", 2)], 1, "a", [("left", 2), ("up", 3)]) &
([("down", 3)], 2, "b", []) &
([], 3, "c", []) & Empty : Graph String String