author Helmut Grohne Sat, 21 Jan 2012 09:58:14 +0000 (10:58 +0100) committer Helmut Grohne 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 patch | blob | history

@@ -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′