get rid of the ListBFF implementation
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 16 Dec 2013 14:47:53 +0000 (15:47 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 16 Dec 2013 14:47:53 +0000 (15:47 +0100)
It is unused, has no proofs and starts to get into the way of
refactoring the union function type.

BFF.agda

index cbb36d3..0cdb231 100644 (file)
--- 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