{-# OPTIONS --rewriting #-}

module A201801.AllVec where

open import A201801.Prelude
open import A201801.Vec


--------------------------------------------------------------------------------


data All {X} (P : X → Set) : ∀ {n} → Vec X n → Set
  where
    ∙   : All P ∙
    _,_ : ∀ {n Ξ A} → All P {n} Ξ → P A → All P (Ξ , A)


maps : ∀ {X P Q n} → {Ξ : Vec X n}
                   → (∀ {A} → P A → Q A) → All P Ξ
                   → All Q Ξ
maps f ∙       = ∙
maps f (ξ , a) = maps f ξ , f a


--------------------------------------------------------------------------------


get : ∀ {X P A n I} → {Ξ : Vec X n}
                    → All P Ξ → Ξ ∋⟨ I ⟩ A
                    → P A
get (ξ , a) zero    = a
get (ξ , b) (suc i) = get ξ i


gets : ∀ {X P n n′ e} → {Ξ : Vec X n} {Ξ′ : Vec X n′}
                      → All P Ξ′ → Ξ′ ⊇⟨ e ⟩ Ξ
                      → All P Ξ
gets ξ       done     = ∙
gets (ξ , b) (drop η) = gets ξ η
gets (ξ , a) (keep η) = gets ξ η , a


--------------------------------------------------------------------------------


infix  _⊇◇⟨_⟩_
data _⊇◇⟨_⟩_ {X P} : ∀ {n n′ e} → {Ξ : Vec X n} {Ξ′ : Vec X n′}
                                → All P Ξ′ → Ξ′ ⊇⟨ e ⟩ Ξ → All P Ξ → Set
  where
    done : ∙ ⊇◇⟨ done ⟩ ∙

    drop : ∀ {A n n′ e} → {Ξ : Vec X n} {Ξ′ : Vec X n′} {η : Ξ′ ⊇⟨ e ⟩ Ξ}
                           {a : P A} {ξ : All P Ξ} {ξ′ : All P Ξ′}
                        → ξ′ ⊇◇⟨ η ⟩ ξ
                        → ξ′ , a ⊇◇⟨ drop η ⟩ ξ

    keep : ∀ {A n n′ e} → {Ξ : Vec X n} {Ξ′ : Vec X n′} {η : Ξ′ ⊇⟨ e ⟩ Ξ}
                           {a : P A} {ξ : All P Ξ} {ξ′ : All P Ξ′}
                        → ξ′ ⊇◇⟨ η ⟩ ξ
                        → ξ′ , a ⊇◇⟨ keep η ⟩ ξ , a


bot⊇◇ : ∀ {X P n} → {Ξ : Vec X n} {ξ : All P Ξ}
                 → ξ ⊇◇⟨ bot⊇ ⟩ ∙
bot⊇◇ {ξ = ∙}     = done
bot⊇◇ {ξ = ξ , a} = drop bot⊇◇


id⊇◇ : ∀ {X P n} → {Ξ : Vec X n} {ξ : All P Ξ}
                 → ξ ⊇◇⟨ id⊇ ⟩ ξ
id⊇◇ {ξ = ∙}     = done
id⊇◇ {ξ = ξ , a} = keep id⊇◇


_∘⊇◇_ : ∀ {X P n n′ n″ e₁ e₂} → {Ξ : Vec X n} {Ξ′ : Vec X n′} {Ξ″ : Vec X n″}
                                 {η₁ : Ξ′ ⊇⟨ e₁ ⟩ Ξ} {η₂ : Ξ″ ⊇⟨ e₂ ⟩ Ξ′}
                                 {ξ : All P Ξ} {ξ′ : All P Ξ′} {ξ″ : All P Ξ″}
                              → ξ′ ⊇◇⟨ η₁ ⟩ ξ → ξ″ ⊇◇⟨ η₂ ⟩ ξ′
                              → ξ″ ⊇◇⟨ η₁ ∘⊇ η₂ ⟩ ξ
𝜂₁      ∘⊇◇ done    = 𝜂₁
𝜂₁      ∘⊇◇ drop 𝜂₂ = drop (𝜂₁ ∘⊇◇ 𝜂₂)
drop 𝜂₁ ∘⊇◇ keep 𝜂₂ = drop (𝜂₁ ∘⊇◇ 𝜂₂)
keep 𝜂₁ ∘⊇◇ keep 𝜂₂ = keep (𝜂₁ ∘⊇◇ 𝜂₂)


--------------------------------------------------------------------------------


infix  _∋◇⟨_⟩_
data _∋◇⟨_⟩_ {X P} : ∀ {A n I} → {Ξ : Vec X n}
                               → All P Ξ → Ξ ∋⟨ I ⟩ A → P A → Set
  where
    zero : ∀ {n A} → {Ξ : Vec X n} {ξ : All P Ξ} {a : P A}
                   → ξ , a ∋◇⟨ zero ⟩ a

    suc : ∀ {B n I A} → {Ξ : Vec X n} {i : Ξ ∋⟨ I ⟩ A}
                         {a : P A} {b : P B} {ξ : All P Ξ}
                      → ξ ∋◇⟨ i ⟩ a
                      → ξ , b ∋◇⟨ suc i ⟩ a


ren∋◇ : ∀ {X P A n n′ e I} → {Ξ : Vec X n} {Ξ′ : Vec X n′}
                              {η : Ξ′ ⊇⟨ e ⟩ Ξ} {i : Ξ ∋⟨ I ⟩ A}
                              {a : P A} {ξ : All P Ξ} {ξ′ : All P Ξ′}
                           → ξ′ ⊇◇⟨ η ⟩ ξ → ξ ∋◇⟨ i ⟩ a
                           → ξ′ ∋◇⟨ ren∋ η i ⟩ a
ren∋◇ done     𝑖       = 𝑖
ren∋◇ (drop 𝜂) 𝑖       = suc (ren∋◇ 𝜂 𝑖)
ren∋◇ (keep 𝜂) zero    = zero
ren∋◇ (keep 𝜂) (suc 𝑖) = suc (ren∋◇ 𝜂 𝑖)


--------------------------------------------------------------------------------


-- zips : ∀ {X Y P Q n} → {Ξ : Vec X n} {Ψ : Vec Y n}
--                      → All P Ξ → All Q Ψ
--                      → All (\ { (A , B) → P A × Q B }) (zip Ξ Ψ)
-- zips ∙       ∙       = ∙
-- zips (ξ , a) (ψ , b) = zips ξ ψ , (a , b)


-- zips∋₁ : ∀ {X Y P Q n I A} → {Ξ : Vec X n} {Ψ : Vec Y n} {i : Ξ ∋⟨ I ⟩ A}
--                               {ξ : All P Ξ} {ψ : All Q Ψ} {a : P A}
--                            → ξ ∋◇⟨ i ⟩ a
--                            → zips ξ ψ ∋◇⟨ zip∋₁ i ⟩ (a , get ψ (within Ψ i))
-- zips∋₁ {ξ = ξ , a} {ψ , b} zero    = zero
-- zips∋₁ {ξ = ξ , b} {ψ , c} (suc 𝑖) = suc (zips∋₁ 𝑖)


-- zips∋₂ : ∀ {X Y P Q n I A} → {Ξ : Vec X n} {Ψ : Vec Y n} {i : Ψ ∋⟨ I ⟩ A}
--                               {ξ : All P Ξ} {ψ : All Q Ψ} {a : Q A}
--                            → ψ ∋◇⟨ i ⟩ a
--                            → zips ξ ψ ∋◇⟨ zip∋₂ i ⟩ (get ξ (within Ξ i) , a)
-- zips∋₂ {ξ = ξ , b} {ψ , a} zero    = zero
-- zips∋₂ {ξ = ξ , b} {ψ , c} (suc 𝑖) = suc (zips∋₂ 𝑖)


-- --------------------------------------------------------------------------------


-- data All◇ {X P} (𝑃 : ∀ {A : X} → P A → Set)
--               : ∀ {n} → {Ξ : Vec X n} → All P Ξ → Set
--   where
--     ∙ : All◇ 𝑃 ∙

--     _,_ : ∀ {A n} → {Ξ : Vec X n}
--                      {ξ : All P Ξ} {a : P A}
--                   → All◇ 𝑃 ξ → 𝑃 a
--                   → All◇ 𝑃 (ξ , a)


-- get◇ : ∀ {X P n I A} → {Ξ : Vec X n} {a : P A}
--                         {ξ : All P Ξ} {i : Ξ ∋⟨ I ⟩ A}
--                         {𝑃 : ∀ {A} → P A → Set}
--                      → All◇ 𝑃 ξ → ξ ∋◇⟨ i ⟩ a
--                      → 𝑃 a
-- get◇ (𝜉 , 𝑎) zero    = 𝑎
-- get◇ (𝜉 , 𝑏) (suc 𝑖) = get◇ 𝜉 𝑖


-- gets◇ : ∀ {X P n n′ e} → {Ξ : Vec X n} {Ξ′ : Vec X n′} {η : Ξ′ ⊇⟨ e ⟩ Ξ}
--                           {ξ : All P Ξ} {ξ′ : All P Ξ′}
--                           {𝑃 : ∀ {A} → P A → Set}
--                        → All◇ 𝑃 ξ′ → ξ′ ⊇◇⟨ η ⟩ ξ
--                        → All◇ 𝑃 ξ
-- gets◇ ∙       done     = ∙
-- gets◇ (𝜉 , 𝑏) (drop 𝜂) = gets◇ 𝜉 𝜂
-- gets◇ (𝜉 , 𝑎) (keep 𝜂) = gets◇ 𝜉 𝜂 , 𝑎


-- maps◇ : ∀ {X P n} → {Ξ : Vec X n} {Q : X → Set}
--                      {f : ∀ {A} → P A → Q A} {ξ : All P Ξ}
--                      {𝑃 : ∀ {A} → P A → Set} {𝑄 : ∀ {A} → Q A → Set}
--                   → (∀ {A} → {a : P A} → 𝑃 a → 𝑄 (f a)) → All◇ 𝑃 ξ
--                   → All◇ 𝑄 (maps f ξ)
-- maps◇ 𝑓 ∙       = ∙
-- maps◇ 𝑓 (𝜉 , 𝑎) = maps◇ 𝑓 𝜉 , 𝑓 𝑎


-- --------------------------------------------------------------------------------