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

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Vec.Bounded where

open import Level using (Level)
open import Data.Nat.Base using (_≤_)
open import Data.Vec.Base using (Vec)
import Data.Vec as Vec using (filter; takeWhile; dropWhile)
open import Function.Base using (id)
open import Relation.Binary.Core using (_Preserves_⟶_)
open import Relation.Unary using (Pred; Decidable)

private
  variable
    a p : Level
    A : Set a

------------------------------------------------------------------------
-- Publicly re-export the contents of the base module

open import Data.Vec.Bounded.Base public

------------------------------------------------------------------------
-- Additional operations

lift :  {f}  f Preserves _≤_  _≤_ 
       (∀ {n}  Vec A n   Vec≤ A (f n)) 
        {n}   Vec≤ A n  Vec≤ A (f n)
lift incr f (as , p) = ≤-cast (incr p) (f as)

lift′ : (∀ {n}  Vec A n   Vec≤ A n) 
        (∀ {n}  Vec≤ A n  Vec≤ A n)
lift′ = lift id

------------------------------------------------------------------------
-- Additional operations

module _ {P : Pred A p} (P? : Decidable P) where

  filter :  {n}  Vec≤ A n  Vec≤ A n
  filter = lift′ (Vec.filter P?)

  takeWhile :  {n}  Vec≤ A n  Vec≤ A n
  takeWhile = lift′ (Vec.takeWhile P?)

  dropWhile :  {n}  Vec≤ A n  Vec≤ A n
  dropWhile = lift′ (Vec.dropWhile P?)