From 0c61d92540f0913f24951c88d3d3d4dc15347853 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Fri, 11 Oct 2024 16:48:28 +0200 Subject: [PATCH] Upstream classes from `iog-agda-prelude` --- Class/Allable.agda | 4 ++++ Class/Allable/Core.agda | 18 ++++++++++++++++++ Class/Allable/Instance.agda | 34 ++++++++++++++++++++++++++++++++++ Class/Anyable.agda | 4 ++++ Class/Anyable/Core.agda | 18 ++++++++++++++++++ Class/Anyable/Instance.agda | 31 +++++++++++++++++++++++++++++++ Class/Decidable/Core.agda | 3 +++ Class/Default.agda | 11 ++++++++++- Class/Monoid/Instances.agda | 10 ++++++++++ Class/Prelude.agda | 2 +- Class/Semigroup/Instances.agda | 10 ++++++++++ standard-library-classes.agda | 2 ++ 12 files changed, 145 insertions(+), 2 deletions(-) create mode 100644 Class/Allable.agda create mode 100644 Class/Allable/Core.agda create mode 100644 Class/Allable/Instance.agda create mode 100644 Class/Anyable.agda create mode 100644 Class/Anyable/Core.agda create mode 100644 Class/Anyable/Instance.agda diff --git a/Class/Allable.agda b/Class/Allable.agda new file mode 100644 index 0000000..c34d38c --- /dev/null +++ b/Class/Allable.agda @@ -0,0 +1,4 @@ +module Class.Allable where + +open import Class.Allable.Core public +open import Class.Allable.Instance public diff --git a/Class/Allable/Core.agda b/Class/Allable/Core.agda new file mode 100644 index 0000000..7ca9ca3 --- /dev/null +++ b/Class/Allable/Core.agda @@ -0,0 +1,18 @@ +module Class.Allable.Core where + +open import Class.Prelude + +record Allable (F : Set ℓ → Set ℓ) : Set (lsuc ℓ) where + field All : ∀ {A} → (A → Set) → F A → Set ℓ + + ∀∈-syntax = All + ∀∈-syntax′ = All + ¬∀∈-syntax = λ {A} P → ¬_ ∘ All {A} P + ¬∀∈-syntax′ = ¬∀∈-syntax + infix 2 ∀∈-syntax ∀∈-syntax′ ¬∀∈-syntax ¬∀∈-syntax′ + syntax ∀∈-syntax P xs = ∀[∈ xs ] P + syntax ∀∈-syntax′ (λ x → P) xs = ∀[ x ∈ xs ] P + syntax ¬∀∈-syntax P xs = ¬∀[∈ xs ] P + syntax ¬∀∈-syntax′ (λ x → P) xs = ¬∀[ x ∈ xs ] P + +open Allable ⦃...⦄ public diff --git a/Class/Allable/Instance.agda b/Class/Allable/Instance.agda new file mode 100644 index 0000000..8d45a7d --- /dev/null +++ b/Class/Allable/Instance.agda @@ -0,0 +1,34 @@ +module Class.Allable.Instance where + +open import Class.Prelude +open import Class.Allable.Core + +import Data.List.Relation.Unary.All as L +import Data.Vec.Relation.Unary.All as V +import Data.Maybe.Relation.Unary.All as M + +instance + Allable-List : Allable {ℓ} List + Allable-List .All = L.All + + Allable-Vec : ∀ {n} → Allable {ℓ} (flip Vec n) + Allable-Vec .All P = V.All P + + Allable-Maybe : Allable {ℓ} Maybe + Allable-Maybe .All = M.All + +private + open import Class.Decidable + open import Class.HasOrder + + _ : ∀[ x ∈ List ℕ ∋ 1 ∷ 2 ∷ 3 ∷ [] ] x > 0 + _ = auto + + _ : ∀[ x ∈ just 42 ] x > 0 + _ = auto + + _ : ∀[ x ∈ nothing ] x > 0 + _ = auto + + _ : ¬∀[ x ∈ just 0 ] x > 0 + _ = auto diff --git a/Class/Anyable.agda b/Class/Anyable.agda new file mode 100644 index 0000000..dadcee3 --- /dev/null +++ b/Class/Anyable.agda @@ -0,0 +1,4 @@ +module Class.Anyable where + +open import Class.Anyable.Core public +open import Class.Anyable.Instance public diff --git a/Class/Anyable/Core.agda b/Class/Anyable/Core.agda new file mode 100644 index 0000000..04437cc --- /dev/null +++ b/Class/Anyable/Core.agda @@ -0,0 +1,18 @@ +module Class.Anyable.Core where + +open import Class.Prelude + +record Anyable (F : Set ℓ → Set ℓ) : Set (lsuc ℓ) where + field Any : ∀ {A} → (A → Set) → F A → Set ℓ + + ∃∈-syntax = Any + ∃∈-syntax′ = Any + ∄∈-syntax = λ {A} P → ¬_ ∘ Any {A} P + ∄∈-syntax′ = ∄∈-syntax + infix 2 ∃∈-syntax ∃∈-syntax′ ∄∈-syntax ∄∈-syntax′ + syntax ∃∈-syntax P xs = ∃[∈ xs ] P + syntax ∃∈-syntax′ (λ x → P) xs = ∃[ x ∈ xs ] P + syntax ∄∈-syntax P xs = ∄[∈ xs ] P + syntax ∄∈-syntax′ (λ x → P) xs = ∄[ x ∈ xs ] P + +open Anyable ⦃...⦄ public diff --git a/Class/Anyable/Instance.agda b/Class/Anyable/Instance.agda new file mode 100644 index 0000000..c2b6f48 --- /dev/null +++ b/Class/Anyable/Instance.agda @@ -0,0 +1,31 @@ +module Class.Anyable.Instance where + +open import Class.Prelude +open import Class.Anyable.Core + +import Data.List.Relation.Unary.Any as L +import Data.Vec.Relation.Unary.Any as V +import Data.Maybe.Relation.Unary.Any as M + +instance + Anyable-List : Anyable {ℓ} List + Anyable-List .Any = L.Any + + Anyable-Vec : ∀ {n} → Anyable {ℓ} (flip Vec n) + Anyable-Vec .Any P = V.Any P + + Anyable-Maybe : Anyable {ℓ} Maybe + Anyable-Maybe .Any = M.Any + +private + open import Class.Decidable + open import Class.HasOrder + + _ : ∃[ x ∈ List ℕ ∋ 1 ∷ 2 ∷ 3 ∷ [] ] x > 0 + _ = auto + + _ : ∃[ x ∈ just 42 ] x > 0 + _ = auto + + _ : ∄[ x ∈ nothing ] x > 0 + _ = auto diff --git a/Class/Decidable/Core.agda b/Class/Decidable/Core.agda index 8f69ffb..2253ac7 100644 --- a/Class/Decidable/Core.agda +++ b/Class/Decidable/Core.agda @@ -77,3 +77,6 @@ module _ {A B C : Type ℓ} where infix -100 auto∶_ auto∶_ : ∀ (X : Type ℓ) → ⦃ X ⁇ ⦄ → Type auto∶_ A = True ¿ A ¿ + +dec-✓ : ∀ {P : Type ℓ} ⦃ _ : P ⁇ ⦄ (p : P) → ∃[ p′ ] ¿ P ¿ ≡ yes p′ +dec-✓ = dec-yes ¿ _ ¿ diff --git a/Class/Default.agda b/Class/Default.agda index 74f8ac1..951aebd 100644 --- a/Class/Default.agda +++ b/Class/Default.agda @@ -6,12 +6,15 @@ module Class.Default where open import Class.Prelude +import Data.Vec as V record Default (A : Type ℓ) : Type ℓ where constructor ⌞_⌟ field def : A open Default ⦃...⦄ public +private variable n : ℕ + instance Default-⊤ : Default ⊤ Default-⊤ = ⌞ tt ⌟ @@ -34,11 +37,17 @@ instance Default-ℤ : Default ℤ Default-ℤ = ⌞ ℤ.pos def ⌟ - Default-Fin : ∀ {n : ℕ} → Default (Fin (suc n)) + Default-Fin : Default (Fin (suc n)) Default-Fin = ⌞ zero ⌟ Default-List : Default (List A) Default-List = ⌞ [] ⌟ + Default-Vec-zero : Default (Vec A 0) + Default-Vec-zero = ⌞ V.[] ⌟ + + Default-Vec-suc : ⦃ Default A ⦄ → Default (Vec A (suc n)) + Default-Vec-suc = ⌞ V.replicate _ def ⌟ + Default-→ : ⦃ Default B ⦄ → Default (A → B) Default-→ = ⌞ const def ⌟ diff --git a/Class/Monoid/Instances.agda b/Class/Monoid/Instances.agda index bc66803..495bb49 100644 --- a/Class/Monoid/Instances.agda +++ b/Class/Monoid/Instances.agda @@ -43,6 +43,16 @@ module _ where instance _ = Monoid-ℕ-* MonoidLaws-ℕ-* = MonoidLaws≡ ℕ ∋ record {ε-identity = *-identityˡ , *-identityʳ} +-- ** natural numbers +module _ where + open import Data.Nat.Binary + open import Data.Nat.Binary.Properties + + instance _ = Semigroup-ℕᵇ-+ + Monoid-ℕᵇ-+ = Monoid ℕᵇ ∋ λ where .ε → zero + instance _ = Monoid-ℕᵇ-+ + MonoidLaws-ℕᵇ-+ = MonoidLaws≡ ℕᵇ ∋ record {ε-identity = +-identityˡ , +-identityʳ} + -- ** integers module _ where open import Data.Integer.Properties diff --git a/Class/Prelude.agda b/Class/Prelude.agda index 99f51fe..d4a523e 100644 --- a/Class/Prelude.agda +++ b/Class/Prelude.agda @@ -13,7 +13,7 @@ open import Data.Empty public open import Data.Unit public using (⊤; tt) open import Data.Product public - using (_×_; _,_; proj₁; proj₂; Σ; ∃; -,_) + using (_×_; _,_; proj₁; proj₂; Σ; ∃; ∃-syntax; -,_) open import Data.Sum public using (_⊎_; inj₁; inj₂) open import Data.Bool public diff --git a/Class/Semigroup/Instances.agda b/Class/Semigroup/Instances.agda index 853d4ea..e9a02f0 100644 --- a/Class/Semigroup/Instances.agda +++ b/Class/Semigroup/Instances.agda @@ -56,6 +56,16 @@ module _ where record {◇-assocʳ = *-assoc; ◇-comm = *-comm} where instance _ = Semigroup-ℕ-* +-- ** binary natural numbers +module _ where + open import Data.Nat.Binary + open import Data.Nat.Binary.Properties + + Semigroup-ℕᵇ-+ = Semigroup ℕᵇ ∋ λ where ._◇_ → _+_ + SemigroupLaws-ℕᵇ-+ = SemigroupLaws ℕᵇ _≡_ ∋ + record {◇-assocʳ = +-assoc; ◇-comm = +-comm} + where instance _ = Semigroup-ℕᵇ-+ + -- ** integers module _ where open import Data.Integer diff --git a/standard-library-classes.agda b/standard-library-classes.agda index 6b92c14..0fe598e 100644 --- a/standard-library-classes.agda +++ b/standard-library-classes.agda @@ -18,6 +18,8 @@ open import Class.DecEq.WithK public open import Class.Decidable public -- ** Others +open import Class.Allable public +open import Class.Anyable public open import Class.Default public open import Class.HasAdd public open import Class.HasOrder public