From: Luca Padovani Date: Mon, 3 Oct 2005 15:16:55 +0000 (+0000) Subject: incomplete snapshot .... X-Git-Tag: V_0_7_2_3~260 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e4e8adaec753165a73a3acfa20c5d97a405e5dfa;p=helm.git incomplete snapshot .... --- diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex index f73dc2168..9885e5420 100644 --- a/helm/ocaml/cic_notation/doc/main.tex +++ b/helm/ocaml/cic_notation/doc/main.tex @@ -1,4 +1,4 @@ -\documentclass[a4paper]{article} +\documentclass[a4paper,draft]{article} \usepackage{manfnt} \usepackage{a4wide} @@ -21,7 +21,8 @@ \newcommand{\NVAR}[1]{#1:\mathtt{number}} \newcommand{\IVAR}[1]{#1:\mathtt{name}} \newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}} -\newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^1} +\newcommand{\ITO}[2]{|[#1|]_{\mathcal#2}^1} +\newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^2} \newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}} \newcommand{\NAMES}{\mathit{names}} \newcommand{\DOMAIN}{\mathit{domain}} @@ -130,7 +131,7 @@ used in different contexts. \end{table} \[ -\IOT{\cdot}{{}} : P -> \mathit{Env} -> T +\ITO{\cdot}{{}} : P -> \mathit{Env} -> T \] \begin{table} @@ -138,23 +139,23 @@ used in different contexts. \hrule \[ \begin{array}{rcll} - \IOT{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\IOT{(P_1)}{E},\dots,\IOT{(P_n)}{E} ] \\ - \IOT{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\ - \IOT{\BREAK}{E} & = & \BREAK \\ - \IOT{(P)}{E} & = & \IOT{P}{E} \\ - \IOT{(P_1\cdots P_n)}{E} & = & B_H^{00}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\ - \IOT{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\ - \IOT{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\ - \IOT{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\ - \IOT{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\ - \IOT{\mathtt{opt}~P}{E} & = & \IOT{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\ + \ITO{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\ITO{(P_1)}{E},\dots,\ITO{(P_n)}{E} ] \\ + \ITO{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\ + \ITO{\BREAK}{E} & = & \BREAK \\ + \ITO{(P)}{E} & = & \ITO{P}{E} \\ + \ITO{(P_1\cdots P_n)}{E} & = & B_H^{00}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\ + \ITO{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\ + \ITO{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\ + \ITO{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\ + \ITO{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\ + \ITO{\mathtt{opt}~P}{E} & = & \ITO{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\ & & & \mathcal{E}'(x)=\left\{ \begin{array}{@{}ll} v, & \mathcal{E}(x) = \mathtt{Some}~v \\ \mathcal{E}(x), & \mbox{otherwise} \end{array} \right. \\ - \IOT{\mathtt{list}k~P~l?}{E} & = & \IOT{P}{{E}_1}~{l?}\cdots {l?}~\IOT{P}{{E}_n} & + \ITO{\mathtt{list}k~P~l?}{E} & = & \ITO{P}{{E}_1}~{l?}\cdots {l?}~\ITO{P}{{E}_n} & \mathcal{E}(\NAMES(P)) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\ & & & n\ge k \\ & & & \mathcal{E}_i(x) = \left\{ @@ -163,7 +164,7 @@ used in different contexts. \mathcal{E}(x), & \mbox{otherwise} \end{array} \right. \\ - \IOT{l}{E} & = & l \\ + \ITO{l}{E} & = & l \\ %% & | & (P) & \mbox{(fenced)} \\ %% & | & M & \mbox{(magic)} \\ @@ -240,7 +241,7 @@ used in different contexts. \newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}} \begin{table} -\caption{\label{tab:addparens} Where are parentheses added? Look here.\strut} +\caption{\label{tab:addparens} Can't read the AST and need parentheses? Here you go!.\strut} \hrule \[ \begin{array}{rcll} @@ -296,6 +297,8 @@ used in different contexts. \newcommand{\NT}[1]{\langle\mathit{#1}\rangle} \begin{table} +\caption{\label{tab:synl2} Concrete syntax of level 2 patterns.\strut} +\hrule \[ \begin{array}{@{}rcll@{}} \NT{term} & ::= & & \mbox{\bf terms} \\ @@ -334,7 +337,7 @@ used in different contexts. & & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex] \NT{meta} & ::= & & \mbox{\bf meta} \\ - & & \BLOB(\NT{term},\dots,\NT{term}) & (term blob) \\ + & & \BLOB(\NT{term},\dots,\NT{term}) & \mbox{(term blob)} \\ & | & [\verb+term+]~x \\ & | & \verb+number+~x \\ & | & \verb+ident+~x \\ @@ -346,6 +349,7 @@ used in different contexts. & | & \verb+fail+ \end{array} \] +\hrule \end{table} \begin{table} @@ -355,11 +359,11 @@ used in different contexts. \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} + {P_i :: D_i} {\BLOB[P_1,\dots,P_n] :: D_i \oplus \cdots \oplus D_j} \\ \inference[\sc TermVar] {} - {[\mathtt{term}]~x :: x : \mathtt{Term}} + {\mathtt{term}~x :: x : \mathtt{Term}} \quad \inference[\sc NumVar] {} @@ -391,7 +395,7 @@ used in different contexts. \qquad \inference[\sc Fail] {} - {\mathtt{fail} : \emptyset} + {\mathtt{fail} :: \emptyset} %% & | & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\ %% & | & \verb+fail+ \end{array} @@ -399,6 +403,66 @@ used in different contexts. \hrule \end{table} +\begin{table} +\caption{...} +\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{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_2}{E'} +& \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\ +& & & \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] \\ + \mathcal{E}(y) & \mbox{otherwise} \\ + \end{array} + \right. \\ +& & & \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} \\ + \end{array} + \right. \\ +\end{array} \\ +\] +\end{table} + \begin{table} \caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut} \hrule @@ -461,19 +525,20 @@ used in different contexts. {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\{ + \inference[\sc FoldRec] + {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'} + {t \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''} + \\ + \mbox{where}~\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)::\mathcal{E}'(y) & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{right} \\ + \mathcal{E}'(y)@[\mathcal{E}(y)] & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{left} \\ \mathcal{E}'(y) & \mbox{otherwise} \end{array} \right. \\ - \inference[\sc FoldB] + \inference[\sc FoldBase] {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 @@ -491,34 +556,62 @@ used in different contexts. \section{Type checking} +\newcommand{\GUARDED}{\mathit{guarded}} +\newcommand{\TRUE}{\mathit{true}} +\newcommand{\FALSE}{\mathit{false}} + \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{table} +\caption{\label{tab:guarded} Guarded condition of level 2 +pattern. Note that the recursive case of the \texttt{fold} magic is +not explicitly required to be guarded. The point is that it must +contain at least two distinct names, and this guarantees that whatever +is matched by the recursive pattern, the terms matched by those two +names will be smaller than the whole matched term.\strut} \hrule \[ -\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 +\begin{array}{rcll} + \GUARDED(C(M(P))) & = & \GUARDED(P) \\ + \GUARDED(C(t_1,\dots,t_n)) & = & \TRUE \\ + \GUARDED(\mathtt{term}~x) & = & \FALSE \\ + \GUARDED(\mathtt{number}~x) & = & \FALSE \\ + \GUARDED(\mathtt{ident}~x) & = & \FALSE \\ + \GUARDED(\mathtt{fresh}~x) & = & \FALSE \\ + \GUARDED(\mathtt{anonymous}) & = & \TRUE \\ + \GUARDED(\mathtt{default}~P_1~P_2) & = & \GUARDED(P_1) \wedge \GUARDED(P_2) \\ + \GUARDED(\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3) & = & \GUARDED(P_2) \wedge \GUARDED(P_3) \\ + \GUARDED(\mathtt{fail}) & = & \TRUE \\ + \GUARDED(\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2) & = & \GUARDED(P_2) \end{array} \] +\hrule +\end{table} + +%% 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} \[ @@ -526,6 +619,7 @@ We say that a \emph{bidirectional transformation} \] is well-formed if: \begin{itemize} + \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 @@ -554,4 +648,4 @@ concrete syntax we may want to forget about redundant structure Relationship with grammatical frameworks? -\end{document} \ No newline at end of file +\end{document}