25bdbaa6de064f69b1d04b65c1dd7680cb50e4b3
[~helmut/bidiragda.git] / Examples.agda
1 module Examples where
2
3 open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_ ; ⌈_/2⌉)
4 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_)
5 open import Function using (id)
6 open import Function.Injection using () renaming (id to id↪)
7
8 open import Generic using (≡-to-Π)
9 import GetTypes
10 import FreeTheorems
11
12 open GetTypes.PartialVecVec using (Get)
13 open FreeTheorems.PartialVecVec using (assume-get)
14
15 reverse' : Get
16 reverse' = assume-get id↪ (≡-to-Π id) reverse
17
18 double' : Get
19 double' = assume-get id↪ (≡-to-Π g) f
20   where g : ℕ → ℕ
21         g zero = zero
22         g (suc n) = suc (suc (g n))
23         f : {A : Set} {n : ℕ} → Vec A n → Vec A (g n)
24         f []      = []
25         f (x ∷ v) = x ∷ x ∷ f v
26
27 double'' : Get
28 double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v)
29
30 take' : ℕ → Get
31 take' n = assume-get id↪ (≡-to-Π _) (f n)
32   where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ⊓ n)
33         f n       []       = []
34         f zero    (x ∷ xs) = []
35         f (suc n) (x ∷ xs) = x ∷ f n xs
36
37 drop' : ℕ → Get
38 drop' n = assume-get id↪ (≡-to-Π _) (f n)
39   where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ∸ n)
40         f zero    xs       = xs
41         f (suc n) []       = []
42         f (suc n) (x ∷ xs) = f n xs
43
44 sieve' : Get
45 sieve' = assume-get id↪ (≡-to-Π _) f
46   where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
47         f []           = []
48         f (x ∷ [])     = x ∷ []
49         f (x ∷ _ ∷ xs) = x ∷ f xs