From fbbcd7203703b841648ee5c84887e61484cbc0b5 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 2 Mar 2024 15:18:10 -0800
Subject: [PATCH] Some early refactors of FiniteValueMap

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/FiniteValueMap.agda | 40 +++++++++++++++++++++++++++++++------
 1 file changed, 34 insertions(+), 6 deletions(-)

diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda
index a62184e..1e5dfaf 100644
--- a/Lattice/FiniteValueMap.agda
+++ b/Lattice/FiniteValueMap.agda
@@ -4,7 +4,8 @@
 
 open import Lattice
 open import Equivalence
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
+open import Relation.Binary.PropositionalEquality as Eq
+    using (_≡_; refl; sym; trans; cong; subst)
 open import Relation.Binary.Definitions using (Decidable)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Function.Definitions using (Inverseˡ; Inverseʳ)
@@ -27,18 +28,45 @@ open import Data.List.Relation.Unary.All using (All)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Relation.Nullary using (¬_)
 
-open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional; Expr-Provenance; _∩_; _∪_; `_; in₁; in₂; bothᵘ; single; ⊔-combines)
+open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
+    using
+        ( subset-impl
+        ; locate; forget
+        ; _∈_
+        ; Map-functional
+        ; Expr-Provenance
+        ; _∩_; _∪_; `_
+        ; in₁; in₂; bothᵘ; single
+        ; ⊔-combines
+        )
 open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB public
 
 module IterProdIsomorphism where
     open import Data.Unit using (⊤; tt)
-    open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ; ≈-equiv to ≈ᵘ-equiv; fixedHeight to fixedHeightᵘ)
-    open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ as IP using (IterProd)
-    open IsLattice lB using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; FixedHeight to FixedHeight₂)
+    open import Lattice.Unit using ()
+        renaming
+            ( _≈_ to _≈ᵘ_
+            ; _⊔_ to _⊔ᵘ_
+            ; _⊓_ to _⊓ᵘ_
+            ; ≈-dec to ≈ᵘ-dec
+            ; isLattice to isLatticeᵘ
+            ; ≈-equiv to ≈ᵘ-equiv
+            ; fixedHeight to fixedHeightᵘ
+            )
+    open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ
+        as IP
+        using (IterProd)
+    open IsLattice lB using ()
+        renaming
+            ( ≈-trans to ≈₂-trans
+            ; ≈-sym to ≈₂-sym
+            ; FixedHeight to FixedHeight₂
+            )
 
     from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks)
     from {[]} (([] , _) , _) = tt
-    from {k ∷ ks'} (((k' , v) ∷ fm' , push _ uks') , refl) = (v , from ((fm' , uks'), refl))
+    from {k ∷ ks'} (((k' , v) ∷ fm' , push _ uks') , refl) =
+        (v , from ((fm' , uks'), refl))
 
     to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks
     to {[]} _ ⊤ = (([] , empty) , refl)