From 7b2114cd0fcb31ce909fb797bfc76eb2f06b1392 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 25 Jul 2025 15:21:43 +0200 Subject: [PATCH] Use a convenience function for creating the "greatest path" Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 62ebae7..d17c730 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -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₂)