@@ -346,6 +346,11 @@ Note: AQL now requires mapping literals to be a list of mappings $m_1, \ldots$ o
\subsection{{\tt options}}
Allowable options are {\tt timeout} and {\tt dont\_validate\_unsafe}, which disables checking that equations preserved.
\section{{\tt pivot <instance> <options>}}
Computes the schema mapping $pivot(I)\to I$.
\chapter{Kind {\tt query}}
A query $S \to T$ assigns to each entity $en$ in $S$ a (``frozen'') instance on $T$, which we will write as $[en]$, and to each foreign key $fk : e \to e'$ a transform $[fk] : [e']\to[e]$ (note the reversal), and to each attribute $att : e \to\tau$ a term of type $\tau$ in context $[e]$.
...
...
@@ -380,6 +385,10 @@ A {\tt <instance>, ctx(<attribute>, <term>)}, i.e., a single from/where/return (
The expression ${\tt getMapping}\ C \ X$ gets the mapping $X \to C$ associated with schema $X$ in the colimit of schemas $C$.
\section{{\tt pivot <instance> <options>}}
Computes the 'schema of elements' for an instance $I$. Each row in $I$ is an entity in $pivot(I)$.
\chapter{Kind {\tt constraints}}
\section{{\tt literal : <schema>}}
...
...
@@ -573,6 +582,11 @@ If the chase succeeds, the result instance will satisfy the constraints. The op
Allowable options are the same as for an instance.
\section{{\tt pivot <instance> <options>}}
Computes the canonical instance $J$ associated with 'schema of elements' for an instance $I$. Each row in $I$ is an entity in $pivot(I)$, and we have a mapping $pivot(I) : pivot(I)\to I$ as well. This instance $J$ has the property that $\Sigma_{pivot(I)}(J)=I$.
\section{{\tt random : <schema>}}
Constructs a random instance with the specified number of generators per entity or type. Then for each generator $e:s$ and fk/att $f : s \to t$, it adds equation $f(e)= y$, where $y:t$ is a randomly selected generator (or no equation if t has no generators).
...
...
@@ -941,6 +955,12 @@ Applies only to weakly orthogonal theories. Interprets all equations $p = q$ as
Interprets all equations $p = q$ as rewrite rules $p \to q$ regardless of termination behavior. Can diverge.
Interprets all equations $p = q$ as rewrite rules $p \to q$ regardless of confluence. Can diverge.
\subsection{{\tt completion}}
Applies unfailing (ordered) Knuth-Bendix completion specialized to lexicographic path ordering. If no completion precedence is given, attempts to infer a precedence using constraint-satisfaction techniques.