X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Fdoc%2Fmain.tex;h=1fdade8d66dcac3adce5dc4bb5ee1a5b4801816f;hb=2b0e0897ce58921e06793ad49ea1111e3b7b915b;hp=9885e542079ccc5a4401c05b0211eb63f0cead90;hpb=e4e8adaec753165a73a3acfa20c5d97a405e5dfa;p=helm.git diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex index 9885e5420..1fdade8d6 100644 --- a/helm/ocaml/cic_notation/doc/main.tex +++ b/helm/ocaml/cic_notation/doc/main.tex @@ -18,14 +18,18 @@ \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|]_{\mathcal#2}^2} +\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}} +\newcommand{\UPDATE}[2]{#1[#2]} \mathlig{~>}{\leadsto} \mathlig{|->}{\mapsto} @@ -135,7 +139,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} @@ -304,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)} \\ @@ -404,61 +409,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} @@ -554,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}} @@ -619,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 @@ -648,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} +