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