From: Stefano Zacchiroli Date: Mon, 10 Oct 2005 17:37:24 +0000 (+0000) Subject: added level2 <-> level3 transformations X-Git-Tag: V_0_7_2_3~224 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2b0e0897ce58921e06793ad49ea1111e3b7b915b;p=helm.git added level2 <-> level3 transformations --- diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex index 4d0ccbec2..1fdade8d6 100644 --- a/helm/ocaml/cic_notation/doc/main.tex +++ b/helm/ocaml/cic_notation/doc/main.tex @@ -18,11 +18,14 @@ \newcommand{\BREAK}{\mathtt{break}} \newcommand{\TVAR}[1]{#1:\mathtt{term}} +\newcommand{\IMPVAR}{\TVAR{\_}} \newcommand{\NVAR}[1]{#1:\mathtt{number}} \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|]_{#2}^2} +\newcommand{\IAP}[2]{|[#1|]_{#2}^a} +\newcommand{\IAPP}[3]{|[#1|]_{#2,#3}^a} \newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}} \newcommand{\NAMES}{\mathit{names}} \newcommand{\DOMAIN}{\mathit{domain}} @@ -305,6 +308,7 @@ used in different contexts. \NT{term} & ::= & & \mbox{\bf terms} \\ & & x & \mbox{(identifier)} \\ & | & n & \mbox{(number)} \\ + & | & s & \mbox{(symbol)} \\ & | & \mathrm{URI} & \mbox{(URI)} \\ & | & \verb+?+ & \mbox{(implicit)} \\ & | & \verb+%+ & \mbox{(placeholder)} \\ @@ -590,8 +594,130 @@ used in different contexts. \hrule \end{table} +\begin{table} + \caption{\label{tab:synl3} Abstract syntax of level 3 terms and patterns.} + \hrule + \[ + \begin{array}{@{}ll@{}} + \begin{array}[t]{rcll} + T & : := & & \mbox{(\bf terms)} \\ + & & u & \mbox{(uri)} \\ + & | & \lambda x.T & \mbox{($\lambda$-abstraction)} \\ + & | & (T_1 \dots T_n) & \mbox{(application)} \\ + & | & \dots \\[2ex] + \end{array} & + \begin{array}[t]{rcll} + P & : := & & \mbox{(\bf patterns)} \\ + & & u & \mbox{(uri)} \\ + & | & V & \mbox{(variable)} \\ + & | & (P_1 \dots P_n) & \mbox{(application)} \\[2ex] + V & : := & & \mbox{(\bf variables)} \\ + & & \TVAR{x} & \mbox{(term variable)} \\ + & | & \IMPVAR & \mbox{(implicit variable)} \\ + \end{array} \\ + \end{array} + \] + \hrule +\end{table} + +\begin{table} +\caption{\label{tab:wfl3} Well-formedness rules for level 3 patterns.\strut} +\hrule +\[ +\renewcommand{\arraystretch}{3.5} +\begin{array}{@{}c@{}} + \inference[\sc Uri] {} {u :: \emptyset} \quad + \inference[\sc ImpVar] {} {\TVAR{x} :: \emptyset} \quad + \inference[\sc TermVar] {} {\TVAR{x} :: x:\mathtt{Term}} \\ + \inference[\sc Appl] + {P_i :: D_i + \quad \forall i,j,i\neq j=>\DOMAIN(D_i)\cap\DOMAIN(D_j)=\emptyset} + {P_1\cdots P_n :: D_1\oplus\cdots\oplus D_n} \\ +\end{array} +\] +\hrule +\end{table} + +\begin{table} + \caption{\label{tab:synargp} Abstract syntax of applicative symbol patterns.} + \hrule + \[ + \begin{array}{rcll} + P & : := & & \mbox{(\bf patterns)} \\ + & & s ~ \{ \mathit{arg} \} & \mbox{(symbol pattern)} \\[2ex] + \mathit{arg} & : := & & \mbox{(\bf argument)} \\ + & & \TVAR{x} & \mbox{(term variable)} \\ + & | & \eta.\mathit{arg} & \mbox{($\eta$-abstraction)} \\ + \end{array} + \] + \hrule +\end{table} + +\begin{table} +\caption{\label{tab:wfargp} Well-formedness rules for applicative symbol +patterns.\strut} +\hrule +\[ +\renewcommand{\arraystretch}{3.5} +\begin{array}{@{}c@{}} + \inference[\sc Pattern] + {\mathit{arg}_i :: D_i + \quad \forall i,j,i\neq j=>\DOMAIN(D_i)\cap\DOMAIN(D_j)=\emptyset} + {s~\mathit{arg}_1\cdots\mathit{arg}_n :: D_1\oplus\cdots\oplus D_n} \\ + \inference[\sc TermVar] + {} + {\TVAR{x} :: x : \mathtt{Term}} + \quad + \inference[\sc EtaAbs] + {\mathit{arg} :: D} + {\eta.\mathit{arg} :: D} + \\ +\end{array} +\] +\hrule +\end{table} + +\begin{table} +\caption{\label{tab:l3match} Pattern matching of level 3 terms.\strut} +\hrule +\[ +\renewcommand{\arraystretch}{3.5} +\begin{array}{@{}c@{}} + \inference[\sc Uri] {} {u\in u ~> []} \quad + \inference[\sc Appl] {t_i\in P_i ~> \mathcal{E}_i} + {(t_1\dots t_n)\in(P_1\dots P_n) ~> + \mathcal{E}_1\oplus\cdots\oplus\mathcal{E}_n} \\ + \inference[\sc TermVar] {} {t\in \TVAR{x} ~> [x |-> \mathtt{Term}~t]} \quad + \inference[\sc ImpVar] {} {t\in \IMPVAR ~> []} \\ +\end{array} +\] +\hrule +\end{table} + +\begin{table} +\caption{\label{tab:iapf3} Instantiation of applicative symbol patterns (from +level 3).\strut} +\hrule +\[ +\begin{array}{rcll} + \IAP{s~a_1\cdots a_n}{\mathcal{E}} & = & + (s~\IAPP{a_1}{\mathcal{E}}{0}\cdots\IAPP{a_n}{\mathcal{E}}{0}) & \\ + \IAPP{\TVAR{x}}{\mathcal{E}}{0} & = & t & \mathcal{E}(x)=\mathtt{Term}~t \\ + \IAPP{\TVAR{x}}{\mathcal{E}}{i+1} & = & \lambda y.\IAPP{t}{\mathcal{E}}{i} + & \mathcal{E}(x)=\mathtt{Term}~\lambda y.t \\ + \IAPP{\TVAR{x}}{\mathcal{E}}{i+1} & = + & \lambda y_1.\cdots.\lambda y_{i+1}.t~y_1\cdots y_{i+1} + & \mathcal{E}(x)=\mathtt{Term}~t\wedge\forall y,t\neq\lambda y.t \\ + \IAPP{\eta.a}{\mathcal{E}}{i} & = & \IAPP{a}{\mathcal{E}}{i+1} \\ +\end{array} +\] +\hrule +\end{table} + \section{Type checking} +\subsection{Level 1 $<->$ Level 2} + \newcommand{\GUARDED}{\mathit{guarded}} \newcommand{\TRUE}{\mathit{true}} \newcommand{\FALSE}{\mathit{false}} @@ -655,9 +781,10 @@ We say that a \emph{bidirectional transformation} \] is well-formed if: \begin{itemize} + \item $P_1$ is a well-formed \emph{level 1 pattern} in some context $D$ and + $P_2$ is a well-formed \emph{level 2 pattern} in the very same context $D$, + that is $P_1 :: D$ and $P_2 :: D$; \item the pattern $P_2$ is guarded, that is $\GUARDED(P_2)=\TRUE$; - \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 @@ -684,4 +811,18 @@ concrete syntax we may want to forget about redundant structure Relationship with grammatical frameworks? +\subsection{Level 2 $<->$ Level 3} + +We say that an \emph{interpretation} +\[ + P_2 <=> P_3 +\] +is well-formed if: +\begin{itemize} + \item $P_2$ is a well-formed \emph{applicative symbol pattern} in some context + $D$ and $P_3$ is a well-formed \emph{level 3 pattern} in the very same + context $D$, that is $P_2 :: D$ and $P_3 :: D$. +\end{itemize} + \end{document} +