@@ -278,45 +278,47 @@ in the QL language specification.
278
278
Built-in modules
279
279
****************
280
280
281
- QL defines a `QlBuiltins ` module, which is a built-in module that is always in scope.
281
+ QL defines a `` QlBuiltins `` module that is always in scope.
282
282
Currently, it defines a single parameterized sub-module
283
- `EquivalenceRelation `, that provides an efficient abstraction for working with
283
+ `` EquivalenceRelation ` `, that provides an efficient abstraction for working with
284
284
(partial) equivalence relations in QL.
285
285
286
286
Equivalence relations
287
287
=====================
288
288
289
- The built-in `EquivalenceRelation ` module is parameterized by a type `T ` and a
290
- binary base relation `eq ` on `T ` . The symmetric and transitive closure of `eq `
291
- induces a partial equivalence relation on `T ` . If ` eq ` is reflexive, then the
292
- induced relation is an equivalence relation on `T `.
289
+ The built-in `` EquivalenceRelation `` module is parameterized by a type `` T ` ` and a
290
+ binary base relation `` base `` on `` T `` . The symmetric and transitive closure of `` base ` `
291
+ induces a partial equivalence relation on `` T `` . If every value of `` T `` appears in
292
+ `` base ``, then the induced relation is an equivalence relation on `` T ` `.
293
293
294
- The `EquivalenceRelation ` module exports a `getEquivalenceClass ` predicate that
295
- gets the equivalence class, if any, associated with a given `T ` element by the
296
- (partial) equivalence relation induced by `eq `.
294
+ The `` EquivalenceRelation `` module exports a `` getEquivalenceClass ` ` predicate that
295
+ gets the equivalence class, if any, associated with a given `` T ` ` element by the
296
+ (partial) equivalence relation induced by `` base ` `.
297
297
298
- The following example illustrates an application of the `EquivalenceRelation `
299
- module to generate a custom equivalence relation on an :ref: ` algebraic datatype < algebraic-datatypes >` :
298
+ The following example illustrates an application of the `` EquivalenceRelation ` `
299
+ module to generate a custom equivalence relation:
300
300
301
301
.. code-block :: ql
302
302
303
- newtype Node = MkNode(int x) { x in [1 .. 6] }
303
+ class Node extends int {
304
+ Node() { this in [1 .. 6] }
305
+ }
304
306
305
- predicate base(Node x, Node y) {
306
- x = MkNode(1) and y = MkNode(2)
307
- or
308
- x = MkNode(3) and y = MkNode(4)
309
- }
307
+ predicate base(Node x, Node y) {
308
+ x = 1 and y = 2
309
+ or
310
+ x = 3 and y = 4
311
+ }
310
312
311
- module Equiv = QlBuiltins::EquivalenceRelation<Node, base/2>;
313
+ module Equiv = QlBuiltins::EquivalenceRelation<Node, base/2>;
312
314
313
- from int x, int y
314
- where Equiv::getEquivalenceClass(MkNode(x)) = Equiv::getEquivalenceClass(MkNode(y) )
315
- select x, y
315
+ from int x, int y
316
+ where Equiv::getEquivalenceClass(x) = Equiv::getEquivalenceClass(y )
317
+ select x, y
316
318
317
- Since `base ` does not relate `MkNode(5) ` or `MkNode(6) ` to any nodes, the induced
318
- relation is a partial equivalence relation on `Node ` and does not relate `MkNode(5) `
319
- or `MkNode(6) ` to any nodes either.
319
+ Since `` base `` does not relate `` 5 `` or `` 6 ` ` to any nodes, the induced
320
+ relation is a partial equivalence relation on `` Node `` and does not relate `` 5 ` `
321
+ or `` 6 ` ` to any nodes either.
320
322
321
323
The above select clause returns the following partial equivalence relation:
322
324
0 commit comments