------------------------------------------------------------------------
-- The Agda standard library
--
-- Container combinators
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Container.Combinator where

open import Level using (Level; _⊔_; lower)
open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
open import Data.Product.Base as Product using (_,_; <_,_>; proj₁; proj₂; ∃)
open import Data.Sum.Base as Sum using ([_,_]′)
open import Data.Unit.Polymorphic.Base using (⊤)
import Function.Base as F

open import Data.Container.Core
open import Data.Container.Relation.Unary.Any

------------------------------------------------------------------------
-- Combinators

module _ {s p : Level} where

-- Identity.

  id : Container s p
  id .Shape    = ⊤
  id .Position = F.const ⊤

  to-id : ∀ {a} {A : Set a} → F.id A → ⟦ id ⟧ A
  to-id x = (_ , λ _ → x)

  from-id : ∀ {a} {A : Set a} → ⟦ id ⟧ A → F.id A
  from-id xs = proj₂ xs _

-- Constant.

  const : Set s → Container s p
  const A .Shape    = A
  const A .Position = F.const ⊥

  to-const : ∀ {b} (A : Set s) {B : Set b} → A → ⟦ const A ⟧ B
  to-const _ = _, ⊥-elim {Whatever = F.const _}

  from-const : ∀ {b} (A : Set s) {B : Set b} → ⟦ const A ⟧ B → A
  from-const _ = proj₁

module _ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where

-- Composition.

  infixr  _∘_

  _∘_ : Container (s₁ ⊔ s₂ ⊔ p₁) (p₁ ⊔ p₂)
  _∘_ .Shape    = ⟦ C₁ ⟧ (Shape C₂)
  _∘_ .Position = ◇ C₁ (Position C₂)

  to-∘ : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A) → ⟦ _∘_ ⟧ A
  to-∘ (s , f) = ((s , proj₁ F.∘ f) , Product.uncurry (proj₂ F.∘ f) F.∘′ ◇.proof)

  from-∘ : ∀ {a} {A : Set a} → ⟦ _∘_ ⟧ A → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A)
  from-∘ ((s , f) , g) = (s , < f , Product.curry (g F.∘′ any) >)

-- Product. (Note that, up to isomorphism, this is a special case of
-- indexed product.)

  infixr  _×_

  _×_ : Container (s₁ ⊔ s₂) (p₁ ⊔ p₂)
  _×_ .Shape    = Shape C₁ Product.× Shape C₂
  _×_ .Position = Product.uncurry λ s₁ s₂ → (Position C₁ s₁) Sum.⊎ (Position C₂ s₂)

  to-× : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A Product.× ⟦ C₂ ⟧ A → ⟦ _×_ ⟧ A
  to-× ((s₁ , f₁) , (s₂ , f₂)) = ((s₁ , s₂) , [ f₁ , f₂ ]′)

  from-× : ∀ {a} {A : Set a} → ⟦ _×_ ⟧ A → ⟦ C₁ ⟧ A Product.× ⟦ C₂ ⟧ A
  from-× ((s₁ , s₂) , f) = ((s₁ , f F.∘ Sum.inj₁) , (s₂ , f F.∘ Sum.inj₂))

-- Indexed product.

module _ {i s p} (I : Set i) (Cᵢ : I → Container s p) where

  Π : Container (i ⊔ s) (i ⊔ p)
  Π .Shape    = ∀ i → Shape (Cᵢ i)
  Π .Position = λ s → ∃ λ i → Position (Cᵢ i) (s i)

  to-Π : ∀ {a} {A : Set a} → (∀ i → ⟦ Cᵢ i ⟧ A) → ⟦ Π ⟧ A
  to-Π f = (proj₁ F.∘ f , Product.uncurry (proj₂ F.∘ f))

  from-Π : ∀ {a} {A : Set a} → ⟦ Π ⟧ A → ∀ i → ⟦ Cᵢ i ⟧ A
  from-Π (s , f) = λ i → (s i , λ p → f (i , p))

-- Constant exponentiation. (Note that this is a special case of
-- indexed product.)

infix  const[_]⟶_

const[_]⟶_ : ∀ {i s p} → Set i → Container s p → Container (i ⊔ s) (i ⊔ p)
const[ A ]⟶ C = Π A (F.const C)

-- Sum. (Note that, up to isomorphism, this is a special case of
-- indexed sum.)

module _ {s₁ s₂ p} (C₁ : Container s₁ p) (C₂ : Container s₂ p) where

  infixr  _⊎_

  _⊎_ : Container (s₁ ⊔ s₂) p
  _⊎_ .Shape    = (Shape C₁ Sum.⊎ Shape C₂)
  _⊎_ .Position = [ Position C₁ , Position C₂ ]′

  to-⊎ : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A Sum.⊎ ⟦ C₂ ⟧ A → ⟦ _⊎_ ⟧ A
  to-⊎ = [ Product.map Sum.inj₁ F.id , Product.map Sum.inj₂ F.id ]′

  from-⊎ : ∀ {a} {A : Set a} → ⟦ _⊎_ ⟧ A → ⟦ C₁ ⟧ A Sum.⊎ ⟦ C₂ ⟧ A
  from-⊎ (Sum.inj₁ s₁ , f) = Sum.inj₁ (s₁ , f)
  from-⊎ (Sum.inj₂ s₂ , f) = Sum.inj₂ (s₂ , f)

-- Indexed sum.

module _ {i s p} (I : Set i) (C : I → Container s p) where

  Σ : Container (i ⊔ s) p
  Σ .Shape    = ∃ λ i → Shape (C i)
  Σ .Position = λ s → Position (C (proj₁ s)) (proj₂ s)

  to-Σ : ∀ {a} {A : Set a} → (∃ λ i → ⟦ C i ⟧ A) → ⟦ Σ ⟧ A
  to-Σ (i , (s , f)) = ((i , s) , f)

  from-Σ : ∀ {a} {A : Set a} → ⟦ Σ ⟧ A → ∃ λ i → ⟦ C i ⟧ A
  from-Σ ((i , s) , f) = (i , (s , f))