QL language spec: Document built-in equivalence relation module

Author: kaspersv

docs/codeql/ql-language-reference/modules.rst

@@ -273,4 +273,63 @@ The ``<module_expression>`` itself can be a module name, a selection, or a quali
 reference. For more information, see ":ref:`name-resolution`."
 
 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>`__"
-in the QL language specification. 
+in the QL language specification. 
+
+Built-in modules
+****************
+
+QL defines a `QlBuiltins` module, which is a built-in module that all databases
+include. Currently, it defines a single parameterized sub-module
+`EquivalenceRelation`, that provides an efficient abstraction for working with
+(partial) equivalence relations in QL.
+
+Equivalence relations
+=====================
+
+The built-in `EquivalenceRelation` module is parameterized by a type `T` and a
+binary base relation `eq` on `T`. The symmetric and transitive closure of `eq`
+induces a partial equivalence relation on `T`. If `eq` is reflexive, then the
+induced relation is an equivalence relation on `T`.
+
+The `EquivalenceRelation` module exports a `getEquivalenceClass` predicate that
+gets the equivalence class, if any, associated with a given `T` element by the
+(partial) equivalence relation induced by `eq`.
+
+The following example illustrates an application of the `EquivalenceRelation`
+module to generate a custom equivalence relation on an :ref:`algebraic datatype <algebraic-datatypes>`:
+
+.. code-block:: ql
+
+    newtype Node = MkNode(int x) {  x in [1..6] }
+    predicate base(Node x, Node y) {(x = MkNode(1) and y = MkNode(2)) or (x = MkNode(3) and y = MkNode(4)) }
+    module Equiv = QlBuiltins::EquivalenceRelation<Node, base/2>;
+
+    from int x, int y
+    where Equiv::getEquivalenceClass(MkNode(x)) = Equiv::getEquivalenceClass(MkNode(y))
+    select x, y
+
+Since `base` does not relate `MkNode(5)` or `MkNode(6)` to any nodes, the induced
+relation is a partial equivalence relation on `Node` and does not relate `MkNode(5)`
+or `MkNode(6)` to any nodes either.
+
+The above select clause returns the following partial equivalence relation:
+
++---+---+
+| x | y |
++===+===+
+| 1 | 1 |
++---+---+
+| 1 | 2 |
++---+---+
+| 2 | 1 |
++---+---+
+| 2 | 2 |
++---+---+
+| 3 | 3 |
++---+---+
+| 3 | 4 |
++---+---+
+| 4 | 3 |
++---+---+
+| 4 | 4 |
++---+---+