module Ornament.ParallelComposition where

open import Prelude
open import Description
open import Ornament

open import Data.Product using (Σ; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)


mutual

  pcROrn : ∀ {I J K} {e : J → I} {f : K → I} {D E F} → ROrn e D E → ROrn f D F → ROrnDesc (e ⋈ f) pull D
  pcROrn ∎        ∎        = ∎
  pcROrn ∎        (Δ T P)  = Δ[ t ∶ T ] pcROrn ∎ (P t)
  pcROrn (ṿ idx)  (ṿ idx') = ṿ (ok (from≡ idx , from≡ idx'))
  pcROrn (ṿ idx)  (Δ T P)  = Δ[ t ∶ T ] pcROrn (ṿ idx) (P t)
  pcROrn (σ S O)  (σ .S P) = σ[ s ∶ S ] pcROrn (O s) (P s)
  pcROrn (σ f O)  (Δ T P)  = Δ[ t ∶ T ] pcROrn (σ f O) (P t)
  pcROrn (σ S O)  (∇ s P)  = ∇ s (pcROrn (O s) P)
  pcROrn (Δ T O)  P        = Δ[ t ∶ T ] pcROrn (O t) P
  pcROrn (∇ s O)  (σ S P)  = ∇ s (pcROrn O (P s))
  pcROrn (∇ s O)  (Δ T P)  = Δ[ t ∶ T ] pcROrn (∇ s O) (P t)
  pcROrn (∇ s O)  (∇ s' P) = Δ (s ≡ s') (pcROrn-double∇ O P)
  pcROrn (O * O') (Δ T P)  = Δ[ t ∶ T ] pcROrn (O * O') (P t)
  pcROrn (O * O') (P * P') = pcROrn O P * pcROrn O' P'

  pcROrn-double∇ : ∀ {I J K S} {e : J → I} {f : K → I} {D E F} {s s' : S} →
                   ROrn e (D s) E → ROrn f (D s') F → s ≡ s' → ROrnDesc (e ⋈ f) pull (σ S D)
  pcROrn-double∇ {s = s} O P refl = ∇ s (pcROrn O P)

_⊗_ : ∀ {I J K} {e : J → I} {f : K → I} {D E F} → Orn e D E → Orn f D F → OrnDesc (e ⋈ f) pull D
_⊗_ {e = e} {f} {D} {E} {F} (wrap O) (wrap P) =
  wrap λ { (j , k) → pcROrn (subst (λ i → ROrn e (D at i) (E at (und j))) (to≡ j) (O (und j)))
                            (subst (λ i → ROrn f (D at i) (F at (und k))) (to≡ k) (P (und k))) }

-- left difference ornament

mutual

  diffROrn-l : ∀ {I J K} {e : J → I} {f : K → I} {D E F}
               (O : ROrn e D E) (P : ROrn f D F) → ROrn π₁ E (toRDesc (pcROrn O P))
  diffROrn-l ∎        ∎        = ∎
  diffROrn-l ∎        (Δ T P)  = Δ T λ t → diffROrn-l ∎ (P t)
  diffROrn-l (ṿ refl) (ṿ idx') = ṿ refl
  diffROrn-l (ṿ refl) (Δ T P)  = Δ T λ t → diffROrn-l (ṿ refl) (P t)
  diffROrn-l (σ S O)  (σ .S P) = σ S λ s → diffROrn-l (O s) (P s)
  diffROrn-l (σ S O)  (Δ T P)  = Δ T λ t → diffROrn-l (σ S O) (P t)
  diffROrn-l (σ S O)  (∇ s P)  = ∇ s (diffROrn-l (O s) P)
  diffROrn-l (Δ T O)  P        = σ T λ t → diffROrn-l (O t) P
  diffROrn-l (∇ s O)  (σ S P)  = diffROrn-l O (P s)
  diffROrn-l (∇ s O)  (Δ T P)  = Δ T λ t → diffROrn-l (∇ s O) (P t)
  diffROrn-l (∇ s O)  (∇ s' P) = Δ (s ≡ s') (diffROrn-l-double∇ O P)
  diffROrn-l (O * O') (Δ T P)  = Δ T λ t → diffROrn-l (O * O') (P t)
  diffROrn-l (O * O') (P * P') = diffROrn-l O P * diffROrn-l O' P'

  diffROrn-l-double∇ : ∀ {I J K} {e : J → I} {f : K → I} {S} {D E F} {s s' : S} →
                       (O : ROrn e (D s) E) (P : ROrn f (D s') F) (eq : s ≡ s') →
                       ROrn π₁ E (toRDesc (pcROrn-double∇ {D = D} O P eq))
  diffROrn-l-double∇ O P refl = diffROrn-l O P

diffOrn-l : ∀ {I J K} {e : J → I} {f : K → I} {D E F}
            (O : Orn e D E) (P : Orn f D F) → Orn π₁ E ⌊ O ⊗ P ⌋
diffOrn-l {e = e} {f} {D} {E} {F} (wrap O) (wrap P) =
  wrap λ { (j , k) → diffROrn-l (subst (λ i → ROrn e (D at i) (E at (und j))) (to≡ j) (O (und j)))
                                (subst (λ i → ROrn f (D at i) (F at (und k))) (to≡ k) (P (und k))) }

-- right difference ornament

mutual

  diffROrn-r : ∀ {I J K} {e : J → I} {f : K → I} {D E F} →
               (O : ROrn e D E) (P : ROrn f D F) → ROrn π₂ F (toRDesc (pcROrn O P))
  diffROrn-r ∎        ∎        = ∎
  diffROrn-r ∎        (Δ T P)  = σ T λ t → diffROrn-r ∎ (P t)
  diffROrn-r (ṿ idx)  (ṿ refl) = ṿ refl
  diffROrn-r (ṿ idx)  (Δ T P)  = σ T λ t → diffROrn-r (ṿ idx) (P t)
  diffROrn-r (σ S O)  (σ .S P) = σ S λ s → diffROrn-r (O s) (P s)
  diffROrn-r (σ S O)  (Δ T P)  = σ T λ t → diffROrn-r (σ S O) (P t)
  diffROrn-r (σ S O)  (∇ s P)  = diffROrn-r (O s) P
  diffROrn-r (Δ T O)  P        = Δ T λ t → diffROrn-r (O t) P
  diffROrn-r (∇ s O)  (σ S P)  = ∇ s (diffROrn-r O (P s))
  diffROrn-r (∇ s O)  (Δ T P)  = σ T λ t → diffROrn-r (∇ s O) (P t)
  diffROrn-r (∇ s O) (∇ s' P)  = Δ (s ≡ s') (diffROrn-r-double∇ O P)
  diffROrn-r (O * O') (Δ T P)  = σ T λ t → diffROrn-r (O * O') (P t)
  diffROrn-r (O * O') (P * P') = diffROrn-r O P * diffROrn-r O' P'

  diffROrn-r-double∇ : ∀ {I J K} {e : J → I} {f : K → I} {S} {D E F} {s s' : S} →
                       (O : ROrn e (D s) E) (P : ROrn f (D s') F) (eq : s ≡ s') →
                       ROrn π₂ F (toRDesc (pcROrn-double∇ {D = D} O P eq))
  diffROrn-r-double∇ O P refl = diffROrn-r O P

diffOrn-r : ∀ {I J K} {e : J → I} {f : K → I} {D E F}
            (O : Orn e D E) (P : Orn f D F) → Orn π₂ F ⌊ O ⊗ P ⌋
diffOrn-r {e = e} {f} {D} {E} {F} (wrap O) (wrap P) =
  wrap λ { (j , k) → diffROrn-r (subst (λ i → ROrn e (D at i) (E at (und j))) (to≡ j) (O (und j)))
                                (subst (λ i → ROrn f (D at i) (F at (und k))) (to≡ k) (P (und k))) }