From: Ferruccio Guidi Date: Tue, 13 Apr 2004 15:58:12 +0000 (+0000) Subject: updating the introduction X-Git-Tag: dead_dir_walking~71 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ddda5da099a3b64dbff7038382c7c6422b1337df;p=helm.git updating the introduction --- diff --git a/helm/mathql/doc/mathql_introduction.tex b/helm/mathql/doc/mathql_introduction.tex index 07894cb18..61cc88c02 100644 --- a/helm/mathql/doc/mathql_introduction.tex +++ b/helm/mathql/doc/mathql_introduction.tex @@ -20,7 +20,5 @@ the query results. \input{mathql_introduction_avsets} \input{mathql_introduction_property} \input{mathql_introduction_core} -\input{mathql_introduction_textual} - - - +\input{mathql_introduction_basic} +% \input{mathql_introduction_textual} diff --git a/helm/mathql/doc/mathql_introduction_avsets.tex b/helm/mathql/doc/mathql_introduction_avsets.tex index f90ea9247..d9943f1cf 100644 --- a/helm/mathql/doc/mathql_introduction_avsets.tex +++ b/helm/mathql/doc/mathql_introduction_avsets.tex @@ -193,7 +193,7 @@ string of a single {\av} with no attributes. \item The boolean value \emph{false} is stored as an empty {\av} set, whereas -a non-empty {\av} set may be interpreted as the boolean value \emph{true}. +an inhabited {\av} set may be interpreted as the boolean value \emph{true}. The default representation of \emph{true} is a single {\av} with an empty head string and no attributes. diff --git a/helm/mathql/doc/mathql_introduction_core.tex b/helm/mathql/doc/mathql_introduction_core.tex index fbb2d95f5..c277f1852 100644 --- a/helm/mathql/doc/mathql_introduction_core.tex +++ b/helm/mathql/doc/mathql_introduction_core.tex @@ -27,9 +27,10 @@ result, whose attributes (if any) are discarded. \item Variable assignment. -Variables for {\av} sets (called \emph{set variables}) can be assigned using -a standard \emph{let-in} construction and may appear wherever an {\av} set -({\ie} a query result) is allowed. +Variables for {\av} sets (preceded by a \TT{\$} sign and called +\emph{set variables}) can be assigned using a standard \emph{let-in} +construction and may appear wherever an {\av} set ({\ie} a query result) is +allowed. \newline The assignment has the form: \TT{let \$}\EM{variable} \TT{=} \EM{av-set} \TT{in} \EM{av-set} @@ -48,20 +49,130 @@ follows: the two {\av} sets are evaluated one after the other and the first one is discarded but the variables assigned in the first {\av} set are available to the second one. +\item +Unbounded iteration. +\newline +This construction comes in two forms: + +\TT{while} \EM{av-set} \TT{sup} \EM{av-set}: +\newline +iterates the evaluation of the second {\av} set until the first {\av set} is +empty and returns the {\MathQL} set-theoretic union of all the evaluiations +of the second {\av set}. + +\TT{while} \EM{av-set} \TT{inf} \EM{av-set}: +\newline +like the former but set-theoretic intersection is used instead of +set-theoretic union. + +In order for \TT{while} to work as expected, both {\av} sets are evaluaed in +a common context during the iteration ({\ie} the variables defined in both +are alailable to both) and this context is also propagated outside the +\TT{while} for convenience. + \item Bounded iteration. +\newline +Also this construction comes in two forms: +\TT{for @}\EM{variable} \TT{in} \EM{av-set} \TT{sup} \EM{av-set}: +\newline +iterates the evaluation of the second \EM{av-set} assigning the \EM{variable} +to each element in the first \EM{av-set} and builds the {\MathQL} +set-theoretic union of the obtained results. -\end{itemize} +\TT{for @}\EM{variable} \TT{in} \EM{av-set} \TT{inf} \EM{av-set}: +\newline +like the former but set-theoretic intersection is used instead of +set-theoretic union. -\xcomment { +The variables for attributed values (preceded by a \TT{@} sign and called +\emph{element variables}) may appear wherever an {\av} set is allowed and +and in some additional places. +\newline +The element variables are kept distinct from the set variables (therefore +\TT{\$variable} and \TT{@variable} may appear in the same query without +abiguity). + +Concerning the scope rules used in these constructions, the variables +assigned by the first {\av} set are available to the second {\av} set during +the iteration and the variables assigned by both {\av} sets are available +outside the \TT{for} as in the previous case. -Attributed values can be used to store any auxiliary information needed during -query execution. -In particular, {\MathQL} provides variables for {\av}'s which, in its textual -syntax, are identifiers% -\footnote{To be understood as in programming languages.} -preceded by the @ sign, as in \TT{@variable}, and that are introduced by the -\TT{for} and \TT{select} constructions to be explained below. +\item +Addition of groups. + +\TT{add} \EM{optional-flag} \EM{attribute-groups} \TT{in} \EM{av-set} +\newline +builds an {\av} set adding the specified \EM{attribute-groups} to each element +of the given {\av} set. +If no \EM{flag} is specified the addition is set-theoretic, whereas with the +\TT{distr} flag the addition is distributive. +The \EM{attribute-groups} can be given explicitly (in the same syntax used for +explicit {\av} sets) or they can be replaced by an element variable. In the +latter case the attribute groups of the {\av} stored in the variable are +considered. -} % \xcomment +\figref{Add} shows how to build a one-element {\av} set using \TT{add}. + +\begin{figure}[ht] +\begin{footnotesize} \begin{verbatim} +The set of attributed values given explicitly: +["head" attr {"attribute-name" = property /"metadata" of "resource"}] + +The same set built with the add operator +add {"attribute-name" = property /"metadata" of "resource"} in "head" +\end{verbatim} \end{footnotesize} +\vskip-1pc +\caption{A simple use of the add operator} +\label{Add} +\end{figure} + +\item +Existential test. + +The existential test has the form \TT{ex} \EM{av-set} where the +specification of the {\av} set contains some instances of the construction +\TT{@}\EM{variable}\TT{.}\EM{attribute-name}, and runs as follows: +the given {\av} set is evaluated replacing each +\TT{@}\EM{variable}\TT{.}\EM{attribute-name} +with the contents of \EM{attribute-name} in an attribute group of the {\av} +stored in \TT{@}\EM{variable} and the evaluation is repeated for every +possible choice of the groups (recall that different groups are allowed to +contain attributes with the same name). If one evaluation gives a non empty +result, the defaut representation of \emph{true} is returned (the test +succeded) in the other case the empty {\av} set, {\ie} \emph{false}, is +returned (the test failed). + +\item +Function invocation: + +The core language allows to invoke two kinds of external functions (with +which a language extension may be provided): the functions of the first kind +return an {\av} set, the functions of the second kind return a piece of +{\MathQL} code representing an {\av} set ({\ie} they interface a {\MathQL} +code generator). In particular: + +\EM{function-name} \verb+{+ +\EM{name} \TT{,} $\cdots$ \TT{,} \EM{name} \verb+} {+ +\EM{av-set} \TT{,} $\cdots$ \TT{,} \EM{av-set} \verb+}+ +\newline +invokes the specified function of the firs kind on the given arguments and +returns it result. The \EM{name} argument are {\MathQL} paths and usually +represent attribute names. + +\TT{gen} \EM{function-name} \verb+{+ +\EM{av-set} \TT{,} $\cdots$ \TT{,} \EM{av-set} \verb+}+ +\newline +invokes the specified function of the second kind on the given arguments and +replaces the function invocation with its result. + +The function names are {\MathQL} paths exactly as the attribute nanes and the +graph paths used by the \TT{property} operator. The names of the two kinds of +functions are kept in distinct environments so they do not clash. + +{\MathQL}.4 comes with a basic library of functions of the first kind +(see \subsecref{IBasic}) that integrate the core language providing several +facilities to the user. + +\end{itemize} diff --git a/helm/mathql/doc/mathql_introduction_textual.tex b/helm/mathql/doc/mathql_introduction_textual.tex index dd225479c..2899a24ce 100644 --- a/helm/mathql/doc/mathql_introduction_textual.tex +++ b/helm/mathql/doc/mathql_introduction_textual.tex @@ -86,8 +86,8 @@ The meaning of the escaped sequences is shown in \figref{EscTS} {\MathQL} character escaping syntax aims at complying with W3C character model for the World Wide Web \cite{W3Ca} which recommends a support for standard -Unicode characters (U+0000 to U+FFFF) and escape sequences with -start/end delimiters. +Unicode characters (U+0000 to U+FFFF) and escape sequences with start/end +delimiters. In particular {\MathQL} escape delimiters (backslash and caret) are chosen among the {\em unwise} characters for URI references (see \cite{URI}) because URI references are the natural content of constant strings and these @@ -95,7 +95,8 @@ characters should not be so frequent in them. Query expressions can contain variables for {\av}'s (production \GP{avar}) and variables for {\av} sets, {\ie} for query results (production \GP{svar}) -according to the syntax of \figref{VarTS}. +according to the syntax of \figref{VarTS}.% +\footnote{This syntax resembles the one of programming languages identifiers.} \begin{figure}[ht] \begin{footnotesize} \begin{verbatim} @@ -160,14 +161,19 @@ The syntax of result expressions (production \GP{avs}) is described in \caption{Textual syntax of results} \label{ResultTS} \end{figure} -\xcomment { +The textual syntax of the language extension provided by the basic library +is in \figref{BasicTS}. \begin{figure}[ht] \begin{footnotesize} \begin{verbatim} - | "select" "from" "where" + ::= "empty" | "false" | "true" + | "not" + | [ "and" | "or" | "xor"| "sub" | "meet" | "eq" | "le"| "lt" ] + | [ "union" | "intersect" ] | { } + | "if" "then" "else" + | "select" "from" "where" \end{verbatim} \end{footnotesize} \vskip-1pc -\caption{Textual syntax of basic query extensions} \label{BasicTS} +\caption{Textual syntax of basic extension} \label{BasicTS} \end{figure} -}