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 9885e542079ccc5a4401c05b0211eb63f0cead90..4d0ccbec2abbc684a9dbae9b1679ecafc37bbb9c 100644 (file)
--- 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}