add back original bff function before shape updates
[~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.Nat.Properties using (m+n∸n≡m)
8 open import Data.Maybe using (Maybe ; just ; nothing)
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 using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq)
13 open import Relation.Nullary using (yes ; no)
14 open import Function using (flip ; id ; _∘_)
15 open import Function.Equality using (_⟶_)
16 open import Function.LeftInverse using (_RightInverseOf_)
17
18 import BFF
19 import GetTypes
20 import Examples
21
22 open DecSetoid A using (Carrier)
23 open GetTypes.VecVec public using (Get)
24 open BFF.VecBFF A public
25
26 bffsameshape : (G : Get) → {n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n)
27 bffsameshape G {n} = bff G n
28
29 bffplug : (G : Get) → (ℕ → ℕ → Maybe ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (∃ λ l → Vec Carrier l)
30 bffplug G sput {n} {m} s v with sput n m
31 ...                        | nothing = nothing
32 ...                        | just l with Get.getlen G l ≟ m
33 ...                                 | no getlenl≢m  = nothing
34 bffplug G sput {n}     s v | just l | yes refl with bff G l s v
35 ...                                            | nothing = nothing
36 ...                                            | just s′ = just (l , s′)
37
38 as-Π : {A B : Set} → (f : A → B) → PropEq A ⟶ PropEq B
39 as-Π f = record { _⟨$⟩_ = f; cong = cong f }
40
41 _SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set
42 f SimpleRightInvOf g = as-Π f RightInverseOf as-Π g
43
44 bffinv : (G : Get) → (nelteg : ℕ → ℕ) → nelteg SimpleRightInvOf Get.getlen G → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (nelteg m))
45 bffinv G nelteg inv {n} {m} s v = bff G (nelteg m) s (subst (Vec Carrier) (sym (inv m)) v)
46
47 module InvExamples where
48   open Examples using (reverse' ; drop' ; sieve')
49   
50   reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
51   reverse-put = bffinv reverse' id (λ _ → refl)
52
53   drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (m + k))
54   drop-put k = bffinv (drop' k) (flip _+_ k) (flip m+n∸n≡m k)
55
56   double : ℕ → ℕ
57   double zero    = zero
58   double (suc n) = suc (suc (double n))
59
60   sieve-inv-len : double SimpleRightInvOf ⌈_/2⌉
61   sieve-inv-len zero          = refl
62   sieve-inv-len (suc zero)    = refl
63   sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x)
64
65   sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (double m))
66   sieve-put = bffinv sieve' double sieve-inv-len