\usepackage{euler}
\usepackage{amssymb}
\usepackage{stmaryrd}
+\usepackage{wasysym}
-\title{A MathML Editor Based on \TeX{} Syntax\\Formal Specification}
+\title{\EdiTeX: a MathML Editor Based on \TeX{} Syntax\\\small Description and Formal Specification}
\author{Paolo Marinelli\\Luca Padovani\\\small\{{\tt pmarinel},{\tt lpadovan}\}{\tt @cs.unibo.it}\\\small Department of Computer Science\\\small University of Bologna}
\date{}
+\newcommand{\EdiTeX}{Edi\TeX}
+
\newcommand{\tmap}[1]{\llbracket#1\rrbracket}
\newcommand{\tadvance}{\vartriangle}
\newcommand{\tnext}{\rhd}
\newcommand{\ROW}{\texttt{row}}
\newcommand{\SLDROP}{\blacktriangleleft}
\newcommand{\NLDROP}{\vartriangleleft}
-\newcommand{\RGROUP}{\vartriangleleft_{rg}}
+\newcommand{\RDROP}{\vartriangleright}
\begin{document}
\maketitle
+\section{Introduction}
+
+MathML~\cite{MathML1,MathML2,MathML2E} is an XML application for the
+representation of mathematical expressions. As most XML applications,
+MathML is unsuitable to be hand-written, except for the simplest
+cases, because of its verbosity. In fact, the MathML specification
+explicitly states that
+\begin{quote}
+``While MathML is human-readable, it is anticipated that, in all but
+the simplest cases, authors will use equation editors, conversion
+programs, and other specialized software tools to generate MathML''
+\end{quote}
+
+The statement about human readability of MathML is already too strong,
+as the large number of mathematical symbols, operators, and
+diacritical marks that are used in mathematical notation cause MathML
+documents to make extensive use of Unicode characters that typically
+are not in the ``visible'' range of common text editors. Such
+characters may appear as entity references, whose name indicates
+somehow the kind of symbol used, or character references or they are
+directly encoded in the document encoding scheme (for instance,
+UTF-8).
+
+It is thus obvious that authoring MathML documents assumes the
+assistance of dedicated tools. As of today, such tools can be
+classified into two main categories:
+\begin{enumerate}
+ \item WYSIWYG (What You See Is What You Get) editors that allow the
+ author to see the formatted document on the screen as it is
+ composed;
+ \item conversion tools that generate MathML markup from different
+ sources, typically other markup languages for scientific
+ documents, such as \TeX.
+\end{enumerate}
+
+While the former tools are certainly more appealing, especially to the
+unexperienced user, as they give a direct visual feedback, the
+existance of tools in the second category takes into account the large
+availability of existing documents in \TeX{} format, and also the fact
+that experienced or ``lazy'' users may continue to prefer the use of a
+markup language other than MathML for editing, and generate MathML
+only as a final step of the authoring process. The ``laziness'' is not
+really intended as a way of being reluctant towards a new technology,
+but rather as a justified convincement that WYSIWYG editors are ``nice
+to look at'' but after all they may slow down the authoring process.
+WYSIWYG editors often involve the use of menus, palettes of symbols,
+and, in general, an extensive use of the pointing device (the mouse)
+for completing most operations. The use of shortcuts is of little
+help, as it implies very soon a challenging exercise for the fingers
+and the mind. Moreover, authors \emph{cannot improve} their authoring
+speed with time. On the other side, the gap between the syntax of any
+markup language for mathematics and mathematical notation may be
+relevant, especially for large, non-trivial formulas and authoring is
+a re-iterated process in which the author repeadtedly types the markup
+in the editor, compiles, and looks at the result inside a pre-viewer.
+
+\EdiTeX{} tries to synthesize the ``best of both worlds'' in a single
+tool. The basic idea is that of creating a WYSIWYG editor in which
+editing is achieved by typing \TeX{} markup as the author would do in
+a text editor. The \TeX{} markup is tokenized and parsed on-the-fly
+and a corresponding MathML representation is created and
+displayed. This way, the author can see the rendered document as it
+changes. The advantages of this approach can be summarized as follows:
+\begin{itemize}
+ \item the document is rendered concurrently with the editing, the
+ user has an immediate feedback hence it is easier to spot errors;
+ \item the author types in a concrete (and likely familiar) syntax
+ improving the editing speed;
+ \item the usual WYSIWYG mechanisms are still available. In
+ particular, it is possible to select \emph{visually} a fragment of
+ the document that needs re-editing, or that was left behind for
+ subsequent editing.
+\end{itemize}
+
+\paragraph{The Name of the Game:} there is no reference to MathML in
+the name ``\EdiTeX.'' In fact, the architecture of the editor is not
+tied to MathML markup. Although we focus on MathML editing, by
+changing a completely modularized component of the editor it is
+virtually possible to generate any other markup language.
+
+\paragraph{Acknowledgments.} Stephen M. Watt and Igor Rodionov for
+their work on the \TeX{} to MathML conversion tool; Stan Devitt for an
+illuminating discussion about the architecture of \TeX{} to XML
+conversion tools; Claudio Sacerdoti Coen for the valuable feedback and
+uncountable bug reports.
+
+\section{Architecture}
+
+\section{Customization}
+
+\subsection{Short and Long Identifiers}
+
+\subsection{The Dictionary}
+
+\subsection{Stylesheets and Trasformations}
+
+\subsection{Rendering}
+
+\section{XML Representation of \TeX{} Markup}
+
\section{Tokens}
The following tokens are defined:
\end{tabular}
%$
-%% \section{Description and Semantics of the Pattern Language}
+\section{Description and Semantics of the Pattern Language}
%% \begin{eqnarray*}
%% \mathit{NodeTest} & ::= & \mathtt{*} \\
%% & | & \mathit{AttributeName}\mathtt{='}\mathit{Text}\mathtt{'}
%% \end{eqnarray*}
+\begin{table}
+\[
+\begin{array}{rcl@{\hspace{3em}}rcl@{\hspace{3em}}rcl}
+ C &::=& . & Q &::=& \langle*\rangle & P &::=& P'\#P' \\
+ &|& .. & &|& \langle!*\rangle & &|& \cent P'\#P'\\
+ &|& / & &|& \langle n_1\mid\cdots\mid n_k\rangle & &|& P'\#P'\$\\%$
+ &|& Q & &|& \langle!n_1\mid\cdots\mid n_k\rangle & &|& \cent P'\#P'\$\\%$
+ &|& (C) & &|& Q[@n] & & &\\
+ &|& \{C:\Gamma\} & &|& Q[!@n] & P' &::=& \\
+ &|& C\&C & &|& Q[@n=v] & &|& C\;P'\\
+ &|& C\mid C & &|& Q[!@n=v] & & &\\
+ &|& C+ & &|& Q[P] & & &\\
+ &|& C? & &|& Q[!P] & & &\\
+ &|& C* & & & & & &\\
+ &|& C\;C & & & & & &\\
+ &|& !C & & & & & &\\
+\end{array}
+\]
+\caption{Syntax of the regular context language. $n$, $n_i$ denote
+names, $v$ denotes a string enclosed in single or double quotes}
+\end{table}
+
+
\section{Insert Rules}
\paragraph{Begin Group:} $\{$
\begin{description}
- %********* rules that try to express situations completely specified (there is an effective deletion) ******
-
- % in the rules below, a token is either an i node, an n node, an o node, an s node or an empty c node.
- % an empty c node is either an undefined macro or an empty macro. These c node are handled as they actually were
- % tokens (i, n, o, s).
- % An important observation is: a sequence of groups with id, in which every group has one and only one child and where
- % the last group contains the cursor, is equivalent to the cursor (Is it clear?). For example:
- % <g id="id1"><g id="id2">...<g id="idn"><cursor/></g>...</g></g> is equivalent to:
- % <cursor/>
-
- \item{\verb+<g|p>[(i|n|o|s|c[ ])#]/(g[@id][^#$]/++\verb+)?cursor+}\\
- remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and replace the token with the $\RGROUP$.
-
- \item{\verb+<g|p>[g#]/(g[@id][^#$]/++\verb+)?cursor+}\\
- remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and append $\NLDG$ to the \G{} node preceding the cursor
-
- %% there is an optional sequence of groups with id, all of which having one and only one child. The last
- %% child of this sequence (or the root, if the sequence is empty) is a group with id, has as first element a
- %% token and has as second and last element an eventually empty sequence of groups with id, all of which having
- %%one and only one child. The last element of this sequence has the cursor as its child.
- %\item{\verb+(g[@id][^#$]/++\verb+)?g[@id][^(i|n|o|s|c[ ])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
- %replace the whole fragment with the cursor.
-
- % the cursor is a macro's child. There is an eventually empty sequence of delimiters, which precedes the
- % cursor. Before this sequence, there is a p node. This p node has as its last child a token
- \item{\verb+c[p[(i|n|o|s|c[ ])$]((i|n|o|s|c[ ])*)#]/cursor+}\\
- remove the cursor and replace the token with the cursor.
-
- % there is a token, which precedes the cursor. The cursor is child of either a group or a parameter.
- % the case where the cursor is child of a group with id, there are no nodes after the cusror and there
- % are no nodes preceding the token, is handled by the first rule.
- % This rule is duplicated below, but that one could have a wrong syntax. This one has been tested.
- \item{\verb+<g|p>[(i|n|o|c[ ])#]/cursor+}\\
- remove the cursor and replace the token with the cursor.
-
- % cursor's parent is a script (the cursor is not the base). The script's base is an empty group with id.
- % The script is preceded by a token.The script's parent is group or a parameter.
- % The case where the script's parent is a group with id and the token is the first child, while
- % the script is the last one, is handled some rules later.
- \item{\verb+<g|p>[(i|n|o|s|c[ ])#]/<sp|sb>[^(g[@id][ ])#$]/cursor+}\\
- remove the script and replace the token with the cursor.
-
- % As above, but: we don't care who precedes the script (we do not have to remove it); the script's base
- % is still an empty group, but it has no id.
- % Ad above, we have to precise that the situation where the script is the only child of a group with id
- % is handled some rules later.
- \item{\verb+<g|p>/<sp|sb>[^(g[!@id][ ])#$]/curosr+}\\
- replace the script with the cursor.
-
- % The cursor is the last child of a script. The script's base is token.
- \item{\verb+<g|p>/<sp|sb>[^(i|n|o|s|c[ ])#$]/cursor+}\\
- repalce the script with the cursor.
-
-
- %*******************************************************************************************************
- %************** rules handling the case in which the cursor has a preceding node ***********************
- %*******************************************************************************************************
-
- %************************* the cursor's parent is a group or a parameter *******************************
-
- %we consider an empty macro as a token. An empty macro is either undefined or simply empty.
-
- %rule handling the case where the cursor has a preceding token and this is the first node of a group with id
- \item{\verb+g[@id][^(i||n||o||s||c[^$])#]/cursor+}\\
- remove the cursor and replace the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node with the $\NLDROP$.
- \item{\verb+<g|p>[(i||n||o||s||c[^$])#]/cursor+}\\
- remove the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node.
- %it corresponds to the drop_prev_group(false).
- \item{\verb+<g|p>[g#]/cursor+}\\
- remove the cursor and append the $\NLDROP$ to the \G{} node.
- %corresponds to the drop_prev_script(false).
- \item{\verb+<g|p>[(<sp|sb>)#]/cursor+}\\
- remove the cursor and append the $\NLDROP$ to the \SP{} or \SB{} node.
- %rules handling the right open macros preceding the cursor.
- \item{\verb+<g|p>[(c[^p[@right-open='1']$])#]/cursor+}\\
- remove the cursor and append the $\NLDROP$ to the \PNODE{} node.
- %we don't have a macro of this kind, but we don't know the future...
- \item{\verb+<g|p>[(c[^p[!(@right-open='1')][@left-open='1'][^$]$])#]/cursor+}\\
- remove the cursor and replace the \CNODE node with the $\NLDROP$.
- \item{\verb+<g|p>[(c[^p[!(@right-open='1')][@left-open='1']$])#]/cursor+}\\
- replace the \CNODE{} node with the content of the \PNODE node and replace the cursor with the $\NLDROP$.
- %rules handling macro with parameter(s) and preceding the cursor.
- \item{\verb+<g|p>[c#]/cursor+}\\
- remove the cursor and append the $\NLDROP$ to the \CNODE{} node.
- %rule handling table with rows preceding the cursor.
- \item{\verb+<g|p>[(table[row[cell[^g$]$]$])#]/cursor+}\\
- remove the cursor and append the $\NLDROP$ to the \G{} node, which is child of the \CELL{} node.
- %rule handling tables without rows preceding the cursor.
- \item{\verb+<g|p>[table#]/cursor+}\\
- remove the cursor and append the $\NLDROP$ to the \TABLE{} node
-
- %********************************* the cursor's parent is a script ******************************
-
- %rule handling the case where the script's base is an empty group with id.
- \item{\verb+<sp|sb>[^(g[@id][^$])#$]/cursor+}\\
- replace the \SP{} or \SB{} node with the $\NLDROP$.
- %rule handling the case where the script's base is an empty group without id
- \item{\verb+<sp|sb>[^(g[^$])#$]/cursor+}\\
- replace the \SP{} or \SB{} node with the cursor.
- %rule handling the case where the script's base is something else
- \item{\verb+<sp|sb>[^*#$]/cursor+}\\
- replace the \SP{} or \SB{} node with it's first child and insert the $\NLDROP$ after it.
-
- %********************************* the cursor's parent is a macro ********************************
-
- %rule handling the case where the preceding node is a parameter
- \item{\verb+c[p#]/cursor+}\\
- remove the cursor and append the $\NLDROP$ to the PNODE{} node.
- %rule handling the case where the preceding node is a delimiter
- \item{\verb+c[(<i|n|o|s|c>)#]/cursor+}\\
- remove the cursor and insert the $\NLDROP$ before the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node.
-
- %*************************************************************************************************
- %*********** rules handling the case in which the cursor has no preceding nodes ******************
- %*************************************************************************************************
-
- %rule handling the case where the cursor has something else after it
- \item{\verb+<g|p>[#*]/cursor+}\\
- nothing to drop.
-
- %rules handling the case where the cursor's parent is a p node and the cursor has no nodes after it.
-
- %rule handling the case where the p node is a left and right open macro's child and the first p node has no elements.
- \item{\verb+c[^(p[@left-open='1'][^$])#$]/p[@right-open='1'][^#$]/cursor+}\\
- replace the \CNODE{} with the $\NLDROP$.
- %rule handling the case where the p node is a left and right open macro's child and the first p node has elements.
- \item{\verb+c[^(p[@left-open='1']#$]/p[@right-open='1'][^#$]/cursor+}\\
- replace the \CNODE{} with the content of the PNODE{} with attribute texttt{left-open='1'} and insert $\NLDROP$ after this.
- %rule handling the case where the p node is right open macro's child.
- \item{\verb+c[^#$]/p[@right-open='1'][^#$]/cursor+}\\
- replace the \CNODE{} with the $\NLDROP$.
- %rule handling the case where the p node is a macro's child and this macro has parameter.
- \item{\verb+c/p[^#$]/cursor+}\\
- remove the cursor and insert the $\NLDROP$ before the \PNODE{} node.
-
- %rule handling the case where the cursor has no nodes after it and its parent is a group with id
- \item{\verb+g[@id][^#$]/cursor+}\\
- replace the \G{} node with the $\NLDROP$.
+ \item{\verb+cursor+}\\
+ replace the cursor with the $\NLDROP$.
\end{description}
\begin{description}
- %*******************************************************************************************************
- %************** rules handling the case in which the cursor has a preceding node ***********************
- %*******************************************************************************************************
-
- %************************* the cursor's parent is a group or a parameter *******************************
-
- %this rule is more specific than the one below which handle the case of the cursor preceded by a c node
- \item{\verb+<g|p>[(i||n||o||s||c[^$])#]/cursor+}\\
- remove the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node.
- %it corresponds to the drop_prev_group(true).
- \item{\verb+<g|p>[g#]/cursor+}\\
- remove the cursor and append the it to the \G{} node.
- %corresponds to the drop_prev_script(true).
- \item{\verb+<g|p>[(<sp|sb>)#]/cursor+}\\
- remove the cursor and append the $\SLDROP$ to the \SP{} or \SB{} node.
- %rules handling the right open macros preceding the cursor.
- \item{\verb+<g|p>[(c[^p[@right-open='1']$])#]/cursor+}\\
- remove the cursor and append the $\SLDROP$ to the \PNODE{} node.
- %we don't have a macro of this kind, but we don't know the future...
- \item{\verb+<g|p>[(c[^p[!(@right-open='1')][@left-open='1'][^$]$])#]/cursor+}\\
- remove the cursor and replace the \CNODE node with the cursor.
- \item{\verb+<g|p>[(c[^p[!(@right-open='1')][@left-open='1']$])#]/cursor+}\\
- replace the \CNODE{} node with the content of the \PNODE node.
- %rule handling macro with parameter(s) and preceding the cursor.
- \item{\verb+<g|p>[c#]/cursor+}\\
- remove the cursor and append the $\SLDROP$ to the \CNODE{} node.
- %rule handling table with rows preceding the cursor.
- \item{\verb+<g|p>[(table[row[cell[^g$]$]$])#]/cursor+}\\
- remove the cursor and append the it to the \G{} node, which is child of the \CELL{} node.
- %rule handling tables without rows preceding the cursor.
- \item{\verb+<g|p>[table#]/cursor+}\\
- remove the cursor and append the $\SLDROP$ to the \TABLE{} node
-
- %********************************* the cursor's parent is a script ******************************
-
- %rule handling the case where the script's base is an empty group with id.
- \item{\verb+<sp|sb>[^(g[@id][^$])#$]/cursor+}\\
- replace the \SP{} or \SB{} node with the \G{} node and insert the cursor after it.
- %rule handling the case where the script's base is an empty group without id
- \item{\verb+<sp|sb>[^(g[^$])#$]/cursor+}\\
- replace the \SP{} or \SB{} node with the cursor.
- %rule handling the case where the scrip's base is something else
- \item{\verb+<sp|sb>[^*#$]/cursor+}\\
- replace the \SP{} or \SB{} node with it's first child and insert the cursor after it.
-
- %********************************* the cursor's parent is a macro ********************************
-
- %rule handling the case where the preceding node is a parameter
- \item{\verb+c[p#]/cursor+}\\
- remove the cursor and append the $\SLDROP$ to the PNODE{} node.
- %rule handling the case where the preceding node is a delimiter
- \item{\verb+c[(<i|n|o|s|c>)#]/cursor+}\\
- remove the cursor and insert the it before the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node.
-
- %*************************************************************************************************
- %*********** rules handling the case in which the cursor has no preceding nodes ******************
- %*************************************************************************************************
-
- %rule handling the case where the cursor has something else after it
- \item{\verb+<g|p>[#*]/cursor+}\\
- nothing to drop.
-
- %rules handling the case where the cursor's parent is a p node and the cursor has no nodes after it.
-
- %rule handling the case where the p node is a left and right open macro's child and the first p node has no elements.
- \item{\verb+c[^(p[@left-open='1'][^$])#$]/p[@right-open='1'][^#$]/cursor+}\\
- replace the \CNODE{} with the cursor.
- %rule handling the case where the p node is a left and right open macro's child and the first p node has elements.
- \item{\verb+c[^(p[@left-open='1']#$]/p[@right-open='1'][^#$]/cursor+}\\
- replace the \CNODE{} with the content of the PNODE{} with attribute texttt{left-open='1'} and insert cursor after this.
- %rule handling the case where the p node is right open macro's child.
- \item{\verb+c[^#$]/p[@right-open='1'][^#$]/cursor+}\\
- replace the \CNODE{} with the cursor.
- %rule handling the case where the p node is a macro's child and this macro has parameter.
- \item{\verb+c/p[^#$]/cursor+}\\
- remove the cursor and insert the $\SLDROP$ before the \PNODE{} node.
-
- %rule handling the case where the cursor has no nodes after it and its parent is a group with id
- \item{\verb+g[@id][^#$]/cursor+}\\
- replace the \G{} node with the cursor.
+ \item{\verb+cursor+}\\
+ replace the cursor with the $\SLDROP$.
\end{description}
\section{Right Drop Rules}
+\begin{description}
+
+ \item{\verb+cursor+}\\
+ replace the cursor with the $\RDROP$.
+
+\end{description}
+
\section{$\varepsilon$-rules}
\paragraph{Nromal Left Drop}
\begin{description}
- %********************* epsilon rules concerning the rgreplace_father ********************
-
- \item{\verb+(g[@id][^#$]/++\verb+)+$\RGROUP$}\\
- replace the whole fragment with the cursor.
-
- \item{\verb+*[!@id]/+$\RGROUP$}\\
- replace the $\RGROUP$ with the cursor.
-
- \item{\verb+g[@id][*#]/+$\RGROUP$}\\
- replace the $\RGROUP$ with the cursor
-
- \item{\verb+g[@id][#*]/+$\RGROUP$}\\
- replace the $\RGROUP$ with the cursor.
- % maybe it's not the correct action
-
-
-
- %********************************************* \NLDROP has a preceding node *********************************************
-
- %rule handling the case where the preceding node is a token or an empty macro.
- \item{\verb+*[(i||n||o||s||c[^$])#]/+$\NLDROP$}\\
- remove the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or the \CNODE{} node.
- %rule handling the case where the preceding node is a group
- \item{\verb+*[g#]/+$\NLDROP$}\\
- remove the $\NLDROP$ append it to the \G{} node.
- %rule handling the case where the preceding node is a script
- \item{\verb+*[<sp|sb>#]/+$\NLDROP$}\\
- remove the $\NLDROP$ append it to the \SP{} or \SB{} node.
- %rule handling the case where the preceding node is an open-right macro
- \item{\verb+*[(c[^p[@right-open='1']$])#]/+$\NLDROP$}\\
- remove the $\NLDROP$ and append it to the \PNODE{} node.
- %rule handling the case where the preceding node is a left-open macro (and not right-open), and the p node of this macro has no children
- \item{\verb+*[(c[^p[!(@right-open='1')][@left-open='1'][^$]$])#]/+$\NLDROP$}\\
- remove the \CNODE node.
- %rule handling the case where the preceding node is a left-open macro (and not right-open), and the p node of this macro has children
- \item{\verb+*[(c[^p[!(@right-open='1')][@left-open='1']$])#]/+$\NLDROP$}\\
- replace the \CNODE{} node with the content of the \PNODE{} node.
- %rule handling the case where the preceding node is a macro with parameter(s)
- \item{\verb+*[c#]/+$\NLDROP$}\\
- remove the $\NLDROP$ and append it to the \CNODE{} node.
-
- %rule handling the deletion of primes in superscript
-
- %there are more than one prime in the phantom group
- \item{\verb+sp[!(@id)][*#$]/g[!(@id)][o#]/+$\NLDROP$}\\
- remove the \ONODE node, remove the $\NLDROP$ and insert the cursor after the \SP{} node.
- %there is one and only one prime in the phantom group
- \item{\verb+sp[!(@id)][*#$]/g[!(@id)][^o#]/+$\NLDROP$}\\
- replace the \SP{} node with it's first child and insert the cursor after it
-
- %*** rules handling the case where the \NLDROP's parent is a macro (with parameter) ***
-
- %the node preceding the \NLDROP is a delimiter
- \item{\verb+c[(<i|n|o|s|c>)#]/+$\NLDROP$}\\
- remove the $\NLDROP$ and insert it before the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node.
- %the node preceding the \NLDROP is parameter
- \item{\verb+c[p#]/+$\NLDROP$}\\
- remove the $\NLDROP$ and append it to the \PNODE{} node.
+ \item{\verb+math/g[^#]/+$\NLDROP$}\\
+ repalce the $\NLDROP$ with the cursor.
+
+ %**************************************************************************************
+ %****************************** epsilon-rules with \NLDROP ****************************
+ %**************************************************************************************
- %********************************************* the \NLDROP has no preceding nodes ****************************************************
+ %************** \NLDROP has neither preceding nor following nodes ********************
- %if the \NLDROP has no preceding nodes, but has following nodes...
- \item{\verb+<g|p>[#*]/+$\NLDROP$}\\
+ \item{\verb+math[^#$]/+$\NLDROP$}\\
replace the $\NLDROP$ with the cursor.
- %rule handling the case where the $\NLDROP$ is the only child of a group with id.
- \item{\verb+g[@id][^#$]/+$\NLDROP$}\\
+
+ \item{\verb+g[^#$]/+$\NLDROP$}\\
replace the \G{} node with the $\NLDROP$.
- %\NLDROP is the first child of a macro with no inserted parameter
- \item{\verb+c[!(p[*])][^#]/+$\NLDROP$}\\
- replace the \CNODE{} with the $\NLDROP$.
- %\NLDROP is the first child of a macro with some inserted parameter
- \item{\verb+c[p[*]][^#]/+$\NLDROP$}\\
- put the cursor in the first \PNODE{} node.
-
-
- %**** rule handling the case where the \NLDROP has a preceding token or a preceding empty macro, which is either undefined or empty ****
-
- %%the \NLDROP's parent is neither a macro nor a phantom group which in turn is a sp's child and the token is a prime
- %\item{\verb+*[(i||n||o||s||c[^$])#]/+$\NLDROP$}\\
- %replace the \INODE{}, \NNODE{}, \SNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node with the cursor and remove the $\NLDROP$.
- %%the \NLDROP's parent is a macro with argument
- %\item{\verb+c[((!(p[@left-open='1']))&(!(p[@right-open+'1'])))][(i||n||o||s||c[^$])#]/+$\NLDROP$}\\
- %remove the $\NLDROP$ and insert it before the \INODE{}, \NNODE{}, \ONODE{}, \SNODE{} or \CNODE{} node.
- %%rule handling the case where the \NLDROP's parent is a phantom group, which in turn is a sp's child
- %\item{\verb+sp[!(@id)][^*#$]/g[!(@id)][o#$]/+$\NLDROP$}\\
- %remove the \ONODE{} node
-
- %********************************* rules handling the case where the \NLDROP has a preceding group **************************************
- \item{\verb+*[g#]/+$\NLDROP$}\\
- remove the $\NLDROP$ and append it to the \G{} node.
+
+ % this rule is overridden by the two ones below
+ \item{\verb+c/p[^#$]/+$\NLDROP$}\\
+ remove the $\NLDROP$ and insert it before the \PNODE{} node.
+
+ \item{\verb+c[p[@left-open='1'][*]#$]/p[@right-open='1'][^#$]/+$\NLDROP$}\\
+ replace the \CNODE{} node with the content of the first \PNODE{} node and insert the $\NLDROP$ after this content
+
+ \item{\verb+c[p[@left-open='1'][!*]#$]/p[@right-open='1'][^#$]/+$\NLDROP$}\\
+ replace the \CNODE{} node with the $\NLDROP$.
+
+ \item{\verb+c[^#][!p(*)]/+$\NLDROP$}\\
+ replace the \CNODE{} node with the $\NLDROP$.
+
+ \item{\verb+cell[^#$]/+$\NLDROP$}\\
+ replace the cell with the $\NLDROP_n$.
+
+ \item{\verb+table[^#$]/+$\NLDROP$}\\
+ replace the \TABLE{} node with the $\NLDROP$.
+
+ %************************* \NLDROP has at least one preceding node *********************
+
+ % general rules
+
+ % this rule should also handles the case where the \NLDROP is the third (and last) child of a script.
+ \item{\verb+*[*#]/+$\NLDROP$}\\
+ remove the $\NLDROP$ and append it as the last child of its ex preceding brother.
+
+ % this rule overrides the one above
+ \item{\verb+*[(i|n|o|s|c[!*])#]/+$\NLDROP$}\\
+ remove the $\NLDROP$ and replace the token with the $\NLDROP_n$.
+
+ % special rules
+
+ \item{\verb+<sp|sb>[^*#$]+/$\NLDROP$}\\
+ replace the script node with its first child and insert the $\NLDROP$ after it.
+
+ % this rule overrides the one above.
+ \item{\verb+<sp|sb>[^g[!@id][!*]#$]/+$\NLDROP$}\\
+ replace the script with the cursor.
+
+ % this rule overrides the one above
+ \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']++\verb+o[@name='prime']$]]#]/+$\NLDROP$}\\
+ remove the last \ONODE{} node and replace the $\NLDROP$ with the cursor.%$\NLDROP_n$.
+
+ \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']$]]#]/+$\NLDROP$}\\
+ replace the script with its first child and replace the $\NLDROP$ with the cursor.%$\NLDROP_n$.
+
+ \item{\verb+c[(i|n|o|s|c[!*])#]/+$\NLDROP$}\\
+ move the $\NLDROP$ before the delimiter.
+
+ % this rule is true for both right-open and parameterized macros.
+ \item{\verb+c[p#]/+$\NLDROP$}\\
+ move the $\NLDROP$ into the \PNODE{} node.
+
+ %**************** \NLDROP has no preceding nodes, but has following nodes **************
+
+ % general rule
+ \item{\verb+*[^#*]/+$\NLDROP$}\\
+ remove the $\NLDROP$ and insert it before its parent.
+
+ % special rules
+
+ % this rule is applicable to all macros.
+ \item{\verb+c[^#][p[*]]/+$\NLDROP$}\\
+ remove the $\NLDROP$ and insert it before the \CNODE{} node.
\end{description}
\begin{description}
- \item{special left}\\
+ %********************************************************************************************************
+ %************************************ epsilon-rules with \SLDROP ****************************************
+ %********************************************************************************************************
+
+ \item{\verb+math/+$\SLDROP$}\\
+ replace the $\SLDROP$ with the cursor.
+
+ \item{\verb+math/g[^#]/+$\NLDROP$}\\
+ replace the $\NLDROP$ with the cursor.
+
+ %************************ \SLDROP has neither preceding nor following nodes *****************************
+
+ \item{\verb+g[^#$]/+$\SLDROP$}\\
+ replace the \G{} node with the cursor.
+
+ \item{\verb+c[p[@left-open='1'][*]#$]/p[@right-open='1'][^#$]/+$\SLDROP$}\\
+ replace the \CNODE{} node with the content of the first \PNODE{} node and insert the cursor after this content
+
+ \item{\verb+c[p[@left-open='1'][!*]#$]/p[@right-open='1'][^#$]/+$\SLDROP$}\\
+ replace the \CNODE{} node with the cursor.
+
+ \item{\verb+c/p[^#$]/+$\SLDROP$}\\
+ remove the $\SLDROP$ and insert it before the \PNODE{} node.
+
+ \item{\verb+c[^#][!p(*)]/+$\SLDROP$}\\
+ replace the \CNODE{} node with the cursor.
+
+ \item{\verb+cell[^#$]/+$\SLDROP$}\\
+ replace the cell with the $\NLDROP_n$.
+
+ \item{\verb+table[^#$]/+$\SLDROP$}\\
+ replace the \TABLE{} node with the cursor.
+
+ %*********************** \SLDROP has at least one preceding node ***********************************
+
+ \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']++\verb+o[@name='prime']$]]#]/+$\SLDROP$}\\
+ remove the last \ONODE{} node and replace the $\SLDROP$ with the cursor.
+
+ \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']$]]#]/+$\SLDROP$}\\
+ replace the script with its first child and replace the $\SLDROP$ with the cursor.%$\NLDROP_n$.
+
+ \item{\verb+<sp|sb>[^g[!@id][!*]#$]/+$\SLDROP$}\\
+ replace the script with the cursor.
+
+ % this rule is overridden by the three rules above.
+ \item{\verb+<sp|sb>[^*#$]+/$\SLDROP$}\\
+ replace the script node with its first child and insert the cursor after it.
+
+ \item{\verb+c[(i|n|o|s|c[!*])#]/+$\SLDROP$}\\
+ remove the $\SLDROP$ and insert the cursor before the delimiter.
+
+ \item{\verb+c[p#(i|n|o|s|c[!*])]/+$\SLDROP$}\\
+ remove the $\SLDROP$ and insert the cursor into the \PNODE{} node.
+
+ \item{\verb+c[p[@right-open='1']#]+}\\
+ remove the $\SLDROP$ and append the curor as last child of the \PNODE{} node.
+
+ % this rule is overridden by the two ones above.
+ \item{\verb+c[p#]/+$\SLDROP$}\\
+ move the $\SLDROP$ into the \PNODE{} node.
+
+ \item{\verb+*[(i|n|o|s|c[!*])#]/+$\SLDROP$}\\
+ remove the $\SLDROP$ and replace the token with the cursor.
+
+ \item{\verb+*[table#]/+$\SLDROP$}\\
+ remove the $\SLDROP$ and append the $\NLDROP_n$ as the last child of the \TABLE{} node.
+
+ \item{\verb+*[c#]/+$\SLDROP$}\\
+ move the $\SLDROP$ into the \CNODE{} node.
+
+ \item{\verb+*[g#]/+$\SLDROP$}\\
+ remove the $\SLDROP$ and append the cursor as the last child of the \G{} node.
+
+ %********** \SLDROP has no preceding node, but has following ones **************
+
+ \item{\verb+c[^#p][p(*)]/+$\SLDROP$}\\
+ remove the $\SLDROP$ and insert the cursor before the \CNODE{} node.
+
+ % general rule
+ \item{\verb+*[^#*]/+$\SLDROP$}\\
+ remove the $\SLDROP$ and insert the cursor before its parent.
+
+\end{description}
+
+\paragraph{Normalize Left Drop}
+
+\begin{description}
+
+ %****************************************************************************************
+ %***************************** epsilon-rules with \NLDROP_n *****************************
+ %****************************************************************************************
+
+ \item{\verb+*[*#]/+$\NLDROP_n$}\\
+ replace the $\NLDROP_n$ with the cursor.
+
+ \item{\verb+row[cell#]/+$\NLDROP_n$}\\
+ remove the $\NLDROP_n$ and append the cursor as the last child of the \CELL{} node.
+
+ \item{\verb+row[^#$]/+$\NLDROP_n$}\\
+ replace the \ROW{} node with the $\NLDROP_n$
+
+ \item{\verb+table[row#]/+$\NLDROP_n$}\\
+ remove the $\NLDROP_n$ and append it as last child of the \ROW{} node.
+
+ \item{\verb+table[^#$]/+$\NLDROP_n$}\\
+ replace the \TABLE{} with the cursor.%$\NLDROP_n$.
+
+ \item{\verb+g[@id][^#$]/+$\NLDROP_n$}\\
+ replace the \G{} node with the $\NLDROP_n$.
+
+ \item{$\NLDROP_n$}\\
+ replace the $\NLDROP_n$ with the cursor.
+
+\end{description}
+
+\paragraph{Right Drop}
+
+\begin{description}
+
+ %************************* \RDROP has at least a following node ****************************************
+
+ \item{\verb+c[#(i|n|o|s|c[!*])]/+$\RDROP$}\\
+ remove the $\RDROP$ and append it after the delimiter
+
+ \item{\verb+*[#(i|n|o|s|c[!*])]/+$\RDROP$}\\
+ remove the token and replace the $\RDROP$ with the cursor $\RDROP_n$.
+
+ % this rule is overridden by those ones above.
+ \item{\verb+*[#*]/+$\RDROP$}\\
+ remove the $\RDROP$ and append it as the first child of the following node.
+
+ %************************** \RDROP has neither following nor preceding nodes ******************************
+
+ \item{\verb+c[#$][!p[*]]/+$\RDROP$}\\
+ replace the \CNODE{} with the $\RDROP$.
+
+ \item{\verb+p[^#$]/+$\RDROP$}\\
+ move the $\RDROP$ after the \PNODE{} node.
+
+ \item{\verb+g[^#$]/+$\RDROP$}\\
+ replace the \G{} node with the $\RDROP$.
+
+\end{description}
+
+\paragraph{Normalize Right Drop}
+
+\begin{description}
+
+ % at the moment it's the only rule, defined for this symbol.
+ \item{\verb+g[@id][^#$]/+$\RDROP_n$}\\
+ replace the \G{} node with the $\RDROP_n$.
+
+ \item{$\RDROP_n$}\\
+ replace the $\RDROP$ with the cursor.
\end{description}
% g[@id][^#$]/cursor <- cursor
% (!g[@id][^#$])[A#B]/(g[@id][^#$]/)+cursor <- (!g[@id][^#$])[A#B]/cursor
+\clearpage
+\appendix
+\section{Semantics of the Regular Context Language}
+
+\newcommand{\CSEM}[2]{\mathcal{C}\llbracket#1\rrbracket#2}
+\newcommand{\QSEM}[2]{\mathcal{Q}\llbracket#1\rrbracket#2}
+\newcommand{\TSEMUP}[2]{\mathcal{T}^\uparrow\llbracket#1\rrbracket#2}
+\newcommand{\TSEMDOWN}[2]{\mathcal{T}_\downarrow\llbracket#1\rrbracket#2}
+\newcommand{\NSEM}[2]{\mathcal{N}\llbracket#1\rrbracket#2}
+\newcommand{\PSEM}[1]{\mathcal{P}\llbracket#1\rrbracket}
+\newcommand{\LSEM}[2]{\mathcal{L}\llbracket#1\rrbracket#2}
+\newcommand{\RSEM}[2]{\mathcal{R}\llbracket#1\rrbracket#2}
+\newcommand{\FSEM}[2]{\mathcal{F}\llbracket#1\rrbracket(#2)}
+\newcommand{\PARENT}[1]{\mathit{parent}(#1)}
+\newcommand{\CHILDREN}[1]{\mathit{children}(#1)}
+\newcommand{\CHILD}[1]{\mathit{child}(#1)}
+\newcommand{\ANCESTORS}[1]{\mathit{ancestors}(#1)}
+\newcommand{\DESCENDANTS}[1]{\mathit{descendants}(#1)}
+\newcommand{\HASATTRIBUTE}[2]{\mathit{hasAttribute}(#1,#2)}
+\newcommand{\HASNOATTRIBUTE}[2]{\mathit{hasNoAttribute}(#1,#2)}
+\newcommand{\ATTRIBUTE}[2]{\mathit{attribute}(#1,#2)}
+\newcommand{\ISELEMENT}[1]{\mathit{isElement}(#1)}
+\newcommand{\NAME}[1]{\mathit{name}(#1)}
+\newcommand{\PREV}[1]{\mathit{prev}(#1)}
+\newcommand{\NEXT}[1]{\mathit{next}(#1)}
+\newcommand{\PREDICATE}[1]{\mathit{predicate}(#1)}
+\newcommand{\IFV}[3]{\begin{array}[t]{@{}l}\mathbf{if}~#1~\mathbf{then}\\\quad#2\\\mathbf{else}\\\quad#3\end{array}}
+\newcommand{\IFH}[3]{\mathbf{if}~#1~\mathbf{then}~#2~\mathbf{else}~#3}
+\newcommand{\TRUE}{\mathbf{true}}
+\newcommand{\FALSE}{\mathbf{false}}
+\newcommand{\FUN}[2]{\lambda#1.#2}
+\newcommand{\LET}[3]{\mathbf{let}~#1=#2~\mathbf{in}~#3}
+\newcommand{\REC}[2]{\mathbf{rec}~#1=#2}
+\newcommand{\APPLY}[2]{(#1\;#2)}
+\newcommand{\APPLYX}[3]{(#1\;#2\;#3)}
+\newcommand{\AND}{\wedge}
+\newcommand{\OR}{\vee}
+\newcommand{\AAND}{\,\vec{\AND}\,}
+\newcommand{\AOR}{\,\vec{\OR}\,}
+\newcommand{\MATCH}[4]{\begin{array}[t]{@{}c@{~\to~}l@{}l@{}}\multicolumn{2}{@{}l@{}}{\mathbf{match}~#1~\mathbf{with}}\\\phantom{|}\quad\{#2\}\\|\quad\emptyset\end{array}}
+
+\[
+\begin{array}{rcl}
+ \CSEM{q}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \QSEM{q}{x_1}\}\\
+ \CSEM{..}{x} &=& \PARENT{x}\\
+ \CSEM{/}{x} &=& \CHILDREN{x}\\
+ \CSEM{c_1\;c_2}{x} &=& \CSEM{c_2}{\CSEM{c_1}{x}}\\
+ \CSEM{(c)}{x} &=& \CSEM{c}{x}\\
+ \CSEM{\{c:\alpha\}}{x} &=& \alpha(x,\CSEM{c}{x})\\
+ \CSEM{c_1\&c_2}{x} &=& \CSEM{c_1}{x} \cap \CSEM{c_2}{x}\\
+ \CSEM{c_1\mid c_2}{x} &=& \CSEM{c_1}{x} \cup \CSEM{c_2}{x}\\
+ \CSEM{c+}{x} &=& \CSEM{c}{x} \cup \CSEM{c+}{\CSEM{c}{x}}\\
+ \CSEM{c?}{x} &=& \{x\}\cup\CSEM{c}{x}\\
+ \CSEM{c*}{x} &=& \CSEM{{c+}?}{x}\\[3ex]
+ \QSEM{c}{x} &=& \CSEM{c}{x}\ne\emptyset\\
+ \QSEM{!c}{x} &=& \CSEM{c}{x}=\emptyset\\
+ \QSEM{\langle*\rangle}{x} &=& \TRUE\\
+ \QSEM{\langle n\rangle}{x} &=& \NAME{x}=n\\
+ \QSEM{@n}{x} &=& \HASATTRIBUTE{x}{n}\\
+ \QSEM{@n=v}{x} &=& \ATTRIBUTE{x}{n}=v\\
+ \QSEM{[p_1\#p_2]}{x} &=& \LSEM{p_1}{\PREV{x}}\wedge\RSEM{p_2}{\NEXT{x}}\\[3ex]
+ \LSEM{}{\alpha} &=& \TRUE\\
+ \LSEM{\cent}{\alpha} &=& \alpha=\emptyset\\
+ \LSEM{p\;q}{\emptyset} &=& \FALSE\\
+ \LSEM{p\;q}{\{x\}} &=& \QSEM{q}{x}\wedge\LSEM{p}{\PREV{x}}\\[3ex]
+ \RSEM{}{\alpha} &=& \TRUE\\
+ \RSEM{\$}{\alpha} &=& \alpha=\emptyset\\
+ \RSEM{q\;p}{\emptyset} &=& \FALSE\\
+ \RSEM{q\;p}{\{x\}} &=& \QSEM{q}{x}\wedge\RSEM{p}{\NEXT{x}}\\[3ex]
+ \PREDICATE{q} &=& \TRUE\\
+ \PREDICATE{..} &=& \FALSE\\
+ \PREDICATE{/} &=& \FALSE\\
+ \PREDICATE{c_1\;c_2} &=& \PREDICATE{c_1}\wedge\PREDICATE{c_2}\\
+ \PREDICATE{(c)} &=& \PREDICATE{c}\\
+ \PREDICATE{c_1\&c_2} &=& \PREDICATE{c_1}\wedge\PREDICATE{c_2}\\
+ \PREDICATE{c_1\mid c_2} &=& \PREDICATE{c_1}\wedge\PREDICATE{c_2}\\
+ \PREDICATE{c+} &=& \PREDICATE{c}\\
+ \PREDICATE{c?} &=& \PREDICATE{c}\\
+ \PREDICATE{c*} &=& \PREDICATE{c}
+\end{array}
+\]
+
+\[
+\begin{array}{rcl}
+ \PSEM{q} &=& \FUN{x}{\APPLY{\QSEM{q}{}}{x}} \\
+ \PSEM{..} &=& \FUN{x}{\neg\APPLY{\mathit{null}}{\PARENT{x}}}\\
+ \PSEM{/} &=& \FUN{x}{\neg\APPLY{\mathit{null}}{\CHILD{x}}}\\
+ \PSEM{(c)} &=& \PSEM{c}\\
+ \PSEM{\{c:\alpha\}} &=& \FUN{x}{\APPLY{\PSEM{c}}{x}\AAND\APPLY{\alpha}{x}}\\
+ \PSEM{c_1\;c_2} &=& \IFV{\PREDICATE{c_1}}{\FUN{x}{(\PSEM{c_1}\;x)\wedge(\PSEM{c_2}\;x)}}{\FSEM{c_1}{\PSEM{c_2},\FUN{\_}{\FALSE}}}\\
+ \PSEM{c_1\&c_2} &=& \IFV{\PREDICATE{c_1}\wedge\PREDICATE{c_2}}{\FUN{x}{(\PSEM{c_1}\;x)\wedge(\PSEM{c_2}\;x)}}{\FSEM{c_1\&c_2}{\FUN{\_}{\TRUE},\FUN{\_}{\FALSE}}}\\
+ \PSEM{c_1\mid c_2} &=& \FUN{x}{(\PSEM{c_1}\;x)\vee(\PSEM{c_2}\;x)}\\
+ \PSEM{c+} &=& \PSEM{c}\\
+ \PSEM{c?} &=& \FUN{\_}{\TRUE}\\
+ \PSEM{c*} &=& \FUN{\_}{\TRUE}\\[3ex]
+ \FSEM{q}{t,f} &=& \FUN{x}{(\APPLY{\PSEM{q}}{x}\AAND\APPLY{t}{x})\AOR\APPLY{f}{x}}\\
+ \FSEM{..}{t,f} &=& \FUN{x}{\MATCH{\PARENT{x}}{y}{\APPLY{t}{y}}{\APPLY{f}{x}}}\\
+% \FSEM{/}{t,f} &=& \FUN{x}{(\vee_{y\in\CHILDREN{x}} \APPLY{t}{y})\AOR\APPLY{f}{x}}\\
+ \FSEM{/}{t,f} &=& \FUN{x}{\APPLYX{\mathit{exists}}{t}{\CHILD{x}}\AOR\APPLY{f}{x}}\\
+ \FSEM{(c)}{t,f} &=& \FSEM{c}{t,f}\\
+ \FSEM{\{c:\alpha\}}{t,f} &=& \FSEM{c}{\FUN{x}{\PSEM{c}\AAND\APPLY{\alpha}{x}\AAND\APPLY{t}{x},f}}\\
+ \FSEM{c_1\;c_2}{t,f} &=& \FUN{x}{\APPLY{\FSEM{c_1}{\FSEM{c_2}{t,\FUN{\_}{\APPLY{f}{x}}},f}}{x}}\\
+ \FSEM{c_1\&c_2}{t,f} &=& \FUN{x}{\APPLY{\FSEM{c_1}{\FUN{y}{\APPLY{\FSEM{c_2}{\FUN{z}{(y=z)\AAND\APPLY{t}{z}},\FUN{\_}{\APPLY{f}{x}}}}{x}},f}}{x}}\\
+ \FSEM{c_1\mid c_2}{t,f} &=& \FSEM{c_1}{t,\FSEM{c_2}{t,f}}\\
+ \FSEM{c+}{t,f} &=& \FSEM{c}{\FSEM{c+}{t,t},f}\\
+ \FSEM{c?}{t,f} &=& \FSEM{c}{t,t}\\
+ \FSEM{c*}{t,f} &=& \FSEM{{c+}?}{t,f}\\[3ex]
+ \QSEM{c}{} &=& \PSEM{c}\\
+ \QSEM{!c}{} &=& \FUN{x}{\neg\APPLY{\PSEM{c}}{x}}\\
+ \QSEM{\langle*\rangle}{} &=& \FUN{\_}{\TRUE}\\
+ \QSEM{\langle n\rangle}{} &=& \FUN{x}{\NAME{x}=n}\\
+ \QSEM{@n}{} &=& \FUN{x}{\HASATTRIBUTE{x}{n}}\\
+ \QSEM{@n=v}{} &=& \FUN{x}{\ATTRIBUTE{x}{n}=v}\\
+ \QSEM{[p_1\#p_2]}{} &=& \FUN{x}{\APPLY{\LSEM{p_1}{}}{\PREV{x}}\wedge\APPLY{\RSEM{p_2}{}}{\NEXT{x}}}\\[3ex]
+ \LSEM{}{} &=& \FUN{\_}{\TRUE}\\
+ \LSEM{\cent}{} &=& \mathit{null}\\
+ \LSEM{p\;q}{} &=& \FUN{x}{\MATCH{x}{y}{\QSEM{q}{y}\AAND\APPLY{\LSEM{p}}{\PREV{y}}}{\FALSE}}\\
+ \RSEM{}{} &=& \FUN{\_}{\TRUE}\\
+ \RSEM{\$}{} &=& \mathit{null}\\
+ \RSEM{p\;q}{} &=& \FUN{x}{\MATCH{x}{y}{\QSEM{q}{y}\AAND\APPLY{\RSEM{p}}{\NEXT{y}}}{\FALSE}}\\
+ \mathit{null} &=& \FUN{x}{\MATCH{x}{\_}{\FALSE}{\TRUE}}\\
+ \mathit{exists} &=& \FUN{t}{\REC{a}{\FUN{x}{\MATCH{x}{y}{\APPLY{t}{y}\AOR\APPLY{a}{\NEXT{x}}}{\FALSE}}}}
+\end{array}
+\]
+
+
+
\end{document}
projects / helm.git / blobdiff