use drop, tail and take from Data.Vec in examples
[~helmut/bidiragda.git] / BFFPlug.agda
1 open import Level using () renaming (zero to ℓ₀)
2 open import Relation.Binary using (DecSetoid)
3
4 module BFFPlug (A : DecSetoid ℓ₀ ℓ₀) where
5
6 open import Data.Nat using (ℕ ; _≟_ ; _+_ ; zero ; suc ; ⌈_/2⌉)
7 open import Data.Maybe using (Maybe ; just ; nothing)
8 open import Data.Vec using (Vec)
9 open import Data.Product using (∃ ; _,_)
10 open import Relation.Binary using (module DecSetoid)
11 open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq)
12 open import Relation.Nullary using (yes ; no)
13 open import Function using (flip ; id ; _∘_)
14 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
15 open import Function.LeftInverse using (_RightInverseOf_)
16
17 open import Generic using (≡-to-Π)
18 import BFF
19 import GetTypes
20 import Examples
21
22 open DecSetoid A using (Carrier)
23 open GetTypes.PartialVecVec public using (Get)
24 open BFF.PartialVecBFF A public
25
26 bffsameshape : (G : Get) → {i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i))
27 bffsameshape G {i} = bff G i
28
29 bffplug : (G : Get) → (Get.|I| G → ℕ → Maybe (Get.|I| G)) → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (∃ λ j → Vec Carrier (Get.|gl₁| G j))
30 bffplug G sput {i} {m} s v with sput i m
31 ...                        | nothing = nothing
32 ...                        | just j with Get.|gl₂| G j ≟ m
33 ...                                 | no gl₂j≢m  = nothing
34 bffplug G sput {i}     s v | just j | yes refl with bff G j s v
35 ...                                            | nothing = nothing
36 ...                                            | just s′ = just (j , s′)
37
38 _SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set
39 f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g
40
41 bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverseOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec Carrier (Get.|gl₁| G (nelteg ⟨$⟩ m)))
42 bffinv G nelteg inv {m = m} s v = bff G (nelteg ⟨$⟩ m) s (subst (Vec Carrier) (sym (inv m)) v)
43
44 module InvExamples where
45   open Examples using (reverse' ; drop' ; sieve' ; tail' ; take')
46   
47   reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
48   reverse-put = bffinv reverse' (≡-to-Π id) (λ _ → refl)
49
50   drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec Carrier (k + m))
51   drop-put k = bffinv (drop' k) (≡-to-Π id) (λ _ → refl)
52
53   double : ℕ → ℕ
54   double zero    = zero
55   double (suc n) = suc (suc (double n))
56
57   sieve-inv-len : double SimpleRightInvOf ⌈_/2⌉
58   sieve-inv-len zero          = refl
59   sieve-inv-len (suc zero)    = refl
60   sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x)
61
62   sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (double m))
63   sieve-put = bffinv sieve' (≡-to-Π double) sieve-inv-len
64
65   tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec Carrier (suc m))
66   tail-put = bffinv tail' (≡-to-Π id) (λ _ → refl)
67
68   take-put : (k : ℕ) → {n : ℕ}  → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n))
69   take-put k = bffsameshape (take' k)