blob: 9f45db105ca668d11ab4da5d6b404a0290363f73 (
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
|
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)
open import Data.Vec using (Vec)
open import Data.Product using (∃ ; _,_)
open import Relation.Binary using (module DecSetoid)
open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq)
open import Relation.Nullary using (yes ; no)
open import Function using (flip ; id ; _∘_)
open import Function.Equality using (_⟶_ ; _⟨$⟩_)
open import Function.LeftInverse using (_RightInverseOf_)
open import Generic using (≡-to-Π)
import BFF
import GetTypes
import Examples
open DecSetoid A using (Carrier)
open GetTypes.PartialVecVec public using (Get)
open BFF.PartialVecBFF A public
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} = bff 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 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 refl with bff G j s v
... | nothing = nothing
... | just s′ = just (j , s′)
_SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set
f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g
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)))
bffinv G nelteg inv {m = m} s v = bff G (nelteg ⟨$⟩ m) s (subst (Vec Carrier) (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 = bffinv reverse' (≡-to-Π id) (λ _ → refl)
drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec Carrier (k + m))
drop-put k = bffinv (drop' k) (≡-to-Π id) (λ _ → refl)
double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
sieve-inv-len : double SimpleRightInvOf ⌈_/2⌉
sieve-inv-len zero = refl
sieve-inv-len (suc zero) = refl
sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x)
sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (double m))
sieve-put = bffinv sieve' (≡-to-Π double) sieve-inv-len
tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec Carrier (suc m))
tail-put = bffinv tail' (≡-to-Π id) (λ _ → refl)
take-put : (k : ℕ) → {n : ℕ} → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n))
take-put k = bffsameshape (take' k)
|
