{-# OPTIONS --without-K --safe #-}
{-# OPTIONS --hidden-argument-puns #-}

open import Level using (Level; _⊔_)
open import Relation.Binary using (Setoid; Rel; IsEquivalence)

module Data.Vector.Core {c ℓ : Level} (S : Setoid c ℓ) where

import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
import Data.Vec.Relation.Binary.Pointwise.Inductive as PW

open import Categories.Category.Instance.Nat using (Natop)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor using (Functor)
open import Data.Fin using (Fin)
open import Data.Nat using (ℕ)
open import Data.Setoid using (∣_∣)
open import Data.Vec using (Vec; lookup; tabulate)
open import Data.Vec.Properties using (tabulate∘lookup; lookup∘tabulate; tabulate-cong)
open import Data.Vec.Relation.Binary.Equality.Setoid S using (_≋_; ≋-isEquivalence)
open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_)
open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)

open Func
open Setoid S
open Vec
open Fin

private
  variable
    n A B C : ℕ

opaque

  -- Vectors over the rig
  Vector : ℕ → Set c
  Vector = Vec ∣ S ∣

  -- Pointwise equivalence of vectors
  _≊_ : Rel (Vector n) (c ⊔ ℓ)
  _≊_ A B = A ≋ B

  -- Pointwise equivalence is an equivalence relation
  ≊-isEquiv : IsEquivalence (_≊_ {n})
  ≊-isEquiv {n} = ≋-isEquivalence n

-- A setoid of vectors for every natural number
Vectorₛ : ℕ → Setoid c (c ⊔ ℓ)
Vectorₛ n = record
    { Carrier = Vector n
    ; _≈_ = _≊_
    ; isEquivalence = ≊-isEquiv
  }

module ≊ {n} = Setoid (Vectorₛ n)

infix 4 _≊_

opaque

  unfolding Vector

  pull : (Fin B → Fin A) → Vectorₛ A ⟶ₛ Vectorₛ B
  pull f .to v = tabulate (λ i → lookup v (f i))
  pull f .cong ≊v = PW.tabulate⁺ (λ i → PW.lookup ≊v (f i))

  pull-id : {v : Vector n} → pull id ⟨$⟩ v ≊ v
  pull-id {v} = ≊.reflexive (tabulate∘lookup v)

  pull-∘
      : {f : Fin B → Fin A}
        {g : Fin C → Fin B}
        {v : Vector A}
      → pull (f ∘ g) ⟨$⟩ v ≊ pull g ⟨$⟩ (pull f ⟨$⟩ v)
  pull-∘ {f} {g} {v} = ≊.reflexive (≡.sym (tabulate-cong (λ i → lookup∘tabulate (lookup v ∘ f) (g i))))

  pull-cong
      : {f g : Fin B → Fin A}
      → f ≗ g
      → {v : Vector A}
      → pull f ⟨$⟩ v ≊ pull g ⟨$⟩ v
  pull-cong f≗g {v} = ≊.reflexive (tabulate-cong (λ i → ≡.cong (lookup v) (f≗g i)))

-- Copying, deleting, and rearranging elements
-- of a vector according to a function on indices
-- gives a contravariant functor from Nat to Setoids
Pull : Functor Natop (Setoids c (c ⊔ ℓ))
Pull = record
    { F₀ = Vectorₛ
    ; F₁ = pull
    ; identity = pull-id
    ; homomorphism = pull-∘
    ; F-resp-≈ = pull-cong
    }