From: Paolo Marinelli <paolo.marinelli@unibo.it>
Date: Sat, 29 Mar 2003 20:43:35 +0000 (+0000)
Subject: Removed many rules in the "Left Drop" section. Every epsilon-rule in the
X-Git-Tag: before_refactoring~79
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=28edc4349551681f63c8491eb09b163b5dedd875;p=helm.git

Removed many rules in the "Left Drop" section. Every epsilon-rule in the
normal left drop paragraph has been changed.
---

diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex
index 1a99fdbd0..3e3964272 100644
--- a/helm/DEVEL/mathml_editor/doc/spec.tex
+++ b/helm/DEVEL/mathml_editor/doc/spec.tex
@@ -26,11 +26,13 @@
 \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}} % at the moment it's not used.
+\newcommand{\NLDMACRO}{\vartriangleleft_{c}}
+\newcommand{\NLDTABLE}{\vartriangleleft_{t}}
 
 \begin{document}
 
@@ -410,105 +412,135 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 
 \begin{description}
 
-  % in the rules below, a token is either an i node, an n node, an o node, an s node or an empty c node.
-  % an empty c node is either an undefined macro or an empty macro. These c node are handled as they actually were 
-  % tokens (i, n, o, s).
-  % An important observation is: a sequence of groups with id, in which every group has one and only one child and where 
-  % the last group contains the cursor, is equivalent to the cursor (Is it clear?). For example:
-  % <g id="id1"><g id="id2">...<g id="idn"><cursor/></g>...</g></g> is equivalent to:
-  % <cursor/>
+  \item{\verb+cursor+}\\
+  replace the cursor with the $\NLDROP$.
 
-  %************************************************************************************************************
-  %************************** there is at least one node preceding the cursor *********************************
-  %************************************************************************************************************
+\end{description}
 
-  %************************** cursor's parent is a group or a parameter (p node).
+\paragraph{Special Left Drop:} $\SLDROP$
 
-  \item{\verb+<g|p>[(i|n|o|s|c[!*])#]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and replace the token with the cursor.
-  
-  \item{\verb+g[@id][(i|n|o|s|c[!*])#]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and replace the token with the $\RGROUP$.
+\begin{description}
 
-  \item{\verb+<g|p>[g#]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and append $\NLDGP$ to the \G{} node preceding the cursor.
+  %*******************************************************************************************************
+  %************** rules handling the case in which the cursor has a preceding node ***********************
+  %*******************************************************************************************************
 
-  \item{\verb+<g|p>[<sp|sb>#]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and append the $\NLDSCRIPT$ to script node.
+  %************** cursor's parent is a group or a parameter (a p node)
 
-  \item{\verb+<g|p>[c[p[@right-open="1"]$]#]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and apeend the $\NLDGP$ to the \PNODE{} node.
+  \item{\verb+<g|p>[(i|n|o|s|c[!*])#]/cursor+}\\
+  remove the token.
 
-  % we don't have this kind of macro
-  %\item{\verb+<g|p>[c[^p[@left-open="1"]$]#]/(g[@id][^#$]/++\verb+)?cursor+}\\
+  \item{\verb+<g|p>[g#]/cursor+}\\
+  remove the cursor and append it to the \G{} node.
 
-  \item{\verb+<g|p>[c[p[!@left-open="1"][!@right-open="1"](c[!*]|i|n|o|s)*$]#]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and append the $\NLDGP$ to the \PNODE{} node.
+  \item{\verb+<g|p>[<sp|sb>#]cursor+}\\
+  remove the cursor and append the $\SLDSCRIPT$
 
-  \item{\verb+*[sp[^*g[!@id][^o[@name="prime"]$]]#]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  replace (if present) the sequence of \G{} nodes with attribute \texttt{id} with the cursor and replace the \SP{} node with its first child.
+  \item{\verb+<g|p>[c[p[@right-open="1"]$]#]/cursor+}\\
+  remove the cursor and append the it to the \PNODE{} node.
 
-  \item{\verb+*[sp[^*g[!@id][^o[@name="prime"]++\verb+o[@name="prime"]$]]#]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  replace (if present) the sequence of \G{} nodes with attribute \texttt{id} with the cursor and remove the last \ONODE{}, which is \G{} node's child.
+  % remember to add the rules handling the primes
 
-  %************************************ cursor's parent is a script
+  %*************************************************************************************************
+  %*********** rules handling the case in which the cursor has no preceding nodes ******************
+  %*************************************************************************************************
 
-  \item{\verb+<g|p>/<sp|sb>[(i|n|o|s|c[!*])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  remove replace the script with the cursor.
+  \item{\verb+g[@id][^#$]/cursor+}\\
+  replace the \G{} node with the cursor.
 
-  \item{\verb+g[@id]/<sp|sb>[(i|n|o|s|c[!*])#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  replace the script with the $\RGROUP$.
+\end{description}
 
-  \item{\verb+<sp|sb>[g#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  repalce the script with it's first child (the \G{} node) and append the $\NLDGP$ to it.
+\section{Right Drop Rules}
 
-  \item{\verb+<sp|sb>[^c[p[@right-open="1"]$]#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  remove the cursor (and eventually the sequence of \G{} nodes with attribute \texttt{id}) and append the $\NLDGP$ to the \PNODE{} node.
+\section{$\varepsilon$-rules}
 
-  % we don't have a macro of this kind
-  %\item{\verb+<sp|sb>[^c[^p[@left-open="1"]$]#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
+\paragraph{Nromal Left Drop}
 
-  \item{\verb+<sp|sb>[^c[p[!@left-open="1"][!@right-open="1"](c[!*]|i|n|o|s)*$]#$]/(g[@id][^#$]/++\verb+)?cursor+}\\
-  replace the script with the \CNODE{} node and append the $\NLDGP$ to the \PNODE{} node.
+\begin{description}
 
-\end{description}
+  %**************************************************************************************
+  %****************************** epsilon-rules with \NLDROP ****************************
+  %**************************************************************************************
 
-\paragraph{Special Left Drop:} $\SLDROP$
+  %***************************** \NLDROP has no preceding nodes *************************
 
-%\begin{description}
+  \item{\verb+g[^#$]/+$\NLDROP$}\\
+  replace the \G{} node with the $\NLDROP$.
 
-  %*******************************************************************************************************
-  %************** rules handling the case in which the cursor has a preceding node ***********************
-  %*******************************************************************************************************
+  \item{\verb+c/p[^#$]/+$\NLDROP$}\\
+  remove the $\NLDROP$ and insert it before the \PNODE{} node.
 
-  %*************************************************************************************************
-  %*********** rules handling the case in which the cursor has no preceding nodes ******************
-  %*************************************************************************************************
+  \item{\verb+cell[^#$]/+$\NLDROP$}\\
+  replace the cell with the $\NLDROP_n$.
 
-%\end{description}
+  \item{\verb+table[^#$]/+$\NLDROP$}\\
+  replace the \TABLE{} node with the $\NLDROP$.
 
-\section{Right Drop Rules}
+  \item{\verb+c[p[@left-open='1'][*]#$]/p[@right-open='1'][^#$]/+$\NLDROP$}\\
+  replace the \CNODE{} node with the content of the first \PNODE{} node and insert the $\NLDROP$ after this content
 
-\section{$\varepsilon$-rules}
+  \item{\verb+c[p[@left-open='1'][!*]#$]/p[@right-open='1'][^#$]/+$\NLDROP$}\\
+  replace the \CNODE{} node with the $\NLDROP$.
 
-\paragraph{Nromal Left Drop}
+  \item{\verb+c[^#][!p(*)]/+$\NLDROP$}\\
+  replace the \CNODE{} node with the $\NLDROP$.
 
-\begin{description}
+  %************************* \NLDROP has at least one preceding node *********************
+
+  % general rules
+
+  % this rule should also handle the case where the \NLDROP is the third (and last) child of a script.
+  \item{\verb+*[*#]/+$\NLDROP$}\\
+  remove the $\NLDROP$ and append it as the last child of its ex preceding brother.
+
+  % this rule overrides the one above
+  \item{\verb+*[<i|n|o|s>#]/+$\NLDROP$}\\
+  remove the $\NLDROP$ and replace the token with the $\NLDROP_n$.
+
+  % special rules
+
+  \item{\verb+<sp|sb>[^*#$]+/$\NLDROP$}\\
+  replace the script node with its first child and insert the $\NLDROP$ after it.
+
+  % this rule overrides the one above.
+  \item{\verb+<sp|sb>[^g[!@id][!*]#$]/+$\NLDROP$}\\
+  replace the script with the cursor.
+
+  % this rule overrides the one above
+  \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']++\verb+o[@name='prime']$]]#]/+$\NLDROP$}\\
+  remove the last \ONODE{} node and replace the $\NLDROP$ with the %$\NLDROP_n$.
+
+  \item{\verb+*[sp[!@id][^*g[!@id][^o[@name='prime']$]]#]/+$\NLDROP$}\\
+  replace the script with its first child and replace the $\NLDROP$ with the cursor.%$\NLDROP_n$.
+
+  \item{\verb+c[(i|n|o|s|c[!*])#]/+$\NLDROP$}\\
+  move the $\NLDROP$ before the delimiter.
+
+  % this rule is true for both right-open and parameterized macros.
+  \item{\verb+c[p#]/+$\NLDROP$}\\
+  move the $\NLDROP$ into the \PNODE{} node.
+
+  %****************************************************************************************
+  %***************************** epsilon-rules with \NLDROP_n *****************************
+  %****************************************************************************************
+
+  \item{\verb+*[*#]/+$\NLDROP_n$}\\
+  replace the $\NLDROP_n$ with the cursor.
 
-  %********************* epsilon rules concerning the rgreplace_father ********************
+  \item{\verb+row[cell#]/+$\NLDROP_n$}\\
+  remove the $\NLDROP_n$ and append the cursor as the last child of the \CELL{} node.
 
-  \item{\verb+(g[@id][^#$]/++\verb+)+$\RGROUP$}\\
-  replace the whole fragment with the cursor.
+  \item{\verb+row[^#$]/+$\NLDROP_n$}\\
+  replace the \ROW{} node with the $\NLDROP_n$
 
-  \item{\verb+*[!@id]/+$\RGROUP$}\\
-  replace the $\RGROUP$ with the cursor.
+  \item{\verb+table[row#]/+$\NLDROP_n$}\\
+  remove the $\NLDROP_n$ and append it as last child of the \ROW{} node.
 
-  \item{\verb+g[@id][*#]/+$\RGROUP$}\\
-  replace the $\RGROUP$ with the cursor
+  \item{\verb+table[^#$]/+$\NLDROP_n$}\\
+  replace the \texttt{table} with the cursor.$\NLDROP_n$.
 
-  \item{\verb+g[@id][#*]/+$\RGROUP$}\\
-  replace the $\RGROUP$ with the cursor.
-  % maybe it's not the correct action
+  \item{\verb+g[@id][^#$]/+$\NLDROP_n$}\\
+  replace the \G{} node with the $\NLDROP_n$.
 
 \end{description}