module Ornament where

open import Prelude
open import Description

open import Function using (_∘_)
open import Data.Unit using (⊤; tt)
open import Data.Product using (Σ; _,_; proj₁)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)


--------
-- ornaments

data ROrn {I J} (e : J → I) : RDesc I → RDesc J → Set₁ where
  ∎   : ROrn e ∎ ∎
  ṿ   : ∀ {j i} (idx : e j ≡ i) → ROrn e (ṿ i) (ṿ j)
  σ   : (S : Set) → ∀ {D E} (O : ∀ s → ROrn e (D s) (E s)) → ROrn e (σ S D) (σ S E)
  Δ   : (T : Set) → ∀ {D E} (O : ∀ t → ROrn e D (E t)) → ROrn e D (σ T E)
  ∇   : {S : Set} (s : S) → ∀ {D E} (O : ROrn e (D s) E) → ROrn e (σ S D) E
  _*_ : ∀ {D E} (O : ROrn e D E) → ∀ {D' E'} (O' : ROrn e D' E') → ROrn e (D * D') (E * E')

syntax σ S (λ s → O) = σ[ s ∶ S ] O
syntax Δ T (λ t → O) = Δ[ t ∶ T ] O

erase : ∀ {I J} {e : J → I} {D E} → ROrn e D E → ∀ {X} → ⟦ E ⟧ (X ∘ e) → ⟦ D ⟧ X
erase ∎        _        = tt
erase (ṿ refl) x        = x
erase (σ S O)  (s , xs) = s , erase (O s) xs
erase (Δ T O)  (t , xs) = erase (O t) xs
erase (∇ s O)  xs       = s , erase O xs
erase (O * O') (x , x') = erase O x , erase O' x'

data Orn {I J : Set} (e : J → I) (D : Desc I) (E : Desc J) : Set₁ where
  wrap : (∀ j → ROrn e (D at (e j)) (E at j)) → Orn e D E

unwrap : ∀ {I J} {e : J → I} {D E} → Orn e D E → ∀ j → ROrn e (D at (e j)) (E at j)
unwrap (wrap O) = O

-- ornamental algebra

ornAlg : ∀ {I J} {e : J → I} {D E} (O : Orn e D E) → Ḟ E (μ D ∘ e) ⇒ μ D ∘ e
ornAlg {D = D} (wrap O) {j} = con ∘ erase (O j)

forget : ∀ {I J} {e : J → I} {D E} (O : Orn e D E) → μ E ⇒ μ D ∘ e
forget O = fold (ornAlg O)


--------
-- ornamental descriptions

data ROrnDesc {I : Set} (J : Set) (e : J → I) : RDesc I → Set₁ where
  ∎   : ROrnDesc J e ∎
  ṿ   : ∀ {i} (j : e ⁻¹ i) → ROrnDesc J e (ṿ i)
  σ   : (S : Set) → ∀ {D} (O : ∀ s → ROrnDesc J e (D s)) → ROrnDesc J e (σ S D)
  Δ   : (T : Set) → ∀ {D} (O : T → ROrnDesc J e D) → ROrnDesc J e D
  ∇   : {S : Set} (s : S) → ∀ {D} (O : ROrnDesc J e (D s)) → ROrnDesc J e (σ S D)
  _*_ : ∀ {D} (O : ROrnDesc J e D) → ∀ {D'} (O' : ROrnDesc J e D') → ROrnDesc J e (D * D')

data OrnDesc {I : Set} (J : Set) (e : J → I) (D : Desc I) : Set₁ where
  wrap : (∀ j → ROrnDesc J e (D at (e j))) → OrnDesc J e D

toRDesc : ∀ {I J} {e : J → I} {D} → ROrnDesc J e D → RDesc J
toRDesc ∎             = ∎
toRDesc (ṿ (ok j))    = ṿ j
toRDesc (σ S O)       = σ[ s ∶ S ] toRDesc (O s)
toRDesc (Δ T O)       = σ[ t ∶ T ] toRDesc (O t)
toRDesc (∇ s O)       = toRDesc O
toRDesc (O * O')      = toRDesc O * toRDesc O'

⌊_⌋ : ∀ {I J} {e : J → I} {D} → OrnDesc J e D → Desc J
⌊ wrap O ⌋ = wrap λ j → toRDesc (O j)

toROrn : ∀ {I J} {e : J → I} {D} → (O : ROrnDesc J e D) → ROrn e D (toRDesc O)
toROrn ∎          = ∎
toROrn (ṿ (ok j)) = ṿ refl
toROrn (σ S O)    = σ[ s ∶ S ] toROrn (O s)
toROrn (Δ T O)    = Δ[ t ∶ T ] toROrn (O t)
toROrn (∇ s O)    = ∇ s (toROrn O)
toROrn (O * O')   = toROrn O * toROrn O'

⌈_⌉ : ∀ {I J} {e : J → I} {D} → (O : OrnDesc J e D) → Orn e D ⌊ O ⌋
⌈ wrap O ⌉ = wrap λ i → toROrn (O i)


--------
-- singleton ornaments

erode : ∀ {I} (D : RDesc I) → ∀ {J} → ⟦ D ⟧ J → ROrnDesc (Σ I J) proj₁ D
erode ∎       _          = ∎
erode (ṿ i)   j          = ṿ (ok (i , j))
erode (σ S D) (s , js)   = ∇ s (erode (D s) js)
erode (D * E) (js , js') = erode D js * erode E js'

singOrn : ∀ {I} (D : Desc I) → OrnDesc (Σ I (μ D)) proj₁ D
singOrn D = wrap λ { (i , con d) → erode (D at i) d }