Factor out comparison

1 files changed, 13 insertions, 13 deletions

diff --git a/FinMerge.agda b/FinMerge.agda
index 51e7a67..c62fe14 100644
--- a/FinMerge.agda
+++ b/FinMerge.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --without-K --safe #-}
 module FinMerge where
 
 open import Data.Empty using (⊥-elim)
@@ -6,7 +7,7 @@ open import Data.Fin.Properties using (¬Fin0)
 open import Data.Nat using (ℕ; _+_; _≤_; _<_ ; z<s; s≤s)
 open import Data.Nat.Properties using (≤-trans)
 open import Data.Sum.Base using (_⊎_)
-open import Data.Product using (_×_; _,_; Σ-syntax; map₂)
+open import Data.Product using (_×_; _,_; Σ-syntax; map₂; proj₂)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
 open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
 open import Function using (id ; _∘_ ; _$_)
@@ -30,16 +31,19 @@ pluck (_≤_.s≤s m) (Fin.suc x) = Data.Maybe.Base.map Fin.suc (pluck m x)
 merge : {i j : ℕ} → i < j ≤ n → Fin (ℕ.suc n) → Fin n
 merge (lt , le) x = fromMaybe (fromℕ< (≤-trans lt le)) (pluck le x)
 
+glue-once : Fin (ℕ.suc n) → Fin (ℕ.suc n) → Σ[ x ∈ ℕ ] (Fin (ℕ.suc n) → Fin x)
+glue-once {n} f0 g0 with compare f0 g0
+... | less (f0<g0 , s≤s g0≤n) = n , merge (f0<g0 , g0≤n)
+... | equal f0≡g0 = ℕ.suc n , id
+... | greater (g0<f0 , s≤s f0≤n) = n , merge (g0<f0 , f0≤n)
+
 -- Glue together the image of two finite-set functions
 glue : (Fin m → Fin n) → (Fin m → Fin n) → Σ[ x ∈ ℕ ] (Fin n → Fin x)
 glue {ℕ.zero} {n} _ _ = n , id
 glue {ℕ.suc _} {ℕ.zero} f _ = ⊥-elim (¬Fin0 (f (# 0)))
 glue {ℕ.suc _} {ℕ.suc _} f g with glue (f ∘ Fin.suc) (g ∘ Fin.suc)
 ... | ℕ.zero , h = ⊥-elim (¬Fin0 (h (# 0)))
-... | ℕ.suc x , h with compare (h (f (# 0))) (h (g (# 0)))
-...     | less (f0<g0 , s≤s g0<n) = x , merge (f0<g0 , g0<n) ∘ h
-...     | equal f0≡g0 = ℕ.suc x , h
-...     | greater (g0<f0 , s≤s f0<n) = x , merge (g0<f0 , f0<n) ∘ h
+... | ℕ.suc _ , h = map₂ (_∘ h) (glue-once (h (f (# 0))) (h (g (# 0))))
 
 -- Glue together the image of two finite-set functions, iterative
 glue-iter
@@ -49,11 +53,7 @@ glue-iter
     → (Fin n → Fin y)
     → Σ[ x ∈ ℕ ] (Fin n → Fin x)
 glue-iter {ℕ.zero} {n} {y} f g h = y , h
-glue-iter {ℕ.suc m} {n} {y} f g h with compare (f (# 0)) (g (# 0))
-... | less (f0<g0 , s≤s g0≤n) =
-        let p = merge (f0<g0 , g0≤n) in
-        glue-iter (p ∘ f ∘ Fin.suc) (p ∘ g ∘ Fin.suc) (p ∘ h)
-... | equal _ = glue-iter (f ∘ Fin.suc) (g ∘ Fin.suc) h
-... | greater (g0<f0 , s≤s f0≤n) =
-        let p = merge (g0<f0 , f0≤n) in
-        glue-iter (p ∘ f ∘ Fin.suc) (p ∘ g ∘ Fin.suc) (p ∘ h)
+glue-iter {ℕ.suc m} {n} {ℕ.zero} f g h = ⊥-elim (¬Fin0 (f (# 0)))
+glue-iter {ℕ.suc m} {n} {ℕ.suc y} f g h =
+    let p = proj₂ (glue-once (f (# 0)) (g (# 0))) in
+    glue-iter (p ∘ f ∘ Fin.suc) (p ∘ g ∘ Fin.suc) (p ∘ h)