replaced NatMap with FinMap
authorHelmut Grohne <helmut@subdivi.de>
Thu, 19 Jan 2012 11:27:53 +0000 (12:27 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 19 Jan 2012 11:27:53 +0000 (12:27 +0100)
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.

Bidir.agda

index 1c94b8f..9a1dad1 100644 (file)
@@ -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)