X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fmathml_editor%2Fdoc%2Fspec.tex;h=be9ba51bb68495a7dd80a18f213ae626b790cdb5;hb=ced0086b4bb5b10e6c4a8268ea781624a41394dd;hp=ed95dcf14c7647c905b1b06dbfa27af06bf8d59d;hpb=ef1b1369e26bdae74fb721abe4cd51c954ef48f6;p=helm.git diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex index ed95dcf14..be9ba51bb 100644 --- a/helm/DEVEL/mathml_editor/doc/spec.tex +++ b/helm/DEVEL/mathml_editor/doc/spec.tex @@ -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} @@ -28,13 +29,8 @@ \newcommand{\CELL}{\texttt{cell}} \newcommand{\ROW}{\texttt{row}} \newcommand{\SLDROP}{\blacktriangleleft} -\newcommand{\SLDSCRIPT}{\blacktriangleleft_{s}} \newcommand{\NLDROP}{\vartriangleleft} -\newcommand{\RGROUP}{\vartriangleleft_{rg}} -\newcommand{\NLDGP}{\vartriangleleft_{g}} -\newcommand{\NLDSCRIPT}{\vartriangleleft_{s}} -\newcommand{\NLDMACRO}{\vartriangleleft_{c}} -\newcommand{\NLDTABLE}{\vartriangleleft_{t}} +\newcommand{\RDROP}{\vartriangleright} \begin{document} @@ -185,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{*} \\ @@ -201,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++ & & &\\ +\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:} $\{$ @@ -530,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 **************************** %************************************************************************************** @@ -548,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. @@ -614,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. @@ -634,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. @@ -692,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$}\\ @@ -703,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. @@ -741,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} @@ -780,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}