------------------------------------------------------------------------
-- 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 _◅◅◅_