------------------------------------------------------------------------ -- The Agda standard library -- -- Decorated star-lists ------------------------------------------------------------------------ module Data.Star.Decoration where open import Data.Star open import Relation.Binary open import Function open import Data.Unit open import Level -- A predicate on relation "edges" (think of the relation as a graph). EdgePred : {I : Set} → Rel I zero → Set₁ EdgePred T = ∀ {i j} → T i j → Set data NonEmptyEdgePred {I : Set} (T : Rel I zero) (P : EdgePred T) : Set where nonEmptyEdgePred : ∀ {i j} {x : T i j} (p : P x) → NonEmptyEdgePred T P -- Decorating an edge with more information. data DecoratedWith {I : Set} {T : Rel I zero} (P : EdgePred T) : Rel (NonEmpty (Star T)) zero where ↦ : ∀ {i j k} {x : T i j} {xs : Star T j k} (p : P x) → DecoratedWith P (nonEmpty (x ◅ xs)) (nonEmpty xs) edge : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} → DecoratedWith {T = T} P i j → NonEmpty T edge (↦ {x = x} p) = nonEmpty x decoration : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} → (d : DecoratedWith {T = T} P i j) → P (NonEmpty.proof (edge d)) decoration (↦ p) = p -- Star-lists decorated with extra information. All P xs means that -- all edges in xs satisfy P. All : ∀ {I} {T : Rel I zero} → EdgePred T → EdgePred (Star T) All P {j = j} xs = Star (DecoratedWith P) (nonEmpty xs) (nonEmpty {y = j} ε) -- We can map over decorated vectors. gmapAll : ∀ {I} {T : Rel I zero} {P : EdgePred T} {J} {U : Rel J zero} {Q : EdgePred U} {i j} {xs : Star T i j} (f : I → J) (g : T =[ f ]⇒ U) → (∀ {i j} {x : T i j} → P x → Q (g x)) → All P xs → All {T = U} Q (gmap f g xs) gmapAll f g h ε = ε gmapAll f g h (↦ x ◅ xs) = ↦ (h x) ◅ gmapAll f g h xs -- Since we don't automatically have gmap id id xs ≡ xs it is easier -- to implement mapAll in terms of map than in terms of gmapAll. mapAll : ∀ {I} {T : Rel I zero} {P Q : EdgePred T} {i j} {xs : Star T i j} → (∀ {i j} {x : T i j} → P x → Q x) → All P xs → All Q xs mapAll {P = P} {Q} f ps = map F ps where F : DecoratedWith P ⇒ DecoratedWith Q F (↦ x) = ↦ (f x) -- We can decorate star-lists with universally true predicates. decorate : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j} → (∀ {i j} (x : T i j) → P x) → (xs : Star T i j) → All P xs decorate f ε = ε decorate f (x ◅ xs) = ↦ (f x) ◅ decorate f xs -- We can append Alls. Unfortunately _◅◅_ does not quite work. infixr 5 _◅◅◅_ _▻▻▻_ _◅◅◅_ : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j k} {xs : Star T i j} {ys : Star T j k} → All P xs → All P ys → All P (xs ◅◅ ys) ε ◅◅◅ ys = ys (↦ x ◅ xs) ◅◅◅ ys = ↦ x ◅ xs ◅◅◅ ys _▻▻▻_ : ∀ {I} {T : Rel I zero} {P : EdgePred T} {i j k} {xs : Star T j k} {ys : Star T i j} → All P xs → All P ys → All P (xs ▻▻ ys) _▻▻▻_ = flip _◅◅◅_