\usepackage{euler}
\usepackage{amssymb}
\usepackage{stmaryrd}
+\usepackage{wasysym}
\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}
\newcommand{\ROW}{\texttt{row}}
\newcommand{\SLDROP}{\blacktriangleleft}
\newcommand{\NLDROP}{\vartriangleleft}
+\newcommand{\RDROP}{\vartriangleright}
\begin{document}
\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:} $\{$
\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}
+ \item{\verb+math/g[^#]/+$\NLDROP$}\\
+ repalce the $\NLDROP$ with the cursor.
+
%**************************************************************************************
%****************************** epsilon-rules with \NLDROP ****************************
%**************************************************************************************
\item{\verb+g[^#$]/+$\NLDROP$}\\
replace the \G{} node with the $\NLDROP$.
- % this rule overrides the one above
- \item{\verb+math/g[^#$]/+$\NLDROP$}\\
- replace the $\NLDROP$ with the cursor.
-
% this rule is overridden by the two ones below
\item{\verb+c/p[^#$]/+$\NLDROP$}\\
remove the $\NLDROP$ and insert it before the \PNODE{} node.
% special rules
- \item{\verb+math/g[^#*]/+$\NLDROP$}\\
- replace the $\NLDROP$ with the cursor.
-
% this rule is applicable to all macros.
\item{\verb+c[^#][p[*]]/+$\NLDROP$}\\
remove the $\NLDROP$ and insert it before the \CNODE{} node.
\item{\verb+math/+$\SLDROP$}\\
replace the $\SLDROP$ with the cursor.
- %************************ \SLDROP has neither preceding nor following nodes *****************************
+ \item{\verb+math/g[^#]/+$\NLDROP$}\\
+ replace the $\NLDROP$ with the cursor.
- % this rule overrides the one below
- \item{\verb+math/g[^#$]/+$\SLDROP$}\\
- replace the $\SLDROP$ with the cursor.
+ %************************ \SLDROP has neither preceding nor following nodes *****************************
\item{\verb+g[^#$]/+$\SLDROP$}\\
replace the \G{} node with the cursor.
\item{\verb+*[(i|n|o|s|c[!*])#]/+$\SLDROP$}\\
remove the $\SLDROP$ and replace the token with the cursor.
- \item{\verb+*[table#]/$\SLDROP$+}\\
+ \item{\verb+*[table#]/+$\SLDROP$}\\
remove the $\SLDROP$ and append the $\NLDROP_n$ as the last child of the \TABLE{} node.
\item{\verb+*[c#]/+$\SLDROP$}\\
%********** \SLDROP has no preceding node, but has following ones **************
- \item{\verb+math/g[^#*]/+$\SLDROP$}\\
- replace the $\SLDROP$ with the cursor.
-
\item{\verb+c[^#p][p(*)]/+$\SLDROP$}\\
remove the $\SLDROP$ and insert the cursor before the \CNODE{} node.
\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}
\paragraph{Advance}
% 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}[2]{\mathcal{P}\llbracket#1\rrbracket#2}
+\newcommand{\PPSEM}[2]{\mathcal{P'}\llbracket#1\rrbracket(#2)}
+\newcommand{\PARENT}[1]{\mathit{parent}(#1)}
+\newcommand{\CHILDREN}[1]{\mathit{children}(#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)}
+
+\[
+\begin{array}{rcl}
+ \CSEM{.}{x} &=& \{x\}\\
+ \CSEM{..}{x} &=& \PARENT{x}\\
+ \CSEM{/}{x} &=& \CHILDREN{x}\\
+ \CSEM{q}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \QSEM{q}{x_1}\}\\
+ \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} &=& \CSEM{.\mid c}{x}\\
+ \CSEM{c*}{x} &=& \CSEM{{c+}?}{x}\\
+ \CSEM{c_1\;c_2}{x} &=& \CSEM{c_2}{\CSEM{c_1}{x}}\\
+ \CSEM{!c}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \CSEM{c}{x}=\emptyset\}\\[3ex]
+ \QSEM{\langle*\rangle}{x} &=& \ISELEMENT{x}\\
+ \QSEM{\langle!*\rangle}{x} &=& \neg\QSEM{\langle*\rangle}{x}\\
+ \QSEM{\langle n_1\mid\cdots\mid n_k\rangle}{x} &=& \exists i\in\{1,\dots,k\}:\NAME{x}=n_i\\
+ \QSEM{\langle !n_1\mid\cdots\mid n_k\rangle}{x} &=& \neg\QSEM{\langle n_1\mid\cdots\mid n_k\rangle}{x}\\
+ \QSEM{q[@n]}{x} &=& \QSEM{q}{x} \wedge \HASATTRIBUTE{x}{n}\\
+ \QSEM{q[!@n]}{x} &=& \QSEM{q}{x} \wedge \HASNOATTRIBUTE{x}{n}\\
+ \QSEM{q[@n=v]}{x} &=& \QSEM{q}{x} \wedge \ATTRIBUTE{x}{n}= v\\
+ \QSEM{q[!@n=v]}{x} &=& \QSEM{q}{x} \wedge \ATTRIBUTE{x}{n}\ne v\\
+ \QSEM{q[p]}{x} &=& \QSEM{q}{x} \wedge \PSEM{p}{x}\\
+ \QSEM{q[!p]}{x} &=& \QSEM{q}{x} \wedge \neg\PSEM{p}{x}\\[3ex]
+ \PSEM{p_1\#p_2}{x} &=& \PPSEM{p_1}{*,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},*}\\
+ \PSEM{\cent p_1\#p_2}{x} &=& \PPSEM{p_1}{\cent,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},*}\\
+ \PSEM{p_1\#p_2\$}{x} &=& \PPSEM{p_1}{*,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},\$}\\
+ \PSEM{\cent p_1\#p_2\$}{x} &=& \PPSEM{p_1}{\cent,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},\$}\\[3ex]
+ \PPSEM{}{*,\alpha} &=& \mathit{true}\\
+ \PPSEM{}{\cent,\alpha} &=& \alpha=\emptyset\\
+ \PPSEM{p\;c}{\alpha,\emptyset} &=& \mathit{false}\\
+ \PPSEM{p\;c}{\alpha,\{x\}} &=& \CSEM{c}{x}\ne\emptyset\wedge\PPSEM{p}{\alpha,\PREV{x}}\\
+ \PPSEM{}{\alpha,*} &=& \mathit{true}\\
+ \PPSEM{}{\alpha,\$} &=& \alpha=\emptyset\\
+ \PPSEM{c\;p}{\emptyset,\alpha} &=& \mathit{false}\\
+ \PPSEM{c\;p}{\{x\},\alpha} &=& \CSEM{c}{x}\ne\emptyset\wedge\PPSEM{p}{\NEXT{x},\alpha}\\
+\end{array}
+\]
+
\end{document}
projects / helm.git / blobdiff