From 586d72e18898311d975f5748bca397c403b6a83b Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Fri, 7 Feb 2014 16:15:03 +0100 Subject: allow shape shape updates in bff MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Unlike the original version in VoigtlaenderHMW13, we do not request an sput : ℕ → ℕ → Maybe ℕ function for determining the updated source shape from the original source and updated view shape. Instead we ask the caller directly to provide the result of sput together with a proof that its getlen matches with the provided, updated view. The precondition assoc-enough is not enriched in this way and still requires a non-changing shape. I.e. it says what it said before. --- FinMap.agda | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'FinMap.agda') diff --git a/FinMap.agda b/FinMap.agda index ce76f18..34e2fc1 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -40,6 +40,11 @@ fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs) fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A fromFunc = mapV just ∘ tabulate +reshape : {n : ℕ} {A : Set} → FinMapMaybe n A → (l : ℕ) → FinMapMaybe l A +reshape m zero = [] +reshape [] (suc l) = nothing ∷ (reshape [] l) +reshape (x ∷ xs) (suc l) = x ∷ (reshape xs l) + union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMapMaybe n A → FinMapMaybe n A union m1 m2 = tabulate (λ f → maybe′ just (lookupM f m2) (lookupM f m1)) @@ -109,6 +114,10 @@ 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-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n ≡ m +lemma-reshape-id [] = refl +lemma-reshape-id (x ∷ xs) = cong (_∷_ x) (lemma-reshape-id xs) + 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) -- cgit v1.2.3