allow shape shape updates in bff

Unlike the original version in VoigtlaenderHMW13, we do not request an
  sput : ℕ → ℕ → Maybe ℕ
function for determining the updated source shape from the original
source and updated view shape. Instead we ask the caller directly to
provide the result of sput together with a proof that its getlen matches
with the provided, updated view.

The precondition assoc-enough is not enriched in this way and still
requires a non-changing shape. I.e. it says what it said before.

1 files changed, 9 insertions, 5 deletions

diff --git a/BFF.agda b/BFF.agda
index 1770b5e..56ba359 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -30,14 +30,18 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   enumerate : {n : ℕ} → Vec Carrier n → Vec (Fin n) n
   enumerate _ = tabulate id
 
+  enumeratel : (n : ℕ) → Vec (Fin n) n
+  enumeratel _ = tabulate id
+
   denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
   denumerate = flip lookupV
 
-  bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n))
-  bff G s v = let   s′ = enumerate s
+  bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m)
+  bff G m s v = let s′ = enumerate s
                     t′ = Get.get G s′
                     g  = fromFunc (denumerate s)
                     g′ = delete-many t′ g
-                    h  = assoc t′ v
-                    h′ = (flip union g′) <$> h
-                in h′ >>= flip mapMV s′ ∘ flip lookupM
+                    t  = enumeratel m
+                    h  = assoc (Get.get G t) v
+                    h′ = (flip union (reshape g′ m)) <$> h
+                in h′ >>= flip mapMV t ∘ flip lookupM