------------------------------------------------------------------------
-- The Agda standard library
--
-- N-ary products
------------------------------------------------------------------------

-- Vectors (as in Data.Vec) also represent n-ary products, so what is
-- the point of this module? The n-ary products below are intended to
-- be used with a fixed n, in which case the nil constructor can be
-- avoided: pairs are represented as pairs (x , y), not as triples
-- (x , y , unit).

module Data.Product.N-ary where

open import Data.Nat
open import Data.Product
open import Data.Unit
open import Data.Vec
open import Function.Inverse
open import Level using (Lift; lift)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

-- N-ary product.

infix 8 _^_

_^_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ
A ^ 0           = Lift ⊤
A ^ 1           = A
A ^ suc (suc n) = A × A ^ suc n

-- Conversions.

↔Vec : ∀ {a} {A : Set a} n → A ^ n ↔ Vec A n
↔Vec n = record
  { to         = P.→-to-⟶ (toVec n)
  ; from       = P.→-to-⟶ fromVec
  ; inverse-of = record
    { left-inverse-of  = fromVec∘toVec n
    ; right-inverse-of = toVec∘fromVec
    }
  }
  where
  toVec : ∀ {a} {A : Set a} n → A ^ n → Vec A n
  toVec 0             (lift tt) = []
  toVec 1             x         = [ x ]
  toVec (suc (suc n)) (x , xs)  = x ∷ toVec _ xs

  fromVec : ∀ {a} {A : Set a} {n} → Vec A n → A ^ n
  fromVec []           = lift tt
  fromVec (x ∷ [])     = x
  fromVec (x ∷ y ∷ xs) = (x , fromVec (y ∷ xs))

  fromVec∘toVec : ∀ {a} {A : Set a} n (xs : A ^ n) →
                  fromVec (toVec n xs) ≡ xs
  fromVec∘toVec 0                   (lift tt)    = P.refl
  fromVec∘toVec 1                   x            = P.refl
  fromVec∘toVec 2                   (x , y)      = P.refl
  fromVec∘toVec (suc (suc (suc n))) (x , y , xs) =
    P.cong (_,_ x) (fromVec∘toVec (suc (suc n)) (y , xs))

  toVec∘fromVec : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
                  toVec n (fromVec xs) ≡ xs
  toVec∘fromVec []           = P.refl
  toVec∘fromVec (x ∷ [])     = P.refl
  toVec∘fromVec (x ∷ y ∷ xs) = P.cong (_∷_ x) (toVec∘fromVec (y ∷ xs))