1
------------------------------------------------------------------------
2
-- Decorated star-lists
3
------------------------------------------------------------------------
5
module Data.Star.Decoration where
8
open import Relation.Binary
9
open import Data.Function
13
-- A predicate on relation "edges" (think of the relation as a graph).
15
EdgePred : ∀ {I} → Rel I zero → Set₁
16
EdgePred T = ∀ {i j} → T i j → Set
18
data NonEmptyEdgePred {I : Set}
19
(T : Rel I zero) (P : EdgePred T) : Set where
20
nonEmptyEdgePred : ∀ {i j} {x : T i j}
21
(p : P x) → NonEmptyEdgePred T P
23
-- Decorating an edge with more information.
25
data DecoratedWith {I : Set} {T : Rel I zero} (P : EdgePred T)
26
: Rel (NonEmpty (Star T)) zero where
27
↦ : ∀ {i j k} {x : T i j} {xs : Star T j k}
28
(p : P x) → DecoratedWith P (nonEmpty (x ◅ xs)) (nonEmpty xs)
30
edge : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} →
31
DecoratedWith {T = T} P i j → NonEmpty T
32
edge (↦ {x = x} p) = nonEmpty x
34
decoration : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} →
35
(d : DecoratedWith {T = T} P i j) →
36
P (NonEmpty.proof (edge d))
39
-- Star-lists decorated with extra information. All P xs means that
40
-- all edges in xs satisfy P.
42
All : ∀ {I} {T : Rel I zero} → EdgePred T → EdgePred (Star T)
44
Star (DecoratedWith P) (nonEmpty xs) (nonEmpty {y = j} ε)
46
-- We can map over decorated vectors.
48
gmapAll : ∀ {I} {T : Rel I zero} {P : EdgePred T}
49
{J} {U : Rel J zero} {Q : EdgePred U}
50
{i j} {xs : Star T i j}
51
(f : I → J) (g : T =[ f ]⇒ U) →
52
(∀ {i j} {x : T i j} → P x → Q (g x)) →
53
All P xs → All {T = U} Q (gmap f g xs)
55
gmapAll f g h (↦ x ◅ xs) = ↦ (h x) ◅ gmapAll f g h xs
57
-- Since we don't automatically have gmap id id xs ≡ xs it is easier
58
-- to implement mapAll in terms of map than in terms of gmapAll.
60
mapAll : ∀ {I} {T : Rel I zero} {P Q : EdgePred T} {i j} {xs : Star T i j} →
61
(∀ {i j} {x : T i j} → P x → Q x) →
63
mapAll {P = P} {Q} f ps = map F ps
65
F : DecoratedWith P ⇒ DecoratedWith Q
68
-- We can decorate star-lists with universally true predicates.
70
decorate : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} →
71
(∀ {i j} (x : T i j) → P x) →
72
(xs : Star T i j) → All P xs
74
decorate f (x ◅ xs) = ↦ (f x) ◅ decorate f xs
76
-- We can append Alls. Unfortunately _◅◅_ does not quite work.
80
_◅◅◅_ : ∀ {I} {T : Rel I zero} {P : EdgePred T}
81
{i j k} {xs : Star T i j} {ys : Star T j k} →
82
All P xs → All P ys → All P (xs ◅◅ ys)
84
(↦ x ◅ xs) ◅◅◅ ys = ↦ x ◅ xs ◅◅◅ ys
86
_▻▻▻_ : ∀ {I} {T : Rel I zero} {P : EdgePred T}
87
{i j k} {xs : Star T j k} {ys : Star T i j} →
88
All P xs → All P ys → All P (xs ▻▻ ys)
added
removed
src/Data/Star/Decoration.agda
