------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors defined in terms of the reflexive-transitive closure, Star
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Star.Vec where

open import Data.Star.Nat using (ℕ; zero; suc; 1#; _+_; length)
open import Data.Star.Fin using (Fin)
open import Data.Star.Decoration using (All; ↦; _◅◅◅_; decoration)
open import Data.Star.Pointer as Pointer using (result)
open import Data.Star.List using (List)
open import Level using (Level)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (ε; _◅_; gmap)
open import Function.Base using (const; case_of_)
open import Data.Unit.Base using (tt)

private
  variable
    a : Level
    A : Set a

-- The vector type. Vectors are natural numbers decorated with extra
-- information (i.e. elements).

Vec : Set a → ℕ → Set a
Vec A = All (λ _ → A)

-- Nil and cons.

[] : Vec A zero
[] = ε

infixr  _∷_

_∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
x ∷ xs = ↦ x ◅ xs

-- Projections.

head : ∀ {n} → Vec A (1# + n) → A
head (↦ x ◅ _) = x

tail : ∀ {n} → Vec A (1# + n) → Vec A n
tail (↦ _ ◅ xs) = xs

-- Append.

infixr  _++_

_++_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m + n)
_++_ = _◅◅◅_

-- Safe lookup.

lookup : ∀ {n} → Vec A n → Fin n → A
lookup xs i with result _ x ← Pointer.lookup xs i = x

------------------------------------------------------------------------
-- Conversions

fromList : (xs : List A) → Vec A (length xs)
fromList ε        = []
fromList (x ◅ xs) = x ∷ fromList xs

toList : ∀ {n} → Vec A n → List A
toList = gmap (const tt) decoration