From ec2b1ec3ba4bf9a35336b6a43da14f0b141ca760 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 2 Mar 2024 14:54:44 -0800
Subject: [PATCH] Format FiniteMap a little bit better

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/FiniteMap.agda | 36 ++++++++++++++++++++++++++----------
 1 file changed, 26 insertions(+), 10 deletions(-)

diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda
index 5bbb5b5..c3f433b 100644
--- a/Lattice/FiniteMap.agda
+++ b/Lattice/FiniteMap.agda
@@ -1,13 +1,13 @@
 open import Lattice
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
-open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.PropositionalEquality as Eq
+    using (_≡_;refl; sym; trans; cong; subst)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Data.List using (List)
 
 module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
     (_≈₂_ : B → B → Set b)
     (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
-    (≡-dec-A : Decidable (_≡_ {a} {A}))
+    (≡-dec-A : IsDecidable (_≡_ {a} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
 open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
@@ -43,22 +43,36 @@ module _ (ks : List A) where
     ≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂)
 
     _⊔_ : FiniteMap → FiniteMap → FiniteMap
-    _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊔ᵐ m₂ , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
+    _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) =
+        ( m₁ ⊔ᵐ m₂
+        , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks))))
+                km₁≡ks
+        )
 
     _⊓_ : FiniteMap → FiniteMap → FiniteMap
-    _⊓_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊓ᵐ m₂ , trans (sym (⊓-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
+    _⊓_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) =
+        ( m₁ ⊓ᵐ m₂
+        , trans (sym (⊓-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks))))
+                km₁≡ks
+        )
 
     ≈-equiv : IsEquivalence FiniteMap _≈_
     ≈-equiv = record
-        { ≈-refl = λ {(m , _)} → IsEquivalence.≈-refl ≈ᵐ-equiv {m}
-        ; ≈-sym = λ {(m₁ , _)} {(m₂ , _)} → IsEquivalence.≈-sym ≈ᵐ-equiv {m₁} {m₂}
-        ; ≈-trans = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} → IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
+        { ≈-refl =
+            λ {(m , _)} → IsEquivalence.≈-refl ≈ᵐ-equiv {m}
+        ; ≈-sym =
+            λ {(m₁ , _)} {(m₂ , _)} → IsEquivalence.≈-sym ≈ᵐ-equiv {m₁} {m₂}
+        ; ≈-trans =
+            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} →
+                IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
         }
 
     isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
     isUnionSemilattice = record
         { ≈-equiv = ≈-equiv
-        ; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
+        ; ≈-⊔-cong =
+            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
+                ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
         ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
         ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
         ; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
@@ -67,7 +81,9 @@ module _ (ks : List A) where
     isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
     isIntersectSemilattice = record
         { ≈-equiv = ≈-equiv
-        ; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
+        ; ≈-⊔-cong =
+            λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
+                ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
         ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
         ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
         ; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m