[ new ] functions in Codata.Stream (#516)

Author: gallais

CHANGELOG.md

@@ -60,6 +60,18 @@ Deprecated features
 Other minor additions
 ---------------------
 
+* Added new functions to `Codata.Stream`:
+  ```agda
+  splitAt    : (n : ℕ) → Stream A ∞ → Vec A n × Stream A ∞
+  drop       : ℕ → Stream A ∞ → Stream A ∞
+  interleave : Stream A i → Thunk (Stream A) i → Stream A i
+  ```
+
+* Added new proof to `Codata.Stream.Properties`:
+  ```agda
+  splitAt-map : splitAt n (map f xs) ≡ map (map f) (map f) (splitAt n xs)
+  ```
+
 * Added new proof to `Algebra.FunctionProperties.Consequences`:
   ```agda
   wlog : Commutative f → Total _R_ → (∀ a b → a R b → P (f a b)) → ∀ a b → P (f a b)

src/Codata/Stream.agda

@@ -36,9 +36,15 @@ module _ {ℓ} {A : Set ℓ} where
  lookup zero    xs = head xs
  lookup (suc k) xs = lookup k (tail xs)
 
+ splitAt : (n : ℕ) → Stream A ∞ → Vec A n × Stream A ∞
+ splitAt zero    xs       = [] , xs
+ splitAt (suc n) (x ∷ xs) = P.map₁ (x ∷_) (splitAt n (xs .force))
+
  take : (n : ℕ) → Stream A ∞ → Vec A n
- take zero    xs = []
- take (suc n) xs = head xs ∷ take n (tail xs)
+ take n xs = proj₁ (splitAt n xs)
+
+ drop : ℕ → Stream A ∞ → Stream A ∞
+ drop n xs = proj₂ (splitAt n xs)
 
  infixr 5 _++_ _⁺++_
  _++_ : ∀ {i} → List A → Stream A i → Stream A i
@@ -54,6 +60,9 @@ module _ {ℓ} {A : Set ℓ} where
  concat : ∀ {i} → Stream (List⁺ A) i → Stream A i
  concat (xs ∷ xss) = xs ⁺++ λ where .force → concat (xss .force)
 
+ interleave : ∀ {i} → Stream A i → Thunk (Stream A) i → Stream A i
+ interleave (x ∷ xs) ys = x ∷ λ where .force → interleave (ys .force) xs
+
 module _ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} where
 
  map : ∀ {i} → (A → B) → Stream A i → Stream B i

src/Codata/Stream/Properties.agda

@@ -7,11 +7,14 @@
 module Codata.Stream.Properties where
 
 open import Size
-open import Data.Nat.Base
-import Data.Vec as Vec
 open import Codata.Thunk using (Thunk; force)
 open import Codata.Stream
 open import Codata.Stream.Bisimilarity
+
+open import Data.Nat.Base
+import Data.Vec as Vec
+import Data.Product as Prod
+
 open import Function
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
 
@@ -40,16 +43,27 @@ module _ {a b} {A : Set a} {B : Set b} where
  ap-repeat-commute f a = Eq.refl ∷ λ where .force → ap-repeat-commute f a
 
 
+------------------------------------------------------------------------
 -- Functor laws
 
 module _ {a} {A : Set a} where
 
  map-identity : ∀ (as : Stream A ∞) {i} → i ⊢ map id as ≈ as
  map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force)
 
-
 module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
 
  map-map-fusion : ∀ (f : A → B) (g : B → C) as {i} → i ⊢ map g (map f as) ≈ map (g ∘ f) as
  map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force)
 
+
+------------------------------------------------------------------------
+-- splitAt
+
+module _ {a b} {A : Set a} {B : Set b} where
+
+  splitAt-map : ∀ n (f : A → B) xs →
+    splitAt n (map f xs) ≡ Prod.map (Vec.map f) (map f) (splitAt n xs)
+  splitAt-map zero    f xs       = Eq.refl
+  splitAt-map (suc n) f (x ∷ xs) =
+    Eq.cong (Prod.map₁ (f x Vec.∷_)) (splitAt-map n f (xs .force))