Commit 7faea53
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
@@ -273,4 +273,63 @@ The ``<module_expression>`` itself can be a module name, a selection, or a quali | |||
| 273 | 273 | reference. For more information, see ":ref:`name-resolution`." | |
| 274 | 274 | ||
| 275 | 275 | For information about how import statements are looked up, see "`Module resolution <https://codeql.github.com/docs/ql-language-reference/ql-language-specification/#module-resolution>`__" | |
| 276 | - in the QL language specification. | ||
| 276 | + in the QL language specification. | ||
| 277 | + | ||
| 278 | + Built-in modules | ||
| 279 | + **************** | ||
| 280 | + | ||
| 281 | + QL defines a `QlBuiltins` module, which is a built-in module that all databases | ||
| 282 | + include. Currently, it defines a single parameterized sub-module | ||
| 283 | + `EquivalenceRelation`, that provides an efficient abstraction for working with | ||
| 284 | + (partial) equivalence relations in QL. | ||
| 285 | + | ||
| 286 | + Equivalence relations | ||
| 287 | + ===================== | ||
| 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`. | ||
| 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`. | ||
| 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>`: | ||
| 300 | + | ||
| 301 | + .. code-block:: ql | ||
| 302 | + | ||
| 303 | + newtype Node = MkNode(int x) { x in [1..6] } | ||
| 304 | + predicate base(Node x, Node y) {(x = MkNode(1) and y = MkNode(2)) or (x = MkNode(3) and y = MkNode(4)) } | ||
| 305 | + module Equiv = QlBuiltins::EquivalenceRelation<Node, base/2>; | ||
| 306 | + | ||
| 307 | + from int x, int y | ||
| 308 | + where Equiv::getEquivalenceClass(MkNode(x)) = Equiv::getEquivalenceClass(MkNode(y)) | ||
| 309 | + select x, y | ||
| 310 | + | ||
| 311 | + Since `base` does not relate `MkNode(5)` or `MkNode(6)` to any nodes, the induced | ||
| 312 | + relation is a partial equivalence relation on `Node` and does not relate `MkNode(5)` | ||
| 313 | + or `MkNode(6)` to any nodes either. | ||
| 314 | + | ||
| 315 | + The above select clause returns the following partial equivalence relation: | ||
| 316 | + | ||
| 317 | + +---+---+ | ||
| 318 | + | x | y | | ||
| 319 | + +===+===+ | ||
| 320 | + | 1 | 1 | | ||
| 321 | + +---+---+ | ||
| 322 | + | 1 | 2 | | ||
| 323 | + +---+---+ | ||
| 324 | + | 2 | 1 | | ||
| 325 | + +---+---+ | ||
| 326 | + | 2 | 2 | | ||
| 327 | + +---+---+ | ||
| 328 | + | 3 | 3 | | ||
| 329 | + +---+---+ | ||
| 330 | + | 3 | 4 | | ||
| 331 | + +---+---+ | ||
| 332 | + | 4 | 3 | | ||
| 333 | + +---+---+ | ||
| 334 | + | 4 | 4 | | ||
| 335 | + +---+---+ | ||
0 commit comments