Merge branch feature-shape-update into master

The branch enables shape updates in variety of flavours:
 * explicitly passing the desired target shape
 * providing a plugin sput : ℕ → ℕ → Maybe ℕ
 * providing a right-inverse to getlen
It also provides a backwards compatibility function to facilitate
shape-retaining updates.

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