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.

4 files changed, 61 insertions, 49 deletions

diff --git a/BFF.agda b/BFF.agda
index 6943f0d..9fc0afe 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -14,7 +14,7 @@ open import Function using (id ; _∘_ ; flip)
 open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid)
 
 open import FinMap
-open import Generic using (mapMV ; ≡-to-Π)
+open import Generic using (sequenceV ; ≡-to-Π)
 import CheckInsert
 open import GetTypes using (VecVec-to-PartialVecVec)
 
@@ -36,7 +36,7 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
   denumerate = flip lookupV
 
-  bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j))
+  bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G j))
   bff G i s v = let s′ = enumerate s
                     t′ = Get.get G s′
                     g  = fromFunc (denumerate s)
@@ -44,7 +44,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
                     t  = enumeratel (Get.|gl₁| G i)
                     h  = assoc (Get.get G t) v
                     h′ = (flip union (reshape g′ (Get.|gl₁| G i))) <$> h
-                in h′ >>= flip mapMV t ∘ flip lookupM
+                in (flip mapV t ∘ flip lookupM) <$> h′
+
+  sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j))
+  sbff G j s v = bff G j s v >>= sequenceV
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.VecVec public using (Get)
@@ -53,5 +56,8 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
 
   open PartialVecBFF A public using (assoc ; enumerate ; denumerate)
 
-  bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m)
+  bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec (Maybe Carrier) m)
   bff G = PartialVecBFF.bff A (VecVec-to-PartialVecVec G)
+
+  sbff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m)
+  sbff G = PartialVecBFF.sbff A (VecVec-to-PartialVecVec G)
diff --git a/BFFPlug.agda b/BFFPlug.agda
index 9f45db1..12ee980 100644
--- a/BFFPlug.agda
+++ b/BFFPlug.agda
@@ -13,8 +13,10 @@ open import Relation.Nullary using (yes ; no)
 open import Function using (flip ; id ; _∘_)
 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
 open import Function.LeftInverse using (_RightInverseOf_)
+import Category.Monad
+open Category.Monad.RawMonad {ℓ₀} Data.Maybe.monad using (_>>=_)
 
-open import Generic using (≡-to-Π)
+open import Generic using (sequenceV ; ≡-to-Π)
 import BFF
 import GetTypes
 import Examples
@@ -24,9 +26,9 @@ open GetTypes.PartialVecVec public using (Get)
 open BFF.PartialVecBFF A public
 
 bffsameshape : (G : Get) → {i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i))
-bffsameshape G {i} = bff G i
+bffsameshape G {i} = sbff G i
 
-bffplug : (G : Get) → (Get.|I| G → ℕ → Maybe (Get.|I| G)) → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (∃ λ j → Vec Carrier (Get.|gl₁| G j))
+bffplug : (G : Get) → (Get.|I| G → ℕ → Maybe (Get.|I| G)) → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (∃ λ j → Vec (Maybe Carrier) (Get.|gl₁| G j))
 bffplug G sput {i} {m} s v with sput i m
 ...                        | nothing = nothing
 ...                        | just j with Get.|gl₂| G j ≟ m
@@ -38,16 +40,16 @@ bffplug G sput {i}     s v | just j | yes refl with bff G j s v
 _SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set
 f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g
 
-bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverseOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec Carrier (Get.|gl₁| G (nelteg ⟨$⟩ m)))
+bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverseOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G (nelteg ⟨$⟩ m)))
 bffinv G nelteg inv {m = m} s v = bff G (nelteg ⟨$⟩ m) s (subst (Vec Carrier) (sym (inv m)) v)
 
 module InvExamples where
   open Examples using (reverse' ; drop' ; sieve' ; tail' ; take')
   
   reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
-  reverse-put = bffinv reverse' (≡-to-Π id) (λ _ → refl)
+  reverse-put s v = bffinv reverse' (≡-to-Π id) (λ _ → refl) s v >>= sequenceV
 
-  drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec Carrier (k + m))
+  drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m))
   drop-put k = bffinv (drop' k) (≡-to-Π id) (λ _ → refl)
 
   double : ℕ → ℕ
@@ -59,10 +61,10 @@ module InvExamples where
   sieve-inv-len (suc zero)    = refl
   sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x)
 
-  sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (double m))
+  sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec (Maybe Carrier) (double m))
   sieve-put = bffinv sieve' (≡-to-Π double) sieve-inv-len
 
-  tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec Carrier (suc m))
+  tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (suc m))
   tail-put = bffinv tail' (≡-to-Π id) (λ _ → refl)
 
   take-put : (k : ℕ) → {n : ℕ}  → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n))
diff --git a/Bidir.agda b/Bidir.agda
index 43d8580..adb9800 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -123,7 +123,7 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin
   as ∎)
   where open ≡-Reasoning
 
-theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just s
+theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (map just s)
 theorem-1 G {i} s = begin
   bff G i s (get s)
     ≡⟨ cong (bff G i s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩
@@ -141,17 +141,17 @@ theorem-1 G {i} s = begin
     ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩
   (h′↦r ∘ just) (fromFunc (denumerate s))
     ≡⟨ refl ⟩
-  mapMV (flip lookupM (fromFunc (denumerate s))) (enumerate s)
-    ≡⟨ mapMV-cong (lemma-lookupM-fromFunc (denumerate s)) (enumerate s) ⟩
-  mapMV (Maybe.just ∘ denumerate s) (enumerate s)
-    ≡⟨ mapMV-purity (denumerate s) (enumerate s) ⟩
-  just (map (denumerate s) (enumerate s))
-    ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩
-  just s ∎
+  just (map (flip lookupM (fromFunc (denumerate s))) (enumerate s))
+    ≡⟨ cong just (map-cong (lemma-lookupM-fromFunc (denumerate s)) (enumerate s)) ⟩
+  just (map (Maybe.just ∘ denumerate s) (enumerate s))
+    ≡⟨ cong just (map-∘ just (denumerate s) (enumerate s)) ⟩
+  just (map just (map (denumerate s) (enumerate s)))
+    ≡⟨ cong (Maybe.just ∘ map just) (lemma-map-denumerate-enumerate s) ⟩
+  just (map just s) ∎
     where open ≡-Reasoning
           open Get G
           h↦h′ = _<$>_ (flip union (reshape (delete-many (get (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G i)))
-          h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupM)
+          h′↦r = _<$>_ (flip map (enumerate s) ∘ flip lookupM)
 
 
 lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
@@ -212,18 +212,27 @@ sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong
 sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 sequence-cong {S}                                       (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 
-theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
-theorem-2 G j s v u p with (lemma->>=-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G j))) <$> (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v)) p)
+theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (map just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
+theorem-2 G j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G j))) <$> (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v)) p)
 theorem-2 G j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v) ph′)
-theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin
+theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩
   get <$> (just u)
-    ≡⟨ cong (_<$>_ get) (sym p) ⟩
-  get <$> (bff G j s v)
-    ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
-  get <$> h′↦r (h↦h′ h)
+    ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence u)) ⟩
+  get <$> (just (map just u) >>= sequenceV)
+    ≡⟨ cong (_<$>_ get ∘ flip _>>=_ sequenceV) (sym p) ⟩
+  get <$> (bff G j s v >>= sequenceV)
+    ≡⟨ cong (_<$>_ get ∘ flip _>>=_ sequenceV ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
+  get <$> sequenceV (h′↦r (h↦h′ h))
+    ≡⟨ lemma-get-sequenceV G (begin⟨ EqSetoid _ ⟩
+      sequenceV (h′↦r (h↦h′ h))
+        ≡⟨ cong (flip _>>=_ sequenceV ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) (sym ph) ⟩
+      (h′↦r <$> (h↦h′ <$> assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v) >>= sequenceV)
+        ≡⟨ cong (flip _>>=_ sequenceV) p ⟩
+      sequenceV (map just u)
+        ≡⟨ lemma-just-sequence u ⟩
+      just u ∎) ⟩
+  sequenceV (get (h′↦r (h↦h′ h)))
     ≡⟨ refl ⟩
-  get <$> sequenceV (map (flip lookupM (h↦h′ h)) t)
-    ≡⟨ lemma-get-sequenceV G (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) ⟩
   sequenceV (get (map (flip lookupM (h↦h′ h)) t))
     ≡⟨ cong sequenceV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩
   sequenceV (map (flip lookupM (h↦h′ h)) (get t))
@@ -233,11 +242,11 @@ theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin
   sequenceV (map just v)
     ≡⟨ lemma-just-sequence v ⟩
   just v ∎)
-    where open EqR (MaybeSetoid (VecISetoid A.setoid at _))
+    where open SetoidReasoning
           open Get G
           s′   = enumerate s
           g    = fromFunc (denumerate s)
           g′   = delete-many (get s′) g
           t    = enumeratel (Get.|gl₁| G j)
           h↦h′ = flip union (reshape g′ (Get.|gl₁| G j))
-          h′↦r = flip mapMV t ∘ flip lookupM
+          h′↦r = flip map t ∘ flip lookupM
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)