* the documents passed to the ocaml binding have been turned into strings

[helm.git] / helm / DEVEL / mathml_editor / doc / spec.tex

diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex
index be9ba51bb68495a7dd80a18f213ae626b790cdb5..7849651d98a32d3693d23b1ccb831ef2b6e02dc1 100644 (file)
--- a/helm/DEVEL/mathml_editor/doc/spec.tex
+++ b/helm/DEVEL/mathml_editor/doc/spec.tex
@@ -200,22 +200,23 @@ The following tokens are defined:
 \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+>+  & & &\\
+  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 pattern language. $n$, $n_i$ denote names, $v$
-denotes a string enclosed in single or double quotes}
+\caption{Syntax of the regular context language. $n$, $n_i$ denote
+names, $v$ denotes a string enclosed in single or double quotes}
 \end{table}
 
 
@@ -872,13 +873,14 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
   \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:\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} &=& \CSEM{.\mid c}{x}\\
   \CSEM{c*}{x} &=& \CSEM{{c+}?}{x}\\
-  \CSEM{c_1\;c_2}{x} &=& \CSEM{c_2}{\CSEM{c_1}{x}}\\[3ex]
+  \CSEM{c_1\;c_2}{x} &=& \CSEM{c_2}{\CSEM{c_1}{x}}\\
+  \CSEM{!c}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \CSEM{c}{x}=\emptyset\}\\[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\\
@@ -889,16 +891,18 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
   \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}\\
+  \PSEM{p_1\#p_2}{x} &=& \PPSEM{p_1}{*,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},*}\\
+  \PSEM{\cent p_1\#p_2}{x} &=& \PPSEM{p_1}{\cent,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},*}\\
+  \PSEM{p_1\#p_2\$}{x} &=& \PPSEM{p_1}{*,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},\$}\\
+  \PSEM{\cent p_1\#p_2\$}{x} &=& \PPSEM{p_1}{\cent,\PREV{x}}\wedge\PPSEM{p_2}{\NEXT{x},\$}\\[3ex]
+  \PPSEM{}{*,\alpha} &=& \mathit{true}\\
+  \PPSEM{}{\cent,\alpha} &=& \alpha=\emptyset\\
+  \PPSEM{p\;c}{\alpha,\emptyset} &=& \mathit{false}\\
+  \PPSEM{p\;c}{\alpha,\{x\}} &=& \CSEM{c}{x}\ne\emptyset\wedge\PPSEM{p}{\alpha,\PREV{x}}\\
+  \PPSEM{}{\alpha,*} &=& \mathit{true}\\
+  \PPSEM{}{\alpha,\$} &=& \alpha=\emptyset\\
+  \PPSEM{c\;p}{\emptyset,\alpha} &=& \mathit{false}\\
+  \PPSEM{c\;p}{\{x\},\alpha} &=& \CSEM{c}{x}\ne\emptyset\wedge\PPSEM{p}{\NEXT{x},\alpha}\\
 \end{array}
 \]