diff options
Diffstat (limited to 'BFFPlug.agda')
| -rw-r--r-- | BFFPlug.agda | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/BFFPlug.agda b/BFFPlug.agda index 9f45db1..12ee980 100644 --- a/BFFPlug.agda +++ b/BFFPlug.agda @@ -13,8 +13,10 @@ open import Relation.Nullary using (yes ; no) open import Function using (flip ; id ; _∘_) open import Function.Equality using (_⟶_ ; _⟨$⟩_) open import Function.LeftInverse using (_RightInverseOf_) +import Category.Monad +open Category.Monad.RawMonad {ℓ₀} Data.Maybe.monad using (_>>=_) -open import Generic using (≡-to-Π) +open import Generic using (sequenceV ; ≡-to-Π) import BFF import GetTypes import Examples @@ -24,9 +26,9 @@ 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 +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 Carrier (Get.|gl₁| G j)) +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 @@ -38,16 +40,16 @@ bffplug G sput {i} s v | just j | yes refl with bff G j s v _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 : 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 (Maybe 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) + reverse-put s v = bffinv reverse' (≡-to-Π id) (λ _ → refl) s v >>= sequenceV - drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec Carrier (k + m)) + drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m)) drop-put k = bffinv (drop' k) (≡-to-Π id) (λ _ → refl) double : ℕ → ℕ @@ -59,10 +61,10 @@ module InvExamples where 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 : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec (Maybe 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 : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe 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)) |