From 7276a09107901570b11deb6bc18f017a4982a158 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Thu, 19 Jan 2012 12:11:01 +0100
Subject: first attempt to define bff (with holes)

---
 Bidir.agda | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'Bidir.agda')

diff --git a/Bidir.agda b/Bidir.agda
index 507c03f..1c94b8f 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -52,10 +52,6 @@ assoc _  []       []       = just empty
 assoc eq (i ∷ is) (b ∷ bs) = maybe′ (checkInsert eq i b) nothing (assoc eq is bs)
 assoc _  _        _        = nothing
 
---data Equal? where
---  same ...
---  different ...
-
 generate : {A : Set} → (ℕ → A) → List ℕ → NatMap A
 generate f []       = empty
 generate f (n ∷ ns) = insert n (f n) (generate f ns)
@@ -64,3 +60,14 @@ generate f (n ∷ ns) = insert n (f n) (generate f ns)
 lemma-1 : {τ : Set} → (eq : (x y : τ) → Dec (x ≡ y)) → (f : ℕ → τ) → (is : List ℕ) → assoc eq is (map f is) ≡ just (generate f is)
 lemma-1 eq f []        = refl
 lemma-1 eq f (i ∷ is′) = {!!}
+
+idrange : ℕ → List ℕ
+idrange zero = []
+idrange (suc n) = zero ∷ (map suc (idrange n))
+
+bff : ({A : Set} → List A → List A) → ({B : Set} → ((x y : B) → Dec (x ≡ y)) → List B → List B → Maybe (List B))
+bff get eq s v = let s′ = idrange (length s)
+                     g  = fromAscList (zip s′ s)
+                     h  = assoc eq (get s′) v
+                     h′ = maybe′ (λ jh → just (union jh g)) nothing h
+                 in maybe′ (λ jh′ → just (map {!!} s′)) nothing h′
-- 
cgit v1.2.3