remove the sequenceV call from bff

This allows bff to be more precise with regard to its failure modes,
even though we are not yet making use of that projected precision. It
allows inserting a default value for entries that could not be recovered
in a shape changing update as described in VoigtlaenderHMW13.

1 files changed, 12 insertions, 17 deletions

diff --git a/Precond.agda b/Precond.agda
index 3a48757..45076f3 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -25,13 +25,12 @@ open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ;
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)
 
-open import Generic using (mapMV ; sequenceV)
 open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id)
 import CheckInsert
 open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
 import Bidir
-open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
+open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain)
 import GetTypes
 open GetTypes.PartialVecVec using (Get ; module Get)
 open BFF.PartialVecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff ; enumeratel)
@@ -63,23 +62,19 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A
           maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
         inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)
 
-assoc-enough : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G i s v ≡ just u
+assoc-enough : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G i s v ≡ just (map just u)
 assoc-enough G {i} s v (h , p) = _ , (begin
   bff G i s v
-    ≡⟨ cong (flip _>>=_ (flip mapMV t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Get.|gl₁| G i)))) p ⟩
-  mapMV (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t
-    ≡⟨ refl ⟩
-  sequenceV (map (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t)
-    ≡⟨ cong (sequenceV ∘ flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
-  sequenceV (map (flip lookupM (union h g′)) t)
-    ≡⟨ cong (sequenceV ∘ flip map t ∘ flip lookupM) (proj₂ wp) ⟩
-  sequenceV (map (flip lookupM (fromFunc (proj₁ wp))) t)
-    ≡⟨ cong sequenceV (map-cong (lemma-lookupM-fromFunc (proj₁ wp)) t) ⟩
-  sequenceV (map (Maybe.just ∘ proj₁ wp) t)
-    ≡⟨ cong sequenceV (map-∘ just (proj₁ wp) t) ⟩
-  sequenceV (map Maybe.just (map (proj₁ wp) t))
-    ≡⟨ lemma-just-sequence (map (proj₁ wp) t) ⟩
-  just (map (proj₁ wp) t) ∎)
+    ≡⟨ cong (_<$>_ (flip map t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Get.|gl₁| G i)))) p ⟩
+  just (map (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t)
+    ≡⟨ cong (Maybe.just ∘ flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
+  just (map (flip lookupM (union h g′)) t)
+    ≡⟨ cong (Maybe.just ∘ flip map t ∘ flip lookupM) (proj₂ wp) ⟩
+  just (map (flip lookupM (fromFunc (proj₁ wp))) t)
+    ≡⟨ cong Maybe.just (map-cong (lemma-lookupM-fromFunc (proj₁ wp)) t) ⟩
+  just (map (Maybe.just ∘ proj₁ wp) t)
+    ≡⟨ cong just (map-∘ just (proj₁ wp) t) ⟩
+  just (map Maybe.just (map (proj₁ wp) t)) ∎)
   where open Get G
         s′ = enumerate s
         g  = fromFunc (denumerate s)