split FinMap to FinMapMaybe
authorHelmut Grohne <helmut@subdivi.de>
Sat, 21 Jan 2012 09:58:14 +0000 (10:58 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Sat, 21 Jan 2012 09:58:14 +0000 (10:58 +0100)
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.

Bidir.agda

index 9a1dad1..84d3b73 100644 (file)
@@ -13,43 +13,45 @@ open import Relation.Binary.Core
 
 module FinMap where
 
 
 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)
 
   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
 
   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
 
 
 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)
 
 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
 
 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)
 
 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)
 
 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
                      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′