------------------------------------------------------------------------
-- The Agda standard library
--
-- Bounded vectors
------------------------------------------------------------------------

-- Vectors of a specified maximum length.

module Data.BoundedVec where

open import Data.Nat
open import Data.List as List using (List)
open import Data.Vec as Vec using (Vec)
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties
open SemiringSolver hiding (_↑)

------------------------------------------------------------------------
-- The type

abstract

  data BoundedVec (a : Set) : ℕ → Set where
    bVec : ∀ {m n} (xs : Vec a n) → BoundedVec a (n + m)

  [] : ∀ {a n} → BoundedVec a n
  [] = bVec Vec.[]

  infixr  _∷_

  _∷_ : ∀ {a n} → a → BoundedVec a n → BoundedVec a (suc n)
  x ∷ bVec xs = bVec (Vec._∷_ x xs)

------------------------------------------------------------------------
-- Pattern matching

infixr  _∷v_

data View (a : Set) : ℕ → Set where
  []v  : ∀ {n} → View a n
  _∷v_ : ∀ {n} (x : a) (xs : BoundedVec a n) → View a (suc n)

abstract

  view : ∀ {a n} → BoundedVec a n → View a n
  view (bVec Vec.[])         = []v
  view (bVec (Vec._∷_ x xs)) = x ∷v bVec xs

------------------------------------------------------------------------
-- Increasing the bound

abstract

  ↑ : ∀ {a n} → BoundedVec a n → BoundedVec a (suc n)
  ↑ {a = a} (bVec {m = m} {n = n} xs) =
    subst (BoundedVec a) lemma
            (bVec {m = suc m} xs)
    where
    lemma : n + ( + m) ≡  + (n + m)
    lemma = solve  (λ m n → n :+ (con  :+ m)  :=  con  :+ (n :+ m))
                    refl m n

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

abstract

  fromList : ∀ {a} → (xs : List a) → BoundedVec a (List.length xs)
  fromList {a = a} xs =
    subst (BoundedVec a) lemma
            (bVec {m = zero} (Vec.fromList xs))
    where
    lemma : List.length xs +  ≡ List.length xs
    lemma = solve  (λ m → m :+ con   :=  m) refl _

  toList : ∀ {a n} → BoundedVec a n → List a
  toList (bVec xs) = Vec.toList xs