DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Clean up some definitions

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2026-02-16 12:57:59 -08:00
parent 01555ee203
commit 3f923c2d7d
1 changed files with 14 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

23
Lattice/Builder.agda
View File

@@ -608,7 +608,7 @@ record Graph : Set where
} }
module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set FiniteHeightLattice) 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 : Set
Elem = Σ Node λ n → (proj₁ (𝓛 n)) Elem = Σ Node λ n → (proj₁ (𝓛 n))
@@ -630,12 +630,15 @@ record Graph : Set where
_⊔_ : Elem → Elem → Elem _⊔_ : Elem → Elem → Elem
_⊔_ e₁ e₂ _⊔_ e₁ e₂
using n₁ ← proj₁ e₁ using n₂ ← proj₁ e₂ using n₁ ← proj₁ e₁ using n₂ ← proj₁ e₂
with n' ← n₁ ⊔ᵇ 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₂ with n' ≟ n₁ | n' ≟ n₂
... | yes refl | yes refl = (n' , FiniteHeightLattice._⊔_ (proj₂ (𝓛 n')) (proj₂ e₁) (proj₂ e₂)) ... | yes refl | yes refl = FiniteHeightLattice._⊔_ (proj₂ (𝓛 n')) l₁ l₂
... | yes refl | _ = (n' , proj₂ e₁) ... | yes refl | _ = l₁
... | _ | yes refl = (n' , proj₂ e₂) ... | _ | yes refl = l₂
... | no _ | no _ = (n' , FiniteHeightLattice.⊥ (proj₂ (𝓛 n'))) ... | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n'))
⊔-idemp : ∀ e → (e ⊔ e) ≈ e ⊔-idemp : ∀ e → (e ⊔ e) ≈ e
⊔-idemp (n , l) rewrite ⊔ᵇ-idemp n ⊔-idemp (n , l) rewrite ⊔ᵇ-idemp n
@@ -692,9 +695,9 @@ record Graph : Set where
-- A key simplifying property is that notionally, only the -- A key simplifying property is that notionally, only the
-- "elements with the final tag" in the expression matter. All -- "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 ⊥. -- 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))
_⊔ⁿ_ = FiniteHeightLattice._⊔_ (proj₂ (𝓛 n)) _⊔ⁿ_ = FiniteHeightLattice._⊔_ (proj₂ (𝓛 n))
in (eval _⊔_ e) ≈ (n , Maybe.maybe′ (eval _⊔ⁿ_) ⊥ⁿ (filterᵉ n e)) 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₃) ⊔-assoc e₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃)
using exprˡ ← (((` e₁) ⊔ᵉ (` e₂)) ⊔ᵉ (` e₃)) using exprˡ ← (((` e₁) ⊔ᵉ (` e₂)) ⊔ᵉ (` e₃))
using exprʳ ← ((` e₁) ⊔ᵉ ((` e₂) ⊔ᵉ (` e₃))) using exprʳ ← ((` e₁) ⊔ᵉ ((` e₂) ⊔ᵉ (` e₃)))
with nˡ ← eval _⊔ᵇ_ (mapᵉ proj₁ exprˡ) in pˡ with nˡ ← proj₁ (eval _⊔_ exprˡ) in pˡ
with nʳ ← eval _⊔ᵇ_ (mapᵉ proj₁ exprʳ) in pʳ with nʳ ← proj₁ (eval _⊔_ exprʳ) in pʳ
with final₁ ← Expr-final exprˡ with final₁ ← Expr-final exprˡ
with final₂ ← Expr-final exprʳ with final₂ ← Expr-final exprʳ
rewrite pˡ rewrite pʳ rewrite pˡ rewrite pʳ