X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fmathml_editor%2Fdoc%2Fspec.tex;h=a9ccdc2637a59eefd9bc8c2f311e9073670eb86a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=4495c805e32d13b9fc90cbeb52a637e1c8961be7;hpb=0593f47412b947a4af005b2ccec2eb13dd8dee90;p=helm.git diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex index 4495c805e..a9ccdc263 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} @@ -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,29 @@ 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 &::=& \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:} $\{$ @@ -524,12 +549,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 +577,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 +639,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 +656,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 +713,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 +724,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 +759,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 +843,131 @@ 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}[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}