[WIP] Demonstrate partial lattice construction

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice/Builder.agda

@@ -148,6 +148,10 @@ record IsPartialSemilattice {a} {A : Set a}
                 with a₁ ⊔? x | refl⇒a₁⊔?x=nothing refl | x-absorbʳ a₁
         ...       | nothing | refl | ()
 
+
+PartialAbsorb : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗₁_ : A → A → Maybe A) (_⊗₂_ : A → A → Maybe A) → Set a
+PartialAbsorb {a} {A} _≈_ _⊗₁_ _⊗₂_ = ∀ (x y : A) →  maybe (λ x⊗₂y → lift-≈ _≈_ (x ⊗₁ x⊗₂y) (just x)) (Trivial _) (x ⊗₂ y)
+
 record IsPartialLattice {a} {A : Set a}
     (_≈_ : A → A → Set a)
     (_⊔?_ : A → A → Maybe A)
@@ -157,8 +161,8 @@ record IsPartialLattice {a} {A : Set a}
         {{partialJoinSemilattice}} : IsPartialSemilattice _≈_ _⊔?_
         {{partialMeetSemilattice}} : IsPartialSemilattice _≈_ _⊓?_
 
-        absorb-⊔-⊓ : (x y : A) →  maybe (λ x⊓y → lift-≈ _≈_ (x ⊔? x⊓y) (just x)) (Trivial _) (x ⊓? y)
-        absorb-⊓-⊔ : (x y : A) →  maybe (λ x⊔y → lift-≈ _≈_ (x ⊓? x⊔y) (just x)) (Trivial _) (x ⊔? y)
+        absorb-⊔-⊓ : PartialAbsorb _≈_ _⊔?_ _⊓?_
+        absorb-⊓-⊔ : PartialAbsorb _≈_ _⊓?_ _⊔?_
 
     open IsPartialSemilattice partialJoinSemilattice
         renaming (HasAbsorbingElement to HasGreatestElement)
@@ -213,6 +217,7 @@ record PartialLattice {a} (A : Set a) : Set (lsuc a) where
     least-⊔-identˡ le x = ≈?-trans (⊔-comm (HasLeastElement.x le) x) (least-⊔-identʳ le x)
 
 record PartialLatticeType (a : Level) : Set (lsuc a) where
+    constructor mkPartialLatticeType
     field
         EltType : Set a
         {{partialLattice}} : PartialLattice EltType
@@ -508,6 +513,24 @@ eval _⊔?_ (e₁ ∨ e₂) = (eval _⊔?_ e₁) >>= (λ v₁ →  (eval _⊔?_
 PartiallySubHomo : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (_⊕_ : A → A → Maybe A) (_⊗_ : B → B → Maybe B) → Set (a ⊔ℓ b)
 PartiallySubHomo {A = A} f _⊕_ _⊗_ = ∀ (a₁ a₂ : A) →  (f a₁ ⊗ f a₂) ≡ Maybe.map f (a₁ ⊕ a₂)
 
+PartialAbsorb-map : ∀ {a b} {A : Set a} {B : Set b}
+                      (f : A → B)
+                      (_≈ᵃ_ : A → A → Set a) (_≈ᵇ_ : B → B → Set b) →
+                      (∀ a₁ a₂ → a₁ ≈ᵃ a₂ → f a₁ ≈ᵇ f a₂) →
+                    ∀ (_⊕₁_ : A → A → Maybe A) (_⊕₂_ : A → A → Maybe A)
+                      (_⊗₁_ : B → B → Maybe B) (_⊗₂_ : B → B → Maybe B) →
+                      PartiallySubHomo f _⊕₁_ _⊗₁_ →
+                      PartiallySubHomo f _⊕₂_ _⊗₂_ →
+                      PartialAbsorb _≈ᵃ_ _⊕₁_ _⊕₂_ →
+                      ∀ (x y : A) →  maybe (λ x⊗₂y → lift-≈ _≈ᵇ_ (f x ⊗₁ x⊗₂y) (just (f x))) (Trivial _) (f x ⊗₂ f y)
+PartialAbsorb-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ⇒≈ᵇ _⊕₁_ _⊕₂_ _⊗₁_ _⊗₂_ psh₁ psh₂ absorbᵃ x y
+    with x ⊕₂ y | f x ⊗₂ f y | psh₂ x y | absorbᵃ x y
+...   | nothing | nothing | refl | _ = mkTrivial
+...   | just x⊕₂y | just fx⊗₂fy | refl | x⊕₁xy≈?x
+        with x ⊕₁ x⊕₂y | f x ⊗₁ (f x⊕₂y) | psh₁ x x⊕₂y | x⊕₁xy≈?x
+...       |  just x⊕₁xy | just fx⊗₁fx⊕₂y | refl | ≈-just x⊕₁xy≈x = ≈-just (≈ᵃ⇒≈ᵇ _ _ x⊕₁xy≈x)
+
+
 -- this evaluation property, which depends on PartiallySubHomo, effectively makes
 -- it easier to talk about compound operations and the preservation of their
 -- structure when _⊗_ is PartiallySubHomo.
@@ -609,6 +632,30 @@ lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-co
 lvMeet-idemp : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvMeet L)
 lvMeet-idemp = lvCombine-idemp PartialLatticeType._⊓?_ PartialLatticeType.⊓-idemp
 
+lvCombine-absorb : ∀ {a} (f₁ f₂ : CombineForPLT a) →
+                   (∀ plt →  PartialAbsorb (PartialLatticeType._≈_ plt) (f₁ plt) (f₂ plt)) →
+                   ∀ (L : List (PartialLatticeType a)) →
+                   PartialAbsorb (eqL L) (lvCombine f₁ L) (lvCombine f₂ L)
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ [] ()
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₁ v₁) (inj₁ v₂)
+    = PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (f₁ plt) (f₂ plt)
+                                 (lvCombine f₁ (plt ∷ plts)) (lvCombine f₂ (plt ∷ plts))
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (absorb-f₁-f₂ plt) v₁ v₂
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = mkTrivial
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = mkTrivial
+lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂)
+    = PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (lvCombine f₁ plts) (lvCombine f₂ plts)
+                                 (lvCombine f₁ (plt ∷ plts)) (lvCombine f₂ (plt ∷ plts))
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (lvCombine-absorb f₁ f₂  absorb-f₁-f₂ plts) lv₁ lv₂
+
+absorb-lvJoin-lvMeet : ∀ {a} (L : List (PartialLatticeType a)) → PartialAbsorb (eqL L) (lvJoin L) (lvMeet L)
+absorb-lvJoin-lvMeet = lvCombine-absorb PartialLatticeType._⊔?_ PartialLatticeType._⊓?_ PartialLatticeType.absorb-⊔-⊓
+
+absorb-lvMeet-lvJoin : ∀ {a} (L : List (PartialLatticeType a)) → PartialAbsorb (eqL L) (lvMeet L) (lvJoin L)
+absorb-lvMeet-lvJoin = lvCombine-absorb PartialLatticeType._⊓?_ PartialLatticeType._⊔?_ PartialLatticeType.absorb-⊓-⊔
+
 lvJoin-greatest-total : ∀ {a} {L : Layer a} →  (lv₁ lv₂ : LayerValue L) →  LayerGreatest L →  lvJoin (toList L) lv₁ lv₂ ≡ nothing → ⊥
 lvJoin-greatest-total {L = plt ∷⁺ []} (inj₁ v₁) (inj₁ v₂) (MkLayerGreatest {{hasGreatest = hasGreatest}}) v₁⊔v₂≡nothing
     with IsPartialLattice.HasGreatestElement.not-partial (PartialLatticeType.isPartialLattice plt) hasGreatest v₁ v₂
@@ -946,6 +993,73 @@ pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₁ lv)
 ...   | just lv⊔lv | ≈-just lv⊔lv≈lv = ≈-just lv⊔lv≈lv
 pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-idemp {Ls = ls} p)
 
+absorb-pathJoin'-pathMeet' : ∀ {a} {Ls : Layers a} → PartialAbsorb (eqPath' Ls) (pathJoin' Ls) (pathMeet' Ls)
+absorb-pathJoin'-pathMeet' {Ls = single l} lv₁ lv₂ = absorb-lvJoin-lvMeet (toList l) lv₁ lv₂
+absorb-pathJoin'-pathMeet' {Ls = Ls@(add-via-least l ls)} (inj₁ lv₁) (inj₁ lv₂)
+    = PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (lvJoin (toList l)) (lvMeet (toList l))
+                                 (pathJoin' Ls) (pathMeet' Ls)
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (absorb-lvJoin-lvMeet (toList l)) lv₁ lv₂
+absorb-pathJoin'-pathMeet' {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₁ lv₂)
+    = pathJoin'-idemp {Ls = add-via-least l {{least}} ls} (inj₂ p₁)
+absorb-pathJoin'-pathMeet' {Ls = add-via-least l ls} (inj₁ lv₁) (inj₂ p₂)
+    = ≈-just (eqLv-refl l lv₁)
+absorb-pathJoin'-pathMeet' {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂)
+    with pathMeet' ls p₁ p₂ | absorb-pathJoin'-pathMeet' {Ls = ls} p₁ p₂
+...   | nothing | _ = mkTrivial
+...   | just p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+        with pathJoin' ls p₁ p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+...       | just _ | ≈-just p₁⊔p₁p₂≈p₁ = ≈-just p₁⊔p₁p₂≈p₁
+absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂)
+    with lvMeet (toList l) lv₁ lv₂ | absorb-lvJoin-lvMeet (toList l) lv₁ lv₂
+...   | nothing | _ = ≈-just (eqLv-refl l lv₁)
+...   | just lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+        with lvJoin (toList l) lv₁ lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+...       | just _ | ≈-just lv₁⊔lv₁lv₂≈lv₁ = ≈-just lv₁⊔lv₁lv₂≈lv₁
+absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls {{greatest}} } (inj₂ p₁) (inj₁ lv₂)
+    = pathJoin'-idemp {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁)
+absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂)
+    = ≈-just (eqLv-refl l lv₁)
+absorb-pathJoin'-pathMeet' {Ls = Ls@(add-via-greatest l ls)} (inj₂ p₁) (inj₂ p₂)
+    = PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (pathJoin' ls) (pathMeet' ls)
+                                 (pathJoin' Ls) (pathMeet' Ls)
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (absorb-pathJoin'-pathMeet' {Ls = ls}) p₁ p₂
+
+absorb-pathMeet'-pathJoin' : ∀ {a} {Ls : Layers a} → PartialAbsorb (eqPath' Ls) (pathMeet' Ls) (pathJoin' Ls)
+absorb-pathMeet'-pathJoin' {Ls = single l} lv₁ lv₂ = absorb-lvMeet-lvJoin (toList l) lv₁ lv₂
+absorb-pathMeet'-pathJoin' {Ls = Ls@(add-via-least l ls)} (inj₁ lv₁) (inj₁ lv₂)
+    = PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (lvMeet (toList l)) (lvJoin (toList l))
+                                 (pathMeet' Ls) (pathJoin' Ls)
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (absorb-lvMeet-lvJoin (toList l)) lv₁ lv₂
+absorb-pathMeet'-pathJoin' {Ls = add-via-least l ls} (inj₂ p₁) (inj₁ lv₂)
+    = ≈-just (eqPath'-refl ls p₁)
+absorb-pathMeet'-pathJoin' {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂)
+    = pathMeet'-idemp {Ls = add-via-least l {{least}} ls} (inj₁ lv₁)
+absorb-pathMeet'-pathJoin' {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂)
+    with pathJoin' ls p₁ p₂ | absorb-pathMeet'-pathJoin' {Ls = ls} p₁ p₂
+...   | nothing | _ = ≈-just (eqPath'-refl ls p₁)
+...   | just p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+        with pathMeet' ls p₁ p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
+...       | just _ | ≈-just p₁⊔p₁p₂≈p₁ = ≈-just p₁⊔p₁p₂≈p₁
+absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂)
+    with lvJoin (toList l) lv₁ lv₂ | absorb-lvMeet-lvJoin (toList l) lv₁ lv₂
+...   | nothing | _ = mkTrivial
+...   | just lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+        with lvMeet (toList l) lv₁ lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
+...       | just _ | ≈-just lv₁⊔lv₁lv₂≈lv₁ = ≈-just lv₁⊔lv₁lv₂≈lv₁
+absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂)
+    = ≈-just (eqPath'-refl ls p₁)
+absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₂ p₂)
+    = pathMeet'-idemp {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁)
+absorb-pathMeet'-pathJoin' {Ls = Ls@(add-via-greatest l ls)} (inj₂ p₁) (inj₂ p₂)
+    = PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (pathMeet' ls) (pathJoin' ls)
+                                 (pathMeet' Ls) (pathJoin' Ls)
+                                 (λ _ _ → refl) (λ _ _ → refl)
+                                 (absorb-pathMeet'-pathJoin' {Ls = ls}) p₁ p₂
+
+
 record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
     constructor mk-≈
     field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)
@@ -1026,6 +1140,59 @@ instance
             ; ≈-⊔-cong = ≈-⊓̇-cong {Ls = Ls}
             }
 
+⊔̇-⊓̇-absorb : ∀ {a} {Ls : Layers a} → PartialAbsorb (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+⊔̇-⊓̇-absorb {Ls = Ls} (MkPath p₁) (MkPath p₂)
+    = PartialAbsorb-map MkPath _ _ (λ _ _ → mk-≈) (pathJoin' Ls) (pathMeet' Ls)
+                                   (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+                                   (λ _ _ → refl) (λ _ _ → refl)
+                                   (absorb-pathJoin'-pathMeet' {Ls = Ls}) p₁ p₂
+
+⊓̇-⊔̇-absorb : ∀ {a} {Ls : Layers a} → PartialAbsorb (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+⊓̇-⊔̇-absorb {Ls = Ls} (MkPath p₁) (MkPath p₂)
+    = PartialAbsorb-map MkPath _ _ (λ _ _ → mk-≈) (pathMeet' Ls) (pathJoin' Ls)
+                                   (_⊓̇_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+                                   (λ _ _ → refl) (λ _ _ → refl)
+                                   (absorb-pathMeet'-pathJoin' {Ls = Ls}) p₁ p₂
+
+instance
+    Path-IsPartialLattice : ∀ {a} {Ls : Layers a} → IsPartialLattice (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+    Path-IsPartialLattice {Ls = Ls} =
+        record
+            { absorb-⊔-⊓ = ⊔̇-⊓̇-absorb {Ls = Ls}
+            ; absorb-⊓-⊔ = ⊓̇-⊔̇-absorb {Ls = Ls}
+            }
+
+instance
+    -- IsLattice-IsPartialLattice : ∀ {a} {A : Set a}
+    --     {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A}
+    --     {{lA : IsLattice A _≈_ _⊔_ _⊓_}} → IsPartialLattice _≈_ _⊔_ _⊓_
+    -- IsLattice-IsPartialLattice = {!!}
+
+    Lattice-PartialLattice : ∀ {a} {A : Set a}
+        {{lA : Lattice A }} →  PartialLattice A
+    Lattice-PartialLattice = {!!}
+
+    Lattice-Least : ∀ {a} {A : Set a}
+        {{lA : Lattice A }} → PartialLattice.HasLeastElement (Lattice-PartialLattice {{lA = lA}})
+    Lattice-Least = {!!}
+
+open import Lattice.Unit
+
+ThreeElements : Set
+ThreeElements = Path (add-via-least ((mkPartialLatticeType ⊤) ∷⁺ []) (add-via-least ((mkPartialLatticeType ⊤) ∷⁺ []) (single ((mkPartialLatticeType ⊤) ∷⁺ []))))
+
+e₁ : ThreeElements
+e₁ = MkPath (inj₁ (inj₁ tt))
+
+e₂ : ThreeElements
+e₂ = MkPath (inj₂ (inj₁ (inj₁ tt)))
+
+e₃ : ThreeElements
+e₃ = MkPath (inj₂ (inj₂ (inj₁ tt)))
+
+ex1 : e₁ ⊔̇ e₂ ≡ just e₁
+ex1 = refl
+
 -- data ListValue {a : Level} : List (PartialLatticeType a) → Set (lsuc a) where
 --     here : ∀ {plt : PartialLatticeType a} {pltl : List (PartialLatticeType a)}
 --              (v : PartialLatticeType.EltType plt) → ListValue (plt ∷ pltl)