6 | module Data.Graph.Indexed.Types

  8 | import Data.Array

  9 | import Data.AssocList.Indexed

 10 | import Data.List

 12 | %default total

 18 | public export

 19 | 0 CompFin : Fin k -> Fin k -> Ordering

 20 | CompFin x y = compareNat (finToNat x) (finToNat y)

 22 | 0 weakenL : (x,y : Fin k) -> CompFin (weaken x) (weaken y) === CompFin x y

 23 | weakenL FZ FZ         = Refl

 24 | weakenL FZ (FS x)     = Refl

 25 | weakenL (FS x) FZ     = Refl

 26 | weakenL (FS x) (FS y) = weakenL x y

 28 | 0 weakenLN :

 29 |      (m : Nat)

 30 |   -> (x,y : Fin k)

 31 |   -> CompFin (weakenN m x) (weakenN m y) === CompFin x y

 32 | weakenLN m FZ FZ         = Refl

 33 | weakenLN m FZ (FS x)     = Refl

 34 | weakenLN m (FS x) FZ     = Refl

 35 | weakenLN m (FS x) (FS y) = weakenLN m x y

 37 | 0 finLT : (k : Nat) -> (x : Fin k) -> LT (finToNat x) k

 38 | finLT (S k) FZ     = LTESucc LTEZero

 39 | finLT (S k) (FS x) = LTESucc $ finLT k x

 40 | finLT Z x impossible

 42 | 0 weakenToNatL : (x : Fin k) -> finToNat x === finToNat (weaken x)

 43 | weakenToNatL FZ     = Refl

 44 | weakenToNatL (FS x) = cong S $ weakenToNatL x

 46 | 0 lastLemma : (n : Nat) -> n === finToNat (last {n})

 47 | lastLemma 0     = Refl

 48 | lastLemma (S k) = cong S (lastLemma k)

 50 | 0 ltLemma : (m,n : Nat) -> LT m n -> compareNat m n === LT

 51 | ltLemma 0     (S j) x           = Refl

 52 | ltLemma (S k) (S j) (LTESucc x) = ltLemma k j x

 53 | ltLemma (S k) Z x impossible

 54 | ltLemma Z Z x impossible

 56 | 0 ltLemma2 : (m,n : Nat) -> compareNat m n === LT -> LT m n

 57 | ltLemma2 Z     Z     prf impossible

 58 | ltLemma2 (S x) Z     prf impossible

 59 | ltLemma2 0     (S y) prf = LTESucc LTEZero

 60 | ltLemma2 (S x) (S y) prf = LTESucc $ ltLemma2 x y prf

 62 | 0 edgeLemma :

 63 |      (n : Nat)

 64 |   -> (x : Fin n)

 65 |   -> CompFin (weaken x) (Fin.last {n}) === LT

 66 | edgeLemma n x =

 67 |   let p1 := rewrite (sym $ lastLemma n) in finLT n x

 68 |       p2 := replace {p = \y => LT y (finToNat (last {n}))} (weakenToNatL x) p1

 69 |    in ltLemma _ _ p2

 71 | 0 fromNatLemma :

 72 |      (x,y : Nat)

 73 |   -> (p1 : LT x k)

 74 |   -> (p2 : LT y k)

 75 |   -> (p3 : LT x y)

 76 |   -> CompFin (natToFinLT {n = k} x) (natToFinLT {n = k} y) === LT

 77 | fromNatLemma _ 0 _ _ p3 = absurd p3

 78 | fromNatLemma 0     (S j) (LTESucc x) (LTESucc y) _           = Refl

 79 | fromNatLemma (S i) (S j) (LTESucc x) (LTESucc y) (LTESucc z) =

 80 |   fromNatLemma i j x y z

 82 | 0 ltPlusRight : LT k m -> LT (k + n) (m + n)

 83 | ltPlusRight {k = S x} {m = S y} (LTESucc p) = LTESucc $ ltPlusRight p

 84 | ltPlusRight {k = _}   {m = 0}   p           = absurd p

 85 | ltPlusRight {k = 0}   {m = S y} p           =

 86 |   rewrite plusCommutative y n in LTESucc (lteAddRight n)

 88 | 0 ltPlusLeft : LT k m -> LT (n + k) (n + m)

 89 | ltPlusLeft x =

 90 |   rewrite plusCommutative n k in

 91 |   rewrite plusCommutative n m in ltPlusRight x

 93 | 0 lteAddLeft : (n : Nat) -> LTE n (m + n)

 94 | lteAddLeft n = rewrite plusCommutative m n in lteAddRight n

104 | public export

105 | record Edge (k : Nat) (e : Type) where

106 |   constructor E

107 |   node1 : Fin k

108 |   node2 : Fin k

109 |   label : e

110 |   {auto 0 prf : CompFin node1 node2 === LT}

113 | fromNat :

114 |      (x,y : Nat)

115 |   -> {auto 0 p1 : LT x k}

116 |   -> {auto 0 p2 : LT y k}

117 |   -> {auto 0 p3 : LT x y}

118 |   -> (l : e)

119 |   -> Edge k e

120 | fromNat x y l = E (natToFinLT x) (natToFinLT y) l @{fromNatLemma x y p1 p2 p3}

123 | weakenEdge : Edge k e -> Edge (S k) e

124 | weakenEdge (E x y e @{p}) = E (weaken x) (weaken y) e @{weakenL x y `trans` p}

127 | weakenEdgeN : (0 m : Nat) -> Edge k e -> Edge (k + m) e

128 | weakenEdgeN m (E x y e @{p}) =

129 |   E (weakenN m x) (weakenN m y) e @{weakenLN m x y `trans` p}

133 | incEdge : (k : Nat) -> Edge m e -> Edge (k + m) e

134 | incEdge k (E n1 n2 l @{prf}) =

135 |   fromNat

136 |     (k + finToNat n1)

137 |     (k + finToNat n2)

138 |     @{ltPlusLeft $ finLT m n1}

139 |     @{ltPlusLeft $ finLT m n2}

140 |     @{ltPlusLeft $ ltLemma2 _ _ prf}

141 |     l

150 | compositeEdge : {k : _} -> Fin k -> Fin m -> (l : e) -> Edge (k+m) e

151 | compositeEdge x y l =

152 |   fromNat

153 |     (finToNat x)

154 |     (k + finToNat y)

155 |     @{transitive (finLT k x) (lteAddRight _)}

156 |     @{ltPlusLeft $ finLT m y}

157 |     @{transitive (finLT k x) $ lteAddRight _}

158 |     l

160 | 0 compareGT : (x,y : Fin k) -> CompFin x y === GT -> CompFin y x === LT

161 | compareGT (FS x) FZ     prf = Refl

162 | compareGT (FS x) (FS y) prf = compareGT x y prf

163 | compareGT FZ     FZ prf     impossible

164 | compareGT FZ     (FS x) prf impossible

169 | public export

170 | mkEdge : Fin k -> Fin k -> e -> Maybe (Edge k e)

171 | mkEdge k j l with (compareNat (finToNat k) (finToNat j)) proof prf

172 |   _ | LT = Just (E k j l )

173 |   _ | EQ = Nothing

174 |   _ | GT = Just (E j k l @{compareGT k j prf})

181 | tryFromNat : {k : _} -> (x,y : Nat) -> (l : e) -> Maybe (Edge k e)

182 | tryFromNat x y l =

183 |   let Just fx := tryNatToFin x | Nothing => Nothing

184 |       Just fy := tryNatToFin y | Nothing => Nothing

185 |    in mkEdge fx fy l

187 | public export

188 | edge : {k : _} -> Fin k -> e -> Edge (S k) e

189 | edge x l = E (weaken x) last l @{edgeLemma k x}

191 | public export

192 | Eq e => Eq (Edge k e) where

193 |   E m1 n1 l1 == E m2 n2 l2 = m1 == m2 && n1 == n2 && l1 == l2

195 | public export

196 | Ord e => Ord (Edge k e) where

197 |   compare (E m1 n1 l1) (E m2 n2 l2) =

198 |     let EQ := compare m1 m2 | r => r

199 |         EQ := compare n1 n2 | r => r

200 |      in compare l1 l2

203 | Show e => Show (Edge k e) where

204 |   showPrec p (E x y l) =

205 |     showCon p "E" $ showArg (finToNat x) ++ showArg (finToNat y) ++ showArg l

208 | Functor (Edge k) where

209 |   map f (E x y l) = E x y (f l)

212 | Foldable (Edge k) where

213 |   foldl f x (E _ _ l) = f x l

214 |   foldr f x (E _ _ l) = f l x

215 |   toList (E _ _ l)    = [l]

216 |   foldMap f (E _ _ l) = f l

217 |   null _              = False

220 | Traversable (Edge k) where

221 |   traverse f (E x y l) = map (\v => E x y v) (f l)

234 | public export

235 | record Adj k e n where

236 |   constructor A

237 |   label       : n

238 |   neighbours  : AssocList k e

241 | weakenAdj : Adj k e n -> Adj (S k) e n

242 | weakenAdj (A l ns) = A l $ weakenAL ns

245 | weakenAdjN : (0 m : Nat) -> Adj k e n -> Adj (k + m) e n

246 | weakenAdjN m (A l ns) = A l $ weakenALN m ns

248 | export %inline

249 | fromLabel : n -> Adj k e n

250 | fromLabel v = A v empty

253 | Eq e => Eq n => Eq (Adj k e n) where

254 |   A l1 ns1 == A l2 ns2 = l1 == l2 && ns1 == ns2

257 | Show e => Show n => Show (Adj k e n) where

258 |   showPrec p (A lbl ns) = showCon p "A" $ showArg lbl ++ showArg ns

260 | export %inline

261 | Functor (Adj k e) where

262 |   map f = { label $= f }

265 | Foldable (Adj k e) where

266 |   foldl f a n  = f a n.label

267 |   foldr f a n  = f n.label a

268 |   foldMap  f n = f n.label

269 |   null _       = False

270 |   toList n     = [n.label]

271 |   foldlM f a n = f a n.label

273 | export %inline

274 | Traversable (Adj k e) where

275 |   traverse f (A n l) = (`A` l) <$> f n

277 | namespace AdjFunctor

278 |   export

279 |   [AdjEdge] Functor (\e => Adj k e n) where

280 |     map f = {neighbours $= map f}

282 | namespace AdjFoldable

283 |   export

284 |   [AdjEdge] Foldable (\e => Adj k e n) where

285 |     foldl f a  = foldl f a . neighbours

286 |     foldr f a  = foldr f a . neighbours

287 |     foldMap  f = foldMap f . neighbours

288 |     null       = null . neighbours

289 |     toList     = toList . neighbours

290 |     foldlM f a = foldlM f a . neighbours

293 | Bifunctor (Adj k) where

294 |   bimap  f g (A l es) = A (g l) (map f es)

295 |   mapFst f (A l es)   = A l (map f es)

296 |   mapSnd g (A l es)   = A (g l) es

299 | Bifoldable (Adj k) where

300 |   bifoldr f g acc (A l es) = foldr f (g l acc) es

301 |   bifoldl f g acc (A l es) = g (foldl f acc es) l

302 |   binull                 _ = False

305 | Bitraversable (Adj k) where

306 |   bitraverse f g (A l es) = [| A (g l) (traverse f es) |]

308 | public export

309 | record Context (k : Nat) (e,n : Type) where

310 |   constructor C

311 |   node       : Fin k

312 |   label      : n

313 |   neighbours : AssocList k e

315 | export %inline

316 | Eq e => Eq n => Eq (Context k e n) where

317 |   C n1 l1 ns1 == C n2 l2 ns2 =

318 |     n1 == n2 && l1 == l2 && ns1 == ns2

321 | Show e => Show n => Show (Context k e n) where

322 |   showPrec p (C n l s) =

323 |     showCon p "C" $ showArg (finToNat n) ++ showArg l ++ showArg s

326 | Functor (Context k e) where

327 |   map f = { label $= f }

330 | Foldable (Context k e) where

331 |   foldl f a n  = f a n.label

332 |   foldr f a n  = f n.label a

333 |   foldMap  f n = f n.label

334 |   null _       = False

335 |   toList n     = [n.label]

336 |   foldlM f a n = f a n.label

338 | namespace ContextFunctor

339 |   export

340 |   [CtxtEdge] Functor (\e => Context k e n) where

341 |     map f = {neighbours $= map f}

343 | namespace ContextFoldable

344 |   export

345 |   [CtxtEdge] Foldable (\e => Context k e n) where

346 |     foldl f a  = foldl f a . neighbours

347 |     foldr f a  = foldr f a . neighbours

348 |     foldMap  f = foldMap f . neighbours

349 |     null       = null . neighbours

350 |     toList     = toList . neighbours

351 |     foldlM f a = foldlM f a . neighbours

353 | export %inline

354 | Traversable (Context k e) where

355 |   traverse f (C n l es) =

356 |     (\l2 => C n l2 es) <$> f l

359 | Bifunctor (Context k) where

360 |   bimap  f g (C n l es) = C n (g l) (map f es)

361 |   mapFst f (C n l es)   = C n l (map f es)

362 |   mapSnd g (C n l es)   = C n (g l) es

365 | Bifoldable (Context k) where

366 |   bifoldr f g acc (C _ l es) = foldr f (g l acc) es

367 |   bifoldl f g acc (C _ l es) = g (foldl f acc es) l

368 |   binull _                           = False

371 | Bitraversable (Context k) where

372 |   bitraverse f g (C n l es) =

373 |     [| C (pure n) (g l) (traverse f es) |]

380 | public export

381 | record IGraph (k : Nat) (e,n : Type) where

382 |   constructor IG

383 |   graph : IArray k (Adj k e n)

386 | {k : _} -> Eq e => Eq n => Eq (IGraph k e n) where

387 |   IG g1 == IG g2 = g1 == g2

390 | {k : _} -> Functor (IGraph k e) where

391 |   map f = { graph $= map (map f) }

394 | {k : _} -> Foldable (IGraph k e) where

395 |   foldl f a  = foldl (\a',adj => f a' adj.label) a . graph

396 |   foldr f a  = foldr (f . label) a . graph

397 |   foldMap  f = foldMap (f . label) . graph

398 |   toList     = map label . toList . graph

399 |   null _     = k == 0

402 | {k : _} -> Traversable (IGraph k e) where

403 |   traverse f (IG g) = IG <$> traverse (traverse f) g

405 | namespace IGraphFunctor

406 |   export

407 |   [OnEdge] {k : _} -> Functor (\e => IGraph k e n) where

408 |     map f g = { graph $= map {neighbours $= map f} } g

410 | namespace IGraphFoldable

411 |   export

412 |   [OnEdge] {k : _} -> Foldable (\e => IGraph k e n) where

413 |     foldr f a = foldr (\v,x => foldr f x v.neighbours) a . graph

414 |     foldl f a = foldl (\x,v => foldl f x v.neighbours) a . graph

415 |     foldMap f = foldMap (\v => foldMap f v.neighbours) . graph

416 |     toList g  = toList g.graph >>= toList . neighbours

417 |     null   g  = all (null . neighbours) g.graph

420 | {k : _} -> Bifunctor (IGraph k) where

421 |   bimap  f g (IG m) = IG $ bimap f g <$> m

422 |   mapFst f (IG m)   = IG $ mapFst f <$> m

423 |   mapSnd g (IG m)   = IG $ mapSnd g <$> m

426 | {k : _} -> Bifoldable (IGraph k) where

427 |   bifoldr f g acc =

428 |     foldr (flip $ bifoldr f g) acc . graph

429 |   bifoldl f g acc =

430 |     foldl (bifoldl f g) acc . graph

431 |   binull = null

434 | {k : _} -> Bitraversable (IGraph k) where

435 |   bitraverse f g (IG h) = IG <$> traverse (bitraverse f g) h

442 | public export

443 | record Graph (e,n : Type) where

444 |   constructor G

445 |   order : Nat

446 |   graph : IGraph order e n

449 | Eq e => Eq n => Eq (Graph e n) where

450 |   G s1 g1 == G s2 g2 with (s1 == s2) proof eq

451 |     _ | True  = (rewrite eqOpReflectsEquals s1 s2 eq in g2) == g1

452 |     _ | False = False

455 | Functor (Graph e) where

456 |   map f (G o g) = G o $ map f g

459 | Foldable (Graph e) where

460 |   foldl f a  (G _ g) = foldl f a g

461 |   foldr f a  (G _ g) = foldr f a g

462 |   foldMap  f (G _ g) = foldMap f g

463 |   toList     (G _ g) = toList g

464 |   null       (G o g) = o == 0

467 | Traversable (Graph e) where

468 |   traverse f (G s g) = G s <$> traverse f g

470 | namespace GraphFunctor

471 |   export

472 |   [OnEdge] Functor (\e => Graph e n) where

473 |     map f (G o g) = G o $ map @{IGraphFunctor.OnEdge} f g

475 | namespace GraphFoldable

476 |   export

477 |   [OnEdge] Foldable (\e => Graph e n) where

478 |     foldr f a (G o g) = foldr @{IGraphFoldable.OnEdge} f a g

479 |     foldl f a (G o g) = foldl @{IGraphFoldable.OnEdge} f a g

480 |     foldMap f (G o g) = foldMap @{IGraphFoldable.OnEdge} f g

481 |     toList    (G o g) = toList @{IGraphFoldable.OnEdge} g

482 |     null      (G o g) = null @{IGraphFoldable.OnEdge} g

485 | Bifunctor (Graph) where

486 |   bimap  f g (G o m) = G o $ bimap f g m

487 |   mapFst f (G o m)   = G o $ mapFst f m

488 |   mapSnd g (G o m)   = G o $ mapSnd g m

491 | Bifoldable (Graph) where

492 |   bifoldr f g acc (G o m) = bifoldr f g acc m

493 |   bifoldl f g acc (G o m) = bifoldl f g acc m

494 |   binull                  = null

497 | Bitraversable Graph where

498 |   bitraverse f g (G s h) = G s <$> bitraverse f g h