From 84231ed91ae814d5a256e5fa24810c886ae31369 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 5 Jun 2012 18:03:51 +0200 Subject: make the Vec bff more similar to the List version --- BFF.agda | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/BFF.agda b/BFF.agda index 0cdb5d1..fe89742 100644 --- a/BFF.agda +++ b/BFF.agda @@ -41,12 +41,15 @@ module VecBFF where assoc _ []V []V = just empty assoc eq (i ∷V is) (b ∷V bs) = (assoc eq is bs) >>= (checkInsert eq i b) + enumerate : {A : Set} {n : ℕ} → Vec A n → Vec (Fin n) n + enumerate _ = tabulate id + denumerate : {A : Set} {n : ℕ} → Vec A n → Fin n → A denumerate = flip lookupV - bff : (getlen : ℕ → ℕ) → ({A : Set} {n : ℕ} → Vec A (getlen n) → Vec A n) → ({m : ℕ} {B : Set} → EqInst B → Vec B (getlen m) → Vec B m → Maybe (Vec B (getlen m))) - bff getlen get {m} eq s v = let s′ = allFin (getlen m) - g = fromFunc (denumerate s) - h = assoc eq (get s′) v - h′ = fmap (flip union g) h - in fmap (flip mapV s′ ∘ (flip lookup)) h′ + bff : {getlen : ℕ → ℕ} → ({A : Set} {n : ℕ} → Vec A (getlen n) → Vec A n) → ({m : ℕ} {B : Set} → EqInst B → Vec B (getlen m) → Vec B m → Maybe (Vec B (getlen m))) + bff get eq s v = let s′ = enumerate s + g = fromFunc (denumerate s) + h = assoc eq (get s′) v + h′ = fmap (flip union g) h + in fmap (flip mapV s′ ∘ (flip lookup)) h′ -- cgit v1.2.3