X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fdoc%2Fmathql_introduction_textual.tex;h=2bcb2b4cd0a7592add7d94fccc0e5591ffa5331a;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=dd225479ce475f7168b3a07ff6d19912f46c8a52;hpb=468da7af4b52d01451073ff1cca5aa1949b9657f;p=helm.git

diff --git a/helm/mathql/doc/mathql_introduction_textual.tex b/helm/mathql/doc/mathql_introduction_textual.tex
index dd225479c..2bcb2b4cd 100644
--- a/helm/mathql/doc/mathql_introduction_textual.tex
+++ b/helm/mathql/doc/mathql_introduction_textual.tex
@@ -1,6 +1,8 @@
 \subsection{Textual syntax} \label{Textual}
 
-The syntax of grammatical productions resembles BNF and POSIX notation:
+In this section we present {\MathQL}.4 textual syntax using the same notation
+that we adopted in \cite{GS03,Gui03}. In particular the grammatical
+productions we use resemble {\BNF} with some {\POSIX} formalism:
 
 \begin{itemize}
 
@@ -8,17 +10,13 @@ The syntax of grammatical productions resembles BNF and POSIX notation:
 \TT{::=} defines a grammatical production by means of a regular expression.
 
 Regular expressions are made of the following elements
-(here \TT{...} is a placeholder):
-
-% \item
-% \TT{.} represents any character between U 0020 and U 007F inclusive;
+(\TT{...} is a placeholder):
 
 \item 
 \TT{`...`} represents any character in a character set;
 
 \item 
-\verb+`^ ...`+ represents any character (U+0020 to U+007E) not in a character
-set;
+\verb+`^ ...`+ represents any character (U+20 to U+7E) not in a character set;
 
 \item 
 \TT{"..."} represents a string to be matched verbatim;
@@ -46,13 +44,7 @@ set;
 
 \end{itemize}
 
-\noindent
-{\MathQL} Expressions can contain quoted constant strings with the syntax of
-\figref {StrTS}.%
-\footnote{Note that the first slash of the \GP{path} is not optional as
-in {\MathQL}.3.}
-
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 <dec>     ::= '0 - 9'
 <num>     ::= <dec> [ <dec> ]*
@@ -65,11 +57,7 @@ in {\MathQL}.3.}
 \caption{Textual syntax of numbers, strings and paths} \label{StrTS}
 \end{figure}
 
-\noindent
-The meaning of the escaped sequences is shown in \figref{EscTS}
-(where $ .... $ is a 4-digit placeholder).
-
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize}
 \begin{center} \begin{tabular}{|l|l|c|}
 \hline {\bf Escape sequence} & {\bf Unicode character} & {\bf Text} \\
@@ -84,37 +72,43 @@ The meaning of the escaped sequences is shown in \figref{EscTS}
 \caption{Textual syntax of escaped characters} \label{EscTS}
 \end{figure}
 
+Queries and results can contain quoted constant strings with the syntax of
+\figref {StrTS}%
+\footnote
+{Note that the first slash of the \GP{path} is not optional as in {\MathQL}.3.}
+and the meaning of the escaped sequences is shown in \figref{EscTS} (where 
+$ .... $ is a 4-digit placeholder).
 {\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
-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}.
+among the \emph{unwise} characters for {\URI} references (see \cite{URI}) 
+because {\URI} references are the natural content of constant strings and 
+these characters should not be so frequent in them.
 
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 <alpha> ::= [ 'A - Z' | 'a - z' | `_` ]+
 <id>    ::= <alpha> [ <alpha> | <dec> ]*
-<avar>  ::= "@" <id>
 <svar>  ::= "$" <id>
+<evar>  ::= "@" <id>
 \end{verbatim}\end{footnotesize} %$
 \vskip-1pc
 \caption{Textual syntax of variables} \label{VarTS}
 \end{figure}
 
-\noindent
-The syntax of query expressions (production \GP{query}) is described in
-\figref{QueryTS}.
+Queries can also contain \emph{set} variables (production \GP{svar}) and
+\emph{element} variables (production \GP{evar}) according to the syntax of
+\figref{VarTS}.%
+\footnote{This syntax resembles the one of programming languages identifiers.}
+A set variable holds an {\av} set, {\ie} a query result, while an element
+variable holds an {\av}.
 
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
-<qualifier> ::= [ "inverse" ]? [ "sub" | "super" ]? <path>
+<ref>       ::= [ "sub" | "super" ]?
+<qualifier> ::= [ "inverse" ]? <ref> <path>
 <main>      ::= [ "main" <path> ]? 
 <cons>      ::= <path> [ "in" | "match" ] <query>
 <istrue>    ::= [ "istrue" <cons> [ "," <cons> ]* ]?
@@ -123,16 +117,16 @@ The syntax of query expressions (production \GP{query}) is described in
 <sec>       ::= [ "attr" <exp> [ "," <exp> ]* ]?
 <opt_args>  ::= <main> <istrue> <isfalses> <sec>
 <source>    ::= [ "pattern" ]? <query>
-<paths>     ::= [ <path> [ "," <path> ]* ]?
+<paths>     ::= <path> [ "," <path> ]*
 <query>     ::= "(" <query> ")" | <string> | "[" <xavs> "]"
             |   "property" <qualifier> <opt_args> "of" <source>
             |   "let" <svar> "=" <query> "in" <query>
-            |   <query> ";;" <query> | <svar> | <avar> 
-            |   "ex" <query> | <avar> "." <path>
-            |   "add" [ "distr" ]? [ <xgroups> | <avar> ] "in" <query>
-            |   "for" <avar> "in" <query> [ "sup" | "inf" ] <query>
+            |   <query> ";;" <query> | <svar> | <evar> 
+            |   "ex" <query> | <evar> "." <path>
+            |   "add" [ "distr" ]? [ <xgroups> | <evar> ] "in" <query>
+            |   "for" <evar> "in" <query> [ "sup" | "inf" ] <query>
             |   "while" <query> [ "sup" | "inf" ] <query>
-            |   <path> "{" <paths> "}" "{" <queries> "}"
+            |   <path> "{" [ <paths> ]? "}" "{" <queries> "}"
             |   "gen" <path> [ "{" <queries> "}" | "in" <query> ] 
 <queries>   ::= [ <query> [ "," <query> ]* ]?
 <xattr>     ::= <path> "=" <query>
@@ -145,11 +139,7 @@ The syntax of query expressions (production \GP{query}) is described in
 \caption{Textual syntax of queries} \label{QueryTS}
 \end{figure}
 
-\noindent
-The syntax of result expressions (production \GP{avs}) is described in
-\figref{ResultTS}.
-
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
 <attr>  ::= <path> "=" <string> | "{" <string> [ "," <string> ]* "}" 
 <group> ::= "{" <attr> [ ";" <attr> ]* "}"
@@ -160,14 +150,29 @@ The syntax of result expressions (production \GP{avs}) is described in
 \caption{Textual syntax of results} \label{ResultTS}
 \end{figure}
 
-\xcomment {
-
-\begin{figure}[ht]
+\begin{figure}
 \begin{footnotesize} \begin{verbatim}
-            |   "select" <avar> "from" <query> "where" <query>
+<query> ::= "empty" | "false" | "true"
+        |   [ "not" | "count" | "proj" <path> "of" ] <query>
+        |   <query> [ "and" | "or" | "xor" ] <query>
+        |   <query> [ "sub" | "meet" | "eq" | "le" | "lt" ] <query> 
+        |   <query> [ "union" | "intersect" | "diff" ] <query> 
+        |   "{" <queries> "}"  
+        |   "keep" [ "allbut" ]? [ <paths> "in" ]? <query> 
+        |   "if" <query> "then" <query> "else" <query>
+        |   "select" <evar> "from" <query> "where" <query>
 \end{verbatim} \end{footnotesize}
 \vskip-1pc
-\caption{Textual syntax of basic query extensions} \label{BasicTS}
+\caption{Textual syntax of the basic extension} \label{BasicTS}
 \end{figure}
 
-}
+The core infrastructure of {\MathQL}.4 defines a syntax for queries 
+(\figref{QueryTS}, production \GP{query}) and a syntax for results 
+(\figref{ResultTS}, production \GP{avs}).
+A syntax extension for the most common functions of the basic library is
+also provided for the user's convenience and for backward compatibility with 
+{\MathQL}.3. The syntax extension concerning the functions covered in this
+paper is shown in \figref{BasicTS}.
+Note that this extension makes \GP{avs} an instance of \GP{xavs}.
+
+