@@ -280,8 +280,6 @@ All schemas are ``on'' a typeside, and contain entities, foreign keys, attribute
\section{{\tt empty : <typeside>}}
The empty {\tt schema} with no entities, foreign keys, or attributes, on a particular {\tt typeside}.
\section{{\tt id <schema>}}
The identity mapping on a schema.
\section{{\tt schemaOf <instance>}}
The {\tt schema} of an {\tt instance}.
...
...
@@ -327,7 +325,7 @@ Gets the schema associated with a colimit of schemas.
A schema mapping $F : S \to T$ takes entities in $S$ to entities in $T$, foreign keys in $S$ to paths in $T$, and attributes in $S$ to terms in $T$, in a way that is functorial: if $f : s \to s'$ is a symbol in $S$, then it must be that $F(f) : F(s)\to F(s')$. In addition, if $\forall\Gamma . e = e'$ is provable in $S$, then $\forall F(\Gamma). F(e)= F(e')$ must be provable in $T$.
\section{{\tt id <schema>}}
\section{{\tt identity <schema>}}
The identity schema mapping on a particular schema.
\section{{\tt [<mapping> ; <mapping>]}}
...
...
@@ -351,7 +349,7 @@ Allowable options are {\tt timeout} and {\tt dont\_validate\_unsafe}, which disa
\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]$.
\section{{\tt id <schema>}}
\section{{\tt identity <schema>}}
The identity query on a schema.
\section{{\tt toQuery <mapping>}}
...
...
@@ -453,7 +451,7 @@ If $F : S \to T$ is a mapping and $I$ is an $S$-instance, then $\Sigma_F I$ is a
If $F : S \to T$ is a mapping and $I$ is an $S$-instance, then $\Pi_F I$ is a $T$-instance.
\section{{\tt sigma\_chase <mapping> <instance>}}
Like {\tt sigma}, but uses an alternative chase/left-kan extension based algorithm. See {\tt chase\_style} option.
Like {\tt sigma}, but uses an alternative chase/left-kan extension based algorithm. See {\tt chase\_style} option. Require the input instance to have a free type algebra. Option {\tt timeout} is also supported.
\section{{\tt frozen <query> <target entity>}}
If $Q : S \to T$ is a query and $t$ is a $T$-entity, then $frozen \ Q \ t$ is the ``frozen'' or ``canonical'' $S$-instance for $t$ in $Q$.
...
...
@@ -498,6 +496,23 @@ Expects a list of (single) SQL commands inside a section. Each SQL query should
\section{{\tt quotient\_csv <instance>}}
Expects a list of filenames inside a section. Each file should have 2 columns, where each column has a generator from the input instance. The union of these files defines an equivalence relation and this expression quotients the input instance by this relation.
\section{{\tt quotient\_query <instance>}}
Expects a list of queries, on per entity, e.g.,
\begin{verbatim}
entity E -> {from x:X y:Y where x.a = y.b}
entity F -> {from x:X y:Y}
\end{verbatim}
each query should have no attributes and no foreign keys. The resulting matched pairs $(x,y)$ are treated
as equations for performing the quotient.
\subsection{{\tt options}}
Allowed are {\tt timeout}, {\tt prover} and related options, {\tt always\_reload}, and {\tt require\_consistency}.
By default uses a chase-based algorithm; to disabled, set {\tt quotient\_use\_chase = false}
Imports a SQL database onto an autogenerated AQL schema. The AQL schema will have one attribute per column in the input DB, and one foreign key per foreign key in the input DB, and equations capturing the input DB's foreign key constraints. The type side will have a single type, ``dom''. When the [jdbcclass] and [jdbcuri] are the empty string, their values will be determined by the {\tt jdbc\_default\_class} and {\tt jdbc\_default\_string} options. See also option {\tt import\_col\_seperator}.
...
...
@@ -550,9 +565,9 @@ Allowable options are {\tt timeout}, {\tt prover} and related options, {\tt requ
\subsection{{\tt equations}}
A list of ground (non quantified) equations to quotient by. Allowable options are {\tt timeout}, {\tt prover} and related options, and {\tt require\_consistency}.
Chases the input instance with the input constraints up to the given maximum number of iterations. If the chase succeeds, the result instance will satisfy the constraints. The options will be used for the construction of the intermediate instances during the chase process.
If the chase succeeds, the result instance will satisfy the constraints. The options will be used for the construction of the intermediate instances during the chase process.
\subsection{{\tt options}}
Allowable options are the same as for an instance.
Exports an instance as CSV. The directory name will contain one file named $en.csv$ per entity $en$. The file for $en$ will be a CSV file with a header; the fields of the header will be an ID column name (specified using options), as well as any attributes and foreign keys whose domain is $en$. AQL rows that are not constants will be exported as nulls.
Exports an instance as CSV. The directory name will contain one file named $en.csv$ per entity $en$. The file for $en$ will be a CSV file with a header; the fields of the header will be an ID column name (specified using options), as well as any attributes and foreign keys whose domain is $en$. AQL values that are not constants will be exported as nulls.
\subsection{{\tt options}}
Allowed are {\tt timeout}, {\tt always\_reload}, {\tt csv} related options, and {\tt id\_column\_name}, and {\it start\_ids\_at}.
...
...
@@ -790,7 +805,7 @@ Used with {\tt import\_jdbc\_all} to import no data (only schema).
When disabled, relaxes AQL's nominal typing discipline for colimit instances.
When enabled, mappings and transforms and queries are not checked to be equality-preserving. For a query, when true it also disables decision procedure construction for sub-queries.
...
...
@@ -1074,6 +1089,10 @@ Defines the SQL quasi-type to be used with CONVERT statements when emitting SQL
Either {\tt parallel} (faster, but uses more space) or {\tt leftkan} (slower, but uses less space). Note that parallel will not be compatible with sigma operations such as sigma on transforms, the co-unit, etc. Parallel is recommended only when data volume is too large for the other algorithms.
\subsection{{\tt quotient\_use\_chase}}
In doing instance quotients, determines whether or not to use chase-based algorithm.
