From ae3e2c28b0a9c4cf07b4397dc1e94c56db506bc5 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 1 Mar 2024 21:58:58 -0800
Subject: [PATCH] Create bundles and add a program to evaluate some code with
 finite maps

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Bundles/FiniteValueMap.agda | 22 +++++++++++++++++
 Lattice/Bundles/IterProd.agda       | 38 +++++++++++++++++++++++++++++
 Main.agda                           | 30 +++++++++++++++++++++++
 3 files changed, 90 insertions(+)
 create mode 100644 Lattice/Bundles/FiniteValueMap.agda
 create mode 100644 Lattice/Bundles/IterProd.agda
 create mode 100644 Main.agda

diff --git a/Lattice/Bundles/FiniteValueMap.agda b/Lattice/Bundles/FiniteValueMap.agda
new file mode 100644
index 0000000..57f62c6
--- /dev/null
+++ b/Lattice/Bundles/FiniteValueMap.agda
@@ -0,0 +1,22 @@
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.Definitions using (Decidable)
+
+module Lattice.Bundles.FiniteValueMap (A B : Set) (≡-dec-A : Decidable (_≡_ {_} {A})) where
+
+open import Lattice
+open import Data.List using (List)
+open import Data.Nat using (ℕ)
+open import Utils using (Unique)
+
+module _ (fhB : FiniteHeightLattice B) where
+    open Lattice.FiniteHeightLattice fhB using () renaming
+        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
+        ; height to height₂
+        ; isLattice to isLattice₂
+        ; fixedHeight to fixedHeight₂
+        )
+
+    module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) where
+        import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM
+
+        finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂
diff --git a/Lattice/Bundles/IterProd.agda b/Lattice/Bundles/IterProd.agda
new file mode 100644
index 0000000..3071d0a
--- /dev/null
+++ b/Lattice/Bundles/IterProd.agda
@@ -0,0 +1,38 @@
+open import Lattice
+
+module Lattice.Bundles.IterProd {a} (A B : Set a) where
+open import Data.Nat using (ℕ)
+
+module _ (lA : Lattice A) (lB : Lattice B) where
+    open Lattice.Lattice lA using () renaming
+        ( _≈_ to _≈₁_; _⊔_ to _⊔₁_; _⊓_ to _⊓₁_
+        ; isLattice to isLattice₁
+        )
+
+    open Lattice.Lattice lB using () renaming
+        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
+        ; isLattice to isLattice₂
+        )
+
+    module _ (k : ℕ) where
+        open import Lattice.IterProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_ isLattice₁ isLattice₂ using (lattice) public
+
+module _ (fhA : FiniteHeightLattice A) (fhB : FiniteHeightLattice B) where
+    open Lattice.FiniteHeightLattice fhA using () renaming
+        ( _≈_ to _≈₁_; _⊔_ to _⊔₁_; _⊓_ to _⊓₁_
+        ; height to height₁
+        ; isLattice to isLattice₁
+        ; fixedHeight to fixedHeight₁
+        )
+
+    open Lattice.FiniteHeightLattice fhB using () renaming
+        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
+        ; height to height₂
+        ; isLattice to isLattice₂
+        ; fixedHeight to fixedHeight₂
+        )
+
+    module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) (k : ℕ) where
+        import Lattice.IterProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_ isLattice₁ isLattice₂ as IP
+
+        finiteHeightLattice = IP.finiteHeightLattice k ≈₁-dec ≈₂-dec height₁ height₂ fixedHeight₁ fixedHeight₂
diff --git a/Main.agda b/Main.agda
new file mode 100644
index 0000000..ca4ecae
--- /dev/null
+++ b/Main.agda
@@ -0,0 +1,30 @@
+module Main where
+
+open import IO
+open import Level
+open import Data.Nat.Show using (show)
+open import Data.List using (List; _∷_; [])
+open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Data.Unit using (⊤; tt) renaming (_≟_ to _≟ᵘ_)
+open import Data.List.Relation.Unary.All using (_∷_; [])
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl; trans)
+open import Relation.Nullary using (¬_)
+
+open import Utils using (Unique; push; empty)
+
+xyzw : List String
+xyzw = "x" ∷ "y" ∷ "z" ∷ "w" ∷ []
+
+xyzw-Unique : Unique xyzw
+xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ []) (push [] empty)))
+
+open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice)
+open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_  as AB renaming (≈-dec to ≈ᵘ-dec)
+open AB.Plain renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
+open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ)
+
+fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt)
+
+fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
+
+main = run {0ℓ} (putStrLn (show (FiniteHeightLattice.height fhlⁱᵖ)))