add examples
[~helmut/bidiragda.git] / 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