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

Use a convenience function for creating the "greatest path"

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-25 15:21:43 +02:00
parent 36ae125e1e
commit 7b2114cd0f
1 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
Lattice/Builder.agda
View File

@ -304,6 +304,12 @@ pathJoin' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₁ lv
pathJoin' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₁ lv₂)
pathJoin' (add-via-greatest l ls {{greatest}}) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathJoin' ls p₁ p₂) -- not our job to provide the least element here. If there was a "greatest" there, recursion would've found it (?)
greatestPath : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls)) → Path' Ls
greatestPath Ls greatest
with head Ls | greatest | valueAtHead Ls
... | _ | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
= vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest))
pathMeet' : ∀ {a} (Ls : Layers a) (p₁ p₂ : Path' Ls) → Maybe (Path' Ls)
pathMeet' (single l) lv₁ lv₂ = lvMeet (toList l) lv₁ lv₂
pathMeet' (add-via-least l ls) (inj₁ lv₁) (inj₁ lv₂) = Maybe.map inj₁ (lvMeet (toList l) lv₁ lv₂)
@ -313,10 +319,7 @@ pathMeet' (add-via-least l ls) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (p
pathMeet' (add-via-greatest l ls {{greatest}}) (inj₁ lv₁) (inj₁ lv₂)
with lvMeet (toList l) lv₁ lv₂
... | just lv = just (inj₁ lv)
... | nothing
with head ls | greatest | valueAtHead ls
... | _ | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
= just (inj₂ (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest))))
... | nothing = just (inj₂ (greatestPath ls greatest))
pathMeet' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₂ p₂)
pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₂ p₁)
pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathMeet' ls p₁ p₂)