------------------------------------------------------------------------
-- The Agda standard library
--
-- Code for converting Vec A n → B to and from n-ary functions
------------------------------------------------------------------------

module Data.Vec.N-ary where

open import Data.Nat.Base hiding (_⊔_)
open import Data.Product as Prod
open import Data.Vec
open import Function
open import Function.Equivalence using (_⇔_; equivalence)
open import Level using (Level; _⊔_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable

------------------------------------------------------------------------
-- N-ary functions

N-ary-level : Level  Level    Level
N-ary-level ℓ₁ ℓ₂ zero    = ℓ₂
N-ary-level ℓ₁ ℓ₂ (suc n) = ℓ₁  N-ary-level ℓ₁ ℓ₂ n

N-ary :  {ℓ₁ ℓ₂} (n : )  Set ℓ₁  Set ℓ₂  Set (N-ary-level ℓ₁ ℓ₂ n)
N-ary zero    A B = B
N-ary (suc n) A B = A  N-ary n A B

------------------------------------------------------------------------
-- Conversion

curryⁿ :  {n a b} {A : Set a} {B : Set b}
(Vec A n  B)  N-ary n A B
curryⁿ {zero}  f = f []
curryⁿ {suc n} f = λ x  curryⁿ (f  _∷_ x)

_\$ⁿ_ :  {n a b} {A : Set a} {B : Set b}  N-ary n A B  (Vec A n  B)
f \$ⁿ []       = f
f \$ⁿ (x  xs) = f x \$ⁿ xs

------------------------------------------------------------------------
-- Quantifiers

-- Universal quantifier.

∀ⁿ :  n {a } {A : Set a}
N-ary n A (Set )  Set (N-ary-level a  n)
∀ⁿ zero    P = P
∀ⁿ (suc n) P =  x  ∀ⁿ n (P x)
{- Normalising is very slow for this function for some reason... -}
{-# NO_SMASHING ∀ⁿ #-}

-- Universal quantifier with implicit (hidden) arguments.

∀ⁿʰ :  n {a } {A : Set a}
N-ary n A (Set )  Set (N-ary-level a  n)
∀ⁿʰ zero    P = P
∀ⁿʰ (suc n) P =  {x}  ∀ⁿʰ n (P x)

-- Existential quantifier.

∃ⁿ :  n {a } {A : Set a}
N-ary n A (Set )  Set (N-ary-level a  n)
∃ⁿ zero    P = P
∃ⁿ (suc n) P =  λ x  ∃ⁿ n (P x)

------------------------------------------------------------------------
-- N-ary function equality

Eq :  {a b c } {A : Set a} {B : Set b} {C : Set c} n
REL B C   REL (N-ary n A B) (N-ary n A C) (N-ary-level a  n)
Eq n _∼_ f g = ∀ⁿ n (curryⁿ {n = n} λ xs  (f \$ⁿ xs)  (g \$ⁿ xs))

-- A variant where all the arguments are implicit (hidden).

Eqʰ :  {a b c } {A : Set a} {B : Set b} {C : Set c} n
REL B C   REL (N-ary n A B) (N-ary n A C) (N-ary-level a  n)
Eqʰ n _∼_ f g = ∀ⁿʰ n (curryⁿ {n = n} λ xs  (f \$ⁿ xs)  (g \$ⁿ xs))

------------------------------------------------------------------------
-- Some lemmas

-- The functions curryⁿ and _\$ⁿ_ are inverses.

left-inverse :  {n a b} {A : Set a} {B : Set b} (f : Vec A n  B)
xs  (curryⁿ f \$ⁿ xs)  f xs
left-inverse f []       = refl
left-inverse f (x  xs) = left-inverse (f  _∷_ x) xs

right-inverse :  {a b} {A : Set a} {B : Set b} n (f : N-ary n A B)
Eq n _≡_ (curryⁿ (_\$ⁿ_ {n} f)) f
right-inverse zero    f = refl
right-inverse (suc n) f = λ x  right-inverse n (f x)

-- ∀ⁿ can be expressed in an "uncurried" way.

uncurry-∀ⁿ :  n {a } {A : Set a} {P : N-ary n A (Set )}
∀ⁿ n P  (∀ (xs : Vec A n)  P \$ⁿ xs)
uncurry-∀ⁿ n {a} {} {A} = equivalence ( n) ( n)
where
:  n {P : N-ary n A (Set )}
∀ⁿ n P  (∀ (xs : Vec A n)  P \$ⁿ xs)
zero    p []       = p
(suc n) p (x  xs) =  n (p x) xs

:  n {P : N-ary n A (Set )}
(∀ (xs : Vec A n)  P \$ⁿ xs)  ∀ⁿ n P
zero    p = p []
(suc n) p = λ x   n (p  _∷_ x)

-- ∃ⁿ can be expressed in an "uncurried" way.

uncurry-∃ⁿ :  n {a } {A : Set a} {P : N-ary n A (Set )}
∃ⁿ n P  ( λ (xs : Vec A n)  P \$ⁿ xs)
uncurry-∃ⁿ n {a} {} {A} = equivalence ( n) ( n)
where
:  n {P : N-ary n A (Set )}
∃ⁿ n P  ( λ (xs : Vec A n)  P \$ⁿ xs)
zero    p       = ([] , p)
(suc n) (x , p) = Prod.map (_∷_ x) id ( n p)

:  n {P : N-ary n A (Set )}
( λ (xs : Vec A n)  P \$ⁿ xs)  ∃ⁿ n P
zero    ([] , p)     = p
(suc n) (x  xs , p) = (x ,  n (xs , p))

-- Conversion preserves equality.

curryⁿ-cong :  {n a b c } {A : Set a} {B : Set b} {C : Set c}
(_∼_ : REL B C ) (f : Vec A n  B) (g : Vec A n  C)
(∀ xs  f xs  g xs)
Eq n _∼_ (curryⁿ f) (curryⁿ g)
curryⁿ-cong {zero}  _∼_ f g hyp = hyp []
curryⁿ-cong {suc n} _∼_ f g hyp = λ x
curryⁿ-cong _∼_ (f  _∷_ x) (g  _∷_ x)  xs  hyp (x  xs))

curryⁿ-cong⁻¹ :  {n a b c } {A : Set a} {B : Set b} {C : Set c}
(_∼_ : REL B C ) (f : Vec A n  B) (g : Vec A n  C)
Eq n _∼_ (curryⁿ f) (curryⁿ g)
xs  f xs  g xs
curryⁿ-cong⁻¹ _∼_ f g hyp []       = hyp
curryⁿ-cong⁻¹ _∼_ f g hyp (x  xs) =
curryⁿ-cong⁻¹ _∼_ (f  _∷_ x) (g  _∷_ x) (hyp x) xs

appⁿ-cong :  {n a b c } {A : Set a} {B : Set b} {C : Set c}
(_∼_ : REL B C ) (f : N-ary n A B) (g : N-ary n A C)
Eq n _∼_ f g
(xs : Vec A n)  (f \$ⁿ xs)  (g \$ⁿ xs)
appⁿ-cong _∼_ f g hyp []       = hyp
appⁿ-cong _∼_ f g hyp (x  xs) = appⁿ-cong _∼_ (f x) (g x) (hyp x) xs

appⁿ-cong⁻¹ :  {n a b c } {A : Set a} {B : Set b} {C : Set c}
(_∼_ : REL B C ) (f : N-ary n A B) (g : N-ary n A C)
((xs : Vec A n)  (f \$ⁿ xs)  (g \$ⁿ xs))
Eq n _∼_ f g
appⁿ-cong⁻¹ {zero}  _∼_ f g hyp = hyp []
appⁿ-cong⁻¹ {suc n} _∼_ f g hyp = λ x
appⁿ-cong⁻¹ _∼_ (f x) (g x)  xs  hyp (x  xs))

-- Eq and Eqʰ are equivalent.

Eq-to-Eqʰ :  {a b c } {A : Set a} {B : Set b} {C : Set c}
n (_∼_ : REL B C ) {f : N-ary n A B} {g : N-ary n A C}
Eq n _∼_ f g  Eqʰ n _∼_ f g
Eq-to-Eqʰ zero    _∼_ eq = eq
Eq-to-Eqʰ (suc n) _∼_ eq = Eq-to-Eqʰ n _∼_ (eq _)

Eqʰ-to-Eq :  {a b c } {A : Set a} {B : Set b} {C : Set c}
n (_∼_ : REL B C ) {f : N-ary n A B} {g : N-ary n A C}
Eqʰ n _∼_ f g  Eq n _∼_ f g
Eqʰ-to-Eq zero    _∼_ eq = eq
Eqʰ-to-Eq (suc n) _∼_ eq = λ _  Eqʰ-to-Eq n _∼_ eq