Skip to content

Commit 5cd117b

Browse files
jespercockxjespercockx
authored
Expose instances for decidable equality (#1341)
1 parent 6557a4a commit 5cd117b

File tree

23 files changed

+495
-1
lines changed

23 files changed

+495
-1
lines changed

‎CHANGELOG.md

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,17 @@ New modules
102102
* Added `Reflection.Traversal` for generic de Bruijn-aware traversals of reflected terms.
103103
* Added `Reflection.DeBruijn` with weakening, strengthening and free variable operations
104104
on reflected terms.
105+
* Added `Relation.Binary.TypeClasses` for type classes to be used with instance search.
106+
* Added various modules containing `instance` declarations:
107+
`Data.Bool.Instances`, `Data.Char.Instances`, `Data.Fin.Instances`,
108+
`Data.Float.Instances`, `Data.Integer.Instances`,
109+
`Data.List.Instances`, `Data.Nat.Instances`,
110+
`Data.Nat.Binary.Instances`, `Data.Product.Instances`,
111+
`Data.Rational.Instances`, `Data.Sign.Instances`,
112+
`Data.String.Instances`, `Data.Sum.Instances`,
113+
`Data.These.Instances`, `Data.Unit.Instances`,
114+
`Data.Unit.Polymorphic.Instances`, `Data.Vec.Instances`,
115+
`Data.Word.Instances`, and `Reflection.Instances`.
105116

106117
* Generic divisibility over algebraic structures
107118
```
@@ -115,6 +126,16 @@ New modules
115126
Other major changes
116127
-------------------
117128

129+
* The new module `Relation.Binary.TypeClasses` re-exports `_≟_` from
130+
`IsDecEquivalence` and `_≤?_` from `IsDecTotalOrder` where the
131+
principal argument has been made into an instance argument. This
132+
enables automatic resolution if the corresponding module
133+
`Data.*.Instances` (or `Reflection.Instances`) is imported as well.
134+
For example, if `Relation.Binary.TypeClasses`, `Data.Nat.Instances`,
135+
and `Data.Bool.Instances` have been imported, then `true ≟ true` has
136+
type `Dec (true ≡ true)`, while `0 ≟ 1` has type `Dec (0 ≡ 1)`. More
137+
examples can be found in `README.Relation.Binary.TypeClasses`.
138+
118139
Other minor additions
119140
---------------------
120141

‎README/Relation/Binary/TypeClasses.agda

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Usage examples of typeclasses for binary relations
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module README.Relation.Binary.TypeClasses where
10+
11+
open import Relation.Nullary
12+
open import Relation.Binary.PropositionalEquality
13+
open import Relation.Binary.TypeClasses
14+
15+
open import Data.Bool.Base renaming (_≤_ to _≤Bool)
16+
open import Data.Bool.Instances
17+
open import Data.List.Base
18+
open import Data.List.Instances
19+
open import Data.List.Relation.Binary.Lex.NonStrict using (Lex-≤)
20+
open import Data.Nat.Base renaming (_≤_ to _≤ℕ_)
21+
open import Data.Nat.Instances
22+
open import Data.Product
23+
open import Data.Product.Instances
24+
open import Data.Unit.Base renaming (_≤_ to _≤⊤_)
25+
open import Data.Unit.Instances
26+
open import Data.Vec.Base
27+
open import Data.Vec.Instances
28+
29+
test-Dec≡-Bool : Dec (true ≡ true)
30+
test-Dec≡-Bool = true ≟ true
31+
32+
test-Dec≡-Nat : Dec (0 ≡ 1)
33+
test-Dec≡-Nat = 0 ≟ 1
34+
35+
test-Dec≡-List : Dec (_≡_ {A = List ℕ} (1 ∷ 2 ∷ []) (1 ∷ 2 ∷ []))
36+
test-Dec≡-List = (1 ∷ 2 ∷ []) ≟ (1 ∷ 2 ∷ [])
37+
38+
test-Dec≡-⊤ : Dec (tt ≡ tt)
39+
test-Dec≡-⊤ = _ ≟ _
40+
41+
test-Dec≡-Pair : Dec (_≡_ {A = Bool × Bool} (true , false) (false , true))
42+
test-Dec≡-Pair = _ ≟ _
43+
44+
test-Dec≡-Vec : Dec (_≡_ {A = Vec Bool 2} (true ∷ false ∷ []) (true ∷ false ∷ []))
45+
test-Dec≡-Vec = _ ≟ _
46+
47+
test-Dec≡-Σ : Dec (_≡_ {A = Σ ℕ (Vec Bool)} (0 , []) (1 , true ∷ []))
48+
test-Dec≡-Σ = _ ≟ _
49+
50+
test-Dec≤-Nat : Dec (0 ≤ℕ 1)
51+
test-Dec≤-Nat = 0 ≤? 1
52+
53+
test-Dec≤-List : Dec (Lex-≤ _≡_ _≤ℕ_ (0 ∷ 1 ∷ []) (1 ∷ []))
54+
test-Dec≤-List = _ ≤? _

‎src/Data/Bool/Instances.agda

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances for booleans
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.Bool.Instances where
10+
11+
open import Data.Bool.Properties
12+
open import Relation.Binary.PropositionalEquality.Properties
13+
using (isDecEquivalence)
14+
15+
instance
16+
Bool-≡-isDecEquivalence = isDecEquivalence _≟_
17+
Bool-≤-isDecTotalOrder = ≤-isDecTotalOrder

‎src/Data/Char/Instances.agda

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances for characters
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.Char.Instances where
10+
11+
open import Data.Char.Properties
12+
open import Relation.Binary.PropositionalEquality.Properties
13+
using (isDecEquivalence)
14+
15+
instance
16+
Char-≡-isDecEquivalence = isDecEquivalence _≟_

‎src/Data/Fin/Instances.agda

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances for finite sets
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.Fin.Instances where
10+
11+
open import Data.Fin.Base
12+
open import Data.Fin.Properties
13+
14+
instance
15+
Fin-≡-isDecEquivalence = ≡-isDecEquivalence
16+
Fin-≤-isDecTotalOrder = ≤-isDecTotalOrder

‎src/Data/Float/Instances.agda

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances for floating point numbers
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.Float.Instances where
10+
11+
open import Data.Float.Properties
12+
open import Relation.Binary.PropositionalEquality.Properties
13+
using (isDecEquivalence)
14+
15+
instance
16+
Float-≡-isDecEquivalence = isDecEquivalence _≟_

‎src/Data/Integer/Instances.agda

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances for integers
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.Integer.Instances where
10+
11+
open import Data.Integer.Properties
12+
open import Relation.Binary.PropositionalEquality.Properties
13+
using (isDecEquivalence)
14+
15+
instance
16+
ℤ-≡-isDecEquivalence = isDecEquivalence _≟_
17+
ℤ-≤-isDecTotalOrder = ≤-isDecTotalOrder

‎src/Data/List/Instances.agda

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,25 @@
88

99
module Data.List.Instances where
1010

11+
open import Data.List.Base
1112
open import Data.List.Categorical
13+
open import Data.List.Properties
14+
using (≡-dec)
15+
open import Data.List.Relation.Binary.Pointwise
16+
using (Pointwise)
17+
open import Data.List.Relation.Binary.Lex.NonStrict
18+
using (Lex-≤; ≤-isDecTotalOrder)
19+
open import Level
20+
open import Relation.Binary.Core
21+
open import Relation.Binary.PropositionalEquality.Core
22+
open import Relation.Binary.PropositionalEquality.Properties
23+
using (isDecEquivalence)
24+
open import Relation.Binary.TypeClasses
25+
26+
private
27+
variable
28+
a ℓ₁ ℓ₂ : Level
29+
A : Set a
1230

1331
instance
1432
listFunctor = functor
@@ -19,3 +37,11 @@ instance
1937
listMonadZero = monadZero
2038
listMonadPlus = monadPlus
2139
listMonadT = λ {ℓ} {M} {{inst}} → monadT {ℓ} {M} inst
40+
41+
List-≡-isDecEquivalence : {{IsDecEquivalence {A = A} _≡_}} → IsDecEquivalence {A = List A} _≡_
42+
List-≡-isDecEquivalence = isDecEquivalence (≡-dec _≟_)
43+
44+
List-Lex-≤-isDecTotalOrder : {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂}
45+
→ {{IsDecTotalOrder _≈_ _≼_}}
46+
→ IsDecTotalOrder (Pointwise _≈_) (Lex-≤ _≈_ _≼_)
47+
List-Lex-≤-isDecTotalOrder {{≼-isDecTotalOrder}} = ≤-isDecTotalOrder ≼-isDecTotalOrder

‎src/Data/Nat/Binary/Instances.agda

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances for binary natural numbers
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.Nat.Binary.Instances where
10+
11+
open import Data.Nat.Binary.Properties
12+
open import Relation.Binary.PropositionalEquality.Properties
13+
using (isDecEquivalence)
14+
15+
instance
16+
ℕᵇ-≡-isDecEquivalence = isDecEquivalence _≟_

‎src/Data/Nat/Instances.agda

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances for natural numbers
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --without-K --safe #-}
8+
9+
module Data.Nat.Instances where
10+
11+
open import Data.Nat.Properties
12+
open import Relation.Binary.PropositionalEquality.Properties
13+
using (isDecEquivalence)
14+
15+
instance
16+
ℕ-≡-isDecEquivalence = isDecEquivalence _≟_
17+
ℕ-≤-isDecTotalOrder = ≤-isDecTotalOrder

0 commit comments

Comments
 (0)