split FinMap to FinMapMaybe

The FinMapMaybe is what FinMap previously was. The FinMap instead now really
maps its whole domain to something. This property is needed to avoid the
usage of fromJust in the definition of bff. With this split applied the
definition of bff is now complete.

1 files changed, 22 insertions, 20 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 9a1dad1..84d3b73 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -13,43 +13,45 @@ open import Relation.Binary.Core
 
 module FinMap where
 
-  FinMap : ℕ → Set → Set
-  FinMap n A = Vec (Maybe A) n
-
-  lookup : {A : Set} {n : ℕ} → Fin n → FinMap n A → Maybe A
-  lookup = lookupVec
+  FinMapMaybe : ℕ → Set → Set
+  FinMapMaybe n A = Vec (Maybe A) n
 
-  notMember : {A : Set} → {n : ℕ} → Fin n → FinMap n A → Bool
-  notMember n = not ∘ maybeToBool ∘ lookup n
+  lookupM : {A : Set} {n : ℕ} → Fin n → FinMapMaybe n A → Maybe A
+  lookupM = lookupVec
 
-  insert : {A : Set} {n : ℕ} → Fin n → A → FinMap n A → FinMap n A
+  insert : {A : Set} {n : ℕ} → Fin n → A → FinMapMaybe n A → FinMapMaybe n A
   insert f a m = m [ f ]≔ (just a)
 
-  empty : {A : Set} {n : ℕ} → FinMap n A
+  empty : {A : Set} {n : ℕ} → FinMapMaybe n A
   empty = replicate nothing
 
-  fromAscList : {A : Set} {n : ℕ} → List (Fin n × A) → FinMap 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
 
-  union : {A : Set} {n : ℕ} → FinMap n A → FinMap n A → FinMap n A
-  union m1 m2 = tabulate (λ f → maybe′ just (lookup f m2) (lookup f m1))
+  union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMap n  A → FinMap n A
+  union m1 m2 = tabulate (λ f → maybe′ id (lookup f m2) (lookupM f m1))
 
 open FinMap
 
-checkInsert : {A : Set} {n : ℕ} → ((x y : A) → Dec (x ≡ y)) → Fin n → A → FinMap n A → Maybe (FinMap n A)
-checkInsert eq i b m with lookup i m
+checkInsert : {A : Set} {n : ℕ} → ((x y : A) → Dec (x ≡ y)) → Fin n → A → FinMapMaybe n A → Maybe (FinMapMaybe n A)
+checkInsert eq i b m with lookupM i m
 checkInsert eq i b m | just c with eq b c
 checkInsert eq i b m | just .b | yes refl = just m
 checkInsert eq i b m | just c  | no ¬p    = nothing
 checkInsert eq i b m | nothing = just (insert i b m)
 
-assoc : {A : Set} {n : ℕ} → ((x y : A) → Dec (x ≡ y)) → List (Fin n) → List A → Maybe (FinMap n A)
+assoc : {A : Set} {n : ℕ} → ((x y : A) → Dec (x ≡ y)) → List (Fin n) → List A → Maybe (FinMapMaybe n A)
 assoc _  []       []       = just empty
 assoc eq (i ∷ is) (b ∷ bs) = maybe′ (checkInsert eq i b) nothing (assoc eq is bs)
 assoc _  _        _        = nothing
 
-generate : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMap n A
+generate : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A
 generate f []       = empty
 generate f (n ∷ ns) = insert n (f n) (generate f ns)
 
@@ -62,7 +64,7 @@ idrange n = toList (tabulate id)
 
 bff : ({A : Set} → List A → List A) → ({B : Set} → ((x y : B) → Dec (x ≡ y)) → List B → List B → Maybe (List B))
 bff get eq s v = let s′ = idrange (length s)
-                     g  = fromAscList (zip s′ s)
+                     g  = fromFunc (λ f → lookupVec f (fromList s))
                      h  = assoc eq (get s′) v
                      h′ = maybe′ (λ jh → just (union jh g)) nothing h
-                 in maybe′ (λ jh′ → just (map {!!} s′)) nothing h′
+                 in maybe′ (λ jh′ → just (map (flip lookup jh′) s′)) nothing h′