From: Stefano Zacchiroli Date: Thu, 6 Oct 2005 15:43:34 +0000 (+0000) Subject: completed instantiatian of level 2 patterns from level 1 X-Git-Tag: V_0_7_2_3~236 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d821b9ee4b55dffa907307b24e2df969779331fc;p=helm.git completed instantiatian of level 2 patterns from level 1 --- diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex index 9885e5420..4d0ccbec2 100644 --- a/helm/ocaml/cic_notation/doc/main.tex +++ b/helm/ocaml/cic_notation/doc/main.tex @@ -22,10 +22,11 @@ \newcommand{\IVAR}[1]{#1:\mathtt{name}} \newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}} \newcommand{\ITO}[2]{|[#1|]_{\mathcal#2}^1} -\newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^2} +\newcommand{\IOT}[2]{|[#1|]_{#2}^2} \newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}} \newcommand{\NAMES}{\mathit{names}} \newcommand{\DOMAIN}{\mathit{domain}} +\newcommand{\UPDATE}[2]{#1[#2]} \mathlig{~>}{\leadsto} \mathlig{|->}{\mapsto} @@ -135,7 +136,7 @@ used in different contexts. \] \begin{table} -\caption{\label{tab:il1} Instantiation of level 1 patterns.\strut} +\caption{\label{tab:il1f2} Instantiation of level 1 patterns from level 2.\strut} \hrule \[ \begin{array}{rcll} @@ -404,61 +405,96 @@ used in different contexts. \end{table} \begin{table} -\caption{...} + \caption{\label{tab:il2f1} Instantiation of level 2 patterns from level 1. + \strut} \hrule \[ \begin{array}{rcll} -\IOT{C[t_1,\dots,t_n]}{E} & = & C[\IOT{t_1}{E},\dots,\IOT{t_n}{E}] \\ -\IOT{\mathtt{term}~x}{E} & = & t & \mathcal{E}(x) = \mathtt{Term}~t \\ -\IOT{\mathtt{number}~x}{E} & = & n & \mathcal{E}(x) = \mathtt{Number}~n \\ -\IOT{\mathtt{ident}~x}{E} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\ -\IOT{\mathtt{fresh}~x}{E} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\ -\IOT{\mathtt{default}~P_1~P_2}{E} & = & \IOT{P_2}{E'} & \mathcal{E}(\NAMES(P_1)\setminus\NAMES(P_2)))=\{\mathtt{None}\} \\ -& & & \mathcal{E}'(x) = - \left\{ - \begin{array}{@{}ll} - \bot & x \in \NAMES(P_1)\setminus\NAMES(P_2) \\ - \mathcal{E}(x) & \mbox{otherwise} \\ - \end{array} - \right. \\ -\IOT{\mathtt{default}~P_1~P_2}{E} & = & \IOT{P_2}{E'} & \mathcal{E}(\NAMES(P_1)\setminus\NAMES(P_2)))=\{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\ -& & & \mathcal{E}'(x) = - \left\{ - \begin{array}{@{}ll} - v & x \in \NAMES(P_1)\setminus\NAMES(P_2) \wedge \mathcal{E}(x) = \mathtt{Some}~v\\ - \mathcal{E}(x) & \mbox{otherwise} - \end{array} - \right. \\ -\IOT{\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2}{E} + +\IOT{C[t_1,\dots,t_n]}{\mathcal{E}} & = +& C[\IOT{t_1}{\mathcal{E}},\dots,\IOT{t_n}{\mathcal{E}}] \\ + +\IOT{\mathtt{term}~x}{\mathcal{E}} & = & t & \mathcal{E}(x) = \mathtt{Term}~t \\ + +\IOT{\mathtt{number}~x}{\mathcal{E}} & = +& n & \mathcal{E}(x) = \mathtt{Number}~n \\ + +\IOT{\mathtt{ident}~x}{\mathcal{E}} & = +& y & \mathcal{E}(x) = \mathtt{String}~y \\ + +\IOT{\mathtt{fresh}~x}{\mathcal{E}} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\ + +\IOT{\mathtt{default}~P_1~P_2}{\mathcal{E}} & = +& \IOT{P_1}{\UPDATE{\mathcal{E}}{x_i|->v_i}} +& \mathcal{E}(x_i)=\mathtt{Some}~v_i \\ +& & & \NAMES(P_1)\setminus\NAMES(P_2)=\{x_1,\dots,x_n\} \\ + +\IOT{\mathtt{default}~P_1~P_2}{\mathcal{E}} & = +& \IOT{P_2}{\UPDATE{\mathcal{E}}{x_i|->\bot}} +& \mathcal{E}(x_i)=\mathtt{None} \\ +& & & \NAMES(P_1)\setminus\NAMES(P_2)=\{x_1,\dots,x_n\} \\ + +\IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}} & = -& \IOT{P_2}{E'} -& \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[]\} \\ -& & & \mathcal{E}'(y) = - \left\{ - \begin{array}{@{}ll} - \bot & y \in \NAMES(P_2)\setminus\{x\} \\ - \mathcal{E}(y) & \mbox{otherwise} \\ - \end{array} - \right. \\ -\IOT{\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2}{E} +& \IOT{P_1}{\mathcal{E}'} +& \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[],\dots,[]\} \\ +& & \multicolumn{2}{l}{\mathcal{E}'=\UPDATE{\mathcal{E}}{\NAMES(P_2)\setminus\{x\}|->\bot}} +\\ + +\IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}} & = -& \IOT{P_2}{E'} -& \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\ -& & & \mathcal{E}'(y) = +& \IOT{P_2}{\mathcal{E}'} +& \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\ +& & & \NAMES(P_2)\setminus\{x\}=\{y_1,\dots,y_m\} \\ +& & \multicolumn{2}{l}{\mathcal{E}'(y) = \left\{ \begin{array}{@{}ll} - \IOT{\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_e}{E''} & y = x \\ - v_1 & y\in\NAMES(P_2)\setminus\{x\} \wedge \mathcal{E}(y)=[v_1;\dots;v_n] \\ + \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_e}{\mathcal{E}''} + & y=x \\ + v_{i1} & y=y_i \\ \mathcal{E}(y) & \mbox{otherwise} \\ \end{array} - \right. \\ -& & & \mathcal{E}''(y) = + \right.} \\ +& & \multicolumn{2}{l}{\mathcal{E}''(y) = \left\{ \begin{array}{@{}ll} - [v_2;\dots;v_n] & y\in\NAMES(P_2)\setminus\{x\} \wedge \mathcal{E}(y)=[v_1;\dots;v_n] \\ - \mathcal{E}(y) & \mbox{otherwise} \\ + [v_{i2};\dots;v_{in}] & y=y_i \\ + \mathcal{E}(y) & \mbox{otherwise} \\ \end{array} - \right. \\ + \right.} \\ + +\IOT{\mathtt{fold}~\mathtt{left}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}} +& = +& \mathit{eval\_fold}(x,P_2,\mathcal{E}') +& \\ +& & \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|-> +\IOT{P_1}{\UPDATE{\mathcal{E}}{\NAMES(P_2)|->\bot}}}} \\ + +\mathit{eval\_fold}(x,P,\mathcal{E}) +& = +& \mathcal{E}(x) +& \mathcal{E}(\NAMES(P)\setminus\{x\})=\{[],\dots,[]\} \\ + +\mathit{eval\_fold}(x,P,\mathcal{E}) +& = +& \mathit{eval\_fold}(x,P,\mathcal{E}') +& \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\ +& & & \NAMES(P)\setminus{x}=\{y_1,\dots,y_m\} \\ +& +& \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->\IOT{P}{\mathcal{E}''}; ~ y_i |-> [v_{i2};\dots;v_{in_i}]}} +\\ +& +& \multicolumn{2}{l}{\mathcal{E}''(y) = +\left\{ +\begin{array}{ll} + v_1 & y\in \NAMES(P)\setminus\{x\} \\ + \mathcal{E}(x) & y=x \\ + \bot & \mathit{otherwise} \\ +\end{array} +\right. +} +\\ + \end{array} \\ \] \end{table}