diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 7e23e23..dfdbaa5 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -608,7 +608,9 @@ 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; _≼_ to _≼ᵇ_) + open Basic noCycles total-⊔ total-⊓ using () renaming (_⊔_ to _⊔ᵇ_; _⊓_ to _⊓ᵇ_; ⊔-idemp to ⊔ᵇ-idemp; ⊔-comm to ⊔ᵇ-comm; ⊔-assoc to ⊔ᵇ-assoc; _≼_ to _≼ᵇ_; isJoinSemilattice to isJoinSemilatticeᵇ; isMeetSemilattice to isMeetSemilatticeᵇ; isLattice to isLatticeᵇ) + + open IsLattice isLatticeᵇ using () renaming (≈-⊔-cong to ≡-⊔ᵇ-cong) Elem : Set Elem = Σ Node λ n → (proj₁ (𝓛 n)) @@ -657,60 +659,85 @@ record Graph : Set where ... | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n))) private - data Expr (A : Set) : Set where - `_ : A → Expr A - _⊔ᵉ_ : Expr A → Expr A → Expr A + scary : ∀ (n₁ n₂ : Node) → (p : n₁ ≡ n₂) → (n₁ ≟ n₂) ≡ subst (λ n → Dec (n₁ ≡ n)) p (yes refl) + scary n₁ n₂ refl with n₁ ≟ n₂ + ... | yes refl = refl + ... | no n₁≢n₂ = ⊥-elim (n₁≢n₂ refl) - eval : ∀ {A} → (A → A → A) → Expr A → A - eval _ (` v) = v - eval f (e₁ ⊔ᵉ e₂) = f (eval f e₁) (eval f e₂) + payloadˡ : ∀ e₁ e₂ e₃ → let n = proj₁ ((e₁ ⊔ e₂) ⊔ e₃) + in proj₁ (𝓛 n) + payloadˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ + using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (proj₂ (𝓛 n)) + with n ≟ n₁ | n ≟ n₂ | n ≟ n₃ + ... | yes refl | yes refl | yes refl = (l₁ ⊔ⁿ l₂) ⊔ⁿ l₃ + ... | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂ + ... | yes refl | no _ | yes refl = l₁ ⊔ⁿ l₃ + ... | yes refl | no _ | no _ = l₁ + ... | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃ + ... | no _ | yes refl | no _ = l₂ + ... | no _ | no _ | yes refl = l₃ + ... | no _ | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n)) - mapᵉ : ∀ {A B} → (A → B) → Expr A → Expr B - mapᵉ f (` a) = ` (f a) - mapᵉ f (e₁ ⊔ᵉ e₂) = (mapᵉ f e₁) ⊔ᵉ (mapᵉ f e₂) + payloadʳ : ∀ e₁ e₂ e₃ → let n = proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) + in proj₁ (𝓛 n) + payloadʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + with n ← n₁ ⊔ᵇ (n₂ ⊔ᵇ n₃) + using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (proj₂ (𝓛 n)) + with n ≟ n₁ | n ≟ n₂ | n ≟ n₃ + ... | yes refl | yes refl | yes refl = l₁ ⊔ⁿ (l₂ ⊔ⁿ l₃) + ... | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂ + ... | yes refl | no _ | yes refl = l₁ ⊔ⁿ l₃ + ... | yes refl | no _ | no _ = l₁ + ... | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃ + ... | no _ | yes refl | no _ = l₂ + ... | no _ | no _ | yes refl = l₃ + ... | no _ | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n)) - filterᵉ : ∀ (n : Node) → Expr Elem → Maybe (Expr (proj₁ (𝓛 n))) - filterᵉ n (` (n' , l')) - with n ≟ n' - ... | yes refl = just (` l') - ... | no _ = nothing - filterᵉ n (e₁ ⊔ᵉ e₂) - with filterᵉ n e₁ | filterᵉ n e₂ - ... | just e₁' | just e₂' = just (e₁' ⊔ᵉ e₂') - ... | just e₁' | nothing = just e₁' - ... | nothing | just e₂' = just e₂' - ... | nothing | nothing = nothing + Reassocˡ : ∀ e₁ e₂ e₃ → + ((e₁ ⊔ e₂) ⊔ e₃) ≈ (proj₁ ((e₁ ⊔ e₂) ⊔ e₃) , payloadˡ e₁ e₂ e₃) + Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ in pⁿ + with n ≟ n₁ | n ≟ n₂ | n ≟ n₃ + Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + | yes refl | yes refl | yes refl + with (n₁ ⊔ᵇ n₁) ≟ n₁ + ... | no n₁≢n₁ = ⊥-elim (n₁≢n₁ (⊔ᵇ-idemp n₁)) + ... | yes p rewrite p + with n₁ ≟ n₁ + ... | no n₁≢n₁ = ⊥-elim (n₁≢n₁ refl) + ... | yes refl = ≈-refl + Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + | yes refl | yes refl | no _ + with (n₁ ⊔ᵇ n₁) ≟ n₁ + ... | no n₁≢n₁ = ⊥-elim (n₁≢n₁ (⊔ᵇ-idemp n₁)) + ... | yes p rewrite p + with n₁ ≟ n₁ + ... | no n₁≢n₁ = ⊥-elim (n₁≢n₁ refl) + ... | yes refl = ≈-refl + Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + | yes p₁@refl | no n₁≢n₂ | yes p₃@refl + using n₁⊔n₂≡n₁ ← trans (trans (trans (≡-⊔ᵇ-cong (sym (⊔ᵇ-idemp n₁)) (refl {x = n₂})) (⊔ᵇ-assoc n₁ n₁ n₂)) (⊔ᵇ-comm n₁ (n₁ ⊔ᵇ n₂))) pⁿ + with (n₁ ⊔ᵇ n₂) ≟ n₁ + ... | no n₁⊔n₂≢n₁ = ⊥-elim (n₁⊔n₂≢n₁ n₁⊔n₂≡n₁) + ... | yes p rewrite p + with n₁ ≟ n₁ | n₁ ≟ n₂ + ... | no n₁≢n₁ | _ = ⊥-elim (n₁≢n₁ refl) + ... | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂) + ... | yes refl | no _ = ≈-refl + Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + | yes p₁@refl | no n₁≢n₂ | no n₁≢n₃ = {!!} - Node-homo : ∀ e → proj₁ (eval _⊔_ e) ≡ eval _⊔ᵇ_ (mapᵉ proj₁ e) - Node-homo (` _) = refl - Node-homo (e₁ ⊔ᵉ e₂) - with IH₁ ← Node-homo e₁ with IH₂ ← Node-homo e₂ - with (n₁ , l₁) ← eval _⊔_ e₁ with (n₂ , l₂) ← eval _⊔_ e₂ - with n ← n₁ ⊔ᵇ n₂ in p - with n ≟ n₁ | n ≟ n₂ - ... | yes refl | yes refl rewrite sym IH₁ rewrite sym IH₂ = sym (⊔ᵇ-idemp n) - ... | yes refl | no _ rewrite sym IH₁ rewrite sym IH₂ = sym p - ... | no _ | yes refl rewrite sym IH₁ rewrite sym IH₂ = sym p - ... | no _ | no _ rewrite sym IH₁ rewrite sym IH₂ = sym p - - -- A key simplifying property is that notionally, only the - -- "elements with the final tag" in the expression matter. All - -- 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 = proj₁ (eval _⊔_ e) - ⊥ⁿ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n)) - _⊔ⁿ_ = FiniteHeightLattice._⊔_ (proj₂ (𝓛 n)) - in (eval _⊔_ e) ≈ (n , Maybe.maybe′ (eval _⊔ⁿ_) ⊥ⁿ (filterᵉ n e)) - Expr-final = {!!} + Reassocʳ : ∀ e₁ e₂ e₃ → + (e₁ ⊔ (e₂ ⊔ e₃)) ≈ (proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) , payloadʳ e₁ e₂ e₃) + Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) = {!!} ⊔-assoc : ∀ (e₁ e₂ e₃ : Elem) → ((e₁ ⊔ e₂) ⊔ e₃) ≈ (e₁ ⊔ (e₂ ⊔ e₃)) ⊔-assoc e₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃) - using exprˡ ← (((` e₁) ⊔ᵉ (` e₂)) ⊔ᵉ (` e₃)) - using exprʳ ← ((` e₁) ⊔ᵉ ((` e₂) ⊔ᵉ (` e₃))) - with nˡ ← proj₁ (eval _⊔_ exprˡ) in pˡ - with nʳ ← proj₁ (eval _⊔_ exprʳ) in pʳ - with final₁ ← Expr-final exprˡ - with final₂ ← Expr-final exprʳ + with nˡ ← proj₁ ((e₁ ⊔ e₂) ⊔ e₃) in pˡ + with nʳ ← proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) in pʳ + with final₁ ← Reassocˡ e₁ e₂ e₃ + with final₂ ← Reassocʳ e₁ e₂ e₃ rewrite pˡ rewrite pʳ rewrite ⊔ᵇ-assoc n₁ n₂ n₃ rewrite trans (sym pˡ ) pʳ