move imports for agda-stdlib 1.3
[~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 import Data.Maybe.Categorical
9 open import Data.Vec using (Vec)
10 open import Data.Product using (∃ ; _,_)
11 open import Relation.Binary using (module DecSetoid)
12 open import Relation.Binary.PropositionalEquality as P using (module ≡-Reasoning)
13 open import Relation.Nullary using (yes ; no)
14 open import Function using (flip ; id ; _∘_)
15 open import Function.LeftInverse using (_RightInverseOf_)
16 import Category.Monad
17 open Category.Monad.RawMonad {ℓ₀} Data.Maybe.Categorical.monad using (_>>=_)
18
19 open import Generic using (sequenceV ; ≡-to-Π)
20 import BFF
21 import GetTypes
22 import Examples
23
24 open DecSetoid A using (Carrier)
25 open GetTypes.PartialVecVec public using (Get)
26 open BFF.PartialVecBFF A public using (sbff ; bff)
27
28 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))
29 bffsameshape G {i} = sbff G i
30
31 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 (Maybe Carrier) (Get.gl₁ G j))
32 bffplug G sput {i} {m} s v with sput i m
33 ...                        | nothing = nothing
34 ...                        | just j with Get.gl₂ G j ≟ m
35 ...                                 | no gl₂j≢m  = nothing
36 bffplug G sput {i}     s v | just j | yes P.refl with bff G j s v
37 ...                                              | nothing = nothing
38 ...                                              | just s′ = just (j , s′)
39
40 _SimpleRightInvOf_ : {A B : Set} → (A → B) → (B → A) → Set
41 f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g
42
43 bffinv : (G : Get) → (nelteg : ℕ → Get.I G) → nelteg SimpleRightInvOf Get.gl₂ G → {i : Get.I G} → {m : ℕ} → Vec Carrier (Get.gl₁ G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.gl₁ G (nelteg m)))
44 bffinv G nelteg inv {m = m} s v = bff G (nelteg m) s (P.subst (Vec Carrier) (P.sym (inv m)) v)
45
46 module InvExamples where
47   open Examples using (reverse' ; drop' ; sieve' ; tail' ; take')
48   
49   reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
50   reverse-put s v = bffinv reverse' id (λ _ → P.refl) s v >>= sequenceV
51
52   drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m))
53   drop-put k = bffinv (drop' k) id (λ _ → P.refl)
54
55   double : ℕ → ℕ
56   double zero    = zero
57   double (suc n) = suc (suc (double n))
58
59   sieve-inv-len : double SimpleRightInvOf ⌈_/2⌉
60   sieve-inv-len zero          = P.refl
61   sieve-inv-len (suc zero)    = P.refl
62   sieve-inv-len (suc (suc x)) = P.cong (suc ∘ suc) (sieve-inv-len x)
63
64   sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec (Maybe Carrier) (double m))
65   sieve-put = bffinv sieve' double sieve-inv-len
66
67   tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (suc m))
68   tail-put = bffinv tail' id (λ _ → P.refl)
69
70   take-put : (k : ℕ) → {n : ℕ}  → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n))
71   take-put k = bffsameshape (take' k)