hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-29 10:45:15 +02:00
Code Issues Packages Projects Releases Wiki Activity

Address reviewer comments from @jbj

Browse Source
This commit is contained in:
Kasper Svendsen
2022-10-21 12:05:15 +02:00
parent 925fd2eb45
commit b29ed3b85a
1 changed files with 26 additions and 24 deletions
Download Patch File Download Diff File Expand all files Collapse all files

50
docs/codeql/ql-language-reference/modules.rst
View File

@@ -278,45 +278,47 @@ in the QL language specification.
Built-in modules
****************
QL defines a `QlBuiltins` module, which is a built-in module that is always in scope.
QL defines a ``QlBuiltins`` module that is always in scope.
Currently, it defines a single parameterized sub-module
`EquivalenceRelation`, that provides an efficient abstraction for working with
``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 built-in ``EquivalenceRelation`` module is parameterized by a type ``T`` and a
binary base relation ``base`` on ``T``. The symmetric and transitive closure of ``base``
induces a partial equivalence relation on ``T``. If every value of ``T`` appears in
``base``, 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 ``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 ``base``.
The following example illustrates an application of the `EquivalenceRelation`
module to generate a custom equivalence relation on an :ref:`algebraic datatype <algebraic-datatypes>`:
The following example illustrates an application of the ``EquivalenceRelation``
module to generate a custom equivalence relation:
.. code-block:: ql
newtype Node = MkNode(int x) { x in [1 .. 6] }
class Node extends int {
Node() { this in [1 .. 6] }
}
predicate base(Node x, Node y) {
x = MkNode(1) and y = MkNode(2)
or
x = MkNode(3) and y = MkNode(4)
}
predicate base(Node x, Node y) {
x = 1 and y = 2
or
x = 3 and y = 4
}
module Equiv = QlBuiltins::EquivalenceRelation<Node, base/2>;
module Equiv = QlBuiltins::EquivalenceRelation<Node, base/2>;
from int x, int y
where Equiv::getEquivalenceClass(MkNode(x)) = Equiv::getEquivalenceClass(MkNode(y))
select x, y
from int x, int y
where Equiv::getEquivalenceClass(x) = Equiv::getEquivalenceClass(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.
Since ``base`` does not relate ``5`` or ``6`` to any nodes, the induced
relation is a partial equivalence relation on ``Node`` and does not relate ``5``
or ``6`` to any nodes either.
The above select clause returns the following partial equivalence relation: