refactor to get rid of FinMap without Maybe entirely

The union was the only user of this type and now it uses only partial
mappings. So drop remaining uses of FinMap and make everything work with
FinMapMaybe instead.

4 files changed, 28 insertions, 37 deletions

diff --git a/BFF.agda b/BFF.agda
index f7ddd30..896350a 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -35,7 +35,7 @@ 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
                     t′ = get s′
-                    g  = partialize (fromFunc (denumerate s))
+                    g  = fromFunc (denumerate s)
                     g′ = delete-many t′ g
                     h  = assoc t′ v
                     h′ = (flip union g′) <$> h
diff --git a/Bidir.agda b/Bidir.agda
index c74601a..1e65bab 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -113,20 +113,20 @@ theorem-1 get s = begin
     ≡⟨ cong (h′↦r ∘ h↦h′) (lemma-1 (denumerate s) (get (enumerate s))) ⟩
   (h′↦r ∘ h↦h′ ∘ just) (restrict (denumerate s) (toList (get (enumerate s))))
     ≡⟨ refl ⟩
-  (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s)))))
+  (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (fromFunc (denumerate s))))
     ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩
-  (h′↦r ∘ just) (partialize (fromFunc (denumerate s)))
+  (h′↦r ∘ just) (fromFunc (denumerate s))
     ≡⟨ refl ⟩
-  mapMV (flip lookupVec (partialize (fromFunc (denumerate s)))) (enumerate s)
-    ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-partialize-fromFunc (denumerate s)) ⟩
-  mapMV (flip lookupVec (fromFunc (Maybe.just ∘ denumerate s))) (enumerate s)
+  mapMV (flip lookupVec (fromFunc (denumerate s))) (enumerate s)
+    ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-fromFunc-tabulate (denumerate s)) ⟩
+  mapMV (flip lookupVec (tabulate (Maybe.just ∘ denumerate s))) (enumerate s)
     ≡⟨ mapMV-cong (lookup∘tabulate (Maybe.just ∘ 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 ∎
-    where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s)))))
+    where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s))))
           h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec)
 
 
diff --git a/FinMap.agda b/FinMap.agda
index 8cde5a6..c125c47 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -33,17 +33,11 @@ fromAscList : {A : Set} {n : ℕ} → List (Fin n × A) → FinMapMaybe n A
 fromAscList []             = empty
 fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs)
 
-FinMap : ℕ → Set → Set
-FinMap n A = Vec A n
-
-lookup : {A : Set} {n : ℕ} → Fin n → FinMap n A → A
-lookup = lookupVec
-
-fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMap n A
-fromFunc = tabulate
+fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A
+fromFunc = mapV just ∘ tabulate
 
 union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMapMaybe n A → FinMapMaybe n A
-union m1 m2 = fromFunc (λ f → maybe′ just (lookupM f m2) (lookupM f m1))
+union m1 m2 = tabulate (λ f → maybe′ just (lookupM f m2) (lookupM f m1))
 
 restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A
 restrict f is = fromAscList (zip is (map f is))
@@ -54,9 +48,6 @@ delete i m = m [ i ]≔ nothing
 delete-many : {A : Set} {n m : ℕ} → Vec (Fin n) m → FinMapMaybe n A → FinMapMaybe n A
 delete-many = flip (foldr (const _) delete)
 
-partialize : {A : Set} {n : ℕ} → FinMap n A → FinMapMaybe n A
-partialize = mapV just
-
 lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing  → Whatever
 lemma-just≢nothing refl ()
 
@@ -99,9 +90,9 @@ lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g →
 lemma-tabulate-∘ {zero}  {_} {f} {g} f≗g = refl
 lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc))
 
-lemma-partialize-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → partialize (fromFunc f) ≡ fromFunc (just ∘ f)
-lemma-partialize-fromFunc {zero}  f = refl
-lemma-partialize-fromFunc {suc _} f = cong (_∷_ (just (f zero))) (lemma-partialize-fromFunc (f ∘ suc))
+lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (just ∘ f)
+lemma-fromFunc-tabulate {zero}  f = refl
+lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc))
 
 lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f
 lemma-lookupM-delete {i = zero}  {j = zero}  (_ ∷ _)  p with p refl
@@ -110,24 +101,24 @@ lemma-lookupM-delete {i = zero}  {j = suc j} (_ ∷ _)  p = refl
 lemma-lookupM-delete {i = suc i} {j = zero}  (x ∷ xs) p = refl
 lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc)
 
-lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f (toList t)) (delete-many t (partialize (fromFunc f))) ≡ partialize (fromFunc f)
-lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-partialize-fromFunc f))
-    where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (partialize (fromFunc f)))) (lookupM x (restrict f (toList t))) ≡ just (f x)
+lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f (toList t)) (delete-many t (fromFunc f)) ≡ fromFunc f
+lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-fromFunc-tabulate f))
+    where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f (toList t))) ≡ just (f x)
           lemma-inner [] x = begin
-            maybe′ just (lookupM x (partialize (fromFunc f))) (lookupM x empty)
-              ≡⟨ cong (maybe′ just (lookupM x (partialize (fromFunc f)))) (lemma-lookupM-empty x) ⟩
-            lookupM x (partialize (fromFunc f))
-              ≡⟨ cong (lookupM x) (lemma-partialize-fromFunc f) ⟩
-            lookupM x (fromFunc (just ∘ f))
+            maybe′ just (lookupM x (fromFunc f)) (lookupM x empty)
+              ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩
+            lookupM x (fromFunc f)
+              ≡⟨ cong (lookupM x) (lemma-fromFunc-tabulate f) ⟩
+            lookupM x (tabulate (just ∘ f))
               ≡⟨ lookup∘tabulate (just ∘ f) x ⟩
             just (f x) ∎
           lemma-inner (t ∷ ts) x with x ≟ t
-          lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (partialize (fromFunc f))))) (lemma-lookupM-insert x (f x) (restrict f (toList ts)))
+          lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts)))
           lemma-inner (t ∷ ts) x | no ¬p = begin
-            maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f)))) (lookupM x (restrict f (toList (t ∷ ts))))
-              ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f))))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩
-            maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f)))) (lookupM x (restrict f (toList ts)))
-              ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (partialize (fromFunc f))) ¬p) ⟩
-            maybe′ just (lookupM x (delete-many ts (partialize (fromFunc f)))) (lookupM x (restrict f (toList ts)))
+            maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList (t ∷ ts))))
+              ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f)))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩
+            maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList ts)))
+              ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (fromFunc f)) ¬p) ⟩
+            maybe′ just (lookupM x (delete-many ts (fromFunc f))) (lookupM x (restrict f (toList ts)))
               ≡⟨ lemma-inner ts x ⟩
             just (f x) ∎
diff --git a/Precond.agda b/Precond.agda
index 16e452b..40ffd79 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -20,7 +20,7 @@ open import Function using (flip ; _∘_)
 open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
-open import FinMap using (FinMap ; FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty)
+open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty)
 import CheckInsert
 open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF