]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/doc/spec.tex
ocaml 3.09 transition
[helm.git] / helm / DEVEL / mathml_editor / doc / spec.tex
index be9ba51bb68495a7dd80a18f213ae626b790cdb5..a9ccdc2637a59eefd9bc8c2f311e9073670eb86a 100644 (file)
@@ -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}
 
 
@@ -851,10 +852,13 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 \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{\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)}
@@ -864,42 +868,106 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 \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\}&#3\\|\quad\emptyset&#4\end{array}}
 
 \[
 \begin{array}{rcl}
-  \CSEM{.}{x} &=& \{x\}\\
+  \CSEM{q}{x} &=& \{x_1\mid x_1\in\{x\} \wedge \QSEM{q}{x_1}\}\\
   \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_1\;c_2}{x} &=& \CSEM{c_2}{\CSEM{c_1}{x}}\\
   \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]
-  \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}\\
+  \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}