From: Helmut Grohne <helmut@subdivi.de>
Date: Tue, 5 Jun 2012 16:03:51 +0000 (+0200)
Subject: make the Vec bff more similar to the List version
X-Git-Url: https://git.linta.de/?p=~helmut%2Fbidiragda.git;a=commitdiff_plain;h=84231ed91ae814d5a256e5fa24810c886ae31369

make the Vec bff more similar to the List version
---

diff --git a/BFF.agda b/BFF.agda
index 0cdb5d1..fe89742 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -41,12 +41,15 @@ module VecBFF where
   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 (getlen n) → Vec A n) → ({m : ℕ} {B : Set} → EqInst B → Vec B (getlen m) → Vec B m → Maybe (Vec B (getlen m)))
-  bff getlen get {m} eq s v = let s′ = allFin (getlen m)
-                                  g  = fromFunc (denumerate s)
-                                  h  = assoc eq (get s′) v
-                                  h′ = fmap (flip union g) h
-                               in fmap (flip mapV s′ ∘ (flip lookup)) h′
+  bff : {getlen : ℕ → ℕ} → ({A : Set} {n : ℕ} → Vec A (getlen n) → Vec A n) → ({m : ℕ} {B : Set} → EqInst B → Vec B (getlen m) → Vec B m → Maybe (Vec B (getlen m)))
+  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 lookup)) h′