third definition of bff

It is a definition based on Vec but with less assumptions. The VecBFF
has therefore been renamed to VecRevBFF.

VecBFF uses get : \forall n \exists m -> Vec A n -> Vec a m
VecRevBFF uses get : \forall m \exists n -> Vec A n -> Vec a m

1 files changed, 19 insertions, 0 deletions

diff --git a/BFF.agda b/BFF.agda
index fe89742..bde72ee 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -37,6 +37,25 @@ module ListBFF where
                    in fmap (flip map s′ ∘ flip lookup) h′
 
 module VecBFF where
+
+  assoc : {A : Set} {n m : ℕ} → EqInst A → Vec (Fin n) m → Vec A m → Maybe (FinMapMaybe n A)
+  assoc _  []V       []V       = just empty
+  assoc eq (i ∷V is) (b ∷V bs) = (assoc eq is bs) >>= (checkInsert eq i b)
+
+  enumerate : {A : Set} {n : ℕ} → Vec A n → Vec (Fin n) n
+  enumerate _ = tabulate id
+
+  denumerate : {A : Set} {n : ℕ} → Vec A n → Fin n → A
+  denumerate = flip lookupV
+
+  bff : {getlen : ℕ → ℕ} → ({A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)) → ({B : Set} {n : ℕ} → EqInst B → Vec B n → Vec B (getlen n) → Maybe (Vec B n))
+  bff get eq s v = let s′ = enumerate s
+                       g  = fromFunc (denumerate s)
+                       h  = assoc eq (get s′) v
+                       h′ = fmap (flip union g) h
+                   in fmap (flip mapV s′ ∘ flip lookupV) h′
+
+module VecRevBFF where
   assoc : {A : Set} {m n : ℕ} → EqInst A → Vec (Fin m) n → Vec A n → Maybe (FinMapMaybe m A)
   assoc _  []V       []V       = just empty
   assoc eq (i ∷V is) (b ∷V bs) = (assoc eq is bs) >>= (checkInsert eq i b)