From 066861f9cdde4ded6c5442508bef1a27576c68d7 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 17 Dec 2013 08:22:12 +0100 Subject: update bff implementation to use delete In the presence of shape-changing updates, bff needs to shrink one of the mappings before unifying them. As long the shape does not change, the union becomes a disjoint union. With this insight we can adapt the proof of theorem-1 using the adapted lemma-disjoint-union. Unfortunately theorem-2 requires more work and assoc-enough becomes non-trivial due to the introduction of mapMV. --- BFF.agda | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'BFF.agda') diff --git a/BFF.agda b/BFF.agda index 0cdb231..f7ddd30 100644 --- a/BFF.agda +++ b/BFF.agda @@ -14,6 +14,7 @@ open import Function using (id ; _∘_ ; flip) open import Relation.Binary.Core using (Decidable ; _≡_) open import FinMap +open import Generic using (mapMV) import CheckInsert import FreeTheorems @@ -33,7 +34,9 @@ module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n)) bff get s v = let s′ = enumerate s - g = fromFunc (denumerate s) - h = assoc (get s′) v - h′ = (flip union g) <$> h - in (flip mapV s′ ∘ flip lookupV) <$> h′ + t′ = get s′ + g = partialize (fromFunc (denumerate s)) + g′ = delete-many t′ g + h = assoc t′ v + h′ = (flip union g′) <$> h + in h′ >>= flip mapMV s′ ∘ flip lookupV -- cgit v1.2.3 From 88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 17 Dec 2013 08:49:24 +0100 Subject: refactor to get rid of FinMap without Maybe entirely The union was the only user of this type and now it uses only partial mappings. So drop remaining uses of FinMap and make everything work with FinMapMaybe instead. --- BFF.agda | 2 +- Bidir.agda | 12 ++++++------ FinMap.agda | 49 ++++++++++++++++++++----------------------------- Precond.agda | 2 +- 4 files changed, 28 insertions(+), 37 deletions(-) (limited to 'BFF.agda') diff --git a/BFF.agda b/BFF.agda index f7ddd30..896350a 100644 --- a/BFF.agda +++ b/BFF.agda @@ -35,7 +35,7 @@ module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n)) bff get s v = let s′ = enumerate s t′ = get s′ - g = partialize (fromFunc (denumerate s)) + g = fromFunc (denumerate s) g′ = delete-many t′ g h = assoc t′ v h′ = (flip union g′) <$> h diff --git a/Bidir.agda b/Bidir.agda index c74601a..1e65bab 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -113,20 +113,20 @@ theorem-1 get s = begin ≡⟨ cong (h′↦r ∘ h↦h′) (lemma-1 (denumerate s) (get (enumerate s))) ⟩ (h′↦r ∘ h↦h′ ∘ just) (restrict (denumerate s) (toList (get (enumerate s)))) ≡⟨ refl ⟩ - (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s))))) + (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩ - (h′↦r ∘ just) (partialize (fromFunc (denumerate s))) + (h′↦r ∘ just) (fromFunc (denumerate s)) ≡⟨ refl ⟩ - mapMV (flip lookupVec (partialize (fromFunc (denumerate s)))) (enumerate s) - ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-partialize-fromFunc (denumerate s)) ⟩ - mapMV (flip lookupVec (fromFunc (Maybe.just ∘ denumerate s))) (enumerate s) + mapMV (flip lookupVec (fromFunc (denumerate s))) (enumerate s) + ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-fromFunc-tabulate (denumerate s)) ⟩ + mapMV (flip lookupVec (tabulate (Maybe.just ∘ denumerate s))) (enumerate s) ≡⟨ mapMV-cong (lookup∘tabulate (Maybe.just ∘ denumerate s)) (enumerate s) ⟩ mapMV (Maybe.just ∘ denumerate s) (enumerate s) ≡⟨ mapMV-purity (denumerate s) (enumerate s) ⟩ just (map (denumerate s) (enumerate s)) ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩ just s ∎ - where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (partialize (fromFunc (denumerate s))))) + where h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec) diff --git a/FinMap.agda b/FinMap.agda index 8cde5a6..c125c47 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -33,17 +33,11 @@ fromAscList : {A : Set} {n : ℕ} → List (Fin n × A) → FinMapMaybe 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 +fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A +fromFunc = mapV just ∘ tabulate union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMapMaybe n A → FinMapMaybe n A -union m1 m2 = fromFunc (λ f → maybe′ just (lookupM f m2) (lookupM f m1)) +union m1 m2 = tabulate (λ f → maybe′ just (lookupM f m2) (lookupM f m1)) restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A restrict f is = fromAscList (zip is (map f is)) @@ -54,9 +48,6 @@ delete i m = m [ i ]≔ nothing delete-many : {A : Set} {n m : ℕ} → Vec (Fin n) m → FinMapMaybe n A → FinMapMaybe n A delete-many = flip (foldr (const _) delete) -partialize : {A : Set} {n : ℕ} → FinMap n A → FinMapMaybe n A -partialize = mapV just - lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing → Whatever lemma-just≢nothing refl () @@ -99,9 +90,9 @@ lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → lemma-tabulate-∘ {zero} {_} {f} {g} f≗g = refl lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc)) -lemma-partialize-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → partialize (fromFunc f) ≡ fromFunc (just ∘ f) -lemma-partialize-fromFunc {zero} f = refl -lemma-partialize-fromFunc {suc _} f = cong (_∷_ (just (f zero))) (lemma-partialize-fromFunc (f ∘ suc)) +lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (just ∘ f) +lemma-fromFunc-tabulate {zero} f = refl +lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc)) lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p with p refl @@ -110,24 +101,24 @@ lemma-lookupM-delete {i = zero} {j = suc j} (_ ∷ _) p = refl lemma-lookupM-delete {i = suc i} {j = zero} (x ∷ xs) p = refl lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc) -lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f (toList t)) (delete-many t (partialize (fromFunc f))) ≡ partialize (fromFunc f) -lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-partialize-fromFunc f)) - where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (partialize (fromFunc f)))) (lookupM x (restrict f (toList t))) ≡ just (f x) +lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f (toList t)) (delete-many t (fromFunc f)) ≡ fromFunc f +lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-fromFunc-tabulate f)) + where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f (toList t))) ≡ just (f x) lemma-inner [] x = begin - maybe′ just (lookupM x (partialize (fromFunc f))) (lookupM x empty) - ≡⟨ cong (maybe′ just (lookupM x (partialize (fromFunc f)))) (lemma-lookupM-empty x) ⟩ - lookupM x (partialize (fromFunc f)) - ≡⟨ cong (lookupM x) (lemma-partialize-fromFunc f) ⟩ - lookupM x (fromFunc (just ∘ f)) + maybe′ just (lookupM x (fromFunc f)) (lookupM x empty) + ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩ + lookupM x (fromFunc f) + ≡⟨ cong (lookupM x) (lemma-fromFunc-tabulate f) ⟩ + lookupM x (tabulate (just ∘ f)) ≡⟨ lookup∘tabulate (just ∘ f) x ⟩ just (f x) ∎ lemma-inner (t ∷ ts) x with x ≟ t - lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (partialize (fromFunc f))))) (lemma-lookupM-insert x (f x) (restrict f (toList ts))) + lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts))) lemma-inner (t ∷ ts) x | no ¬p = begin - maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f)))) (lookupM x (restrict f (toList (t ∷ ts)))) - ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f))))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩ - maybe′ just (lookupM x (delete-many (t ∷ ts) (partialize (fromFunc f)))) (lookupM x (restrict f (toList ts))) - ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (partialize (fromFunc f))) ¬p) ⟩ - maybe′ just (lookupM x (delete-many ts (partialize (fromFunc f)))) (lookupM x (restrict f (toList ts))) + maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList (t ∷ ts)))) + ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f)))) (sym (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p)) ⟩ + maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList ts))) + ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (fromFunc f)) ¬p) ⟩ + maybe′ just (lookupM x (delete-many ts (fromFunc f))) (lookupM x (restrict f (toList ts))) ≡⟨ lemma-inner ts x ⟩ just (f x) ∎ diff --git a/Precond.agda b/Precond.agda index 16e452b..40ffd79 100644 --- a/Precond.agda +++ b/Precond.agda @@ -20,7 +20,7 @@ open import Function using (flip ; _∘_) open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) -open import FinMap using (FinMap ; FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty) +open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty) import CheckInsert open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) import BFF -- cgit v1.2.3