From 066861f9cdde4ded6c5442508bef1a27576c68d7 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 17 Dec 2013 08:22:12 +0100 Subject: 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. --- BFF.agda | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'BFF.agda') 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 -- cgit v1.2.3