\usepackage{a4wide}
\usepackage{pifont}
\usepackage{semantic}
-\usepackage{stmaryrd}
+\usepackage{stmaryrd,latexsym}
\newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}}
\newcommand{\NAMES}{\mathit{names}}
\newcommand{\DOMAIN}{\mathit{domain}}
+\mathlig{~>}{\leadsto}
+\mathlig{|->}{\mapsto}
+
\begin{document}
\maketitle
\begin{table}
\[
\begin{array}{@{}rcll@{}}
- \NT{term} & ::= & & \mbox{(\bf terms)} \\
- & & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
- & | & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
- & | & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
- & | & \NT{term}~\NT{term} & \mbox{(application)} \\
- & | & x & \mbox{(identifier)} \\
- & | & \mathrm{URI} & \mbox{(URI)} \\
+ \NT{term} & ::= & & \mbox{\bf terms} \\
+ & & x & \mbox{(identifier)} \\
& | & n & \mbox{(number)} \\
+ & | & \mathrm{URI} & \mbox{(URI)} \\
& | & \verb+?+ & \mbox{(implicit)} \\
& | & \verb+%+ & \mbox{(placeholder)} \\
& | & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
+ & | & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
+ & | & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
+ & | & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
+ & | & \NT{term}~\NT{term} & \mbox{(application)} \\
& | & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
& | & [\verb+[+~\NT{term}~\verb+]+]~\verb+match+~\NT{term}~\verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \mbox{(pattern match)} \\
& | & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
& | & \verb+(+~\NT{term}~\verb+)+ \\
- & | & \BLOB & \mbox{(blob)} \\
- \NT{defs} & ::= & & \mbox{(\bf mutual definitions)} \\
+ & | & \BLOB(\NT{meta},\dots,\NT{meta}) & \mbox{(meta blob)} \\
+ \NT{defs} & ::= & & \mbox{\bf mutual definitions} \\
& & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
- \NT{fun} & ::= & & \mbox{(\bf function)} \\
+ \NT{fun} & ::= & & \mbox{\bf functions} \\
& & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
- \NT{binder} & ::= & & \mbox{(\bf binders)} \\
+ \NT{binder} & ::= & & \mbox{\bf binders} \\
& & \verb+\Pi+ \mid \verb+\exists+ \mid \verb+\forall+ \mid \verb+\lambda+ \\
- \NT{arg} & ::= & & \mbox{(\bf single argument)} \\
- & & \verb+_+ \mid x \mid \BLOB \\
- \NT{ptname} & ::= & & \mbox{(\bf possibly typed name)} \\
+ \NT{arg} & ::= & & \mbox{\bf single argument} \\
+ & & \verb+_+ \mid x \mid \BLOB(\NT{meta},\dots,\NT{meta}) \\
+ \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
& & \NT{arg} \\
& | & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
- \NT{ptnames} & ::= & & \mbox{(\bf bound variables)} \\
+ \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
& & \NT{arg} \\
& | & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
- \NT{kind} & ::= & & \mbox{(\bf induction kind)} \\
+ \NT{kind} & ::= & & \mbox{\bf induction kind} \\
& & \verb+rec+ \mid \verb+corec+ \\
- \NT{rule} & ::= & & \mbox{(\bf rules)} \\
+ \NT{rule} & ::= & & \mbox{\bf rules} \\
& & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]
- \NT{meta} & ::= & & \mbox{(\bf meta)} \\
- & & \BLOB \\
+ \NT{meta} & ::= & & \mbox{\bf meta} \\
+ & & \BLOB(\NT{term},\dots,\NT{term}) & (term blob) \\
& | & [\verb+term+]~x \\
& | & \verb+number+~x \\
& | & \verb+ident+~x \\
\]
\end{table}
+\begin{table}
+\caption{\label{tab:wfl2} Well-formedness rules for level 2 patterns.\strut}
+\hrule
+\[
+\renewcommand{\arraystretch}{3.5}
+\begin{array}{@{}c@{}}
+ \inference[\sc Constr]
+ {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
+ {\BLOB[P_1,\dots,P_n] :: D_i \oplus \cdots \oplus D_j} \\
+ \inference[\sc TermVar]
+ {}
+ {[\mathtt{term}]~x :: x : \mathtt{Term}}
+ \quad
+ \inference[\sc NumVar]
+ {}
+ {\mathtt{number}~x :: x : \mathtt{Number}}
+ \\
+ \inference[\sc IdentVar]
+ {}
+ {\mathtt{ident}~x :: x : \mathtt{String}}
+ \quad
+ \inference[\sc FreshVar]
+ {}
+ {\mathtt{fresh}~x :: x : \mathtt{String}}
+ \\
+ \inference[\sc Success]
+ {}
+ {\mathtt{anonymous} :: \emptyset}
+ \\
+ \inference[\sc Fold]
+ {P_1 :: D_1 & P_2 :: D_2 \oplus (x : \mathtt{Term}) & \DOMAIN(D_2)\ne\emptyset & \DOMAIN(D_1)\cap\DOMAIN(D_2)=\emptyset}
+ {\mathtt{fold}~P_1~\mathtt{rec}~x~P_2 :: D_1 \oplus D_2~\mathtt{List}}
+ \\
+ \inference[\sc Default]
+ {P_1 :: D \oplus D_1 & P_2 :: D & \DOMAIN(D_1) \ne \emptyset & \DOMAIN(D) \cap \DOMAIN(D_1) = \emptyset}
+ {\mathtt{default}~P_1~P_2 :: D \oplus D_1~\mathtt{Option}}
+ \\
+ \inference[\sc If]
+ {P_1 :: \emptyset & P_2 :: D & P_3 :: D }
+ {\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 :: D}
+ \qquad
+ \inference[\sc Fail]
+ {}
+ {\mathtt{fail} : \emptyset}
+%% & | & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
+%% & | & \verb+fail+
+\end{array}
+\]
+\hrule
+\end{table}
+
+\begin{table}
+\caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
+\hrule
+\[
+\renewcommand{\arraystretch}{3.5}
+\begin{array}{@{}c@{}}
+ \inference[\sc Constr]
+ {t_i \in P_i ~> \mathcal E_i & i\ne j => \DOMAIN(\mathcal E_i)\cap\DOMAIN(\mathcal E_j)=\emptyset}
+ {C[t_1,\dots,t_n] \in C[P_1,\dots,P_n] ~> \mathcal E_1 \oplus \cdots \oplus \mathcal E_n}
+ \\
+ \inference[\sc TermVar]
+ {}
+ {t \in [\mathtt{term}]~x ~> [x |-> \mathtt{Term}~t]}
+ \quad
+ \inference[\sc NumVar]
+ {}
+ {n \in \mathtt{number}~x ~> [x |-> \mathtt{Number}~n]}
+ \\
+ \inference[\sc IdentVar]
+ {}
+ {x \in \mathtt{ident}~x ~> [x |-> \mathtt{String}~x]}
+ \quad
+ \inference[\sc FreshVar]
+ {}
+ {x \in \mathtt{fresh}~x ~> [x |-> \mathtt{String}~x]}
+ \\
+ \inference[\sc Success]
+ {}
+ {t \in \mathtt{anonymous} ~> \emptyset}
+ \\
+ \inference[\sc DefaultT]
+ {t \in P_1 ~> \mathcal E}
+ {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
+ \quad
+ \mathcal E'(x) = \left\{
+ \renewcommand{\arraystretch}{1}
+ \begin{array}{ll}
+ \mathtt{Some}~\mathcal{E}(x) & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
+ \mathcal{E}(x) & \mbox{otherwise}
+ \end{array}
+ \right.
+ \\
+ \inference[\sc DefaultF]
+ {t \not\in P_1 & t \in P_2 ~> \mathcal E}
+ {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
+ \quad
+ \mathcal E'(x) = \left\{
+ \renewcommand{\arraystretch}{1}
+ \begin{array}{ll}
+ \mathtt{None} & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
+ \mathcal{E}(x) & \mbox{otherwise}
+ \end{array}
+ \right.
+ \\
+ \inference[\sc IfT]
+ {t \in P_1 ~> \mathcal E' & t \in P_2 ~> \mathcal E}
+ {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
+ \quad
+ \inference[\sc IfF]
+ {t \not\in P_1 & t \in P_3 ~> \mathcal E}
+ {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
+ \\
+ \inference[\sc FoldR]
+ {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
+ {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''}
+ \quad
+ \mathcal E''(y) = \left\{
+ \renewcommand{\arraystretch}{1}
+ \begin{array}{ll}
+ \mathcal{E}(y)::\mathcal{E}'(y) & y \in \NAMES(P_2) \setminus \{x\} \\
+ \mathcal{E}'(y) & \mbox{otherwise}
+ \end{array}
+ \right.
+ \\
+ \inference[\sc FoldB]
+ {t \not\in P_2 & t \in P_1 ~> \mathcal E}
+ {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
+ \quad
+ \mathcal E'(y) = \left\{
+ \renewcommand{\arraystretch}{1}
+ \begin{array}{ll}
+ [] & y \in \NAMES(P_2) \setminus \{x\} \\
+ \mathcal{E}(y) & \mbox{otherwise}
+ \end{array}
+ \right.
+\end{array}
+\]
+\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