From: Luca Padovani Date: Sun, 2 Oct 2005 16:39:11 +0000 (+0000) Subject: * well-formedness constraints X-Git-Tag: V_0_7_2_3~267 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4496bf2f1647f61657441b8249c05dab979da091;p=helm.git * well-formedness constraints --- diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex index 2b6f10b55..f73dc2168 100644 --- 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