move all those toList calls inside _in-domain-of_
[~helmut/bidiragda.git] / BFFPlug.agda
index f463a09..5c219a5 100644 (file)
@@ -3,8 +3,7 @@ open import Relation.Binary using (DecSetoid)
 
 module BFFPlug (A : DecSetoid ℓ₀ ℓ₀) where
 
-open import Data.Nat using (ℕ ; _≟_ ; _+_ ; _∸_ ; zero ; suc ; ⌈_/2⌉)
-open import Data.Nat.Properties using (m+n∸n≡m)
+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 (∃ ; _,_)
@@ -14,20 +13,22 @@ 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
 
 open DecSetoid A using (Carrier)
 open GetTypes.PartialVecVec public using (Get)
-open BFF.PartialVecBFF A public
+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} = 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
@@ -39,17 +40,17 @@ 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')
+  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 n → Vec Carrier m → Maybe (Vec Carrier (m + k))
-  drop-put k = bffinv (drop' k) (≡-to-Π (flip _+_ k)) (flip m+n∸n≡m k)
+  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 : ℕ → ℕ
   double zero    = zero
@@ -60,5 +61,11 @@ 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 (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))
+  take-put k = bffsameshape (take' k)