improve readability by introducing EqInst

1 files changed, 9 insertions, 6 deletions

diff --git a/Bidir.agda b/Bidir.agda
index ff20caf..25caa3e 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -44,14 +44,17 @@ module FinMap where
 
 open FinMap
 
-checkInsert : {A : Set} {n : ℕ} → ((x y : A) → Dec (x ≡ y)) → Fin n → A → FinMapMaybe n A → Maybe (FinMapMaybe n A)
+EqInst : Set → Set
+EqInst A = (x y : A) → Dec (x ≡ y)
+
+checkInsert : {A : Set} {n : ℕ} → EqInst A → Fin n → A → FinMapMaybe n A → Maybe (FinMapMaybe n A)
 checkInsert eq i b m with lookupM i m
 checkInsert eq i b m | just c with eq b c
 checkInsert eq i b m | just .b | yes refl = just m
 checkInsert eq i b m | just c  | no ¬p    = nothing
 checkInsert eq i b m | nothing = just (insert i b m)
 
-assoc : {A : Set} {n : ℕ} → ((x y : A) → Dec (x ≡ y)) → List (Fin n) → List A → Maybe (FinMapMaybe n A)
+assoc : {A : Set} {n : ℕ} → EqInst A → List (Fin n) → List A → Maybe (FinMapMaybe n A)
 assoc _  []       []       = just empty
 assoc eq (i ∷ is) (b ∷ bs) = maybe′ (checkInsert eq i b) nothing (assoc eq is bs)
 assoc _  _        _        = nothing
@@ -70,7 +73,7 @@ lemma-insert-same [] () a?
 lemma-insert-same (.(just x) ∷ xs) zero (is-just x) = refl
 lemma-insert-same (x ∷ xs) (suc f′) a? = cong (_∷_ x) (lemma-insert-same xs f′ a?)
 
-lemma-1 : {τ : Set} {n : ℕ} → (eq : (x y : τ) → Dec (x ≡ y)) → (f : Fin n → τ) → (is : List (Fin n)) → assoc eq is (map f is) ≡ just (generate f is)
+lemma-1 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (is : List (Fin n)) → assoc eq is (map f is) ≡ just (generate f is)
 lemma-1 eq f []        = refl
 lemma-1 eq f (i ∷ is′) with assoc eq is′ (map f is′) | generate f is′ | lemma-1 eq f is′
 lemma-1 eq f (i ∷ is′) | nothing | _ | ()
@@ -80,18 +83,18 @@ lemma-1 eq f (i ∷ is′) | just m | .m | refl | just x with eq (f i) x
 lemma-1 eq f (i ∷ is′) | just m | .m | refl | just .(f i) | yes refl = cong just (lemma-insert-same m i {!!})
 lemma-1 eq f (i ∷ is′) | just m | .m | refl | just x | no ¬p = {!!}
 
-lemma-2 : {τ : Set} {n : ℕ} → (eq : (x y : τ) → Dec (x ≡ y)) → (is : List (Fin n)) → (v : List τ) → (h : FinMapMaybe n τ) → just h ≡ assoc eq is v → map (flip lookup h) is ≡ map just v
+lemma-2 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (is : List (Fin n)) → (v : List τ) → (h : FinMapMaybe n τ) → just h ≡ assoc eq is v → map (flip lookup h) is ≡ map just v
 lemma-2 eq is v h p = {!!}
 
 idrange : (n : ℕ) → List (Fin n)
 idrange n = toList (tabulate id)
 
-bff : ({A : Set} → List A → List A) → ({B : Set} → ((x y : B) → Dec (x ≡ y)) → List B → List B → Maybe (List B))
+bff : ({A : Set} → List A → List A) → ({B : Set} → EqInst B → List B → List B → Maybe (List B))
 bff get eq s v = let s′ = idrange (length s)
                      g  = fromFunc (λ f → lookupVec f (fromList s))
                      h  = assoc eq (get s′) v
                      h′ = maybe′ (λ jh → just (union jh g)) nothing h
                  in maybe′ (λ jh′ → just (map (flip lookup jh′) s′)) nothing h′
 
-theorem-1 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : (x y : τ) → Dec (x ≡ y)) → (s : List τ) → bff get eq s (get s) ≡ just s
+theorem-1 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : EqInst τ) → (s : List τ) → bff get eq s (get s) ≡ just s
 theorem-1 get eq s = {!!}