
   0 | ||| A representation for sparse, simple, undirected
   1 | ||| labeled graphs.
   2 | |||
   3 | ||| This module provides only the data types plus
   4 | ||| interface implementations.
   5 | module Data.Graph.Types
   6 | 
   7 | import Data.AssocList
   8 | import Data.BitMap
   9 | import Data.Prim.Bits32
  10 | 
  11 | %default total
  12 | 
  13 | --------------------------------------------------------------------------------
  14 | --          Nodes and Edges
  15 | --------------------------------------------------------------------------------
  16 | 
  17 | export infixl 4 :>, <>
  18 | 
  19 | ||| A node in an undirected graph.
  20 | public export
  21 | Node : Type
  22 | Node = Bits32
  23 | 
  24 | ||| An edge in a simple, undirected graph.
  25 | ||| Since edges go in both directions and loops are not allowed,
  26 | ||| we can enforce without loss of generality
  27 | ||| that `n2 > n1 = True`.
  28 | public export
  29 | record Edge where
  30 |   constructor MkEdge
  31 |   node1 : Node
  32 |   node2 : Node
  33 |   0 prf : node2 > node1
  34 | 
  35 | public export
  36 | mkEdge : Node -> Node -> Maybe Edge
  37 | mkEdge k j = case comp k j of
  38 |   LT p _ _ => Just $ MkEdge k j p
  39 |   GT _ _ p => Just $ MkEdge j k p
  40 |   EQ _ _ _ => Nothing
  41 | 
  42 | public export %inline
  43 | (<>) : (i,j : Node) -> (0 prf : j > i) => Edge
  44 | i <> j = MkEdge i j prf
  45 | 
  46 | public export
  47 | Eq Edge where
  48 |   MkEdge m1 n1 _ == MkEdge m2 n2 _ = m1 == m2 && n1 == n2
  49 | 
  50 | public export
  51 | Ord Edge where
  52 |   compare (MkEdge m1 n1 _) (MkEdge m2 n2 _) =
  53 |     compare m1 m2 <+> compare n1 n2
  54 | 
  55 | export
  56 | Show Edge where
  57 |   showPrec p (MkEdge n1 n2 _) =
  58 |     showCon p "\{show n1} <> \{show n2}" ""
  59 | 
  60 | --------------------------------------------------------------------------------
  61 | --          Labeled Nodes and Edges
  62 | --------------------------------------------------------------------------------
  63 | 
  64 | ||| A labeled node in a graph.
  65 | public export
  66 | record LNode n where
  67 |   constructor MkLNode
  68 |   node  : Node
  69 |   label : n
  70 | 
  71 | public export
  72 | Eq a => Eq (LNode a) where
  73 |   MkLNode n1 l1 == MkLNode n2 l2 = n1 == n2 && l1 == l2
  74 | 
  75 | export
  76 | Show n => Show (LNode n) where
  77 |   showPrec p (MkLNode k l) =
  78 |     showCon p "\{show k} :> \{show l}" ""
  79 | 
  80 | namespace LNode
  81 |   public export %inline
  82 |   (:>) : Node -> n -> LNode n
  83 |   (:>) = MkLNode
  84 | 
  85 | public export %inline
  86 | Functor LNode where
  87 |   map f ln = { label $= f } ln
  88 | 
  89 | public export %inline
  90 | Foldable LNode where
  91 |   foldl f a n  = f a n.label
  92 |   foldr f a n  = f n.label a
  93 |   foldMap  f n = f n.label
  94 |   null _       = False
  95 |   toList n     = [n.label]
  96 |   foldlM f a n = f a n.label
  97 | 
  98 | public export %inline
  99 | Traversable LNode where
 100 |   traverse f (MkLNode n l) = MkLNode n <$> f l
 101 | 
 102 | ||| A labeled edge in an undirected graph
 103 | public export
 104 | record LEdge e where
 105 |   constructor MkLEdge
 106 |   edge  : Edge
 107 |   label : e
 108 | 
 109 | public export
 110 | Eq a => Eq (LEdge a) where
 111 |   MkLEdge e1 l1 == MkLEdge e2 l2 = e1 == e2 && l1 == l2
 112 | 
 113 | public export
 114 | Ord a => Ord (LEdge a) where
 115 |   compare (MkLEdge e1 l1) (MkLEdge e2 l2) =
 116 |     compare e1 e2 <+> compare l1 l2
 117 | 
 118 | export
 119 | Show e => Show (LEdge e) where
 120 |   showPrec p (MkLEdge ed l) =
 121 |     showCon p "\{show ed} :> \{show l}" ""
 122 | 
 123 | namespace LEdge
 124 |   public export %inline
 125 |   (:>) : Edge -> e -> LEdge e
 126 |   (:>) = MkLEdge
 127 | 
 128 | public export %inline
 129 | Functor LEdge where
 130 |   map f le = { label $= f } le
 131 | 
 132 | public export %inline
 133 | Foldable LEdge where
 134 |   foldl f a n  = f a n.label
 135 |   foldr f a n  = f n.label a
 136 |   foldMap  f n = f n.label
 137 |   null _       = False
 138 |   toList n     = [n.label]
 139 |   foldlM f a n = f a n.label
 140 | 
 141 | public export %inline
 142 | Traversable LEdge where
 143 |   traverse f (MkLEdge n l) = MkLEdge n <$> f l
 144 | 
 145 | --------------------------------------------------------------------------------
 146 | --          Context
 147 | --------------------------------------------------------------------------------
 148 | 
 149 | ||| Adjacency info of a `Node` in a labeled graph.
 150 | |||
 151 | ||| This consists of the node's label plus
 152 | ||| a list of all its neighboring nodes and
 153 | ||| the labels of the edges connecting them.
 154 | |||
 155 | ||| This is what is stored in underlying `BitMap`
 156 | ||| representing the graph.
 157 | public export
 158 | record Adj e n where
 159 |   constructor MkAdj
 160 |   label           : n
 161 |   neighbours      : AssocList e
 162 | 
 163 | public export
 164 | Eq e => Eq n => Eq (Adj e n) where
 165 |   MkAdj l1 ns1 == MkAdj l2 ns2 = l1 == l2 && ns1 == ns2
 166 | 
 167 | export
 168 | Show e => Show n => Show (Adj e n) where
 169 |   showPrec p (MkAdj lbl ns) = showCon p "MkAdj" $ showArg lbl ++ showArg ns
 170 | 
 171 | public export
 172 | Functor (Adj e) where
 173 |   map f adj = { label $= f } adj
 174 | 
 175 | public export
 176 | Foldable (Adj e) where
 177 |   foldl f a n  = f a n.label
 178 |   foldr f a n  = f n.label a
 179 |   foldMap  f n = f n.label
 180 |   null _       = False
 181 |   toList n     = [n.label]
 182 |   foldlM f a n = f a n.label
 183 | 
 184 | public export %inline
 185 | Traversable (Adj e) where
 186 |   traverse f (MkAdj n l) = (`MkAdj` l) <$> f n
 187 | 
 188 | namespace AdjFunctor
 189 |   [AdjEdge] Functor (`Adj` n) where
 190 |     map f = {neighbours $= map f}
 191 | 
 192 | namespace AdjFoldable
 193 |   [AdjEdge] Foldable (`Adj` n) where
 194 |     foldl f a  = foldl f a . neighbours
 195 |     foldr f a  = foldr f a . neighbours
 196 |     foldMap  f = foldMap f . neighbours
 197 |     null       = null . neighbours
 198 |     toList     = toList . neighbours
 199 |     foldlM f a = foldlM f a . neighbours
 200 | 
 201 | public export
 202 | Bifunctor Adj where
 203 |   bimap  f g (MkAdj l es) = MkAdj (g l) (map f es)
 204 |   mapFst f (MkAdj l es)   = MkAdj l (map f es)
 205 |   mapSnd g (MkAdj l es)   = MkAdj (g l) es
 206 | 
 207 | public export
 208 | Bifoldable Adj where
 209 |   bifoldr f g acc (MkAdj l es) = foldr f (g l acc) es
 210 |   bifoldl f g acc (MkAdj l es) = g (foldl f acc es) l
 211 |   binull                       _ = False
 212 | 
 213 | public export
 214 | Bitraversable Adj where
 215 |   bitraverse f g (MkAdj l es) = [| MkAdj (g l) (traverse f es) |]
 216 | 
 217 | ||| The Context of a `Node` in a labeled graph
 218 | ||| including the `Node` itself, its label, plus
 219 | ||| its direct neighbors together with the
 220 | ||| labels of the edges leading to them.
 221 | public export
 222 | record Context e n where
 223 |   constructor MkContext
 224 |   node            : Node
 225 |   label           : n
 226 |   neighbours      : AssocList e
 227 | 
 228 | public export
 229 | Eq e => Eq n => Eq (Context e n) where
 230 |   MkContext n1 l1 ns1 == MkContext n2 l2 ns2 =
 231 |     n1 == n2 && l1 == l2 && ns1 == ns2
 232 | 
 233 | export
 234 | Show e => Show n => Show (Context e n) where
 235 |   showPrec p (MkContext n lbl ns) =
 236 |     showCon p "MkContext" $ showArg n ++ showArg lbl ++ showArg ns
 237 | 
 238 | public export
 239 | Functor (Context e) where
 240 |   map f c = { label $= f } c
 241 | 
 242 | public export
 243 | Foldable (Context e) where
 244 |   foldl f a n  = f a n.label
 245 |   foldr f a n  = f n.label a
 246 |   foldMap  f n = f n.label
 247 |   null _       = False
 248 |   toList n     = [n.label]
 249 |   foldlM f a n = f a n.label
 250 | 
 251 | namespace ContextFunctor
 252 |   [CtxtEdge] Functor (`Context` n) where
 253 |     map f = {neighbours $= map f}
 254 | 
 255 | namespace ContextFoldable
 256 |   [CtxtEdge] Foldable (`Context` n) where
 257 |     foldl f a  = foldl f a . neighbours
 258 |     foldr f a  = foldr f a . neighbours
 259 |     foldMap  f = foldMap f . neighbours
 260 |     null       = null . neighbours
 261 |     toList     = toList . neighbours
 262 |     foldlM f a = foldlM f a . neighbours
 263 | 
 264 | public export %inline
 265 | Traversable (Context e) where
 266 |   traverse f (MkContext n l es) =
 267 |     (\l2 => MkContext n l2 es) <$> f l
 268 | 
 269 | public export
 270 | Bifunctor Context where
 271 |   bimap  f g (MkContext n l es) = MkContext n (g l) (map f es)
 272 |   mapFst f (MkContext n l es)   = MkContext n l (map f es)
 273 |   mapSnd g (MkContext n l es)   = MkContext n (g l) es
 274 | 
 275 | public export
 276 | Bifoldable Context where
 277 |   bifoldr f g acc (MkContext _ l es) = foldr f (g l acc) es
 278 |   bifoldl f g acc (MkContext _ l es) = g (foldl f acc es) l
 279 |   binull _                           = False
 280 | 
 281 | public export
 282 | Bitraversable Context where
 283 |   bitraverse f g (MkContext n l es) =
 284 |     [| MkContext (pure n) (g l) (traverse f es) |]
 285 | 
 286 | --------------------------------------------------------------------------------
 287 | --          Graph
 288 | --------------------------------------------------------------------------------
 289 | 
 290 | ||| Internal representation of labeled graphs.
 291 | public export
 292 | GraphRep : (e : Type) -> (n : Type) -> Type
 293 | GraphRep e n = BitMap (Adj e n)
 294 | 
 295 | public export
 296 | record Graph e n where
 297 |   constructor MkGraph
 298 |   graph : GraphRep e n
 299 | 
 300 | export
 301 | Eq e => Eq n => Eq (Graph e n) where
 302 |   MkGraph g1 == MkGraph g2 = g1 == g2
 303 | 
 304 | public export
 305 | Functor (Graph e) where
 306 |   map f g = { graph $= map (map f) } g
 307 | 
 308 | public export
 309 | Foldable (Graph e) where
 310 |   foldl f a  = foldl (\a',adj => f a' adj.label) a . graph
 311 |   foldr f a  = foldr (f . label) a . graph
 312 |   foldMap  f = foldMap (f . label) . graph
 313 |   toList     = map label . toList . graph
 314 |   null g     = isEmpty $ graph g
 315 | 
 316 | namespace GraphFunctor
 317 |   export
 318 |   [OnEdge] Functor (`Graph` n) where
 319 |     map f g = { graph $= map {neighbours $= map f} } g
 320 | 
 321 | namespace GraphFoldable
 322 |   export
 323 |   [OnEdge] Foldable (`Graph` n) where
 324 |     foldr f a = foldr (\v,x => foldr f x v.neighbours) a . graph
 325 |     foldl f a = foldl (\x,v => foldl f x v.neighbours) a . graph
 326 |     foldMap f = foldMap (\v => foldMap f v.neighbours) . graph
 327 |     toList g  = toList g.graph >>= toList . neighbours
 328 |     null   g  = all (null . neighbours) g.graph
 329 | 
 330 | public export %inline
 331 | Traversable (Graph e) where
 332 |   traverse f (MkGraph g) = MkGraph <$> traverse (traverse f) g
 333 | 
 334 | public export
 335 | Bifunctor Graph where
 336 |   bimap  f g (MkGraph m) = MkGraph $ bimap f g <$> m
 337 |   mapFst f (MkGraph m)   = MkGraph $ mapFst f <$> m
 338 |   mapSnd g (MkGraph m)   = MkGraph $ mapSnd g <$> m
 339 | 
 340 | public export
 341 | Bifoldable Graph where
 342 |   bifoldr f g acc =
 343 |     foldr (flip $ bifoldr f g) acc . graph
 344 |   bifoldl f g acc =
 345 |     foldl (bifoldl f g) acc . graph
 346 |   binull = null
 347 | 
 348 | public export
 349 | Bitraversable Graph where
 350 |   bitraverse f g (MkGraph m) =
 351 |     [| MkGraph (traverse (bitraverse f g) m) |]
 352 | 
 353 | --------------------------------------------------------------------------------
 354 | --          Decomposition
 355 | --------------------------------------------------------------------------------
 356 | 
 357 | public export
 358 | data Decomp : (e : Type) -> (n : Type) -> Type where
 359 |   Split : (ctxt : Context e n) -> (gr : Graph e n) -> Decomp e n
 360 |   Empty : Decomp e n
 361 |