------------------------------------------------------------------------
-- The Agda standard library
--
-- The Colist type and some operations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module Codata.Sized.Colist where
open import Codata.Sized.Conat as Conat using (Conat ; zero ; suc)
open import Codata.Sized.Cowriter as CW using (Cowriter; _∷_)
open import Codata.Sized.Delay as Delay using (Delay ; now ; later)
open import Codata.Sized.Stream using (Stream ; _∷_)
open import Codata.Sized.Thunk using (Thunk; force)
open import Data.List.Base using (List; []; _∷_)
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.Nat.Base using (ℕ; suc; zero)
open import Data.Product.Base using (_×_ ; _,_)
open import Data.These.Base using (These; this; that; these)
open import Data.Unit.Base using (⊤)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤)
open import Function.Base using (_$′_; _∘′_; id; _∘_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Size using (Size; ∞)
private
variable
a b c w : Level
i : Size
A : Set a
B : Set b
C : Set c
W : Set w
data Colist (A : Set a) (i : Size) : Set a where
[] : Colist A i
_∷_ : A → Thunk (Colist A) i → Colist A i
infixr 5 _∷_
------------------------------------------------------------------------
-- Relationship to Cowriter.
fromCowriter : Cowriter W A i → Colist W i
fromCowriter CW.[ _ ] = []
fromCowriter (w ∷ ca) = w ∷ λ where .force → fromCowriter (ca .force)
toCowriter : Colist A i → Cowriter A ⊤ i
toCowriter [] = CW.[ _ ]
toCowriter (a ∷ as) = a ∷ λ where .force → toCowriter (as .force)
------------------------------------------------------------------------
-- Basic functions.
[_] : A → Colist A ∞
[ a ] = a ∷ λ where .force → []
length : Colist A i → Conat i
length [] = zero
length (x ∷ xs) = suc λ where .force → length (xs .force)
replicate : Conat i → A → Colist A i
replicate zero a = []
replicate (suc n) a = a ∷ λ where .force → replicate (n .force) a
infixr 5 _++_ _⁺++_
_++_ : Colist A i → Colist A i → Colist A i
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ λ where .force → xs .force ++ ys
lookup : Colist A ∞ → ℕ → Maybe A
lookup [] _ = nothing
lookup (a ∷ as) zero = just a
lookup (a ∷ as) (suc n) = lookup (as .force) n
colookup : Colist A i → Conat i → Delay (Maybe A) i
colookup [] _ = now nothing
colookup (a ∷ as) zero = now (just a)
colookup (a ∷ as) (suc n) =
later λ where .force → colookup (as .force) (n .force)
take : (n : ℕ) → Colist A ∞ → Vec≤ A n
take zero xs = Vec≤.[]
take n [] = Vec≤.[]
take (suc n) (x ∷ xs) = x Vec≤.∷ take n (xs .force)
cotake : Conat i → Stream A i → Colist A i
cotake zero xs = []
cotake (suc n) (x ∷ xs) = x ∷ λ where .force → cotake (n .force) (xs .force)
drop : ℕ → Colist A ∞ → Colist A ∞
drop zero xs = xs
drop (suc n) [] = []
drop (suc n) (x ∷ xs) = drop n (xs .force)
fromList : List A → Colist A ∞
fromList [] = []
fromList (x ∷ xs) = x ∷ λ where .force → fromList xs
fromList⁺ : List⁺ A → Colist A ∞
fromList⁺ = fromList ∘′ List⁺.toList
_⁺++_ : List⁺ A → Thunk (Colist A) i → Colist A i
(x ∷ xs) ⁺++ ys = x ∷ λ where .force → fromList xs ++ ys .force
concat : Colist (List⁺ A) i → Colist A i
concat [] = []
concat (as ∷ ass) = as ⁺++ λ where .force → concat (ass .force)
fromStream : Stream A i → Colist A i
fromStream = cotake Conat.infinity
module ChunksOf (n : ℕ) where
chunksOf : Colist A ∞ → Cowriter (Vec A n) (Vec≤ A n) i
chunksOfAcc : ∀ m →
-- We have two continuations but we are only ever going to use one.
-- If we had linear types, we'd write the type using the & conjunction here.
(k≤ : Vec≤ A m → Vec≤ A n) →
(k≡ : Vec A m → Vec A n) →
-- Finally we chop up the input stream.
Colist A ∞ → Cowriter (Vec A n) (Vec≤ A n) i
chunksOf = chunksOfAcc n id id
chunksOfAcc zero k≤ k≡ as = k≡ [] ∷ λ where .force → chunksOf as
chunksOfAcc (suc k) k≤ k≡ [] = CW.[ k≤ Vec≤.[] ]
chunksOfAcc (suc k) k≤ k≡ (a ∷ as) =
chunksOfAcc k (k≤ ∘ (a Vec≤.∷_)) (k≡ ∘ (a ∷_)) (as .force)
open ChunksOf using (chunksOf) public
-- Test to make sure that the values are kept in the same order
_ : chunksOf 3 (fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ []))
≡ (1 ∷ 2 ∷ 3 ∷ []) ∷ _
_ = refl
map : (A → B) → Colist A i → Colist B i
map f [] = []
map f (a ∷ as) = f a ∷ λ where .force → map f (as .force)
unfold : (A → Maybe (A × B)) → A → Colist B i
unfold next seed with next seed
... | nothing = []
... | just (seed′ , b) = b ∷ λ where .force → unfold next seed′
scanl : (B → A → B) → B → Colist A i → Colist B i
scanl c n [] = n ∷ λ where .force → []
scanl c n (a ∷ as) = n ∷ λ where .force → scanl c (c n a) (as .force)
alignWith : (These A B → C) → Colist A i → Colist B i → Colist C i
alignWith f [] bs = map (f ∘′ that) bs
alignWith f as@(_ ∷ _) [] = map (f ∘′ this) as
alignWith f (a ∷ as) (b ∷ bs) =
f (these a b) ∷ λ where .force → alignWith f (as .force) (bs .force)
zipWith : (A → B → C) → Colist A i → Colist B i → Colist C i
zipWith f [] bs = []
zipWith f as [] = []
zipWith f (a ∷ as) (b ∷ bs) =
f a b ∷ λ where .force → zipWith f (as .force) (bs .force)
align : Colist A i → Colist B i → Colist (These A B) i
align = alignWith id
zip : Colist A i → Colist B i → Colist (A × B) i
zip = zipWith _,_
ap : Colist (A → B) i → Colist A i → Colist B i
ap = zipWith _$′_
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