filter.agda

{-# OPTIONS --copatterns #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality


trans : {A : Set} {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
trans refl refl = refl

sym : {A : Set} {a b : A} -> a ≡ b -> b ≡ a
sym refl = refl

not : Bool -> Bool
not true = false
not false = true


_$_ : {A B : Set} -> (A -> B) -> A -> B
f $ a = f a 


data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} → A → Vec A n → Vec A (suc n)



record Stream (A : Set) : Set where
  coinductive
  constructor _::_

  field
    head : A
    tail : Stream A
open Stream


repeat : {A : Set} (a : A) -> Stream A
head (repeat a) = a
tail (repeat a) = repeat a

map : {A B : Set} -> (A -> B) -> Stream A -> Stream B
head (map f as) = f (head as)
tail (map f as) = map f (tail as)

-- You cannot define filter. Why? consider `filter (const ff) as`
zip : {A B C : Set} -> (A -> B -> C) -> Stream A -> Stream B -> Stream C
head (zip f as bs) = f (head as) (head bs)
tail (zip f as bs) = zip f (tail as) (tail bs)

scan : {A B : Set} -> (B -> A -> B) -> B -> Stream A -> Stream B
head (scan f i as) = f i $ head as
tail (scan f i as) = scan f (f i $ head as) (tail as)

-- These two are where copatterns really shine, I feel
interleave : {A : Set} -> Stream A -> Stream A -> Stream A
head (interleave a b) = head a
tail (interleave a b) = interleave b (tail a)


intersperse : {A : Set} -> A -> Stream A -> Stream A
head (intersperse _ as) = head as
tail (intersperse a as) = a :: (tail as)

-- This one isn't as short when written with copatterns
drop : { A : Set} -> Nat -> Stream A -> Stream A
drop zero as = as
drop (suc n) as = drop n (tail as)


-- I like that I can do this, and n isn't an obvious argument
toVec : {A : Set} {n : Nat} -> Stream A -> Vec A n
toVec {_} {zero} _ = []
toVec {_} {suc m} as = (head as) :: (toVec (tail as))


-- These are pretty nice, tbh
mutual
  trues_falses : Stream Bool
  head (trues_falses) = true
  tail (trues_falses) = falses_trues

  falses_trues : Stream Bool
  head (falses_trues) = false
  tail (falses_trues) = trues_falses


trues = repeat true
falses = repeat false

trues_falses' = interleave trues falses


-- We can't use normal equality (_≡_) here, because it's inductive
-- so we include our own coinductive version
-- I don't know if this can be generalisable, or whether you have to
-- define this per data type
record StreamEq {A : Set} (as : Stream A) (bs : Stream A) : Set where
  coinductive
  constructor MkStreamEq
  field
    head_eq : (head as) ≡ (head bs)
    tail_eq : StreamEq (tail as) (tail bs)
open StreamEq


stream-eq-trans : {A : Set} {as bs cs : Stream A} -> StreamEq as bs -> StreamEq bs cs -> StreamEq as cs
head_eq (stream-eq-trans prfab prfbc) = trans (head_eq prfab) (head_eq prfbc)
tail_eq (stream-eq-trans prfab prfbc) = stream-eq-trans (tail_eq prfab) (tail_eq prfbc)

stream-eq-sym : {A : Set} {as bs : Stream A} -> StreamEq as bs -> StreamEq bs as
head_eq (stream-eq-sym p) = sym (head_eq p)
tail_eq (stream-eq-sym p) = stream-eq-sym (tail_eq p)


-- These are another place it seems copatterns do very well

foo : StreamEq trues trues
head_eq foo = refl
tail_eq foo = foo

bar : StreamEq trues (map not falses)
head_eq bar = refl
tail_eq bar = bar

mutual
  baz1 : StreamEq trues_falses (tail falses_trues)
  head_eq baz1 = refl
  tail_eq baz1 = baz2

  baz2 : StreamEq falses_trues (tail trues_falses)
  head_eq baz2 = refl
  tail_eq baz2 = baz1

  qux1 : StreamEq trues_falses (map not falses_trues)
  head_eq qux1 = refl
  tail_eq qux1 = qux2

  qux2 : StreamEq falses_trues (map not trues_falses)
  head_eq qux2 = refl
  tail_eq qux2 = qux1



quux : StreamEq (tail trues_falses) (map not trues_falses)
quux = stream-eq-trans baz2 qux2