* well-formedness constraints

diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex
index 2b6f10b55465df74a07598c9120a7843f962bdf3..f73dc21681561fe95b051bced72e9f0bec16eb62 100644 (file)
--- a/helm/ocaml/cic_notation/doc/main.tex
+++ b/helm/ocaml/cic_notation/doc/main.tex
@@ -489,4 +489,69 @@ used in different contexts.
 \hrule
 \end{table}
 
+\section{Type checking}
+
+\newcommand{\TN}{\mathit{tn}}
+
+Assume that we have two corresponding patterns $P_1$ (level 1) and
+$P_2$ (level 2) and that we have to check whether they are
+``correct''. First we define the notion of \emph{top-level names} of
+$P_1$ and $P_2$, as follows:
+\[
+\begin{array}{rcl}
+  \TN(C_1[P'_1,\dots,P'_2]) & = & \TN(P'_1) \cup \cdots \cup \TN(P'_2) \\
+  \TN(\TVAR{x}) & = & \{x\} \\
+  \TN(\NVAR{x}) & = & \{x\} \\
+  \TN(\IVAR{x}) & = & \{x\} \\
+  \TN(\mathtt{list0}~P'~l?) & = & \emptyset \\
+  \TN(\mathtt{list1}~P'~l?) & = & \emptyset \\
+  \TN(\mathtt{opt}~P') & = & \emptyset \\[3ex]
+
+  \TN(\BLOB(P''_1,\dots,P''_2)) & = & \TN(P''_1) \cup \cdots \cup \TN(P''_2) \\
+  \TN(\mathtt{term}~x) & = & \{x\} \\
+  \TN(\mathtt{number}~x) & = & \{x\} \\
+  \TN(\mathtt{ident}~x) & = & \{x\} \\
+  \TN(\mathtt{fresh}~x) & = & \{x\} \\
+  \TN(\mathtt{anonymous}) & = & \emptyset \\
+  \TN(\mathtt{fold}~P''_1~\mathtt{rec}~x~P''_2) & = & \TN(P''_1) \\
+  \TN(\mathtt{default}~P''_1~P''_2) & = & \TN(P''_1) \cap \TN(P''_2) \\
+  \TN(\mathtt{if}~P''_1~\mathtt{then}~P''_2~\mathtt{else}~P''_3) & = & \TN(P''_2) \\
+  \TN(\mathtt{fail}) & = & \emptyset
+\end{array}
+\]
+
+We say that a \emph{bidirectional transformation}
+\[
+  P_1 <=> P_2
+\]
+is well-formed if:
+\begin{itemize}
+  \item the two patterns are well-formed in the same context $D$, that
+    is $P_1 :: D$ and $P_2 :: D$;
+  \item for any direct sub-pattern $\mathtt{opt}~P'_1$ of $P_1$ such
+    that $\mathtt{opt}~P'_1 :: X$ there is a sub-pattern
+    $\mathtt{default}~P'_2~P''_2$ of $P_2$ such that
+    $\mathtt{default}~P'_2~P''_2 :: X \oplus Y$ for some context $Y$;
+  \item for any direct sub-pattern $\mathtt{list}~P'_1~l?$ of $P_1$
+    such that $\mathtt{list}~P'_1~l? :: X$ there is a sub-pattern
+    $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2$ of $P_2$ such that
+    $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2 :: X \oplus Y$ for some
+    context $Y$.
+\end{itemize}
+
+A \emph{left-to-right transformation}
+\[
+  P_1 => P_2
+\]
+is well-formed if $P_2$ does not contain \texttt{if}, \texttt{fail},
+or \texttt{anonymous} meta patterns.
+
+Note that the transformations are in a sense asymmetric. Moving from
+the concrete syntax (level 1) to the abstract syntax (level 2) we
+forget about syntactic details. Moving from the abstract syntax to the
+concrete syntax we may want to forget about redundant structure
+(types).
+
+Relationship with grammatical frameworks?
+
 \end{document}
\ No newline at end of file