update bff implementation to use delete

In the presence of shape-changing updates, bff needs to shrink one of
the mappings before unifying them. As long the shape does not change,
the union becomes a disjoint union. With this insight we can adapt the
proof of theorem-1 using the adapted lemma-disjoint-union. Unfortunately
theorem-2 requires more work and assoc-enough becomes non-trivial due to
the introduction of mapMV.

1 files changed, 7 insertions, 4 deletions

diff --git a/BFF.agda b/BFF.agda
index 0cdb231..f7ddd30 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -14,6 +14,7 @@ open import Function using (id ; _∘_ ; flip)
 open import Relation.Binary.Core using (Decidable ; _≡_)
 
 open import FinMap
+open import Generic using (mapMV)
 import CheckInsert
 import FreeTheorems
 
@@ -33,7 +34,9 @@ module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
 
   bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n))
   bff get s v = let s′ = enumerate s
-                    g  = fromFunc (denumerate s)
-                    h  = assoc (get s′) v
-                    h′ = (flip union g) <$> h
-                in (flip mapV s′ ∘ flip lookupV) <$> h′
+                    t′ = get s′
+                    g  = partialize (fromFunc (denumerate s))
+                    g′ = delete-many t′ g
+                    h  = assoc t′ v
+                    h′ = (flip union g′) <$> h
+                in h′ >>= flip mapMV s′ ∘ flip lookupV