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