From: Stefano Zacchiroli Date: Mon, 21 Nov 2005 13:12:51 +0000 (+0000) Subject: split to easy inclusion X-Git-Tag: V_0_7_2_3~18 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=25be0a2deae2c84d626cf77aeb41c39c959ab81a split to easy inclusion --- diff --git a/helm/ocaml/cic_notation/doc/body.tex b/helm/ocaml/cic_notation/doc/body.tex new file mode 100644 index 000000000..f1ce73577 --- /dev/null +++ b/helm/ocaml/cic_notation/doc/body.tex @@ -0,0 +1,788 @@ + +\section{Environment} + +\[ +\begin{array}{rcll} + V & ::= & & \mbox{(\bf values)} \\ + & & \verb+Term+~T & \mbox{(term)} \\ + & | & \verb+String+~s & \mbox{(string)} \\ + & | & \verb+Number+~n & \mbox{(number)} \\ + & | & \verb+None+ & \mbox{(optional value)} \\ + & | & \verb+Some+~V & \mbox{(optional value)} \\ + & | & [V_1,\dots,V_n] & \mbox{(list value)} \\[2ex] +\end{array} +\] + +An environment is a map $\mathcal E : \mathit{Name} -> V$. + +\section{Level 1: concrete syntax} + +\begin{table} +\caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut} +\hrule +\[ +\begin{array}{rcll} + P & ::= & & \mbox{(\bf patterns)} \\ + & & S^{+} \\[2ex] + S & ::= & & \mbox{(\bf simple patterns)} \\ + & & l \\ + & | & S~\verb+\sub+~S\\ + & | & S~\verb+\sup+~S\\ + & | & S~\verb+\below+~S\\ + & | & S~\verb+\atop+~S\\ + & | & S~\verb+\over+~S\\ + & | & S~\verb+\atop+~S\\ + & | & \verb+\frac+~S~S \\ + & | & \verb+\sqrt+~S \\ + & | & \verb+\root+~S~\verb+\of+~S \\ + & | & \verb+(+~P~\verb+)+ \\ + & | & \verb+hbox (+~P~\verb+)+ \\ + & | & \verb+vbox (+~P~\verb+)+ \\ + & | & \verb+hvbox (+~P~\verb+)+ \\ + & | & \verb+hovbox (+~P~\verb+)+ \\ + & | & \verb+break+ \\ + & | & \verb+list0+~S~[\verb+sep+~l] \\ + & | & \verb+list1+~S~[\verb+sep+~l] \\ + & | & \verb+opt+~S \\ + & | & [\verb+term+]~x \\ + & | & \verb+number+~x \\ + & | & \verb+ident+~x \\ +\end{array} +\] +\hrule +\end{table} + +Rationale: while the layout schemata can occur in the concrete syntax +used by user, the box schemata and the magic patterns can only occur +when defining the notation. This is why the layout schemata are +``escaped'' with a backslash, so that they cannot be confused with +plain identifiers, wherease the others are not. Alternatively, they +could be defined as keywords, but this would prevent their names to be +used in different contexts. + +\begin{table} +\caption{\label{tab:l1a} Abstract syntax of level 1 terms and patterns.\strut} +\hrule +\[ +\begin{array}{@{}ll@{}} +\begin{array}[t]{rcll} + T & ::= & & \mbox{(\bf terms)} \\ + & & L_\kappa[T_1,\dots,T_n] & \mbox{(layout)} \\ + & | & B_\kappa^{ab}[T_1\cdots T_n] & \mbox{(box)} \\ + & | & \BREAK & \mbox{(breakpoint)} \\ + & | & \FENCED{T_1\cdots T_n} & \mbox{(fenced)} \\ + & | & l & \mbox{(literal)} \\[2ex] + P & ::= & & \mbox{(\bf patterns)} \\ + & & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\ + & | & B_\kappa^{ab}[P_1\cdots P_n] & \mbox{(box)} \\ + & | & \BREAK & \mbox{(breakpoint)} \\ + & | & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\ + & | & M & \mbox{(magic)} \\ + & | & V & \mbox{(variable)} \\ + & | & l & \mbox{(literal)} \\ +\end{array} & +\begin{array}[t]{rcll} + V & ::= & & \mbox{(\bf variables)} \\ + & & \TVAR{x} & \mbox{(term variable)} \\ + & | & \NVAR{x} & \mbox{(number variable)} \\ + & | & \IVAR{x} & \mbox{(name variable)} \\[2ex] + M & ::= & & \mbox{(\bf magic patterns)} \\ + & & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\ + & | & \verb+list1+~P~l? & \mbox{(non-empty list)} \\ + & | & \verb+opt+~P & \mbox{(option)} \\[2ex] +\end{array} +\end{array} +\] +\hrule +\end{table} + +\[ +\ITO{\cdot}{{}} : P -> \mathit{Env} -> T +\] + +\begin{table} +\caption{\label{tab:il1f2} Instantiation of level 1 patterns from level 2.\strut} +\hrule +\[ +\begin{array}{rcll} + \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. \\ + \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\{ + \begin{array}{@{}ll} + v_i, & \mathcal{E}(x) = [v_1,\dots,v_n] \\ + \mathcal{E}(x), & \mbox{otherwise} + \end{array} + \right. \\ + \ITO{l}{E} & = & l \\ + +%% & | & (P) & \mbox{(fenced)} \\ +%% & | & M & \mbox{(magic)} \\ +%% & | & V & \mbox{(variable)} \\ +%% & | & l & \mbox{(literal)} \\[2ex] +%% V & ::= & & \mbox{(\bf variables)} \\ +%% & & \TVAR{x} & \mbox{(term variable)} \\ +%% & | & \NVAR{x} & \mbox{(number variable)} \\ +%% & | & \IVAR{x} & \mbox{(name variable)} \\[2ex] +%% M & ::= & & \mbox{(\bf magic patterns)} \\ +%% & & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\ +%% & | & \verb+list1+~S~l? & \mbox{(non-empty list)} \\ +%% & | & \verb+opt+~S & \mbox{(option)} \\[2ex] +\end{array} +\] +\hrule +\end{table} + +\begin{table} +\caption{\label{tab:wfl0} Well-formedness rules for level 1 patterns.\strut} +\hrule +\[ +\renewcommand{\arraystretch}{3.5} +\begin{array}[t]{@{}c@{}} + \inference[\sc layout] + {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset} + {L_\kappa[P_1,\dots,P_n] :: D_1\oplus\cdots\oplus D_n} + \\ + \inference[\sc box] + {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset} + {B_\kappa^{ab}[P_1\cdots P_n] :: D_1\oplus\cdots\oplus D_n} + \\ + \inference[\sc fenced] + {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset} + {\FENCED{P_1\cdots P_n} :: D_1\oplus\cdots\oplus D_n} + \\ + \inference[\sc breakpoint] + {} + {\BREAK :: \emptyset} + \qquad + \inference[\sc literal] + {} + {l :: \emptyset} + \qquad + \inference[\sc tvar] + {} + {\TVAR{x} :: \TVAR{x}} + \\ + \inference[\sc nvar] + {} + {\NVAR{x} :: \NVAR{x}} + \qquad + \inference[\sc ivar] + {} + {\IVAR{x} :: \IVAR{x}} + \\ + \inference[\sc list0] + {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}} + {\mathtt{list0}~P~l? :: D'} + \\ + \inference[\sc list1] + {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}} + {\mathtt{list1}~P~l? :: D'} + \\ + \inference[\sc opt] + {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{Option}} + {\mathtt{opt}~P :: D'} +\end{array} +\] +\hrule +\end{table} + +\newcommand{\ATTRS}[1]{\langle#1\rangle} +\newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}} + +\begin{table} +\caption{\label{tab:addparens} Can't read the AST and need parentheses? Here you go!.\strut} +\hrule +\[ +\begin{array}{rcll} + \ADDPARENS{l}{n} & = & l \\ + \ADDPARENS{\BREAK}{n} & = & \BREAK \\ + \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \ADDPARENS{T}{m} & n < m \\ + \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} & n > m \\ + \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=L,\mathit{pos}=R}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\ + \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=R,\mathit{pos}=L}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\ + \ADDPARENS{\ATTRS{\cdots}T}{n} & = & \ADDPARENS{T}{n} \\ + \ADDPARENS{L_\kappa[T_1,\dots,\underline{T_k},\dots,T_m]}{n} & = & L_\kappa[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_k}{\bot},\dots,\ADDPARENS{T_m}{n}] \\ + \ADDPARENS{B_\kappa^{ab}[T_1,\dots,T_m]}{n} & = & B_\kappa^{ab}[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_m}{n}] +\end{array} +\] +\hrule +\end{table} + +\begin{table} +\caption{\label{tab:annpos} Annotation of level 1 meta variable with position information.\strut} +\hrule +\[ +\begin{array}{rcll} + \ANNPOS{l}{p,q} & = & l \\ + \ANNPOS{\BREAK}{p,q} & = & \BREAK \\ + \ANNPOS{x}{1,0} & = & \ATTRS{\mathit{pos}=L}{x} \\ + \ANNPOS{x}{0,1} & = & \ATTRS{\mathit{pos}=R}{x} \\ + \ANNPOS{x}{p,q} & = & \ATTRS{\mathit{pos}=I}{x} \\ + \ANNPOS{B_\kappa^{ab}[P]}{p,q} & = & B_\kappa^{ab}[\ANNPOS{P}{p,q}] \\ + \ANNPOS{B_\kappa^{ab}[\{\BREAK\} P_1\cdots P_n\{\BREAK\}]}{p,q} & = & B_\kappa^{ab}[\begin{array}[t]{@{}l} + \{\BREAK\} \ANNPOS{P_1}{p,0} \\ + \ANNPOS{P_2}{0,0}\cdots\ANNPOS{P_{n-1}}{0,0} \\ + \ANNPOS{P_n}{0,q}\{\BREAK\}] + \end{array} + +%% & & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\ +%% & | & \BREAK & \mbox{(breakpoint)} \\ +%% & | & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\ +%% V & ::= & & \mbox{(\bf variables)} \\ +%% & & \TVAR{x} & \mbox{(term variable)} \\ +%% & | & \NVAR{x} & \mbox{(number variable)} \\ +%% & | & \IVAR{x} & \mbox{(name variable)} \\[2ex] +%% M & ::= & & \mbox{(\bf magic patterns)} \\ +%% & & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\ +%% & | & \verb+list1+~P~l? & \mbox{(non-empty list)} \\ +%% & | & \verb+opt+~P & \mbox{(option)} \\[2ex] +\end{array} +\] +\hrule +\end{table} + +\section{Level 2: abstract syntax} + +\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} \\ + & & x & \mbox{(identifier)} \\ + & | & n & \mbox{(number)} \\ + & | & s & \mbox{(symbol)} \\ + & | & \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(\NT{meta},\dots,\NT{meta}) & \mbox{(meta blob)} \\ + \NT{defs} & ::= & & \mbox{\bf mutual definitions} \\ + & & \NT{fun}~\{\verb+and+~\NT{fun}\} \\ + \NT{fun} & ::= & & \mbox{\bf functions} \\ + & & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\ + \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{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{arg} \\ + & | & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\ + \NT{kind} & ::= & & \mbox{\bf induction kind} \\ + & & \verb+rec+ \mid \verb+corec+ \\ + \NT{rule} & ::= & & \mbox{\bf rules} \\ + & & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex] + + \NT{meta} & ::= & & \mbox{\bf meta} \\ + & & \BLOB(\NT{term},\dots,\NT{term}) & \mbox{(term blob)} \\ + & | & [\verb+term+]~x \\ + & | & \verb+number+~x \\ + & | & \verb+ident+~x \\ + & | & \verb+fresh+~x \\ + & | & \verb+anonymous+ \\ + & | & \verb+fold+~[\verb+left+\mid\verb+right+]~\NT{meta}~\verb+rec+~x~\NT{meta} \\ + & | & \verb+default+~\NT{meta}~\NT{meta} \\ + & | & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\ + & | & \verb+fail+ +\end{array} +\] +\hrule +\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} + {\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:il2f1} Instantiation of level 2 patterns from level 1. + \strut} +\hrule +\[ +\begin{array}{rcll} + +\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_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}{\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}~\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.} \\ +& & \multicolumn{2}{l}{\mathcal{E}''(y) = + \left\{ + \begin{array}{@{}ll} + [v_{i2};\dots;v_{in}] & y=y_i \\ + \mathcal{E}(y) & \mbox{otherwise} \\ + \end{array} + \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} + +\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 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\} \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 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 + \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} + +\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}} + +\newcommand{\TN}{\mathit{tn}} + +\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}{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_1) +\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} +\[ + P_1 <=> P_2 +\] +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 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? + +\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} + diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex index f4eb86c60..36d35026c 100644 --- a/helm/ocaml/cic_notation/doc/main.tex +++ b/helm/ocaml/cic_notation/doc/main.tex @@ -37,792 +37,7 @@ \begin{document} \maketitle -\section{Environment} - -\[ -\begin{array}{rcll} - V & ::= & & \mbox{(\bf values)} \\ - & & \verb+Term+~T & \mbox{(term)} \\ - & | & \verb+String+~s & \mbox{(string)} \\ - & | & \verb+Number+~n & \mbox{(number)} \\ - & | & \verb+None+ & \mbox{(optional value)} \\ - & | & \verb+Some+~V & \mbox{(optional value)} \\ - & | & [V_1,\dots,V_n] & \mbox{(list value)} \\[2ex] -\end{array} -\] - -An environment is a map $\mathcal E : \mathit{Name} -> V$. - -\section{Level 1: concrete syntax} - -\begin{table} -\caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut} -\hrule -\[ -\begin{array}{rcll} - P & ::= & & \mbox{(\bf patterns)} \\ - & & S^{+} \\[2ex] - S & ::= & & \mbox{(\bf simple patterns)} \\ - & & l \\ - & | & S~\verb+\sub+~S\\ - & | & S~\verb+\sup+~S\\ - & | & S~\verb+\below+~S\\ - & | & S~\verb+\atop+~S\\ - & | & S~\verb+\over+~S\\ - & | & S~\verb+\atop+~S\\ - & | & \verb+\frac+~S~S \\ - & | & \verb+\sqrt+~S \\ - & | & \verb+\root+~S~\verb+\of+~S \\ - & | & \verb+(+~P~\verb+)+ \\ - & | & \verb+hbox (+~P~\verb+)+ \\ - & | & \verb+vbox (+~P~\verb+)+ \\ - & | & \verb+hvbox (+~P~\verb+)+ \\ - & | & \verb+hovbox (+~P~\verb+)+ \\ - & | & \verb+break+ \\ - & | & \verb+list0+~S~[\verb+sep+~l] \\ - & | & \verb+list1+~S~[\verb+sep+~l] \\ - & | & \verb+opt+~S \\ - & | & [\verb+term+]~x \\ - & | & \verb+number+~x \\ - & | & \verb+ident+~x \\ -\end{array} -\] -\hrule -\end{table} - -Rationale: while the layout schemata can occur in the concrete syntax -used by user, the box schemata and the magic patterns can only occur -when defining the notation. This is why the layout schemata are -``escaped'' with a backslash, so that they cannot be confused with -plain identifiers, wherease the others are not. Alternatively, they -could be defined as keywords, but this would prevent their names to be -used in different contexts. - -\begin{table} -\caption{\label{tab:l1a} Abstract syntax of level 1 terms and patterns.\strut} -\hrule -\[ -\begin{array}{@{}ll@{}} -\begin{array}[t]{rcll} - T & ::= & & \mbox{(\bf terms)} \\ - & & L_\kappa[T_1,\dots,T_n] & \mbox{(layout)} \\ - & | & B_\kappa^{ab}[T_1\cdots T_n] & \mbox{(box)} \\ - & | & \BREAK & \mbox{(breakpoint)} \\ - & | & \FENCED{T_1\cdots T_n} & \mbox{(fenced)} \\ - & | & l & \mbox{(literal)} \\[2ex] - P & ::= & & \mbox{(\bf patterns)} \\ - & & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\ - & | & B_\kappa^{ab}[P_1\cdots P_n] & \mbox{(box)} \\ - & | & \BREAK & \mbox{(breakpoint)} \\ - & | & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\ - & | & M & \mbox{(magic)} \\ - & | & V & \mbox{(variable)} \\ - & | & l & \mbox{(literal)} \\ -\end{array} & -\begin{array}[t]{rcll} - V & ::= & & \mbox{(\bf variables)} \\ - & & \TVAR{x} & \mbox{(term variable)} \\ - & | & \NVAR{x} & \mbox{(number variable)} \\ - & | & \IVAR{x} & \mbox{(name variable)} \\[2ex] - M & ::= & & \mbox{(\bf magic patterns)} \\ - & & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\ - & | & \verb+list1+~P~l? & \mbox{(non-empty list)} \\ - & | & \verb+opt+~P & \mbox{(option)} \\[2ex] -\end{array} -\end{array} -\] -\hrule -\end{table} - -\[ -\ITO{\cdot}{{}} : P -> \mathit{Env} -> T -\] - -\begin{table} -\caption{\label{tab:il1f2} Instantiation of level 1 patterns from level 2.\strut} -\hrule -\[ -\begin{array}{rcll} - \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. \\ - \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\{ - \begin{array}{@{}ll} - v_i, & \mathcal{E}(x) = [v_1,\dots,v_n] \\ - \mathcal{E}(x), & \mbox{otherwise} - \end{array} - \right. \\ - \ITO{l}{E} & = & l \\ - -%% & | & (P) & \mbox{(fenced)} \\ -%% & | & M & \mbox{(magic)} \\ -%% & | & V & \mbox{(variable)} \\ -%% & | & l & \mbox{(literal)} \\[2ex] -%% V & ::= & & \mbox{(\bf variables)} \\ -%% & & \TVAR{x} & \mbox{(term variable)} \\ -%% & | & \NVAR{x} & \mbox{(number variable)} \\ -%% & | & \IVAR{x} & \mbox{(name variable)} \\[2ex] -%% M & ::= & & \mbox{(\bf magic patterns)} \\ -%% & & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\ -%% & | & \verb+list1+~S~l? & \mbox{(non-empty list)} \\ -%% & | & \verb+opt+~S & \mbox{(option)} \\[2ex] -\end{array} -\] -\hrule -\end{table} - -\begin{table} -\caption{\label{tab:wfl0} Well-formedness rules for level 1 patterns.\strut} -\hrule -\[ -\renewcommand{\arraystretch}{3.5} -\begin{array}[t]{@{}c@{}} - \inference[\sc layout] - {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset} - {L_\kappa[P_1,\dots,P_n] :: D_1\oplus\cdots\oplus D_n} - \\ - \inference[\sc box] - {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset} - {B_\kappa^{ab}[P_1\cdots P_n] :: D_1\oplus\cdots\oplus D_n} - \\ - \inference[\sc fenced] - {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset} - {\FENCED{P_1\cdots P_n} :: D_1\oplus\cdots\oplus D_n} - \\ - \inference[\sc breakpoint] - {} - {\BREAK :: \emptyset} - \qquad - \inference[\sc literal] - {} - {l :: \emptyset} - \qquad - \inference[\sc tvar] - {} - {\TVAR{x} :: \TVAR{x}} - \\ - \inference[\sc nvar] - {} - {\NVAR{x} :: \NVAR{x}} - \qquad - \inference[\sc ivar] - {} - {\IVAR{x} :: \IVAR{x}} - \\ - \inference[\sc list0] - {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}} - {\mathtt{list0}~P~l? :: D'} - \\ - \inference[\sc list1] - {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}} - {\mathtt{list1}~P~l? :: D'} - \\ - \inference[\sc opt] - {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{Option}} - {\mathtt{opt}~P :: D'} -\end{array} -\] -\hrule -\end{table} - -\newcommand{\ATTRS}[1]{\langle#1\rangle} -\newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}} - -\begin{table} -\caption{\label{tab:addparens} Can't read the AST and need parentheses? Here you go!.\strut} -\hrule -\[ -\begin{array}{rcll} - \ADDPARENS{l}{n} & = & l \\ - \ADDPARENS{\BREAK}{n} & = & \BREAK \\ - \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \ADDPARENS{T}{m} & n < m \\ - \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} & n > m \\ - \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=L,\mathit{pos}=R}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\ - \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=R,\mathit{pos}=L}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\ - \ADDPARENS{\ATTRS{\cdots}T}{n} & = & \ADDPARENS{T}{n} \\ - \ADDPARENS{L_\kappa[T_1,\dots,\underline{T_k},\dots,T_m]}{n} & = & L_\kappa[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_k}{\bot},\dots,\ADDPARENS{T_m}{n}] \\ - \ADDPARENS{B_\kappa^{ab}[T_1,\dots,T_m]}{n} & = & B_\kappa^{ab}[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_m}{n}] -\end{array} -\] -\hrule -\end{table} - -\begin{table} -\caption{\label{tab:annpos} Annotation of level 1 meta variable with position information.\strut} -\hrule -\[ -\begin{array}{rcll} - \ANNPOS{l}{p,q} & = & l \\ - \ANNPOS{\BREAK}{p,q} & = & \BREAK \\ - \ANNPOS{x}{1,0} & = & \ATTRS{\mathit{pos}=L}{x} \\ - \ANNPOS{x}{0,1} & = & \ATTRS{\mathit{pos}=R}{x} \\ - \ANNPOS{x}{p,q} & = & \ATTRS{\mathit{pos}=I}{x} \\ - \ANNPOS{B_\kappa^{ab}[P]}{p,q} & = & B_\kappa^{ab}[\ANNPOS{P}{p,q}] \\ - \ANNPOS{B_\kappa^{ab}[\{\BREAK\} P_1\cdots P_n\{\BREAK\}]}{p,q} & = & B_\kappa^{ab}[\begin{array}[t]{@{}l} - \{\BREAK\} \ANNPOS{P_1}{p,0} \\ - \ANNPOS{P_2}{0,0}\cdots\ANNPOS{P_{n-1}}{0,0} \\ - \ANNPOS{P_n}{0,q}\{\BREAK\}] - \end{array} - -%% & & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\ -%% & | & \BREAK & \mbox{(breakpoint)} \\ -%% & | & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\ -%% V & ::= & & \mbox{(\bf variables)} \\ -%% & & \TVAR{x} & \mbox{(term variable)} \\ -%% & | & \NVAR{x} & \mbox{(number variable)} \\ -%% & | & \IVAR{x} & \mbox{(name variable)} \\[2ex] -%% M & ::= & & \mbox{(\bf magic patterns)} \\ -%% & & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\ -%% & | & \verb+list1+~P~l? & \mbox{(non-empty list)} \\ -%% & | & \verb+opt+~P & \mbox{(option)} \\[2ex] -\end{array} -\] -\hrule -\end{table} - -\section{Level 2: abstract syntax} - -\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} \\ - & & x & \mbox{(identifier)} \\ - & | & n & \mbox{(number)} \\ - & | & s & \mbox{(symbol)} \\ - & | & \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(\NT{meta},\dots,\NT{meta}) & \mbox{(meta blob)} \\ - \NT{defs} & ::= & & \mbox{\bf mutual definitions} \\ - & & \NT{fun}~\{\verb+and+~\NT{fun}\} \\ - \NT{fun} & ::= & & \mbox{\bf functions} \\ - & & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\ - \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{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{arg} \\ - & | & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\ - \NT{kind} & ::= & & \mbox{\bf induction kind} \\ - & & \verb+rec+ \mid \verb+corec+ \\ - \NT{rule} & ::= & & \mbox{\bf rules} \\ - & & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex] - - \NT{meta} & ::= & & \mbox{\bf meta} \\ - & & \BLOB(\NT{term},\dots,\NT{term}) & \mbox{(term blob)} \\ - & | & [\verb+term+]~x \\ - & | & \verb+number+~x \\ - & | & \verb+ident+~x \\ - & | & \verb+fresh+~x \\ - & | & \verb+anonymous+ \\ - & | & \verb+fold+~[\verb+left+\mid\verb+right+]~\NT{meta}~\verb+rec+~x~\NT{meta} \\ - & | & \verb+default+~\NT{meta}~\NT{meta} \\ - & | & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\ - & | & \verb+fail+ -\end{array} -\] -\hrule -\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} - {\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:il2f1} Instantiation of level 2 patterns from level 1. - \strut} -\hrule -\[ -\begin{array}{rcll} - -\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_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}{\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}~\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.} \\ -& & \multicolumn{2}{l}{\mathcal{E}''(y) = - \left\{ - \begin{array}{@{}ll} - [v_{i2};\dots;v_{in}] & y=y_i \\ - \mathcal{E}(y) & \mbox{otherwise} \\ - \end{array} - \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} - -\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 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\} \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 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 - \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} - -\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}} - -\newcommand{\TN}{\mathit{tn}} - -\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}{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_1) -\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} -\[ - P_1 <=> P_2 -\] -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 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? - -\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} + \input{body} \end{document}