\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}}
\NT{term} & ::= & & \mbox{\bf terms} \\
& & x & \mbox{(identifier)} \\
& | & n & \mbox{(number)} \\
+ & | & s & \mbox{(symbol)} \\
& | & \mathrm{URI} & \mbox{(URI)} \\
& | & \verb+?+ & \mbox{(implicit)} \\
& | & \verb+%+ & \mbox{(placeholder)} \\
\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}}
\]
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
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}
+
projects / helm.git / commitdiff