module Data.Star.Vec where
open import Data.Star
open import Data.Star.Nat
open import Data.Star.Fin using (Fin)
open import Data.Star.Decoration
import Data.Star.Pointer as Pointer
open Pointer hiding (lookup)
open import Data.Star.List using (List)
open import Relation.Binary
open import Relation.Binary.Consequences
open import Data.Function
open import Data.Unit
Vec : Set → ℕ → Set
Vec a = All (λ _ → a)
[] : ∀ {a} → Vec a zero
[] = ε
infixr 5 _∷_
_∷_ : ∀ {a n} → a → Vec a n → Vec a (suc n)
x ∷ xs = ↦ x ◅ xs
head : ∀ {a n} → Vec a (1# + n) → a
head (↦ x ◅ _) = x
tail : ∀ {a n} → Vec a (1# + n) → Vec a n
tail (↦ _ ◅ xs) = xs
infixr 5 _++_
_++_ : ∀ {a m n} → Vec a m → Vec a n → Vec a (m + n)
_++_ = _◅◅◅_
lookup : ∀ {a n} → Fin n → Vec a n → a
lookup i xs with Pointer.lookup i xs
... | result _ x = x
fromList : ∀ {a} → (xs : List a) → Vec a (length xs)
fromList ε = []
fromList (x ◅ xs) = x ∷ fromList xs
toList : ∀ {a n} → Vec a n → List a
toList = gmap (const tt) decoration