f30faa524c7ab9b2630de920fff4790b92e0342b
[~helmut/bidiragda.git] / Examples.agda
1 module Examples where
2
3 open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉)
4 open import Data.Nat.Properties using (cancel-+-left)
5 import Algebra.Structures
6 open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
7 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop)
8 open import Function using (id)
9 open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong)
10
11 open import Structures using (Shaped)
12 import GetTypes
13 import FreeTheorems
14
15 open GetTypes.PartialVecVec using (Get)
16 open FreeTheorems.PartialVecVec using (assume-get)
17
18 reverse' : Get
19 reverse' = assume-get id id reverse
20
21 double' : Get
22 double' = assume-get id g f
23   where g : ℕ → ℕ
24         g zero = zero
25         g (suc n) = suc (suc (g n))
26         f : {A : Set} {n : ℕ} → Vec A n → Vec A (g n)
27         f []      = []
28         f (x ∷ v) = x ∷ x ∷ f v
29
30 double'' : Get
31 double'' = assume-get id _ (λ v → v ++ v)
32
33 tail' : Get
34 tail' = assume-get suc id tail
35
36 take' : ℕ → Get
37 take' n = assume-get (_+_ n) _ (take n)
38
39 drop' : ℕ → Get
40 drop' n = assume-get (_+_ n) _ (drop n)
41
42 sieve' : Get
43 sieve' = assume-get id _ f
44   where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
45         f []           = []
46         f (x ∷ [])     = x ∷ []
47         f (x ∷ _ ∷ xs) = x ∷ f xs
48
49 intersperse-len : ℕ → ℕ
50 intersperse-len zero          = zero
51 intersperse-len (suc zero)    = suc zero
52 intersperse-len (suc (suc n)) = suc (suc (intersperse-len (suc n)))
53
54 intersperse : {A : Set} {n : ℕ} → A → Vec A n → Vec A (intersperse-len n)
55 intersperse s []          = []
56 intersperse s (x ∷ [])    = x ∷ []
57 intersperse s (x ∷ y ∷ v) = x ∷ s ∷ intersperse s (y ∷ v)
58
59 intersperse' : Get
60 intersperse' = assume-get suc intersperse-len f
61   where f : {A : Set} {n : ℕ} → Vec A (suc n) → Vec A (intersperse-len n)
62         f (s ∷ v)        = intersperse s v
63
64 data PairVec (α : Set) (β : Set) : List α → Set where
65   []P : PairVec α β []L
66   _,_∷P_ : (x : α) → β → {l : List α} → PairVec α β l → PairVec α β (x ∷L l)
67
68 PairVecFirstShaped : (α : Set) → Shaped (List α) (PairVec α)
69 PairVecFirstShaped α = record
70   { arity = length
71   ; content = content
72   ; fill = fill
73   ; isShaped = record
74     { content-fill = content-fill
75     ; fill-content = fill-content
76     } }
77   where content : {β : Set} {s : List α} → PairVec α β s → Vec β (length s)
78         content []P          = []
79         content (a , b ∷P p) = b ∷ content p
80
81         fill : {β : Set} → (s : List α) → Vec β (length s) → PairVec α β s
82         fill []L      v       = []P
83         fill (a ∷L s) (b ∷ v) = a , b ∷P fill s v
84
85         content-fill : {β : Set} {s : List α} → (p : PairVec α β s) → fill s (content p) ≡ p
86         content-fill []P          = refl
87         content-fill (a , b ∷P p) = cong (_,_∷P_ a b) (content-fill p)
88
89         fill-content : {β : Set} → (s : List α) → (v : Vec β (length s)) → content (fill s v) ≡ v
90         fill-content []L      []      = refl
91         fill-content (a ∷L s) (b ∷ v) = cong (_∷_ b) (fill-content s v)