Examples.agda

   1 module Examples where
   2
   3 open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_)
   4 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_)
   5
   6 import GetTypes
   7 import FreeTheorems
   8
   9 open GetTypes.VecVec using (Get)
  10 open FreeTheorems.VecVec using (assume-get)
  11
  12 reverse' : Get
  13 reverse' = assume-get reverse
  14
  15 double' : Get
  16 double' = assume-get f
  17   where g : ℕ → ℕ
  18         g zero = zero
  19         g (suc n) = suc (suc (g n))
  20         f : {A : Set} {n : ℕ} → Vec A n → Vec A (g n)
  21         f []      = []
  22         f (x ∷ v) = x ∷ x ∷ f v
  23
  24 double'' : Get
  25 double'' = assume-get (λ v → v ++ v)
  26
  27 take' : ℕ → Get
  28 take' n = assume-get (f n)
  29   where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ⊓ n)
  30         f n       []       = []
  31         f zero    (x ∷ xs) = []
  32         f (suc n) (x ∷ xs) = x ∷ f n xs
  33
  34 drop' : ℕ → Get
  35 drop' n = assume-get (f n)
  36   where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ∸ n)
  37         f zero    xs       = xs
  38         f (suc n) []       = []
  39         f (suc n) (x ∷ xs) = f n xs