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.
- 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))
-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)
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′