From b0488c9cc631a0396c810f3b520a77853a2242b3 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 4 Jan 2025 18:58:56 -0800 Subject: [PATCH] Make 'IsDecidable' into a record to aid instance search Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 2 +- Analysis/Forward/Lattices.agda | 23 +++--- Analysis/Sign.agda | 18 +++-- Fixedpoint.agda | 3 +- Language.agda | 7 +- Language/Base.agda | 2 +- Lattice.agda | 5 +- Lattice/AboveBelow.agda | 10 ++- Lattice/FiniteMap.agda | 18 +++-- Lattice/IterProd.agda | 18 ++--- Lattice/Map.agda | 11 ++- Lattice/MapSet.agda | 5 +- Lattice/Prod.agda | 133 +++++++++++++++++---------------- Lattice/Unit.agda | 6 +- 14 files changed, 146 insertions(+), 115 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index a7dfd7c..587bbfe 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -65,7 +65,7 @@ module WithProg (prog : Program) where (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂) -- The fixed point of the 'analyze' function is our final goal. - open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂) + open import Fixedpoint ≈ᵐ-Decidable isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂) using () renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result) public diff --git a/Analysis/Forward/Lattices.agda b/Analysis/Forward/Lattices.agda index ae3766d..33863d8 100644 --- a/Analysis/Forward/Lattices.agda +++ b/Analysis/Forward/Lattices.agda @@ -5,7 +5,7 @@ module Analysis.Forward.Lattices {L : Set} {h} {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_) - (≈ˡ-dec : IsDecidable _≈ˡ_) + (≈ˡ-Decidable : IsDecidable _≈ˡ_) (prog : Program) where open import Data.String using () renaming (_≟_ to _≟ˢ_) @@ -29,11 +29,14 @@ open Program prog import Lattice.FiniteMap import Chain +≡-Decidable-String = record { R-dec = _≟ˢ_ } +≡-Decidable-State = record { R-dec = _≟_ } + -- The variable -> abstract value (e.g. sign) map is a finite value-map -- with keys strings. Use a bundle to avoid explicitly specifying operators. -- It's helpful to export these via 'public' since consumers tend to -- use various variable lattice operations. -module VariableValuesFiniteMap = Lattice.FiniteMap.WithKeys _≟ˢ_ isLatticeˡ vars +module VariableValuesFiniteMap = Lattice.FiniteMap.WithKeys ≡-Decidable-String isLatticeˡ vars open VariableValuesFiniteMap using () renaming @@ -42,7 +45,7 @@ open VariableValuesFiniteMap ; _≈_ to _≈ᵛ_ ; _⊔_ to _⊔ᵛ_ ; _≼_ to _≼ᵛ_ - ; ≈₂-dec⇒≈-dec to ≈ˡ-dec⇒≈ᵛ-dec + ; ≈₂-Decidable⇒≈-Decidable to ≈ˡ-Decidable⇒≈ᵛ-Decidable ; _∈_ to _∈ᵛ_ ; _∈k_ to _∈kᵛ_ ; _updating_via_ to _updatingᵛ_via_ @@ -60,13 +63,13 @@ open IsLattice isLatticeᵛ ; ⊔-idemp to ⊔ᵛ-idemp ) public -open Lattice.FiniteMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ +open Lattice.FiniteMap.IterProdIsomorphism ≡-Decidable-String isLatticeˡ using () renaming ( Provenance-union to Provenance-unionᵐ ) public -open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ +open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight ≡-Decidable-String isLatticeˡ vars-Unique ≈ˡ-Decidable _ fixedHeightˡ using () renaming ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ @@ -74,13 +77,13 @@ open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ ) public -≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec +≈ᵛ-Decidable = ≈ˡ-Decidable⇒≈ᵛ-Decidable ≈ˡ-Decidable joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ -- Finally, the map we care about is (state -> (variables -> value)). Bring that in. -module StateVariablesFiniteMap = Lattice.FiniteMap.WithKeys _≟_ isLatticeᵛ states +module StateVariablesFiniteMap = Lattice.FiniteMap.WithKeys ≡-Decidable-State isLatticeᵛ states open StateVariablesFiniteMap using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂) renaming @@ -91,11 +94,11 @@ open StateVariablesFiniteMap ; _∈k_ to _∈kᵐ_ ; locate to locateᵐ ; _≼_ to _≼ᵐ_ - ; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec + ; ≈₂-Decidable⇒≈-Decidable to ≈ᵛ-Decidable⇒≈ᵐ-Decidable ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ ) public -open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ +open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight ≡-Decidable-State isLatticeᵛ states-Unique ≈ᵛ-Decidable _ fixedHeightᵛ using () renaming ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ @@ -108,7 +111,7 @@ open IsFiniteHeightLattice isFiniteHeightLatticeᵐ ) public -≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec +≈ᵐ-Decidable = ≈ᵛ-Decidable⇒≈ᵐ-Decidable ≈ᵛ-Decidable fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ -- We now have our (state -> (variables -> value)) map. diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index 7f80427..af72306 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -7,6 +7,7 @@ open import Data.Sum using (inj₁; inj₂) open import Data.Empty using (⊥; ⊥-elim) open import Data.Unit using (⊤; tt) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) +open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst) open import Relation.Nullary using (¬_; yes; no) @@ -32,7 +33,7 @@ instance } -- g for siGn; s is used for strings and i is not very descriptive. -_≟ᵍ_ : IsDecidable (_≡_ {_} {Sign}) +_≟ᵍ_ : Decidable (_≡_ {_} {Sign}) _≟ᵍ_ + + = yes refl _≟ᵍ_ + - = no (λ ()) _≟ᵍ_ + 0ˢ = no (λ ()) @@ -43,12 +44,15 @@ _≟ᵍ_ 0ˢ + = no (λ ()) _≟ᵍ_ 0ˢ - = no (λ ()) _≟ᵍ_ 0ˢ 0ˢ = yes refl +≡-Decidable-Sign : IsDecidable {_} {Sign} _≡_ +≡-Decidable-Sign = record { R-dec = _≟ᵍ_ } + -- embelish 'sign' with a top and bottom element. -open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB +open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) ≡-Decidable-Sign as AB using () renaming ( AboveBelow to SignLattice - ; ≈-dec to ≈ᵍ-dec + ; ≈-Decidable to ≈ᵍ-Decidable ; ⊥ to ⊥ᵍ ; ⊤ to ⊤ᵍ ; [_] to [_]ᵍ @@ -171,9 +175,9 @@ instance module WithProg (prog : Program) where open Program prog - open import Analysis.Forward.Lattices isFiniteHeightLatticeᵍ ≈ᵍ-dec prog - open import Analysis.Forward.Evaluation isFiniteHeightLatticeᵍ ≈ᵍ-dec prog - open import Analysis.Forward.Adapters isFiniteHeightLatticeᵍ ≈ᵍ-dec prog + open import Analysis.Forward.Lattices isFiniteHeightLatticeᵍ ≈ᵍ-Decidable prog + open import Analysis.Forward.Evaluation isFiniteHeightLatticeᵍ ≈ᵍ-Decidable prog + open import Analysis.Forward.Adapters isFiniteHeightLatticeᵍ ≈ᵍ-Decidable prog eval : ∀ (e : Expr) → VariableValues → SignLattice eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs) @@ -229,7 +233,7 @@ module WithProg (prog : Program) where SignEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ } -- For debugging purposes, print out the result. - output = show (Analysis.Forward.WithProg.result isFiniteHeightLatticeᵍ ≈ᵍ-dec prog) + output = show (Analysis.Forward.WithProg.result isFiniteHeightLatticeᵍ ≈ᵍ-Decidable prog) -- This should have fewer cases -- the same number as the actual 'plus' above. -- But agda only simplifies on first argument, apparently, so we are stuck diff --git a/Fixedpoint.agda b/Fixedpoint.agda index 3f28c38..88009e3 100644 --- a/Fixedpoint.agda +++ b/Fixedpoint.agda @@ -5,7 +5,7 @@ module Fixedpoint {a} {A : Set a} {h : ℕ} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} - (≈-dec : IsDecidable _≈_) + (≈-Decidable : IsDecidable _≈_) (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_) (f : A → A) (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA) @@ -17,6 +17,7 @@ open import Data.Empty using (⊥-elim) open import Relation.Binary.PropositionalEquality using (_≡_; sym) open import Relation.Nullary using (Dec; ¬_; yes; no) +open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec) open IsFiniteHeightLattice flA import Chain diff --git a/Language.agda b/Language.agda index 5d54048..8e1706b 100644 --- a/Language.agda +++ b/Language.agda @@ -16,12 +16,13 @@ open import Data.Nat using (ℕ; suc) open import Data.Product using (_,_; Σ; proj₁; proj₂) open import Data.Product.Properties as ProdProp using () open import Data.String using (String) renaming (_≟_ to _≟ˢ_) +open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality using (_≡_; refl) open import Relation.Nullary using (¬_) open import Lattice open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs) -open import Lattice.MapSet _≟ˢ_ using () +open import Lattice.MapSet (record { R-dec = _≟ˢ_ }) using () renaming ( MapSet to StringSet ; to-List to to-Listˢ @@ -73,10 +74,10 @@ record Program : Set where -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ListMem.∈ vars -- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s} - _≟_ : IsDecidable (_≡_ {_} {State}) + _≟_ : Decidable (_≡_ {_} {State}) _≟_ = FinProp._≟_ - _≟ᵉ_ : IsDecidable (_≡_ {_} {Graph.Edge graph}) + _≟ᵉ_ : Decidable (_≡_ {_} {Graph.Edge graph}) _≟ᵉ_ = ProdProp.≡-dec _≟_ _≟_ open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_) diff --git a/Language/Base.agda b/Language/Base.agda index 35d3f88..2e7f21b 100644 --- a/Language/Base.agda +++ b/Language/Base.agda @@ -39,7 +39,7 @@ data _∈ᵇ_ : String → BasicStmt → Set where in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵇ (k ← e) in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵇ (k' ← e) -open import Lattice.MapSet (String._≟_) +open import Lattice.MapSet (record { R-dec = String._≟_ }) renaming ( MapSet to StringSet ; insert to insertˢ diff --git a/Lattice.agda b/Lattice.agda index 7c6e0ba..20ecacc 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -11,8 +11,9 @@ open import Data.Sum using (_⊎_; inj₁; inj₂) open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_) open import Function.Definitions using (Injective) -IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a -IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂) +record IsDecidable {a} {A : Set a} (R : A → A → Set a) : Set a where + field + R-dec : ∀ (a₁ a₂ : A) → Dec (R a₁ a₂) module _ {a b} {A : Set a} {B : Set b} (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda index f85bc45..d2aecdd 100644 --- a/Lattice/AboveBelow.agda +++ b/Lattice/AboveBelow.agda @@ -5,13 +5,14 @@ open import Relation.Nullary using (Dec; ¬_; yes; no) module Lattice.AboveBelow {a} (A : Set a) (_≈₁_ : A → A → Set a) (≈₁-equiv : IsEquivalence A _≈₁_) - (≈₁-dec : IsDecidable _≈₁_) where + (≈₁-Decidable : IsDecidable _≈₁_) where open import Data.Empty using (⊥-elim) open import Data.Product using (_,_) open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc) open import Function using (_∘_) open import Showable using (Showable; show) +open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl) @@ -20,6 +21,8 @@ import Chain open IsEquivalence ≈₁-equiv using () renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans) +open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec) + data AboveBelow : Set a where ⊥ : AboveBelow ⊤ : AboveBelow @@ -62,7 +65,7 @@ data _≈_ : AboveBelow → AboveBelow → Set a where ; ≈-trans = ≈-trans } -≈-dec : IsDecidable _≈_ +≈-dec : Decidable _≈_ ≈-dec ⊥ ⊥ = yes ≈-⊥-⊥ ≈-dec ⊤ ⊤ = yes ≈-⊤-⊤ ≈-dec [ x ] [ y ] @@ -76,6 +79,9 @@ data _≈_ : AboveBelow → AboveBelow → Set a where ≈-dec [ x ] ⊥ = no λ () ≈-dec [ x ] ⊤ = no λ () +≈-Decidable : IsDecidable _≈_ +≈-Decidable = record { R-dec = ≈-dec } + -- Any object can be wrapped in an 'above below' to make it a lattice, -- since ⊤ and ⊥ are the largest and least elements, and the rest are left -- unordered. That's what this module does. diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index 17c2bda..f4daf57 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -39,7 +39,7 @@ open import Lattice.Map ≡-dec-A lB as Map ; ⊓-idemp to ⊓ᵐ-idemp ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ - ; ≈-dec to ≈ᵐ-dec + ; ≈-Decidable to ≈ᵐ-Decidable ; _[_] to _[_]ᵐ ; []-∈ to []ᵐ-∈ ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ @@ -67,7 +67,6 @@ open import Data.Nat using (ℕ) open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂) open import Equivalence open import Function using (_∘_) -open import Relation.Binary.Definitions using (Decidable) open import Relation.Nullary using (¬_; Dec; yes; no) open import Utils using (Pairwise; _∷_; []; Unique; push; empty; All¬-¬Any) open import Showable using (Showable; show) @@ -86,8 +85,11 @@ module WithKeys (ks : List A) where _≈_ : FiniteMap → FiniteMap → Set _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂ - ≈₂-dec⇒≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_ - ≈₂-dec⇒≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂) + ≈₂-Decidable⇒≈-Decidable : IsDecidable _≈₂_ → IsDecidable _≈_ + ≈₂-Decidable⇒≈-Decidable ≈₂-Decidable = record + { R-dec = λ fm₁ fm₂ → IsDecidable.R-dec (≈ᵐ-Decidable ≈₂-Decidable) + (proj₁ fm₁) (proj₁ fm₂) + } _⊔_ : FiniteMap → FiniteMap → FiniteMap _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = @@ -257,7 +259,7 @@ module IterProdIsomorphism where ( _≈_ to _≈ᵘ_ ; _⊔_ to _⊔ᵘ_ ; _⊓_ to _⊓ᵘ_ - ; ≈-dec to ≈ᵘ-dec + ; ≈-Decidable to ≈ᵘ-Decidable ; isLattice to isLatticeᵘ ; ≈-equiv to ≈ᵘ-equiv ; fixedHeight to fixedHeightᵘ @@ -608,10 +610,10 @@ module IterProdIsomorphism where in (v' , (v₁⊔v₂≈v' , there v'∈fm')) - module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where + module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-Decidable : IsDecidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where import Isomorphism open Isomorphism.TransportFiniteHeight - (IP.isFiniteHeightLattice (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ) (isLattice ks) + (IP.isFiniteHeightLattice (length ks) ≈₂-Decidable ≈ᵘ-Decidable h₂ 0 fhB fixedHeightᵘ) (isLattice ks) {f = to uks} {g = from {ks}} (to-preserves-≈ uks) (from-preserves-≈ {ks}) (to-⊔-distr uks) (from-⊔-distr {ks}) @@ -624,5 +626,5 @@ module IterProdIsomorphism where ⊥-contains-bottoms : ∀ {k : A} {v : B} → (k , v) ∈ᵐ ⊥ → v ≡ (Height.⊥ fhB) ⊥-contains-bottoms {k} {v} k,v∈⊥ - rewrite IP.⊥-built (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ = + rewrite IP.⊥-built (length ks) ≈₂-Decidable ≈ᵘ-Decidable h₂ 0 fhB fixedHeightᵘ = to-build uks k v k,v∈⊥ diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda index 6841d59..37718e4 100644 --- a/Lattice/IterProd.agda +++ b/Lattice/IterProd.agda @@ -39,8 +39,8 @@ build a b (suc s) = (a , build a b s) private record RequiredForFixedHeight : Set (lsuc a) where field - ≈₁-dec : IsDecidable _≈₁_ - ≈₂-dec : IsDecidable _≈₂_ + ≈₁-Decidable : IsDecidable _≈₁_ + ≈₂-Decidable : IsDecidable _≈₂_ h₁ h₂ : ℕ fhA : FixedHeight₁ h₁ fhB : FixedHeight₂ h₂ @@ -58,7 +58,7 @@ private field height : ℕ fixedHeight : IsLattice.FixedHeight isLattice height - ≈-dec : IsDecidable _≈_ + ≈-Decidable : IsDecidable _≈_ ⊥-correct : Height.⊥ fixedHeight ≡ ⊥ @@ -84,7 +84,7 @@ private ; isFiniteHeightIfSupported = λ req → record { height = RequiredForFixedHeight.h₂ req ; fixedHeight = RequiredForFixedHeight.fhB req - ; ≈-dec = RequiredForFixedHeight.≈₂-dec req + ; ≈-Decidable = RequiredForFixedHeight.≈₂-Decidable req ; ⊥-correct = refl } } @@ -101,10 +101,10 @@ private { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest ; fixedHeight = P.fixedHeight - (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest) + (RequiredForFixedHeight.≈₁-Decidable req) (IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest) (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest) (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest) - ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest) + ; ≈-Decidable = P.≈-Decidable (RequiredForFixedHeight.≈₁-Decidable req) (IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest) ; ⊥-correct = cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_) (IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest) @@ -131,15 +131,15 @@ module _ (k : ℕ) where ; isLattice = isLattice } - module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) + module _ (≈₁-Decidable : IsDecidable _≈₁_) (≈₂-Decidable : IsDecidable _≈₂_) (h₁ h₂ : ℕ) (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where private required : RequiredForFixedHeight required = record - { ≈₁-dec = ≈₁-dec - ; ≈₂-dec = ≈₂-dec + { ≈₁-Decidable = ≈₁-Decidable + ; ≈₂-Decidable = ≈₂-Decidable ; h₁ = h₁ ; h₂ = h₂ ; fhA = fhA diff --git a/Lattice/Map.agda b/Lattice/Map.agda index 847960c..b6e49bf 100644 --- a/Lattice/Map.agda +++ b/Lattice/Map.agda @@ -1,12 +1,11 @@ open import Lattice open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst) -open import Relation.Binary.Definitions using (Decidable) open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_) module Lattice.Map {a b : Level} {A : Set a} {B : Set b} {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B} - (≡-dec-A : Decidable (_≡_ {a} {A})) + (≡-Decidable-A : IsDecidable {a} {A} _≡_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) @@ -23,6 +22,8 @@ open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs) open import Data.String using () renaming (_++_ to _++ˢ_) open import Showable using (Showable; show) +open IsDecidable ≡-Decidable-A using () renaming (R-dec to ≡-dec-A) + open IsLattice lB using () renaming ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans ; ≈-⊔-cong to ≈₂-⊔₂-cong; ≈-⊓-cong to ≈₂-⊓₂-cong @@ -625,7 +626,8 @@ Expr-Provenance-≡ {k} {v} e k,v∈e with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget k,v∈e) rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p -module _ (≈₂-dec : IsDecidable _≈₂_) where +module _ (≈₂-Decidable : IsDecidable _≈₂_) where + open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec) private module _ where data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂ @@ -676,6 +678,9 @@ module _ (≈₂-dec : IsDecidable _≈₂_) where ... | _ | no m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) → m₂̷⊆m₁ m₂⊆m₁) ... | no m₁̷⊆m₂ | _ = no (λ (m₁⊆m₂ , _) → m₁̷⊆m₂ m₁⊆m₂) + ≈-Decidable : IsDecidable _≈_ + ≈-Decidable = record { R-dec = ≈-dec } + private module I⊔ = ImplInsert _⊔₂_ private module I⊓ = ImplInsert _⊓₂_ diff --git a/Lattice/MapSet.agda b/Lattice/MapSet.agda index 61ca0d5..2b44a2a 100644 --- a/Lattice/MapSet.agda +++ b/Lattice/MapSet.agda @@ -1,9 +1,8 @@ open import Lattice open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst) -open import Relation.Binary.Definitions using (Decidable) open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_) -module Lattice.MapSet {a : Level} {A : Set a} (≡-dec-A : Decidable (_≡_ {a} {A})) where +module Lattice.MapSet {a : Level} {A : Set a} (≡-Decidable-A : IsDecidable (_≡_ {a} {A})) where open import Data.List using (List; map) open import Data.Product using (_,_; proj₁) @@ -12,7 +11,7 @@ open import Function using (_∘_) open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice) import Lattice.Map -private module UnitMap = Lattice.Map ≡-dec-A ⊤-isLattice +private module UnitMap = Lattice.Map ≡-Decidable-A ⊤-isLattice open UnitMap using (Map; Expr; ⟦_⟧) renaming diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda index 369bb81..87bc45a 100644 --- a/Lattice/Prod.agda +++ b/Lattice/Prod.agda @@ -12,6 +12,7 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) open import Data.Empty using (⊥-elim) open import Relation.Binary.Core using (_Preserves_⟶_ ) open import Relation.Binary.PropositionalEquality using (sym; subst) +open import Relation.Binary.Definitions using (Decidable) open import Relation.Nullary using (¬_; yes; no) open import Equivalence import Chain @@ -103,88 +104,92 @@ lattice = record ; isLattice = isLattice } -module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where - ≈-dec : IsDecidable _≈_ +module _ (≈₁-Decidable : IsDecidable _≈₁_) (≈₂-Decidable : IsDecidable _≈₂_) where + open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec) + open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec) + + ≈-dec : Decidable _≈_ ≈-dec (a₁ , b₁) (a₂ , b₂) with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂ ... | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂) ... | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂) ... | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂) + ≈-Decidable : IsDecidable _≈_ + ≈-Decidable = record { R-dec = ≈-dec } -module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) - (h₁ h₂ : ℕ) - (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where + module _ (h₁ h₂ : ℕ) + (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where - open import Data.Nat.Properties - open IsLattice isLattice using (_≼_; _≺_; ≺-cong) + open import Data.Nat.Properties + open IsLattice isLattice using (_≼_; _≺_; ≺-cong) - module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice - module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice + module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice + module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice - module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong - module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong - module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong + module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong + module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong + module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong - open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁) - open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁) - open ProdChain using (Chain; concat; done; step) + open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁) + open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁) + open ProdChain using (Chain; concat; done; step) - private - a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b)) - a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂) + private + a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b)) + a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂) - a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶ _≈_ - a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂) + a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶ _≈_ + a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂) - ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b)) - ∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b) + ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b)) + ∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b) - ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶ _≈_ - ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl) + ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶ _≈_ + ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl) - open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁) - open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂) + open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁) + open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂) - unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂))) - unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl)) - unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂) - with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂ - ... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b)) - ... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = - ((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂))) - ... | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = - ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂) - , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂) - )) - ... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = - ((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂) - , m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)) + unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂))) + unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl)) + unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂) + with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂ + ... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b)) + ... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = + ((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂))) + ... | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = + ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂) + , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂) )) + ... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = + ((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂) + , m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)) + )) - fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂) - fixedHeight = record - { ⊥ = (⊥₁ , ⊥₂) - ; ⊤ = (⊤₁ , ⊤₂) - ; longestChain = concat - (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁) - (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂) - ; bounded = λ a₁b₁a₂b₂ → - let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂ - in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂)) - } + fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂) + fixedHeight = record + { ⊥ = (⊥₁ , ⊥₂) + ; ⊤ = (⊤₁ , ⊤₂) + ; longestChain = concat + (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁) + (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂) + ; bounded = λ a₁b₁a₂b₂ → + let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂ + in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂)) + } - isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_ - isFiniteHeightLattice = record - { isLattice = isLattice - ; fixedHeight = fixedHeight - } + isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_ + isFiniteHeightLattice = record + { isLattice = isLattice + ; fixedHeight = fixedHeight + } - finiteHeightLattice : FiniteHeightLattice (A × B) - finiteHeightLattice = record - { height = h₁ + h₂ - ; _≈_ = _≈_ - ; _⊔_ = _⊔_ - ; _⊓_ = _⊓_ - ; isFiniteHeightLattice = isFiniteHeightLattice - } + finiteHeightLattice : FiniteHeightLattice (A × B) + finiteHeightLattice = record + { height = h₁ + h₂ + ; _≈_ = _≈_ + ; _⊔_ = _⊔_ + ; _⊓_ = _⊓_ + ; isFiniteHeightLattice = isFiniteHeightLattice + } diff --git a/Lattice/Unit.agda b/Lattice/Unit.agda index 7889b3d..16cc0fd 100644 --- a/Lattice/Unit.agda +++ b/Lattice/Unit.agda @@ -7,6 +7,7 @@ open import Data.Unit using (⊤; tt) public open import Data.Unit.Properties using (_≟_; ≡-setoid) open import Relation.Binary using (Setoid) open import Relation.Binary.PropositionalEquality as Eq using (_≡_) +open import Relation.Binary.Definitions using (Decidable) open import Relation.Nullary using (Dec; ¬_; yes; no) open import Equivalence open import Lattice @@ -24,9 +25,12 @@ _≈_ = _≡_ ; ≈-trans = trans } -≈-dec : IsDecidable _≈_ +≈-dec : Decidable _≈_ ≈-dec = _≟_ +≈-Decidable : IsDecidable _≈_ +≈-Decidable = record { R-dec = ≈-dec } + _⊔_ : ⊤ → ⊤ → ⊤ tt ⊔ tt = tt