author Helmut Grohne Mon, 16 Dec 2013 14:47:53 +0000 (15:47 +0100) committer Helmut Grohne 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 patch | blob | history

index cbb36d3..0cdb231 100644 (file)
--- a/BFF.agda
+++ b/BFF.agda
@@ -17,28 +17,6 @@ open import FinMap
import CheckInsert
import FreeTheorems

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
module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
open FreeTheorems.VecVec public using (get-type)
open CheckInsert Carrier deq