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. --- BFF.agda | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'BFF.agda') diff --git a/BFF.agda b/BFF.agda index 1770b5e..56ba359 100644 --- a/BFF.agda +++ b/BFF.agda @@ -30,14 +30,18 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where enumerate : {n : ℕ} → Vec Carrier n → Vec (Fin n) n enumerate _ = tabulate id + enumeratel : (n : ℕ) → Vec (Fin n) n + enumeratel _ = tabulate id + denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier denumerate = flip lookupV - bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n)) - bff G s v = let s′ = enumerate s + bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m) + bff G m s v = let s′ = enumerate s t′ = Get.get G s′ g = fromFunc (denumerate s) g′ = delete-many t′ g - h = assoc t′ v - h′ = (flip union g′) <$> h - in h′ >>= flip mapMV s′ ∘ flip lookupM + t = enumeratel m + h = assoc (Get.get G t) v + h′ = (flip union (reshape g′ m)) <$> h + in h′ >>= flip mapMV t ∘ flip lookupM -- cgit v1.2.3