\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\verb+/+ & Q &::=& T & P &::=& P' \\
+ &|& Q\verb+//+ & &|& Q\verb+[@+n\verb+=+v\verb+]+ & &|& \verb+^+P'\\
+ &|& \verb+(+C\verb+)+ & &|& Q\verb+[!@+n\verb+=+v\verb+]+ & &|& P'\verb+$+\\%$
+ &|& (\alpha\verb+=+C) & &|& Q\verb+[@+n\verb+]+ & &|& \verb+^+P'\verb+$+\\%$
+ &|& C_1 \verb+&+ C_2 & &|& Q\verb+[+P\verb+]+ & & &\\
+ &|& C_1 \verb+|+ C_2 & & & & P' &::=& P''\\
+ &|& C\verb.+. & T &::=& N & &|& P''\verb+#+P''\\
+ &|& C\verb+*+ & &|& C N & & &\\
+ &|& C\verb+?+ & & & & P'' &::=& \\
+ &|& C_1~C_2 & N &::=& \verb+<*>+ & &|& T\;P''\\
+ &|& \verb+!+C & &|& \verb+<+n_1\verb+|+\cdots\verb+|+n_2\verb+>+ & & &\\
+ & & & &|& \verb+<!+n_1\verb+|+\cdots\verb+|+n_2\verb+>+ & & &\\
+\end{array}
+\]
+\caption{Syntax of the pattern 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{\alpha(c)}{x} &=& \CSEM{c}{x}, \mbox{bind $\alpha$ to $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}}\\[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}{*,x}\wedge\PPSEM{p_2}{x,*}\\
+ \PSEM{\cent p_1\#p_2}{x} &=& \PPSEM{p_1}{\cent,x}\wedge\PPSEM{p_2}{x,*}\\
+ \PSEM{p_1\#p_2\$}{x} &=& \PPSEM{p_1}{*,x}\wedge\PPSEM{p_2}{x,\$}\\
+ \PSEM{\cent p_1\#p_2\$}{x} &=& \PPSEM{p_1}{\cent,x}\wedge\PPSEM{p_2}{x,\$}\\[3ex]
+ \PPSEM{}{*,x} &=& \mathit{true}\\
+ \PPSEM{}{\cent,x} &=& \PREV{x}=\emptyset\\
+ \PPSEM{}{x,*} &=& \mathit{true}\\
+ \PPSEM{}{x,\$} &=& \NEXT{x}=\emptyset\\
+ \PPSEM{p\;c}{\alpha,x} &=& \CSEM{c}{\PREV{x}}\ne\emptyset\wedge\PPSEM{p}{\alpha,\PREV{x}}\\
+ \PPSEM{c\;p}{x,\alpha} &=& \CSEM{c}{\NEXT{x}}\ne\emptyset\wedge\PPSEM{p}{\NEXT{x},\alpha}\\
+\end{array}
+\]
+
\end{document}
projects / helm.git / blobdiff