From 6e458b738fd75fccac1c605091bfcf7486001533 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sat, 21 Jan 2012 10:58:14 +0100 Subject: [PATCH] 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. --- Bidir.agda | 42 ++++++++++++++++++++++-------------------- 1 file 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′ -- 2.20.1