0 | module ControlFlow.Edge
 1 |
 2 | import Theory
 3 |
 4 | export infix 6 ~>, <~
 5 |
 6 | ||| An edge between vertices
 7 | ||| @ a the type of vertex identifiers
 8 | public export
 9 | data Edge a
10 |   = ||| `v ~> w` - an edge from `v` to `w`
11 |     (~>) a a
12 |
13 | public export
14 | (<~) : a -> a -> Edge a
15 | (<~) = flip (~>)
16 |
17 | public export
18 | Dest : Edge a -> a
19 | Dest (from ~> to) = to
20 |
21 | public export
22 | Origin : Edge a -> a
23 | Origin (from ~> to) = from
24 |
25 | export infix 8 ~~>, ~>>, <~~, <<~
26 |
27 | ||| A *collection* of `vs` by `v`
28 | public export
29 | (~~>) : (vs : List a) -> (v : a) -> List (Edge a)
30 | vs ~~> v = map (~> v) vs
31 |
32 | ||| A *distribution* of `v` to `vs`
33 | public export
34 | (~>>) : (v : a) -> (vs : List a) -> List (Edge a)
35 | v ~>> vs = map (v ~>) vs
36 |
37 | ||| Flipped `(~~>)`
38 | public export
39 | (<~~) : (v : a) -> (vs : List a) -> List (Edge a)
40 | (<~~) = flip (~~>)
41 |
42 | ||| Flipped `(~>>)`
43 | public export
44 | (<<~) : (vs : List a) -> (v : a) -> List (Edge a)
45 | (<<~) = flip (~>>)
46 |
47 | |||    A collection    of a   concatenation of two   lists by `v`
48 | ||| is a concatenation of the collections   of these lists by `v`
49 | export
50 | collect_concat : (v : a) -> (vs, ws : List a) -> (vs ++ ws) ~~> v = vs ~~> v ++ ws ~~> v
51 | collect_concat v vs ws = map_concat {f = (~> v)} vs ws
52 |
53 | |||    A distribution  of `v` to a   concatenation        of two   lists
54 | ||| is a concatenation        of the distributions of `v` to these lists
55 | export
56 | distribute_concat : (v : a) -> (vs, ws : List a) -> v ~>> (vs ++ ws) = v ~>> vs ++ v ~>> ws
57 | distribute_concat v vs ws = map_concat {f = (v ~>)} vs ws
58 |
59 | ||| A special case of `collect_concat` where `ws` is a singleton
60 | export
61 | collect_append : (v : a) -> (vs : List a) -> (w : a) -> (vs ++ [w]) ~~> v = vs ~~> v ++ [w ~> v]
62 | collect_append v vs w = collect_concat v vs [w]
63 |
64 | ||| A special case of `distribute_concat` where `ws` is a singleton
65 | export
66 | distribute_append : (v : a) -> (vs : List a) -> (w : a) -> v ~>> (vs ++ [w]) = v ~>> vs ++ [v ~> w]
67 | distribute_append v vs w = distribute_concat v vs [w]
68 |