From 6e458b738fd75fccac1c605091bfcf7486001533 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sat, 21 Jan 2012 10:58:14 +0100
Subject: 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(-)

(limited to 'Bidir.agda')

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′
-- 
cgit v1.2.3