% File:    overflow.tex
% Authors: LC, FM, MA,
% Date:    6-OCT-1993
% Purpose: Section 4.3 omitted from the final submission
%
\subsection{Pattern-based Production Generation}
\label{Sec:Parsing-Patterns}

\begin{figure}
\figsep
\begin{center}\small
\axiom{\jp{g;L;R}{s}{\k{unit}}{s}{\k{unit}}}

\axiom{\jp{g;L;R}{x::s}{``x''}{s}{\k{unit}}}

\axiom{\jp{g;L;R}{x::s}{\k{ide}(Var)}{s}{\k{global}(x)}
       \bigspc x \not\in K(g), x\not\in Dom(L)}

\axiom{\jp{g;L,x:B,L';R}{x::s}{\k{ide}(B)}{s}{x}
       \bigspc x \not\in K(g), x\not\in Dom(L')}

\axiom{\jp{g;L;R}{s}{\k{local}}{s}{\k{local}}}

\axiom{\jp{g;L;R}{s}{\k{global}(x)}{s}{\k{global}(x)}} 

\axiom{\jp{g;L;R,x\leftarrow x',R'}{s}{x}{s}{x'} \bigspc x\not\in Dom(R')}

\dedtwo{
  \jp{g;L;R}{s}{p_1}{s'}{p_1'}
}{
  \jp{g;L;R}{s'}{p_2}{s''}{p_2'}
}{
  \jp{g;L;R}{s}{p_1\ p_2}{s''}{p_1'\ p_2'}
}

\dedtwo{
  \jp{g;L;R}{s}{p_1}{s'}{p_1'}
}{
  \jp{g;L;R\ x\leftarrow x'}{s'}{p_2}{s''}{p_2'} 
   \bigspc x' \not\in Dom(L)\cup Ran(R)
}{
  \jp{g;L;R}{s}{x=p_1\ p_2}{s''}{x'=p_1'\ p_2'}
}

\ded{
  \jp{g;L;R}{s}{p_1}{s'}{p_1'}
}{
  \jp{g;L;R}{s}{p_1\ |\ p_2}{s'}{p_1'}
}
\bigspc
\ded{
  \jp{g;L;R}{s}{p_2}{s'}{p_2'}
}{
  \jp{g;L;R}{s}{p_1\ |\ p_2}{s'}{p_2'}
}

\ded{
  \jp{g;L;R}{s_{j-1}}{p_j}{s_j,}{p_j'} 
      \bigspc 1\leq j\leq k
}{
  \jp{g;L;R}{s_0}{c_{(B_1, \ldots, B_k)B}(p_1, \ldots, p_k)}
            {s_k}{c_{(B_1, \ldots, B_k)B}(p_1', \ldots, p_k')}
} 

\dedthree{
  \jp{g;L;R}{s_{j-1}}{p_j}{s_j,}{p_j'} 
      \bigspc 1\leq j\leq k 
}{
  R'= R, x_1\leftarrow x_1', \ldots,  x_k\leftarrow x_k' \bigspc
  x_i' \not\in Dom(E)\cup Ran(R)  \bigspc
  x_i' \not= x_j' \ {\rm for} \  i\not=j
}{
  \jp{g;L;R'}{s_k}{p}{s'}{p'} 
  \bigspc (x:(x_1{\HT}B_1, \ldots, x_k{\HT}B_k) B \newnt p) \in g
}{
  \jp{g;L;R}{s_0}{x(p_1, \ldots, p_k)}{s'}
                                    {x_1'=p_1'\ \ldots\ x_k'=p_k'\ p'}
}
\end{center}
\figsep 
\caption{Parse rules for patterns in incremental grammar definitions}
\label{Fig:Parsing-Patterns}
\end{figure}

\noindent In the previous section we did not consider the parsing of
productions that are defined by means of patterns enclosed in \p{<<>>}.
In this section we describe aq translation of such patterns into simple
productions which are covered by the parse rules and the theorem given
in the previous section.

A pattern \p{$x$<<$s$>>} is a pair of a token stream $s$ and a
non-terminal $x$ that defines which production is to be used to parse
$s$.  The result of parsing $s$ is itself a production $p$ that neither
contains terminal productions that depend on input tokens nor choice
operators ($p_1\ |\ p_2$).  If $p$ is later executed within an
environment that defines bindings for the pattern variables occurring in
$s$, then $p$ performs the necessary steps to instantiate correctly 
(macro-expand) the pattern by defining term bindings, performing term
constructor applications, and by introducing fresh variables, where
necessary.

We describe the  effect of parsing a pattern \p{p<<s>>} by the notation 
\[\jp{g;L;R}{s}{p}{s'}{p'}\]
\noindent It states that production $p$ when executed in environment $g;L;R$
starting with a token stream $s$ returns a token stream $s'$ (the unread
tokens of $s$) and a constructed production $p'$. 

The environment $L$ contains the names and sorts of the pattern
variables bound in the scope enclosing the pattern. For example,
$L$ contains $\oslash, x:\mbox{Binder}, a:\mbox{Term},  b:\mbox{Term}$
for the pattern \p{term<<\ldots>>} in the following grammar:
\begin{grammar}
\>\k{grammar}
\\ \>  simpleTerm:Term \extendnt
\\ \>       \>"let" x=\k{ide} "=" a=term "in" b=term \>=> term<<(\k{fun}(x) b)(a)>>
\\ \>\k{end}
\end{grammar}
The notation $\jp{g;L;R}{s}{p}{s'}{p'}$  uses a set $R$ of renamings to avoid
name conflicts between the pattern variables in $L$ and term
variables introduced during pattern parsing:
\begin{center}
\begin{tabular}{rll}
$R::=$ & $\oslash$            & empty renaming\\
  $|$  & $R, x\leftarrow x'$  & rename $x$ by $x'$\\
\end{tabular}
\end{center}
The complete set of pattern-parsing rules is given in 
figure~\ref{Fig:Parsing-Patterns}. The following theorem states that
the successful parsing of a pattern \p{p<<s>>} using a production $p$ of
a type-correct grammar $g$ yields a well-typed production:
\begin{theorem}\label{Theo:2}
For all $g, E, L_1, L_2, L_3, p, B$ and $R$ such that
\begin{enumerate}\itemsep 0pt \parsep 0pt \topsep 0pt \parskip 0pt
\item $\jdg{\oslash}{g::E}$ 
\item $\jdg{\oslash}{g\ \k{ok}}$
\item $\jdg{E;L_3}{p:B}$ where $L_3 = \oslash, x_1:B_1, \ldots,  x_n:B_n$
\item $L_1$ and $R$ such that $R=\oslash, x_1\leftarrow x_1', \ldots,
x_n\leftarrow x_n'$ and $Ran(R) \cap Dom(L_1) = \oslash$ and
$x_i'\not=x_j', i\not=j$
\item $\jp{g;L_1;R}{s}{p}{s'}{p'}$
\end{enumerate}
$\jdg{E;L_1,L_2}{p':B}$ holds.
\end{theorem}
The proof can be found in~\cite{CMA93b}. By specializing this
theorem to non-parameterized productions $p_0$ with result sort $B$, we
obtain that a pattern \p{$p_0$<<s>>} in an arbitrary local environment
$L$ can be translated into an equivalent production $p'$ that has 
the result sort $B$ also: 
\begin{corollary}\label{Coro:2}
If 
\begin{itemize}
\item $\jdg{\oslash}{g::E}$
\item $\jdg{\oslash}{g\ \k{ok}}$
\item $\jdg{E;\oslash}{p_0:B}$ 
\item $\jp{g;L;\oslash}{s}{p_0}{*}{p'}$
\end{itemize}
then $\jdg{E;L,\oslash}{p':B}$.
\end{corollary}

