-- Parallel composition of ornaments.

module Ornament.ParallelComposition where

open import Prelude.InverseImage
open import Description
open import Ornament

open import Data.Unit using (; tt)
open import Data.Product using (Σ; Σ-syntax; _,_)
open import Data.List using (List; []; _∷_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)


pc-Ė : {I J K : Set} {e : J  I} {f : K  I} {is : List I} {js : List J} {ks : List K} 
       Ė e js is  Ė f ks is   is (InvImage (pull {J} {K} {I} {e} {f}))
pc-Ė             []           []           = tt
pc-Ė {e = e} {f} (eeq  eeqs) (feq  feqs) = ok (from≡ e eeq , from≡ f feq) , pc-Ė eeqs feqs

mutual

  pcROrn :  {I J K} {e : J  I} {f : K  I} {D : RDesc I} {E : RDesc J} {F : RDesc K}  ROrn e D E  ROrn f D F  ROrnDesc (e  f) pull D
  pcROrn (ṿ eeqs) (ṿ feqs) = ṿ (pc-Ė eeqs feqs)
  pcROrn (ṿ eeqs) (Δ T P)  = Δ[ t  T ] pcROrn (ṿ eeqs) (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-double∇ : {I J K S : Set} {e : J  I} {f : K  I} {D : S  RDesc I} {E : RDesc J} {F : RDesc K} {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 λ { {._} (ok (j , k))  pcROrn (O j) (P k) }


-- left difference ornament

diff-Ė-l :  {I J K} {e : J  I} {f : K  I} {is js ks} (eeqs : Ė e js is) (feqs : Ė f ks is)  Ė π₁ (und-Ṗ is (pc-Ė eeqs feqs)) js
diff-Ė-l         []           _            = []
diff-Ė-l {e = e} (eeq  eeqs) (feq  feqs) = und-from≡ e eeq  diff-Ė-l eeqs feqs

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 (ṿ eeqs) (ṿ feqs) = ṿ (diff-Ė-l eeqs feqs)
  diffROrn-l (ṿ eeqs) (Δ T P)  = Δ[ t  T ] diffROrn-l (ṿ eeqs) (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-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 λ { {._} (ok (j , k))  diffROrn-l (O j) (P k) }


-- right difference ornament

diff-Ė-r :  {I J K} {e : J  I} {f : K  I} {is js ks} (eeqs : Ė e js is) (feqs : Ė f ks is)  Ė π₂ (und-Ṗ is (pc-Ė eeqs feqs)) ks
diff-Ė-r         _            []           = []
diff-Ė-r {f = f} (eeq  eeqs) (feq  feqs) = und-from≡ f feq  diff-Ė-r eeqs feqs

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 (ṿ eeqs) (ṿ feqs) = ṿ (diff-Ė-r eeqs feqs)
  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-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 λ { {._} (ok (j , k))  diffROrn-r (O j) (P k) }