From 3f923c2d7d000ca3cbbd4c6bd9aa2389dbe71d4c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 16 Feb 2026 12:57:59 -0800 Subject: [PATCH] Clean up some definitions Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 630d522..7e23e23 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -608,7 +608,7 @@ record Graph : Set where } module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set FiniteHeightLattice) where - open Basic noCycles total-⊔ total-⊓ using () renaming (_⊔_ to _⊔ᵇ_; _⊓_ to _⊓ᵇ_; ⊔-idemp to ⊔ᵇ-idemp; ⊔-comm to ⊔ᵇ-comm; ⊔-assoc to ⊔ᵇ-assoc) + open Basic noCycles total-⊔ total-⊓ using () renaming (_⊔_ to _⊔ᵇ_; _⊓_ to _⊓ᵇ_; ⊔-idemp to ⊔ᵇ-idemp; ⊔-comm to ⊔ᵇ-comm; ⊔-assoc to ⊔ᵇ-assoc; _≼_ to _≼ᵇ_) Elem : Set Elem = Σ Node λ n → (proj₁ (𝓛 n)) @@ -630,12 +630,15 @@ record Graph : Set where _⊔_ : Elem → Elem → Elem _⊔_ e₁ e₂ using n₁ ← proj₁ e₁ using n₂ ← proj₁ e₂ - with n' ← n₁ ⊔ᵇ n₂ - with n' ≟ n₁ | n' ≟ n₂ - ... | yes refl | yes refl = (n' , FiniteHeightLattice._⊔_ (proj₂ (𝓛 n')) (proj₂ e₁) (proj₂ e₂)) - ... | yes refl | _ = (n' , proj₂ e₁) - ... | _ | yes refl = (n' , proj₂ e₂) - ... | no _ | no _ = (n' , FiniteHeightLattice.⊥ (proj₂ (𝓛 n'))) + using n' ← n₁ ⊔ᵇ n₂ = (n' , select n' e₁ e₂) + where + select : ∀ n' e₁ e₂ → proj₁ (𝓛 n') + select n' (n₁ , l₁) (n₂ , l₂) + with n' ≟ n₁ | n' ≟ n₂ + ... | yes refl | yes refl = FiniteHeightLattice._⊔_ (proj₂ (𝓛 n')) l₁ l₂ + ... | yes refl | _ = l₁ + ... | _ | yes refl = l₂ + ... | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n')) ⊔-idemp : ∀ e → (e ⊔ e) ≈ e ⊔-idemp (n , l) rewrite ⊔ᵇ-idemp n @@ -692,9 +695,9 @@ record Graph : Set where -- A key simplifying property is that notionally, only the -- "elements with the final tag" in the expression matter. All - -- others are subsubed. If none of the elments have the final tag, + -- others are subsumed. If none of the elments have the final tag, -- we've found a better supremum and the second element will be ⊥. - Expr-final : ∀ e → let n = eval _⊔ᵇ_ (mapᵉ proj₁ e) + Expr-final : ∀ e → let n = proj₁ (eval _⊔_ e) ⊥ⁿ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n)) _⊔ⁿ_ = FiniteHeightLattice._⊔_ (proj₂ (𝓛 n)) in (eval _⊔_ e) ≈ (n , Maybe.maybe′ (eval _⊔ⁿ_) ⊥ⁿ (filterᵉ n e)) @@ -704,8 +707,8 @@ record Graph : Set where ⊔-assoc e₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃) using exprˡ ← (((` e₁) ⊔ᵉ (` e₂)) ⊔ᵉ (` e₃)) using exprʳ ← ((` e₁) ⊔ᵉ ((` e₂) ⊔ᵉ (` e₃))) - with nˡ ← eval _⊔ᵇ_ (mapᵉ proj₁ exprˡ) in pˡ - with nʳ ← eval _⊔ᵇ_ (mapᵉ proj₁ exprʳ) in pʳ + with nˡ ← proj₁ (eval _⊔_ exprˡ) in pˡ + with nʳ ← proj₁ (eval _⊔_ exprʳ) in pʳ with final₁ ← Expr-final exprˡ with final₂ ← Expr-final exprʳ rewrite pˡ rewrite pʳ