]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/doc/spec.tex
* major update in regular context language definition and semantics
[helm.git] / helm / DEVEL / mathml_editor / doc / spec.tex
index 4495c805e32d13b9fc90cbeb52a637e1c8961be7..be9ba51bb68495a7dd80a18f213ae626b790cdb5 100644 (file)
@@ -5,6 +5,7 @@
 \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}
@@ -29,6 +30,7 @@
 \newcommand{\ROW}{\texttt{row}}
 \newcommand{\SLDROP}{\blacktriangleleft}
 \newcommand{\NLDROP}{\vartriangleleft}
+\newcommand{\RDROP}{\vartriangleright}
 
 \begin{document}
 
@@ -179,7 +181,7 @@ 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{*} \\
@@ -195,6 +197,28 @@ The following tokens are defined:
 %%   & | & \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:} $\{$
@@ -524,12 +548,22 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 
 \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 ****************************
   %**************************************************************************************
@@ -542,10 +576,6 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
   \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.
@@ -608,9 +638,6 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} 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.
@@ -628,11 +655,10 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} 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.
@@ -686,7 +712,7 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
   \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$}\\
@@ -697,9 +723,6 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 
   %********** \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.
 
@@ -735,6 +758,51 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} 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}
@@ -774,4 +842,64 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 % 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}