]> matita.cs.unibo.it Git - helm.git/blob - helm/mathql/doc/mathql_introduction.tex
The operational semantics of the core language is ready
[helm.git] / helm / mathql / doc / mathql_introduction.tex
1 \section{Introduction}
2
3 This paper presents {\MathQL} version 4 which is the latest version of the
4 language, fully developed by Ferruccio Guidi.  
5 For a description of the previous versions of {\MathQL} see: \cite{Gui03}
6 (version 3), \cite{GS03} (version 2), \cite{Lor02} (version 1).
7
8 \subsection{Textual syntax}
9
10 The syntax of grammatical productions resembles BNF and POSIX notation:
11
12 \begin{itemize}
13
14 \item
15 \TT{::=} defines a grammatical production by means of a regular expression.
16
17 Regular expressions are made of the following elements
18 (here \TT{...} is a placeholder):
19
20 % \item
21 % \TT{.} represents any character between U 0020 and U 007F inclusive;
22
23 \item 
24 \TT{`...`} represents any character in a character set;
25
26 \item 
27 \verb+`^ ...`+ represents any character (U+0020 to U+007E) not in a character
28 set;
29
30 \item 
31 \TT{"..."} represents a string to be matched verbatim;
32
33 \item
34 \GP{...} represents a regular expression defined by a grammatical production;
35
36 \item
37 \TT{... ...} represents a conjunctive regular expression;
38
39 \item
40 \TT{... | ...} represents a disjunctive regular expression;
41
42 \item
43 \TT{[ ... ]?} represents an optional regular expression;
44
45 \item
46 \TT{[ ... ]+} represents a regular expression to be repeated one or more times;
47
48 \item
49 \TT{[ ... ]*} represents a regular expression to be repeated zero or more times;
50
51 \item
52 \TT{[ ... ]} represents a grouped regular expression.
53
54 \end{itemize}
55
56 \noindent
57 {\MathQL} Expressions can contain quoted constant strings with the syntax of
58 \figref {StrTS}.%
59 \footnote{Note that the first slash of the \GP{path} is not optional as
60 in {\MathQL}.3.}
61
62 \begin{figure}[ht]
63 \begin{footnotesize} \begin{verbatim}
64 <dec>     ::= '0 - 9'
65 <num>     ::= <dec> [ <dec> ]*
66 <hex>     ::= <dec> | 'A - F' | 'a - f'
67 <escaped> ::= "u" <hex> <hex> <hex> <hex> | '"' | "\" | "^"  
68 <string>  ::= '"' [ "\" <escaped> "^" | '^ "\^' ]* '"'
69 <path>    ::= "/" | [ "/" <string> ]+ 
70 \end{verbatim} \end{footnotesize}
71 \vskip-1pc
72 \caption{Textual syntax of numbers, strings and paths} \label{StrTS}
73 \end{figure}
74
75 \noindent
76 The meaning of the escaped sequences is shown in \figref{EscTS}
77 (where $ .... $ is a 4-digit placeholder).
78
79 \begin{figure}[ht]
80 \begin{footnotesize}
81 \begin{center} \begin{tabular}{|l|l|c|}
82 \hline {\bf Escape sequence} & {\bf Unicode character} & {\bf Text} \\
83 \hline \verb+\u....^+        & U+....                  &            \\
84 \hline \verb+\"^+            & U+0022                  & \verb+"+   \\
85 \hline \verb+\\^+            & U+005C                  & \verb+\+   \\
86 \hline \verb+\^^+            & U+005E                  & \verb+^+   \\
87 \hline
88 \end{tabular} \end{center}
89 \end{footnotesize}
90 \vskip-1pc
91 \caption{Textual syntax of escaped characters} \label{EscTS}
92 \end{figure}
93
94 {\MathQL} character escaping syntax aims at complying with W3C character model
95 for the World Wide Web \cite{W3Ca} which recommends a support for standard
96 Unicode characters (U+0000 to U+FFFF) and escape sequences with
97 start/end delimiters.
98 In particular {\MathQL} escape delimiters (backslash and caret) are chosen
99 among the {\em unwise} characters for URI references (see \cite{URI}) because
100 URI references are the natural content of constant strings and these
101 characters should not be so frequent in them.
102
103 Query expressions can contain variables for {\av}'s (production \GP{avar})
104 and variables for {\av} sets, {\ie} for query results (production \GP{svar})
105 according to the syntax of \figref{VarTS}.
106
107 \begin{figure}[ht]
108 \begin{footnotesize} \begin{verbatim}
109 <alpha> ::= [ 'A - Z' | 'a - z' | `_` ]+
110 <id>    ::= <alpha> [ <alpha> | <dec> ]*
111 <avar>  ::= "@" <id>
112 <svar>  ::= "$" <id>
113 \end{verbatim}\end{footnotesize} %$
114 \vskip-1pc
115 \caption{Textual syntax of variables} \label{VarTS}
116 \end{figure}
117
118 \noindent
119 The syntax of query expressions (production \GP{query}) is described in
120 \figref{QueryTS}.
121
122 \begin{figure}[ht]
123 \begin{footnotesize} \begin{verbatim}
124 <qualifier> ::= [ "inverse" ]? [ "sub" | "super" ]? <path>
125 <main>      ::= [ "main" <path> ]? 
126 <cons>      ::= <path> [ "in" | "match" ] <query>
127 <istrue>    ::= [ "istrue" <cons> [ "," <cons> ]* ]?
128 <isfalses>  ::= [ "isfalse" <cons> [ "," <cons> ]* ]* 
129 <exp>       ::= <path> [ "as" <path> ]?
130 <sec>       ::= [ "attr" <exp> [ "," <exp> ]* ]?
131 <opt_args>  ::= <main> <istrue> <isfalses> <sec>
132 <source>    ::= [ "pattern" ]? <query>
133 <paths>     ::= [ <path> [ "," <path> ]* ]?
134 <query>     ::= "(" <query> ")" | <string> | "[" <xavs> "]"
135             |   "property" <qualifier> <opt_args> "of" <source>
136             |   "let" <svar> "=" <query> "in" <query>
137             |   <query> ";;" <query> | <svar> | <avar> 
138             |   "ex" <query> | <avar> "." <path>
139             |   "add" [ "distr" ]? [ <xgroups> | <avar> ] "in" <query>
140             |   "for" <avar> "in" <query> [ "sup" | "inf" ] <query>
141             |   "while" <query> [ "sup" | "inf" ] <query>
142             |   <path> "{" <paths> "}" "{" <queries> "}"
143             |   "gen" <path> [ "{" <queries> "}" | "in" <query> ] 
144 <queries>   ::= [ <query> [ "," <query> ]* ]?
145 <xattr>     ::= <path> "=" <query>
146 <xgroup>    ::= "{" <xattr> [ ";" <xattr> ]* "}"
147 <xgroups>   ::= <xgroup> [ "," <xgroup> ]*
148 <xav>       ::= <string> [ "attr" <xgroups> ]?
149 <xavs>      ::= [ <xav> [ ";" <xav> ]* ]?
150 \end{verbatim} \end{footnotesize}
151 \vskip-1pc
152 \caption{Textual syntax of queries} \label{QueryTS}
153 \end{figure}
154
155 \noindent
156 The syntax of result expressions (production \GP{avs}) is described in
157 \figref{ResultTS}.
158
159 \begin{figure}[ht]
160 \begin{footnotesize} \begin{verbatim}
161 <attr>  ::= <path> "=" "{" [ <string> [ "," <string> ]* ]? "}" 
162 <group> ::= "{" <attr> [ ";" <attr> ]* "}"
163 <av>    ::= <string> [ "attr" <group> [ "," <group> ]* ]?
164 <avs>   ::= [ <av> [ ";" <av> ]* ]?
165 \end{verbatim} \end{footnotesize}
166 \vskip-1pc
167 \caption{Textual syntax of results} \label{ResultTS}
168 \end{figure}
169
170 \xcomment {
171
172 \begin{figure}[ht]
173 \begin{footnotesize} \begin{verbatim}
174             |   "select" <avar> "from" <query> "where" <query>
175 \end{verbatim} \end{footnotesize}
176 \vskip-1pc
177 \caption{Textual syntax of basic query extensions} \label{BasicTS}
178 \end{figure}
179
180 }