author Helmut Grohne Thu, 19 Jan 2012 11:27:53 +0000 (12:27 +0100) committer Helmut Grohne 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 patch | blob | history

@@ -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)