------------------------------------------------------------------------
-- The Agda standard library
--
-- Bounded vectors (inefficient implementation)
------------------------------------------------------------------------
-- Vectors of a specified maximum length.
{-# OPTIONS --with-K --safe #-}
module Data.Star.BoundedVec where
import Data.Maybe.Base as Maybe using (Maybe; map)
open import Data.Star.Nat using (ℕ; suc; length)
open import Data.Star.Decoration using (decoration)
open import Data.Star.Pointer
using (Any; this; that; Pointer; step; done; init)
open import Data.Star.List using (List)
open import Data.Unit.Base using (⊤; tt)
open import Function.Base using (const)
open import Relation.Binary.Core using (_=[_]⇒_)
open import Relation.Binary.Consequences using (map-NonEmpty)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
using (gmap; ε; _◅_)
------------------------------------------------------------------------
-- The type
-- Finite sets decorated with elements (note the use of suc).
BoundedVec : Set → ℕ → Set
BoundedVec a n = Any (λ _ → a) (λ _ → ⊤) (suc n)
[] : ∀ {a n} → BoundedVec a n
[] = this tt
infixr 5 _∷_
_∷_ : ∀ {a n} → a → BoundedVec a n → BoundedVec a (suc n)
_∷_ = that
------------------------------------------------------------------------
-- Increasing the bound
-- Note that this operation is linear in the length of the list.
↑ : ∀ {a n} → BoundedVec a n → BoundedVec a (suc n)
↑ {a} = gmap inc lift
where
inc = Maybe.map (map-NonEmpty suc)
lift : Pointer (λ _ → a) (λ _ → ⊤) =[ inc ]⇒
Pointer (λ _ → a) (λ _ → ⊤)
lift (step x) = step x
lift (done _) = done _
------------------------------------------------------------------------
-- Conversions
fromList : ∀ {a} → (xs : List a) → BoundedVec a (length xs)
fromList ε = []
fromList (x ◅ xs) = x ∷ fromList xs
toList : ∀ {a n} → BoundedVec a n → List a
toList xs = gmap (const tt) decoration (init xs)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4