Example: show that PairVec is Shaped
[~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 Algebra.Structures.IsCommutativeSemiring Data.Nat.Properties.isCommutativeSemiring using (+-isCommutativeMonoid)
7 open Algebra.Structures.IsCommutativeMonoid +-isCommutativeMonoid using () renaming (comm to +-comm)
8 open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
9 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop)
10 open import Function using (id)
11 open import Function.Injection using () renaming (Injection to _↪_ ; id to id↪)
12 open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong) renaming (setoid to EqSetoid)
13
14 open import Generic using (≡-to-Π)
15 open import Structures using (Shaped)
16 import GetTypes
17 import FreeTheorems
18
19 open GetTypes.PartialVecVec using (Get)
20 open FreeTheorems.PartialVecVec using (assume-get)
21
22 reverse' : Get
23 reverse' = assume-get id↪ (≡-to-Π id) reverse
24
25 double' : Get
26 double' = assume-get id↪ (≡-to-Π g) f
27   where g : ℕ → ℕ
28         g zero = zero
29         g (suc n) = suc (suc (g n))
30         f : {A : Set} {n : ℕ} → Vec A n → Vec A (g n)
31         f []      = []
32         f (x ∷ v) = x ∷ x ∷ f v
33
34 double'' : Get
35 double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v)
36
37 drop-suc : {n m : ℕ} → suc n ≡ suc m → n ≡ m
38 drop-suc refl = refl
39
40 suc-injection : EqSetoid ℕ ↪ EqSetoid ℕ
41 suc-injection = record { to = ≡-to-Π suc; injective = drop-suc }
42
43 tail' : Get
44 tail' = assume-get suc-injection (≡-to-Π id) tail
45
46 n+-injection : ℕ → EqSetoid ℕ ↪ EqSetoid ℕ
47 n+-injection n = record { to = ≡-to-Π (_+_ n); injective = cancel-+-left n }
48
49 take' : ℕ → Get
50 take' n = assume-get (n+-injection n) (≡-to-Π _) (take n)
51
52 drop' : ℕ → Get
53 drop' n = assume-get (n+-injection n) (≡-to-Π _) (drop n)
54
55 sieve' : Get
56 sieve' = assume-get id↪ (≡-to-Π _) f
57   where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
58         f []           = []
59         f (x ∷ [])     = x ∷ []
60         f (x ∷ _ ∷ xs) = x ∷ f xs
61
62 intersperse-len : ℕ → ℕ
63 intersperse-len zero          = zero
64 intersperse-len (suc zero)    = suc zero
65 intersperse-len (suc (suc n)) = suc (suc (intersperse-len (suc n)))
66
67 intersperse : {A : Set} {n : ℕ} → A → Vec A n → Vec A (intersperse-len n)
68 intersperse s []          = []
69 intersperse s (x ∷ [])    = x ∷ []
70 intersperse s (x ∷ y ∷ v) = x ∷ s ∷ intersperse s (y ∷ v)
71
72 intersperse' : Get
73 intersperse' = assume-get suc-injection (≡-to-Π intersperse-len) f
74   where f : {A : Set} {n : ℕ} → Vec A (suc n) → Vec A (intersperse-len n)
75         f (s ∷ v)        = intersperse s v
76
77 data PairVec (α : Set) (β : Set) : List α → Set where
78   []P : PairVec α β []L
79   _,_∷P_ : (x : α) → β → {l : List α} → PairVec α β l → PairVec α β (x ∷L l)
80
81 PairVecFirstShaped : (α : Set) → Shaped (List α) (PairVec α)
82 PairVecFirstShaped α = record
83   { arity = length
84   ; content = content
85   ; fill = fill
86   ; isShaped = record
87     { content-fill = content-fill
88     ; fill-content = fill-content
89     } }
90   where content : {β : Set} {s : List α} → PairVec α β s → Vec β (length s)
91         content []P          = []
92         content (a , b ∷P p) = b ∷ content p
93
94         fill : {β : Set} → (s : List α) → Vec β (length s) → PairVec α β s
95         fill []L      v       = []P
96         fill (a ∷L s) (b ∷ v) = a , b ∷P fill s v
97
98         content-fill : {β : Set} {s : List α} → (p : PairVec α β s) → fill s (content p) ≡ p
99         content-fill []P          = refl
100         content-fill (a , b ∷P p) = cong (_,_∷P_ a b) (content-fill p)
101
102         fill-content : {β : Set} → (s : List α) → (v : Vec β (length s)) → content (fill s v) ≡ v
103         fill-content []L      []      = refl
104         fill-content (a ∷L s) (b ∷ v) = cong (_∷_ b) (fill-content s v)