replaced NatMap with FinMap

The domain of the map is always limited. So using Fin n as the domain is
natural. Additionally FinMaps are now semantically equal iff their normal form
is the same. That means \== can be used.

diff --git a/Bidir.agda b/Bidir.agda
index 1c94b8f..9a1dad1 100644 (file)
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -2,68 +2,63 @@ module Bidir where
 
 open import Data.Bool hiding (_≟_)
 open import Data.Nat
+open import Data.Fin
 open import Data.Maybe
 open import Data.List hiding (replicate)
+open import Data.Vec hiding (map ; zip) renaming (lookup to lookupVec)
 open import Data.Product hiding (zip ; map)
 open import Function
 open import Relation.Nullary
 open import Relation.Binary.Core
 
-module NatMap where
+module FinMap where
 
-  NatMap : Set → Set
-  NatMap A = List (ℕ × A)
+  FinMap : ℕ → Set → Set
+  FinMap n A = Vec (Maybe A) n
 
-  lookup : {A : Set} → ℕ → NatMap A → Maybe A
-  lookup n []       = nothing
-  lookup n ((m , a) ∷ xs) with n ≟ m
-  lookup n ((.n , a) ∷ xs) | yes refl = just a
-  lookup n ((m , a) ∷ xs)  | no ¬p    = lookup n xs
+  lookup : {A : Set} {n : ℕ} → Fin n → FinMap n A → Maybe A
+  lookup = lookupVec
 
-  notMember : {A : Set} → ℕ → NatMap A → Bool
-  notMember n m = not (maybeToBool (lookup n m))
+  notMember : {A : Set} → {n : ℕ} → Fin n → FinMap n A → Bool
+  notMember n = not ∘ maybeToBool ∘ lookup n
 
-  -- For now we simply prepend the element. This may lead to duplicates.
-  insert : {A : Set} → ℕ → A → NatMap A → NatMap A
-  insert n a m = (n , a) ∷ m
+  insert : {A : Set} {n : ℕ} → Fin n → A → FinMap n A → FinMap n A
+  insert f a m = m [ f ]≔ (just a)
 
-  fromAscList : {A : Set} → List (ℕ × A) → NatMap A
-  fromAscList []       = []
-  fromAscList ((n , a) ∷ xs) = insert n a (fromAscList xs)
+  empty : {A : Set} {n : ℕ} → FinMap n A
+  empty = replicate nothing
 
-  empty : {A : Set} → NatMap A
-  empty = []
+  fromAscList : {A : Set} {n : ℕ} → List (Fin n × A) → FinMap n A
+  fromAscList []       = empty
+  fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs)
 
-  union : {A : Set} → NatMap A → NatMap A → NatMap A
-  union []       m = m
-  union ((n , a) ∷ xs) m = insert n a (union xs m)
+  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))
 
-open NatMap
+open FinMap
 
-checkInsert : {A : Set} → ((x y : A) → Dec (x ≡ y)) → ℕ → A → NatMap A → Maybe (NatMap A)
+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 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} → ((x y : A) → Dec (x ≡ y)) → List ℕ → List A → Maybe (NatMap A)
+assoc : {A : Set} {n : ℕ} → ((x y : A) → Dec (x ≡ y)) → List (Fin n) → List A → Maybe (FinMap 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} → (ℕ → A) → List ℕ → NatMap A
+generate : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMap n A
 generate f []       = empty
 generate f (n ∷ ns) = insert n (f n) (generate f ns)
 
--- this lemma is probably wrong, because two different NatMaps may represent the same semantic value.
-lemma-1 : {τ : Set} → (eq : (x y : τ) → Dec (x ≡ y)) → (f : ℕ → τ) → (is : List ℕ) → assoc eq is (map f is) ≡ just (generate f is)
+lemma-1 : {τ : Set} {n : ℕ} → (eq : (x y : τ) → Dec (x ≡ y)) → (f : Fin n → τ) → (is : List (Fin n)) → assoc eq is (map f is) ≡ just (generate f is)
 lemma-1 eq f []        = refl
 lemma-1 eq f (i ∷ is′) = {!!}
 
-idrange : ℕ → List ℕ
-idrange zero = []
-idrange (suc n) = zero ∷ (map suc (idrange n))
+idrange : (n : ℕ) → List (Fin n)
+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)