From 17fc54ef9c4367f89464290675cbcaaef0163301 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 16 Dec 2013 15:47:53 +0100 Subject: [PATCH] get rid of the ListBFF implementation It is unused, has no proofs and starts to get into the way of refactoring the union function type. --- BFF.agda | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/BFF.agda b/BFF.agda index cbb36d3..0cdb231 100644 --- a/BFF.agda +++ b/BFF.agda @@ -17,28 +17,6 @@ open import FinMap import CheckInsert import FreeTheorems -module ListBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where - open FreeTheorems.ListList public using (get-type) - open CheckInsert Carrier deq - - assoc : {n : ℕ} → List (Fin n) → List Carrier → Maybe (FinMapMaybe n Carrier) - assoc [] [] = just empty - assoc (i ∷ is) (b ∷ bs) = (assoc is bs) >>= (checkInsert i b) - assoc _ _ = nothing - - enumerate : (l : List Carrier) → List (Fin (length l)) - enumerate l = toList (tabulate id) - - denumerate : (l : List Carrier) → Fin (length l) → Carrier - denumerate l = flip lookupV (fromList l) - - bff : get-type → (List Carrier → List Carrier → Maybe (List Carrier)) - bff get s v = let s′ = enumerate s - g = fromFunc (denumerate s) - h = assoc (get s′) v - h′ = (flip union g) <\$> h - in (flip map s′ ∘ flip lookup) <\$> h′ - module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where open FreeTheorems.VecVec public using (get-type) open CheckInsert Carrier deq -- 2.20.1