diff options
| -rw-r--r-- | Bidir.agda | 42 |
1 files changed, 22 insertions, 20 deletions
@@ -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′ |