0 | module Data.Path
 1 |
 2 | %default total
 3 |
 4 | ||| Paths in a typed graph as a sequence of edges with source and target nodes matching up domino-style.
 5 | ||| AKA reflexive-transitive closure.
 6 | public export
 7 | data Path : (t -> t -> Type) -> t -> t -> Type where
 8 |   Nil  : Path g i i
 9 |   (::) : {0 i, j, k : t} ->
10 |          g i j -> Path g j k -> Path g i k
11 |
12 | export
13 | joinPath : Path g i j -> Path g j k -> Path g i k
14 | joinPath []      jk = jk
15 | joinPath (e::ij) jk = e :: joinPath ij jk
16 |
17 | export
18 | snocPath : Path g i j -> g j k -> Path g i k
19 | snocPath []      f = [f]
20 | snocPath (e::ij) f = e :: snocPath ij f
21 |
22 | export
23 | lengthPath : Path g i j -> Nat
24 | lengthPath []     = Z
25 | lengthPath (_::p) = S $ lengthPath p
26 |
27 | export
28 | mapPath : {0 gt : t -> t -> Type} -> {0 gu : u -> u -> Type} -> {0 f : t -> u}
29 |        -> ({0 i, j : t} ->      gt i j ->      gu (f i) (f j))
30 |        ->  {0 i, j : t} -> Path gt i j -> Path gu (f i) (f j)
31 | mapPath gf []     = []
32 | mapPath gf (e::p) = gf e :: mapPath gf p
33 |
34 | export
35 | foldPath : {0 gt : t -> t -> Type} -> {0 gu : u -> u -> Type} -> {0 f : t -> u}
36 |         -> ({0 i, j, k : t} ->      gt i j -> gu (f j) (f k) -> gu (f i) (f k))
37 |         ->  {0 i, j, k : t} -> Path gt i j -> gu (f j) (f k) -> gu (f i) (f k)
38 | foldPath gf []      jk = jk
39 | foldPath gf (e::ij) jk = gf e (foldPath {gu} gf ij jk)
40 |
41 | export
42 | foldlPath : {0 gt : t -> t -> Type} -> {0 gu : u -> u -> Type} -> {0 f : t -> u}
43 |         -> ({0 i, j, k : t} -> gu (f i) (f j) ->      gt j k -> gu (f i) (f k))
44 |         ->  {0 i, j, k : t} -> gu (f i) (f j) -> Path gt j k -> gu (f i) (f k)
45 | foldlPath gf ij []      = ij
46 | foldlPath gf ij (e::jk) = foldlPath {gu} gf (gf ij e) jk
47 |