move definition of get-type to BFF and use it everywhere

4 files changed, 19 insertions, 14 deletions

diff --git a/BFF.agda b/BFF.agda
index bde72ee..9d132ff 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -17,6 +17,8 @@ fmap : {A B : Set} → (A → B) → Maybe A → Maybe B
 fmap f = maybe′ (λ a → just (f a)) nothing
 
 module ListBFF where
+  get-type : Set₁
+  get-type = {A : Set} → List A → List A
 
   assoc : {A : Set} {n : ℕ} → EqInst A → List (Fin n) → List A → Maybe (FinMapMaybe n A)
   assoc _  []       []       = just empty
@@ -29,7 +31,7 @@ module ListBFF where
   denumerate : {A : Set} (l : List A) → Fin (length l) → A
   denumerate l = flip lookupV (fromList l)
 
-  bff : ({A : Set} → List A → List A) → ({B : Set} → EqInst B → List B → List B → Maybe (List B))
+  bff : get-type → ({B : Set} → EqInst B → List B → List B → Maybe (List B))
   bff get eq s v = let s′ = enumerate s
                        g  = fromFunc (denumerate s)
                        h  = assoc eq (get s′) v
@@ -37,6 +39,8 @@ module ListBFF where
                    in fmap (flip map s′ ∘ flip lookup) h′
 
 module VecBFF where
+  get-type : (ℕ → ℕ) → Set₁
+  get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
 
   assoc : {A : Set} {n m : ℕ} → EqInst A → Vec (Fin n) m → Vec A m → Maybe (FinMapMaybe n A)
   assoc _  []V       []V       = just empty
@@ -48,7 +52,7 @@ module VecBFF where
   denumerate : {A : Set} {n : ℕ} → Vec A n → Fin n → A
   denumerate = flip lookupV
 
-  bff : {getlen : ℕ → ℕ} → ({A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)) → ({B : Set} {n : ℕ} → EqInst B → Vec B n → Vec B (getlen n) → Maybe (Vec B n))
+  bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({B : Set} {n : ℕ} → EqInst B → Vec B n → Vec B (getlen n) → Maybe (Vec B n))
   bff get eq s v = let s′ = enumerate s
                        g  = fromFunc (denumerate s)
                        h  = assoc eq (get s′) v
@@ -56,6 +60,9 @@ module VecBFF where
                    in fmap (flip mapV s′ ∘ flip lookupV) h′
 
 module VecRevBFF where
+  get-type : (ℕ → ℕ) → Set₁
+  get-type getlen = {A : Set} {n : ℕ} → Vec A (getlen n) → Vec A n
+
   assoc : {A : Set} {m n : ℕ} → EqInst A → Vec (Fin m) n → Vec A n → Maybe (FinMapMaybe m A)
   assoc _  []V       []V       = just empty
   assoc eq (i ∷V is) (b ∷V bs) = (assoc eq is bs) >>= (checkInsert eq i b)
@@ -66,7 +73,7 @@ module VecRevBFF where
   denumerate : {A : Set} {n : ℕ} → Vec A n → Fin n → A
   denumerate = flip lookupV
 
-  bff : {getlen : ℕ → ℕ} → ({A : Set} {n : ℕ} → Vec A (getlen n) → Vec A n) → ({m : ℕ} {B : Set} → EqInst B → Vec B (getlen m) → Vec B m → Maybe (Vec B (getlen m)))
+  bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({m : ℕ} {B : Set} → EqInst B → Vec B (getlen m) → Vec B m → Maybe (Vec B (getlen m)))
   bff get eq s v = let s′ = enumerate s
                        g  = fromFunc (denumerate s)
                        h  = assoc eq (get s′) v
diff --git a/Bidir.agda b/Bidir.agda
index 0720970..a1f958c 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -24,7 +24,7 @@ open import CheckInsert
 
 open import BFF using (_>>=_ ; fmap)
 
-open BFF.VecBFF using (assoc ; enumerate ; denumerate ; bff)
+open BFF.VecBFF using (get-type ; assoc ; enumerate ; denumerate ; bff)
 
 lemma-1 : {τ : Set} {m n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (is : Vec (Fin n) m) → assoc eq is (map f is) ≡ just (restrict f (toList is))
 lemma-1 eq f []        = refl
@@ -151,7 +151,7 @@ lemma-2 eq (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin
   map just (x ∷ xs) ∎
 
 postulate
-  free-theorem-list-list : {β γ : Set} → {getlen : ℕ → ℕ} → (get : {α : Set} {n : ℕ} → Vec α n → Vec α (getlen n)) → (f : β → γ) → {m : ℕ } → (v : Vec β m) → get (map f v) ≡ map f (get v)
+  free-theorem-list-list : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {m : ℕ} → (v : Vec α m) → get (map f v) ≡ map f (get v)
 
 lemma-map-denumerate-enumerate : {m : ℕ} {A : Set} → (as : Vec A m) → map (denumerate as) (enumerate as) ≡ as
 lemma-map-denumerate-enumerate []       = refl
@@ -168,7 +168,7 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin
     ≡⟨ lemma-map-denumerate-enumerate as ⟩
   as ∎)
 
-theorem-1 : {getlen : ℕ → ℕ} → (get : {α : Set} {n : ℕ} → Vec α n → Vec α (getlen n)) → {m : ℕ} {τ : Set} → (eq : EqInst τ) → (s : Vec τ m) → bff get eq s (get s) ≡ just s
+theorem-1 : {getlen : ℕ → ℕ} → (get : get-type getlen) → {m : ℕ} {τ : Set} → (eq : EqInst τ) → (s : Vec τ m) → bff get eq s (get s) ≡ just s
 theorem-1 get eq s = begin
   bff get eq s (get s)
     ≡⟨ cong (bff get eq s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩
@@ -221,7 +221,7 @@ lemma-union-not-used h h' (i ∷ is') p | x , lookupM-i-h≡just-x = begin
     ≡⟨ cong (_∷_ (lookupM i h)) (lemma-union-not-used h h' is' (Data.List.All.tail p)) ⟩
   lookupM i h ∷ map (flip lookupM h) is' ∎
 
-theorem-2 : {getlen : ℕ → ℕ} (get : {α : Set} {n : ℕ} → Vec α n → Vec α (getlen n)) → {τ : Set} {m : ℕ} → (eq : EqInst τ) → (v : Vec τ (getlen m)) → (s u : Vec τ m) → bff get eq s v ≡ just u → get u ≡ v
+theorem-2 : {getlen : ℕ → ℕ} (get : get-type getlen) → {τ : Set} {m : ℕ} → (eq : EqInst τ) → (v : Vec τ (getlen m)) → (s u : Vec τ m) → bff get eq s v ≡ just u → get u ≡ v
 theorem-2 get eq v s u p with lemma-fmap-just (assoc eq (get (enumerate s)) v) (proj₂ (lemma-fmap-just (fmap (flip union (fromFunc (denumerate s))) (assoc eq (get (enumerate s)) v)) p))
 theorem-2 get eq v s u p | h , ph = begin
   get u
diff --git a/LiftGet.agda b/LiftGet.agda
index 7731f6b..4c335c9 100644
--- a/LiftGet.agda
+++ b/LiftGet.agda
@@ -11,11 +11,9 @@ open import Relation.Binary.Core using (_≡_)
 open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
-get-type : Set₁
-get-type = {A : Set} → List A → List A
-
-getV-type : (ℕ → ℕ) → Set₁
-getV-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
+import BFF
+open BFF.ListBFF using (get-type)
+open BFF.VecBFF using () renaming (get-type to getV-type)
 
 getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type
 getVec-to-getList get = toList ∘ get ∘ fromList
diff --git a/Precond.agda b/Precond.agda
index ba8c203..18d6a85 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -17,9 +17,9 @@ open import CheckInsert using (EqInst ; checkInsert ; lemma-checkInsert-new)
 open import BFF using (fmap ; _>>=_)
 open import Bidir using (lemma-∉-lookupM-assoc)
 
-open BFF.VecBFF using (assoc ; enumerate ; denumerate ; bff)
+open BFF.VecBFF using (get-type ; assoc ; enumerate ; denumerate ; bff)
 
-assoc-enough : {getlen : ℕ → ℕ} (get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)) → {B : Set} {m : ℕ} → (eq : EqInst B) → (s : Vec B m) → (v : Vec B (getlen m)) → (h : FinMapMaybe m B) → assoc eq (get (enumerate s)) v ≡ just h → ∃ λ u → bff get eq s v ≡ just u
+assoc-enough : {getlen : ℕ → ℕ} (get : get-type getlen) → {B : Set} {m : ℕ} → (eq : EqInst B) → (s : Vec B m) → (v : Vec B (getlen m)) → (h : FinMapMaybe m B) → assoc eq (get (enumerate s)) v ≡ just h → ∃ λ u → bff get eq s v ≡ just u
 assoc-enough get {B} {m} eq s v h p = map (flip lookup (union h g)) s′ , (begin
   bff get eq s v
     ≡⟨ refl ⟩