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

labNodes : Graph a b -> List Node
labNodes Empty = []
labNodes ((_,n,_,_) & gr) = n::(labNodes gr)

match : Node -> Graph a b -> (Maybe (Context a b), Graph a b)
match _ Empty = (Nothing, Empty)
match node ((p,v,l,s) & gr) = if node == v 
                              then ((Just (p,v,l,s)), gr) 
                              else match node gr

matchAny : Graph a b -> (Maybe (Context a b), Graph a b)
matchAny Empty = (Nothing, Empty)
matchAny (c & g) = (Just c, g)

suc : Context a b -> List Node
suc (_,_,_,s) = map snd s

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)

ufold : (Context a b -> c -> c) -> c -> Graph a b -> c
ufold f u Empty = u
ufold f u (c & g) = f c (ufold f u g)

nodes : Graph a b -> List Node
nodes = ufold (\(p,v,l,s) => (v ::)) []

undir : Eq b => Graph a b -> Graph a b
undir = gmap (\(p,v,l,s) => let ps = nub (p++s) in (ps,v,l,ps))

gsuc : Node -> Graph a b -> List Node
gsuc v ((_,_,_,s) & g) = map snd s
gsuc _ Empty = []

del : Node -> Graph a b -> Graph a b
del v (_ & g) = g
del _ Empty = Empty

dfs : List Node -> Graph a b -> List Node
dfs [] _     = []
dfs _  Empty = []
dfs (v::vs) g' with (match v g')
  | (Just c, g) = v::dfs (suc c ++ vs) g
  | (Nothing, g) = dfs vs g

bfs : List Node -> Graph a b -> List Node
bfs [] _ = []
bfs _ Empty = []
bfs (v::vs) g' with (match v g')
  | (Just c, g) = v::(bfs (vs ++ suc c) g)
  | (Nothing, g) = bfs vs g
  
n1 : Node
n1 = 1

n2 : Node
n2 = 2

n3 : Node
n3 = 3

n4 : Node
n4 = 4

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

context : Context String String
context =  ([], 3, "c", [])

data Tree a = Br a (List (Tree a))

postorder : Tree a -> List a
postorder (Br v ts) = concatMap postorder ts++[v]