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=c99c659090dd7d5bdaf7f91967aa60624436a07c;hpb=7bbc3826e7478e46a0802334cd1befa7d65e60db;p=helm.git diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex index c99c65909..a9ccdc263 100644 --- a/helm/DEVEL/mathml_editor/doc/spec.tex +++ b/helm/DEVEL/mathml_editor/doc/spec.tex @@ -858,6 +858,7 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \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)} @@ -870,9 +871,18 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \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}{\mathit{true}} -\newcommand{\FALSE}{\mathit{false}} +\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} @@ -885,29 +895,23 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \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} &=& \{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{.}{x} &=& \TRUE\\ - \QSEM{\langle*\rangle}{x} &=& \ISELEMENT{x}\\ - \QSEM{\langle n\rangle}{x} &=& \ISELEMENT{x}\wedge\NAME{x}=n\\ - \QSEM{@n}{x} &=& \ISELEMENT{x}\wedge\HASATTRIBUTE{x}{n}\\ - \QSEM{@n=v}{x} &=& \ISELEMENT{x}\wedge\ATTRIBUTE{x}{n}=v\\ - \QSEM{[p_1\#p_2]}{x} &=& \ISELEMENT{x}\wedge\LSEM{p_1}{\PREV{x}}\wedge\RSEM{p_2}{\NEXT{x}}\\[3ex] + \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} &=& \mathit{false}\\ + \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} &=& \mathit{false}\\ - \RSEM{q\;p}{\{x\}} &=& \QSEM{q}{x}\wedge\RSEM{p}{\NEXT{x}}\\ -\end{array} -\] - -\[ -\begin{array}{rcl} + \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\\ @@ -923,27 +927,47 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node \[ \begin{array}{rcl} - \PSEM{q} &=& \FUN{x}{\QSEM{q}{x}} \\ - \PSEM{..} &=& \FUN{x}{\PARENT{x}\ne\emptyset}\\ - \PSEM{/} &=& \FUN{x}{\CHILDREN{x}\ne\emptyset}\\ - \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}}}\\ + \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_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}}}\\ + \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}{l} &=& \FUN{x}{\IFH{(\PSEM{q}\;x)}{(l\;x)}{\FALSE}}\\ - \FSEM{..}{l} &=& \FUN{x}{\IFH{\PARENT{x}=\{y\}}{(l\;y)}{\FALSE}}\\ - \FSEM{/}{l} &=& \FUN{x}{\vee_{p\in\CHILDREN{x}} (l\;p)}\\ - \FSEM{(c)}{l} &=& \FSEM{c}{l}\\ - \FSEM{c_1\;c_2}{l} &=& \FSEM{c_1}{\FSEM{c_2}{l}}\\ - \FSEM{c_1\&c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{\FUN{y}{(l\;y)\wedge(\FSEM{c_2}{\FUN{z}{z=y}}\;x)}}\;x)}\\ - \FSEM{c_1\mid c_2}{l} &=& \FUN{x}{(\FSEM{c_1}{l}\;x)\vee(\FSEM{c_2}{l}\;x)}\\ - \FSEM{c+}{l} &=& \FSEM{c}{\FUN{y}{(l\;y)\vee(\FSEM{c+}{l}\;y)}}\\ - \FSEM{c?}{l} &=& \FUN{x}{(l\;x)\vee(\FSEM{c}{l}\;x)}\\ - \FSEM{c*}{l} &=& \FSEM{{c+}?}{l}\\ + \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}