% File:    EGrammar-short.tex
% Author:  Luca Cardelli, Florian Matthes, Martin Abadi
% Date:    8-OCT-1993 [adapted to final Springer-Style & shortened (again)]
%          last edited by FM based on comments from MA & LC
% Purpose: DBPL-5 paper on extensible grammar (short version)
%
\documentstyle[twoside,wicsbook,xple_sl,epsf]{article}

%-------------------------------------------------------------------------

% Framed and centered figures:
\newcommand{\figsep}{\noindent\rule{\textwidth}{0.5pt}}
\newcommand{\addstrut}{\vspace*{0.25\baselineskip}}

% -- Macros:
\newcommand{\gseq}{\hbox{\it gseq}}
\newcommand{\newnt}{\hbox{==}}
\newcommand{\extendnt}{\hbox{$|$==}}
\newcommand{\updatent}{\hbox{:==}}

\newcommand{\e}[1]{{\em #1\/}}
\newcommand{\p}[1]{{\tt{}#1}}
\newcommand{\k}[1]{{\bf{}#1}}
\newcommand{\comment}[1]{ [[ #1 ]] }
\newcommand{\synopt}[1]{$[$ #1 $]$}
\newcommand{\synbrack}[1]{$($ #1 $)$}
\newcommand{\synrep}[1]{$\{$ #1 $\}$}
\newcommand{\synquot}[1]{\verb$"${\rm{#1}}\verb$"$}
% has Type with better spacing
\newcommand{\HT}{:}   
\newcommand{\R}{\Rightarrow}
\newcommand{\LL}{M}
\newcommand{\jdg}[2]{#1 \vdash #2}
\newcommand{\jd}[5]{#1 \vdash \langle #2\rangle\,#3\,\R \langle #4\rangle\,#5}
\newcommand{\jp}[5]{#1 \vdash \langle #2\rangle\,#3\,\R \langle #4\rangle\,#5}

% Spacing:
\newcommand{\bigspc}{\hspace{2.5 ex}}

\newcommand{\axiom}[1]{$#1$\addstrut}
\newcommand{\ded}[2]{\begin{tabular}{c}
 \addstrut
  $ #1 $ \\ 
 \hline 
  $ #2 $ 
\end{tabular} \addstrut
}
\newcommand{\dedtwo}[3]{\begin{tabular}{c}
 \addstrut
 $ #1 $ \\ 
 $ #2 $ \\
 \hline 
 $ #3 $ 
\end{tabular} \addstrut
}
\newcommand{\dedtwoh}[3]{\begin{tabular}{c}
 \addstrut
 $ #1 $ \bigspc $ #2 $ \\
 \hline 
 $ #3 $ 
\end{tabular} \addstrut
}
\newcommand{\dedthreeh}[4]{\begin{tabular}{c}
 \addstrut
 $ #1 $ \bigspc $ #2 $ \bigspc $ #3 $ \\
 \hline 
 $ #4 $ 
\end{tabular} \addstrut
}
\newcommand{\dedfourh}[5]{\begin{tabular}{c}
 \addstrut
 $ #1 $ \bigspc $ #2 $ \bigspc $ #3 $  \bigspc $ #4 $ \\
 \hline 
 $ #5 $ 
\end{tabular} \addstrut
}
\newcommand{\dedthree}[4]{\begin{tabular}{c}
 \addstrut
 $ #1 $ \\ 
 $ #2 $ \\
 $ #3 $ \\
 \hline 
 $ #4 $ 
\end{tabular} \addstrut
}
\newcommand{\dedfour}[5]{\begin{tabular}{c}
 \addstrut
 $ #1 $ \\ 
 $ #2 $ \\
 $ #3 $ \\
 $ #4 $ \\
 \hline 
 $ #5 $ 
\end{tabular}\addstrut
}
\newcommand{\dedfive}[6]{\begin{tabular}{c}
 \addstrut
 $ #1 $ \\ 
 $ #2 $ \\
 $ #3 $ \\
 $ #4 $ \\
 $ #5 $ \\
 \hline 
 $ #6 $ 
\end{tabular} \addstrut
}

%       +  2    3 
%  1  = |  
%       +  4    5
\newcommand{\choicetwo}[5]{#1 = \left\{
\begin{array}{ll}
   #2 & \mbox{#3} \\
   #4 & \mbox{#5}
\end{array} \right.}
%       +  2    3 
%  1  = |  4    5
%       +  6    7
\newcommand{\choicethree}[7]{#1 = \left\{
\begin{array}{ll}
   #2 & \mbox{#3} \\
   #4 & \mbox{#5} \\
   #6 & \mbox{#7}
\end{array} \right.}

\newenvironment{grammar}
{\begin{xple}\begin{tabbing}XX\=XXX\=XXXXXXXXXXXXXXXXXXXXXXXXXXXXX\=\kill}{\end{tabbing}\end{xple}}

\newtheorem{theorem}{Theorem}

\newtheorem{corollary}{Corollary}

\title{
\parbox{13.5cm}{\footnotesize\vspace*{-1cm}Appeared in: C. Beeri, A.Ohori, and D.E. Shasha, editors, \e{Proceedings of the Fourth International Workshop on Database Programming Languages, August 1993, Manhatten, New York}, Workshops in Computing. Springer Verlag, Feburary 1994.}\\
$ $\\
\titlesize\bf Extensible Grammars\\for Language
Specialization}
\author{\large Luca Cardelli 
\and Florian Matthes 
\thanks{The second author was supported  by the European Commission,
ESPRIT, EC/US-FIDE Collaborative Activity, 006:9829.}
\and Mart\'{\i}n Abadi}

\date{\normalsize Digital Equipment Corporation\\Systems Research Center\\
130 Lytton Avenue\\Palo Alto, CA 94301, USA}

\begin{document} 
\maketitle
\begin{abstract}\ninesize
\noindent A frequent dilemma in the design of a database programming
language is the choice between a language with a rich set of tailored
notations for schema definitions, query expressions, etc., and a small,
simple core language. We address this dilemma by proposing extensible
grammars, a syntax-definition formalism for incremental language
extensions and restrictions based on an initial core language.

The translation of programs written in rich object languages into a
small core language is defined via syntax-directed patterns. In contrast
to macro-expansion and program-rewriting tools, our extensible grammars
respect scoping rules. Therefore, we can introduce binding constructs
while avoiding problems with unwanted name clashes.

We develop extensible grammars and illustrate their use by extending the
lambda calculus with let-bindings, conditionals, and SQL-style query
expressions.  We then give a formal description of the underlying
parsing, transformation, and substitution rules. Finally, we sketch how
these rules are exploited in the implementation of a generic, extensible
parser package.
\end{abstract}
\thispagestyle{empty}

%----------------------------------------------------------------------
\section{Introduction}

A frequent dilemma in the design of a database programming language is the
choice between a user-friendly language with a rich set of tailored
notations for schema definitions, query expressions, etc., and a small,
conceptually simple core language.  We address this dilemma by proposing
extensible grammars, a syntax-definition formalism for incremental,
problem-specific language extensions and restrictions based on an
initial core language.

The translation of programs written in rich, user-friendly object
languages into a small core language is defined via syntax-directed
patterns.  In contrast to traditional macro-expansion and
program-rewriting tools, our extensible grammars respect scoping rules.
Therefore, we can introduce new binding constructs like quantifiers,
iterators, and type declarations, while avoiding problems with unwanted
name clashes (``variable captures'').

{\bf Syntax extensions} provide syntactic sugar for common
problem-specific abstractions.  For example, embedded query notations
like the relational calculus, the relational algebra, iteration
statements, or set comprehensions can be introduced as abstractions
defined from more primitive iteration constructs
\cite{OBBT89,BTBN91,Trind91,MaSc91b}.  Transactions can be
introduced as stylized patterns for side-effect control and exception
handling. Similarly, structured form definitions in user interface code
can be represented as abstractions over low-level routines for data
formatting, input, and validation. At the type level, data modeling
constructs like classes, objects, and binary relationships can be
viewed as syntactic sugar for more complex type expressions involving
recursive types, record types, function types, or abstract data types
\cite{S*92,SSS88,PiTu93}.

{\bf Syntax restrictions} introduce intentional limitations on the
expressiveness or orthogonality of a core language. The rationale behind
restrictions is to facilitate meta-level reasoning and optimizations
tailored to a particular application domain.  While ad-hoc syntax
restrictions are generally considered harmful in programming language
design (from a pragmatic and a semantic perspective), they are common
practice in database models and database languages. For example, many
schema definition languages disallow nested declarations (nested sets,
nested classes) or limit recursive declarations to top-level
class or type definitions. Furthermore, user-defined types frequently do
not have first-class status, e.g., they may not appear as arguments to
collection-type constructors.  Similarly, query languages typically
impose restrictions to rule out side-effecting operations or calls to
user-defined functions in selection and join predicates \cite{SQLISO}.
Some query languages require static bindings to function identifiers
(disallowing higher-order functions or dynamic method dispatch)
\cite{SFL83}, and some disallow lambda abstractions within quantified
expressions \cite{BTBN91}.  Finally, recursive queries or views
are often subject to stratification constraints \cite{Naqv89}.

The form of extensible grammars discussed in this paper was invented
during the implementation of a polymorphically typed lambda calculus
\cite{Card93}. Here, we develop extensible grammars in a more general
context and describe them in more detail.  Section~\ref{Sec:Overview}
gives a conceptual overview of the issues that must be addressed by a
syntax-extension formalism. In section~3 we introduce extensible
grammars by examples. An initial grammar for the lambda calculus is
extended incrementally with new syntactic forms like let-bindings,
conditionals, as well as algebraic and calculus-style query notations.
In section~5 the static type rules for grammar definitions and the
semantics of parsers generated from extensible grammars are defined. We
also present a soundness result for the type system with respect to the
evaluation semantics. The impact of these foundations on the
implementation of an extensible parser module for the Tycoon database
environment \cite{Matt93} is highlighted in section~\ref{Sec:Package}.
Finally, section~\ref{Sec:Comparison} compares our concept of extensible
grammars with other approaches to syntax extension.

%-----------------------------------------------------------------------
\section{Overview}
\label{Sec:Overview}

The syntax extension formalism described in this paper assumes the
scenario depicted in figure~\ref{Fig:Grammar-Scenario}. Given the
abstract syntax and the scoping structure of a target language \e{TL}, a
new object language \e{OL$_0$} can be defined by giving its context-free
grammar and the rewrite rules that map \e{OL$_0$} terms into \e{TL}
terms.  The mapping also defines the scoping structure of \e{OL$_0$}.
Our formalism is incremental since it allows also the definition of an
object language \e{OL$_n$} by a translation (rewriting) into another
object language \e{OL$_{n-1}$}.

\begin{figure}
\begin{center} \leavevmode
\epsfxsize=\textwidth
\epsfbox{Overview.ps}
\end{center}
\caption{The syntax-extension scenario}
\label{Fig:Grammar-Scenario}
\end{figure}

For example, assuming \e{TL} to be a functional language, the object
language \e{OL$_0$} could have either a Lisp-like list notation or an
Algol-like keyword-based notation:
\begin{xple}
      (\k{defn} succ(x) (plus x 1))
      \k{function} succ (x); \k{begin} \k{return} plus(x, 1); \k{end} succ;
\end{xple}
Both syntactic forms translate into the same abstract syntax tree in the
target language \e{TL} that is passed to the \e{TL} type checker and
code generator:
\begin{xple}
      Abs(x App(App(plus x) 1))
\end{xple}
Section \ref{Sec:Initial} gives a complete example of the target-language
and the object-language definition for an untyped lambda calculus.

A simple example of an incremental syntax definition is the definition
of a language with infix function application (\e{OL$_1$}) as an
extension of a language with only prefix application (\e{OL$_0$}). The
notation \p{A} $\R$ \p{B} is used to indicate that the input \p{A} in an
extended language is equivalent to the input \p{B} in a non-extended
language:
\begin{center}
\small
\begin{tabular}{lcl}
\p{\k{function} succ (x);}                   &    & \p{\k{function} succ(x);} \\
\p{\k{begin} \k{return} x + 1 \k{end} succ;} &$\R$&\p{\k{begin} \k{return} plus(x,1) \k{end} succ;} \\
\end{tabular}
\end{center}

In a database programming setting, \e{OL$_n$} could be a language with
SQL-like query notations that is translated into a lambda calculus,
\e{OL$_{n-1}$}, with primitive operations on a collection type (\p{nil,
cons, iter}) \cite{Trind91}: 
\begin{center}\small
\begin{tabular}{lcl}
\p{\k{select} x.a}           &     & \p{iter(X)(nil)(\k{fun}(x)\k{fun}(z)} \\
\p{\k{from} x \k{in} X}      &$\R$ & \ \ \p{\k{if} p(x) \k{then}
cons(x.a)(z) \k{else} z)}\\
\p{\k{where} p(x)}           &     & \\
\end{tabular}
\end{center}
Incremental grammar definitions are discussed in more detail in
section~\ref{Sec:Incremental} and \ref{Sec:Pattern}. The definition of
an SQL-like grammar in our formalism is given in
section~\ref{Sec:Examples}.

Extensible grammars require extensible parsers. That is, a parser cannot
be generated once for a given target language, but has to be extended
dynamically to handle programmer-defined object languages.  New grammar
definitions should be checked to avoid problems typical of macro
definitions \cite{KeRi77}, such as grammar ambiguity, non-termination of
macro expansion, and generation of illegal syntax trees.  Our checking
is performed already at grammar-definition time and includes standard
grammar analysis \cite{ASU87} to avoid the first two problems.  To
address the third problem, we develop a sorting discipline on
productions (see section~\ref{Sec:Typing}).

A more subtle source of difficulties associated with incremental grammar
definition is the binding structure of the target language. The
rewriting of object-language expressions into target-language
expressions must be sensitive to the scoping rules of the target
language and may require renaming operations to avoid name clashes
(``variable captures''). A small example using C and the C preprocessor
illustrates the issue in a familiar setting:
\begin{xple}
\#define swap(x,y)  \{\k{int} z; z = x; y = x; x = z;\}
\{\k{int} a, b;  swap(a,b);\}   /* ok */
\{\k{int} z, y;  swap(z,y);\}   /* name clash */
\end{xple}
The expansion of \p{swap(z, y)} leads to the program fragment
\p{\{\k{int} z; z = z; y = z; z = z\}}, where the local declaration of
\p{z} hides the variable \p{z} that is passed as an argument to the
macro. Removing the curly brackets in the macro definition does not
solve the problem but yields a name clash between two declarations of
the variable \p{z} in the same scope. 

A solution of the scoping issues associated with rewriting inside
binding structures requires a formalization of the scoping rules of a
specific target language. To adapt our grammar formalism easily to
several target languages, we divide the scoping problem into a generic
bookkeeping task for the extensible parser and a parameterized
language-specific renaming operation. This conceptual division of labor
is exploited in the implementation of the extensible grammar package to
factor out target-language dependencies. Scoping problems are avoided by
distinguishing between binding and applied identifier occurrences, and
by renaming when name clashes between identifiers in input programs and
in rewrite rules could occur. Note that this solution is not an option
for a simple token-based preprocessor. Section~\ref{Sec:Parsing-Terms}
describes the parsing and renaming rules of our formalism (for initial
as well as incremental grammar definitions). We are also able to prove
that these dynamic parse rules are consistent with the static type rules
given in section~\ref{Sec:Typing}.

%-----------------------------------------------------------------------

\section{Grammar Definitions}

In this section we introduce our extensible grammar formalism by
examples. We start with a small initial grammar for an untyped lambda
calculus that is extended incrementally to support database programming
language constructs.

\begin{figure}[ht]
\figsep\begin{grammar}
\>\k{grammar}
\\ \>  simpleTerm:Term \newnt
\\ \>    \>x=\k{ide}                   \>=> mkTermVar(x)
\\ \>  | \>"(" a=term ")"              \>=> a
\\ \>  | \>"fun" "(" x=\k{ide} ")" a=term  \>=> mkTermFun(x a)
\\ \>  | \>"\{" f=fields "\}"          \>=> mkTermRcd(f)
\\ \>  | \>a=\k{pIde}:Term             \>=> a
\\ \> 
\\ \>  fields:Fields \newnt
\\ \>       \>x=\k{ide} "=" a=term f=fields   \>=> mkFieldCons(x a f)
\\ \>  | \>                            \>=> mkFieldNil()
\\ \>  | \>f=\k{pIde}:Fields           \>=> f
\\ \> 
\\ \>  term:Term \newnt
\\ \>    \>a=simpleTerm b=termIter(a) \>=> b
\\ \> 
\\ \>  termIter(a:Term):Term \newnt
\\ \>    \>"(" b=term ")"             \>=> termIter(mkTermApp(a b))
\\ \>  |\>"." x=\k{ide}                \>=> termIter(mkTermDot(a x))
\\ \>  |\>                             \>=> a
\\ \>\k{end}
\end{grammar}\figsep
\caption{Definition of a concrete syntax for the lambda calculus}
\label{Fig:Lambda-Syntax}
\end{figure}


\subsection{Initial Grammar Definitions}
\label{Sec:Initial}

This section explains how to define the abstract syntax and the
scoping rules of a particular target language \e{TL} as well as the
syntax for an initial object language \e{OL$_0$} (see the oval boxes in
figure~\ref{Fig:Grammar-Scenario}). This information is validated by the
grammar checker and then used to generate an initial parser for
\e{OL$_0$} programs.

We use an untyped lambda calculus with records as the target language
for our examples. Given a set of identifiers $x$, the sets of terms ($a,b$) and fields ($f$) are recursively defined as follows:
\begin{xple}
      $a$, $b$ ::= $x$ $|$ $\lambda$$x$.$a$ $|$ $a$($b$) $|$ \{$f$\} $|$ $a$.$x$
      $f$    ::= $\emptyset$ $|$ $x$=$a$ $f$
\end{xple}

The first step in the definition of an extensible grammar is to
define the names of the \e{sorts} and the signatures of the
\e{constructors} available for the construction of target-language
terms. Our example uses the following target-language-specific sorts: 
\begin{center}
\begin{tabular}{ll}
   \p{Term}    & terms of the lambda calculus \\
   \p{Fields}  & ordered associations between field names and terms 
\end{tabular}
\end{center}
Since identifiers require particular attention during expression
rewriting, there are three predefined sorts to distinguish the binding
properties of identifiers:
\begin{center}
\begin{tabular}{ll}
   \p{Binder}& identifiers appearing in binding positions\\
   \p{Var}   & identifiers appearing as variables inside the scope of a binder\\
   \p{Label} & identifiers that are not subject to scoping
\end{tabular}
\end{center}
These sort names appear in the signatures of the term constructors for
the lambda calculus:
\begin{xple}
      mkTermVar(x:Var):Term
      mkTermFun(x:Binder a:Term):Term
      mkTermApp(a:Term b:Term):Term
      mkTermRcd(f:Fields):Term
      mkTermDot(a:Term x:Label)
      mkFieldNil():Fields
      mkFieldCons(x:Label a:Term f:Fields):Fields
\end{xple}
Lambda abstractions (\p{mkTermFun}) introduce identifiers in binding
positions, while other identifiers inside terms (\p{mkTermVar}) appear
in non-binding positions. In our example, field labels (\p{mkTermDot,
mkFieldCons}) are not subject to block-structured scoping rules and are
therefore defined to be of sort \p{Label}. For the purpose of grammar
definitions it is not necessary to present the binding rules of the
target language in more detail. 

Given a target-language description in terms of constructors and sorts,
a context-free grammar is defined as a collection of productions that
translate phrases in an input stream into terms of the target language.
A concrete syntax for the lambda calculus with records is defined
in figure~\ref{Fig:Lambda-Syntax}. The notation used is explained in
the rest of this section. 

This grammar consists of four mutually recursive productions that define
precedence of applications over abstractions and left-associativity of
applications.  Here are examples of input phrases parsed according to
the root production \p{term}:
\begin{center}\small
\begin{tabular}{ll}
\p{peter}               & \p{mkTermVar(peter)} \\
\p{peter.age}           & \p{mkTermDot(mkTermVar(peter) age)} \\
\p{fun(p)p(b)}          & \p{mkTermFun(p mkTermApp(mkTermVar(p) mkTermVar(b)))}
\end{tabular}
\end{center}

The result of parsing is a structured term of the target language. This
term can be viewed as a tree in which the inner nodes correspond to term
constructor applications and the leaves correspond to identifiers (or
literals) extracted from the source text. A token sequence to which no
production applies is rejected by the parser with an error message.

A grammar introduces a set of non-terminals (\p{simpleTerm},
\p{term}, \ldots) as identifiers for productions. Productions can be
parameterized by terms of the target language (see, e.g., \p{termIter}).
The signature of a non-terminal defines its parameter names and sorts as
well as the sort of terms returned by the production.

Each production consists of $n\geq 1$ expression sequences separated
from each other by a vertical bar (\p{|}). Each expression specifies an
input syntax and a result expression (following the \p{=>} symbol) to
construct a term of the target language.  Based on the token sequence
encountered during parsing, one of the alternative expression sequences
is selected and its corresponding result expression is evaluated in an
environment that contains the actual parameter bindings and local
bindings introduced on the left of the \p{=>} symbol.

The input syntax accepted by an alternative is defined using the
following notation:
\begin{center}
\begin{tabular}{lp{10cm}}
\p{"x"}                & accept the keyword \k{x} \\
\p{\k{ide}}            & accept any non-keyword identifier\\
\p{x}                  & accept the input specified by the 
                         production identified by the non-terminal 
                         \p{x}\\
\p{x(y)}               & accept the input specified by the 
                         parameterized production identified by the non-terminal 
                         \p{x} with the argument \p{y}\\
\p{x=y}                & bind the term defined by \p{y} to a local 
                         variable \p{x}\\
\p{\k{pIde}:S}         & accept a pattern variable of sort \p{S}
                         (see section~\ref{Sec:Pattern})\\
\end{tabular}
\end{center}

Each grammar determines a set of keywords reachable from productions of
the grammar. The set of identifiers accepted by \k{ide} in a given
grammar \p{g} excludes the keywords of \p{g}. Therefore, syntax
extensions may introduce new keywords while syntax restrictions may change
existing keywords into identifiers.

The binding structure of the concrete syntax is defined implicitly by
passing identifier tokens from the input as arguments to term
constructors. For example, the variable \p{x} in the grammar definition
\begin{grammar}
\>   \>"fun" "(" x=\k{ide} ")" a=term  \>=> mkTermFun(x a)
\end{grammar}
appears in a \p{Binder} position of the term constructor \p{mkTermFun}.
Therefore, it can be deduced that the variable \p{person} in the 
source text \p{\k{fun}(person) \ldots} appears in a binding position.

The recursive production \p{fields} in figure~\ref{Fig:Lambda-Syntax}
generates right-associative syntax trees for field lists while the
production \p{termIter} generates left-associative syntax trees for
function applications. Because we use an LL(1) parser, left-associative
grammars are handled in our grammar formalism by passing the syntax tree
for the left context of a phrase as a production argument for the
recursive invocation of a production (e.g., \p{a:Term} in production
\p{termIter} in figure~\ref{Fig:Lambda-Syntax}).

%-----------------------------------------------------------------------

\subsection{Incremental Grammar Definitions}
\label{Sec:Incremental}

This section explains how to define the syntax of a new object language
\e{OL$_n$} as an extension or a restriction of an existing object
language \e{OL$_{n-1}$}. Such a syntax redefinition is validated by the
grammar checker and used to derive a parser for \e{OL$_n$} from an
existing parser for \e{OL$_{n-1}$}.

A grammar defines a mapping from non-terminals (e.g., \p{simpleTerm},
\p{term}) to variables that are initialized with productions.
Inside a production, each non-terminal denotes the production identified
by its variable. Three incremental grammar operations are available:
addition, extension, and update.  The rationale behind these operations
is to allow update and re-use of existing non-terminal definitions,
preserving the recursive structure of the grammar.

A grammar addition (\p{==}) defines a mapping from a non-terminal to
a newly created variable initialized with a production. For example,
we could use the standard encoding of let bindings: 
\begin{grammar}
\>  \>\k{let} x=a \k{in} b  \>$\R$ (\k{fun}(x) b)(a) 
\end{grammar}
to add the new non-terminal \p{topLevel}:
\begin{grammar}
\>\k{grammar}
\\ \>  topLevel:Term \newnt
\\ \>    \>a=term               \>=> a
\\ \>  | \>"let" x=\k{ide} "=" a=term 
\\ \>    \>"in" b=topLevel      \>=> mkTermApp(mkTermFun(x b) a)
\\ \>\k{end}
\end{grammar}
The non-terminal \p{topLevel} is mapped to a newly created variable
initialized with a production that accepts terms of the base language and
(nested) let bindings at the top level, but not inside terms. 

A grammar extension (\p{\extendnt}) destructively updates the variable
identified by a non-terminal with a new production. The new production
extends the old production with additional alternatives. For example, to
extend \p{simpleTerm}, we could write:
\begin{grammar}
\>\k{grammar}
\\ \>  simpleTerm:Term \extendnt 
\\ \>    \>"unit"           \>=> mkTermRcd(mkFieldNil())
\\ \>  | \>"let" x=\k{ide} "=" a=term 
\\ \>    \>"in" b=term      \>=> mkTermApp(mkTermFun(x b) a)
\\ \>\k{end}
\end{grammar}
This grammar extension affects all productions referring to \p{term},
allowing \k{unit} and nested \k{let} bindings within terms.

A grammar update (\p{\updatent}) destructively updates the contents
of a variable identified by a non-terminal with a new production that
has the same signature, thereby affecting all productions referring to
that non-terminal. For example, the definition of \p{term} could be
updated as follows:
\begin{grammar}
\>\k{grammar}
\\ \>  term:Term \updatent
\\ \>    \>x=\k{ide}                   \>=> mkTermVar(x)
\\ \>  | \>"(" a=term b=term ")"       \>=> mkTermApp(a b)
\\ \>  | \>"\{" f=fields "\}"          \>=> mkTermRcd(f)
\\ \>\k{end}
\end{grammar}
This redefinition affects all productions referring to \p{term}
(\p{simpleTerm}, \p{fields}, \p{termIter}), thereby restricting the
expressiveness of the original language by disallowing abstractions.

%-----------------------------------------------------------------------

\subsection{Pattern-based Action Definitions}
\label{Sec:Pattern}

In the previous section, abstract syntax trees produced by actions are
specified with explicit constructor applications.  In this section we
introduce patterns which allow us to write grammars more conveniently by
using the existing target language. For example, the syntax for \k{let}
and \k{where} bindings could be written more clearly using a pattern:
\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}
Inside the pattern \p{term<<(\k{fun}(x) b)(a)>>}, the variables \p{x,
a}, and \p{b}, introduced on the left-hand side of the production, act
as placeholders (pattern variables) of sort \p{Binder}, \p{Term},
and \p{Term}, respectively.  A pattern \p{p<<s>>} in a grammar
\p{g} is translated into constructor applications by parsing the input
token stream \p{s} starting with the production \p{p}.  For example, the
pattern \p{term<<(\k{fun}(y) b)(a)>>} yields the nested constructor
application \p{mkTermApp( mkTermFun(y b) a)} when the token stream
\p{(\k{fun}(y) b)(a)} is parsed as a \p{term}.

The keyword \k{pIde} followed by a sort identifier is used in the
initial grammar definition (see section~\ref{Sec:Initial}) to indicates
those positions in the input syntax where pattern identifiers may appear.
Pattern variables of the sorts \p{Binder}, \p{Var}, and \p{Label} may
appear also at those places in the input syntax where the keyword
\k{ide} is used to accept identifier tokens of the appropriate sort.

Many pattern-based syntax extensions require the introduction of
fresh identifiers, i.e., identifiers distinct from other identifiers
appearing in \p{Binding} and \p{Var} positions, to avoid variable captures
and name clashes. For example, the syntax for functional composition
(\p{f * g}) could be defined as:
\begin{grammar}
\>\k{grammar}
\\ \>  termIter(a:Term):Term \extendnt\  
\\ \>       \>"*" b=term x=\k{local}     => termIter(term<<\k{fun}(x)a(b(x))>>)
\\ \>\k{end}
\end{grammar}
The notation \p{x=\k{local}} guarantees that a fresh identifier is bound
to \p{x} for every instantiation of this production during parsing. For
example, \p{f*g*h} is expanded to \p{\k{fun}(x2)(f(\k{fun}(x1)g(h(x1)))
(x2))}, and \p{x*y} is expanded to \p{\k{fun}(x1)(x(y(x1)))}, avoiding a
variable capture of the input variable \p{x} by a binder introduced in
the pattern.

Since grammar definitions can be interspersed with object-language
expressions, it is desirable to allow patterns to contain variables that
refer to global bindings. For example, the boolean constants true
and false are sometimes represented by the following functions
which, when applied to two arguments, return one of them:
\begin{xple}
\k{let} T = \k{fun}(x)\k{fun}(y)x
\k{let} F = \k{fun}(x)\k{fun}(y)y
\end{xple}
In the scope of these definitions, the following grammar could be defined
to replace the keywords \k{true} and \k{false} by the variables \p{T}
and \p{F}, respectively. 
\begin{grammar}
\>\k{grammar}
\\ \>  simpleTerm:Term \extendnt\  
\\ \>   \>"true"                  \>=> term<<T>>
\\ \>  |\>"false"                 \>=> term<<F>>
\\ \>  |\>"if" a=term "then" b=term 
\\ \>   \>"else" c=term           \>=> term<<a(b)(c)>>
\\ \>\k{end}
\end{grammar}
\label{Keyword:Global-Vars}
During expansion of a pattern with free variables (\p{T} and \p{F} in
the example above), unwanted variable captures must be avoided. For
example, a naive macro expansion of the term \p{\k{fun}(T) T(\k{true})}
would yield the term \p{\k{fun}(T) T(T)} where the expansion of the
keyword \k{true} is bound incorrectly.  Therefore, free variables in
extensible grammars are handled as follows: Each occurrence of a free
variable \p{x} in a grammar definition is replaced by a fresh variable
\p{x'}.  During parsing, these modified patterns generate expansions
that contain unbound variables (\p{T'} and \p{F'}).  For example,
\p{T(\k{fun}(T) T(\k{true}))} is expanded to
\p{T(\k{fun}(T) T(T'))}.  After the full input has been parsed, a
target-language-specific renaming function is applied to the parsed
term. It replaces the binder \p{T} and its bound variables by \p{T''}
and \p{T'} by \p{T}. The resulting term \p{T(\k{fun}(T'') T''(T))} is
then submitted to the type checker and code generator.

%-----------------------------------------------------------------------

\subsection{Further Examples: Query Notations}
\label{Sec:Examples}

In this section we show how some typical database query notations can be
viewed as mere ``syntactic sugar'' for the application of a single
higher-order iterator function. The reduction of query notations into a
single canonical iteration construct has been exploited in the
literature to simplify the type checking of database programming
languages \cite{OBBT89}, the code generation for query expressions
\cite{Trind91}, and the verification of functional database programs
\cite{StSh91,SSS88}.  The following examples demonstrate that extensible
grammars provide sufficient expressive power to define the syntax of
typical database query languages as well as their translation into
lambda calculus. This translation preserves the usual scoping rules
defined for these query languages.

We assume the grammar extension for booleans defined above and the
following global definitions that provide a standard encoding of the
list constructors \p{nil} and \p{cons} and a list iterator \p{iter}:
\begin{xple}
\k{let} nil = \k{fun}(x)\k{fun}(n)\k{fun}(c) n
\k{let} cons = \k{fun}(hd)\k{fun}(tl)\k{fun}(n)\k{fun}(c) c(hd)(tl(n)(c))
\k{let} iter = \k{fun}(l)\k{fun}(n)\k{fun}(c) l(n)(c)
\end{xple}
The syntax of a ``list algebra'' with selection, projection, and binary
join can then be defined as follows:
\begin{grammar}
\k{grammar}
\\  simpleTerm:Term \extendnt\ 
\\    "select" x=\k{ide} "in" a=term "where" b=term y=\k{local} 
\\  => term<<iter(a)(nil)(\k{fun}(x)\k{fun}(y)\k{if} b \k{then} cons(x)(y) \k{else} y)>>
\\  | "project" x=\k{ide} "in" a=term "onto" f=fieldList(x) y=\k{local}   
\\  => term<<iter(a)(nil)(\k{fun}(x)\k{fun}(y)cons(\{f\})(y))>>
\\  | "join" x=\k{ide} "in" a=term "," y=\k{ide} "in" b=term 
\\    "where" c=term x2=\k{local} y2=\k{local}
\\  => term<<iter(a)(nil)(\k{fun}(x)\k{fun}(x2)iter(b)(x2)(\k{fun}(y)\k{fun}(y2)
\\           \k{if} c \k{then} cons(\{fst=x snd=y\})(y2)\k{else} y2))>>
\\  fieldList(x:Var):Fields \newnt
\\     y=\k{ide} "," f=fieldList(x) \>\>\>=> fields<<y=x.y f>>
\\  |                               \>\>\>=> fields<<>>
\\\k{end}
\end{grammar}
For example, a selection expression with a variable identifier \p{x}, a
range expression \p{a}, and a selection predicate \p{b} is translated
into an iterative loop. This loop over \p{a} has \p{x} as its loop
variable and starting with the empty list \p{nil} it adds those elements
that satisfy the selection predicate \p{b}:
\begin{xple}
iter(a)(nil)(\k{fun}(x)\k{fun}(y)\k{if} b \k{then} cons(x)(y) \k{else} y)
\end{xple}
In this expression, \p{y} is a fresh local variable which is bound
during iteration to the result of the previous iteration step. This
translation correctly captures the scoping rules for the list algebra,
since the variable \p{x} is visible only in \p{b} and not in \p{a}.
Furthermore, global identifiers are visible in \p{a} and \p{b}.

The parameterized production \p{fieldList} demonstrates how parameters
may be used to distribute terms (in this case a variable identifier
\p{x}) into multiple subterms.  Using the extended grammar one can write,
for example, the following queries that use global identifiers
\p{Persons, thirty,} and \p{equal}:
\begin{xple}
\k{select} p \k{in} Persons \k{where} greater(p.age)(thirty)
\k{project} p \k{in} Persons \k{onto} name, age
\k{join} p \k{in} Persons, s \k{in} Students \k{where} equal(p.name)(s.name)
\end{xple}
Furthermore, it is possible to nest queries and to parameterize
queries:
\begin{xple}
\k{fun}(limit) \k{select} p \k{in}
    \k{select} p \k{in} Persons \k{where} greater(p.salary)(limit)
\k{where} greater(p.age)(thirty)
\end{xple}
Note that the identifier \p{p} in the subquery will be correctly bound to
the inner \p{p} in the generated lambda term.

Simulating SQL expressions is slightly more complicated, since SQL
allows the repetition of range expressions to express selections, projections,
and $n$-way joins using a uniform notation:
\label{Keyword:SQL}
\begin{xple}
\k{select} target(x) \k{from} x \k{in} a \k{where} predicate(x)
\k{select} target(x)(y) \k{from} x \k{in} a, y \k{in} b \k{where} predicate(x)(y)
\k{select} target(x)(y)(z) \k{from} x \k{in} a, y \k{in} b, z \k{in} c 
\k{where} predicate(x)(y)(z)
\ldots
\end{xple}
Therefore, the rewrite rules have to ensure that the target and the
selection expressions appear in the scope of $n$ ($n>1$) \k{fun} binders
in the generated lambda term. The following grammar uses a
recursive, parameterized production \p{rangeIter} to achieve the desired
rewriting: 
\begin{grammar}
\k{grammar}
\\  simpleTerm:Term \extendnt\ 
\\     "select" a=term "from" x=\k{ide} "in" b=term c=rangeIter(a)   
\\  => term<<iter(b)(nil)(\k{fun}(x)c)>>
\\  rangeIter(a:Term):Term \newnt
\\     "," x=\k{ide} "in" b=term c=rangeIter(a) y=\k{local}
\\  => term<<\k{fun}(y)iter(b)(y)(\k{fun}(x)c)>>
\\    |"where" b=term y=\k{local}   
\\  => term<<\k{fun}(y)\k{if} b \k{then} cons(a)(y) \k{else} y>>
\\\k{end}
\end{grammar}
For example, a two-way join would be expanded as follows:
\begin{center}
\small
\begin{tabular}{lcl}
\k{select} \{x.a y.b\}          &     & iter(X)(nil)(\k{fun}(x) \\
\k{from} x \k{in} X, y \k{in} Y &$\R$ & \ \ \k{fun}(z1) iter(Y)(z1)(\k{fun}(y) \\
\k{where} p(x.c)(y.c)           &     & \ \ \ \  \k{fun}(z2) \k{if} p(x.c)(y.c) \k{then} \\
                                &     & \ \ \ \ \ cons(\{x.a y.b\})(z2) \k{else} z2))
\end{tabular}
\end{center}

%-----------------------------------------------------------------------

\section{Formalizing Grammars and Parsers}

In section~\ref{Sec:Typing} we describe the rules that are used in the
grammar checker (see figure~\ref{Fig:Grammar-Scenario}) to statically
decide whether a sequence of grammar definitions and grammar extensions
is well-formed. In section~\ref{Sec:Parsing-Terms} we formalize the
parse rules that define the mapping from an input stream into a
constructed term of the target language. We also present a soundness
result of the dynamic parse rules with respect to the static type rules
of section~\ref{Sec:Typing} which guarantees that parsers derived from
well-typed grammars return well-formed parse trees. This result is
generalized in the full paper to parsers derived from incremental
pattern-based grammar definitions.
% section~\ref{Sec:Parsing-Patterns} 

\subsection{Static Typing of Grammar Definitions}
\label{Sec:Typing}

To describe the type rules for grammar definitions and extensions, we
first define the relevant syntactic objects (sorts, signatures,
productions, grammars, grammar sequences).

The syntax for term sorts $B$ and signatures $S$ is defined as follows:
\begin{center}
\begin{tabular}{rll}
$B::=$ & $\mbox{Unit}\ |\ \mbox{Var}\ |\ \mbox{Binder}\ |\ \mbox{Label}$
                                    & predefined term sorts \\
  $|$  & $\mbox{B}^1\ |\ \ldots\ |\ \mbox{B}^n$   
                                    & target-language-specific sorts 
                                      ($n\geq0$) \\
$S::=$ & $(B_1, \ldots, B_k) B$     & production signatures ($k\geq0$)
\end{tabular}
\end{center}
The abstract syntax of productions is slightly more orthogonal than the
concrete syntax we have used in the examples. In particular, terminal
productions like \p{\k{ide}(B)} or \p{"x"} may appear nested within
constructor and production argument lists. Furthermore, the syntactic
separation of productions into a binding sequence and a constructor
application (to the right and left of the \p{=>}, respectively) is no
longer enforced. For example, the production \p{x=\k{ide} =>
mkTermVar(x)} in the concrete syntax is translated into a simple sequential
composition $x=\k{ide}(\mbox{Var})\ \mbox{\p{mkTermVar}}(x)$. 
\begin{center}
\begin{tabular}{rll}
$p::=$ & $\k{unit}$            & unit production \\
  $|$  & $"x"$                 & keyword token production\\
  $|$  & $\k{ide}(B)$          & variable token production (of sort $B$)\\
  $|$  & $\k{local}$           & fresh object-language variable\\
  $|$  & $\k{global}(x)$       & global object-language variable\\
  $|$  & $x$                   & term variable\\
  $|$  & $p_1\ p_2$            & sequential composition\\
  $|$  & $x=p_1\ p_2$          & pattern variable binding\\
  $|$  & $p_1\ |\ p_2$         & choice\\
  $|$  & $x(p_1, \ldots, p_k)$ & non-terminal application ($k\geq0$)\\
  $|$  & $c_{(B_1, \ldots, B_k)B}(p_1, \ldots, p_k)$ 
                               & sorted constructor application ($k\geq0$)\\
\end{tabular}
\end{center}
The set of constructors $c_{(B_1, \ldots, B_k)B}$ with argument sorts
$B_i$ and result sort $B$ contains the target-language-specific
constructors (e.g., \p{mk\-Term\-Var, mk\-Term\-Fun}).

A grammar consists of a list of non-terminal definitions that define
a signature, a modification operator, and a production.
\begin{center}
\begin{tabular}{rll}
$g::=$ & $[]$                                    & empty grammar \\
  $|$  & $g\ x:(x_1{\HT}B_1, \ldots, x_k{\HT}B_k) B\ a\ p$& non-terminal definition\\
$a::=$ & $\newnt$                                & grammar addition \\
  $|$  & $\updatent$                             & grammar update \\
  $|$  & $\extendnt$                             & grammar extension \\
\end{tabular}
\end{center}
Each grammar is defined in the scope of its preceding grammar definitions:
\begin{center}
\begin{tabular}{rll}
$\gseq::=$ & $        $ & empty grammar sequence \\
     $|$   & $\gseq\ g$ & grammar composition \\
\end{tabular}
\end{center}
A global environment $E$ assigns signatures to non-terminals:
\begin{center}
\begin{tabular}{rll}
$E::=$ & $\oslash$         & empty environment \\
  $|$  & $E,x:S$           & non-terminal $x$ has signature $S$\\
\end{tabular}
\end{center}
A local environment $L$ assigns signatures to term variables:
\begin{center}
\begin{tabular}{rll}
$L::=$ & $\oslash$         & empty environment \\
  $|$  & $L,x:B$           & variable $x$ has sort $B$\\
\end{tabular}
\end{center}
Environment concatenation is written as $E,E'$. The domain of an
environment, denoted by $Dom(E)$, is the set of variables $x$ defined in
$E$. A variable name $x$ may occur more than once in an environment.  In
this case, the type rules for variables retrieve the rightmost sort
or signature assigned to $x$.

The static semantics of grammars involves the following judgements:
\begin{center}
\begin{tabular}{ll}
$\jdg{E;L}{p:B}$     & production $p$ has sort $B$ assuming $E$ and $L$\\
$\jdg{E}{g::E'}$     & grammar $g$ defines signatures $E'$ consistent with $E$\\
$\jdg{E}{g\ \k{ok}}$ & grammar $g$ defines productions consistent with $E$\\
$\jdg{}{\gseq \R E}$ & grammar sequence $\gseq$ defines a final environment $E$\\
\end{tabular}
\end{center}

The structure of the sort rules for productions $p$ resembles the
structure of typing rules for terms in a simply-typed lambda calculus:

\noindent
\begin{tabular}{cc}
\begin{minipage}{4.5cm}
\begin{center}\small
\ 
 
\axiom{\jdg{E;L}{\k{unit}:\mbox{Unit}}}

\axiom{\jdg{E;L}{"x":\mbox{Unit}}}

\axiom{\jdg{E;L}{\k{ide}(B):B}}

\axiom{\jdg{E;L}{\k{local}:\mbox{Binder}}}

\axiom{\jdg{E;L}{\k{global}(x):\mbox{Var}}}

\ded{
 x\not\in Dom(L')
}{
  \jdg{E;L,x:B,L'}{x:B}
}

\dedtwoh{
  \jdg{E;L}{p_1:B}
}{
  \jdg{E;L}{p_2:B'}
}{
  \jdg{E;L}{p_1\ p_2:B'}
}

\end{center}
\end{minipage}
&

\begin{minipage}{7cm}
\begin{center}\small
\dedtwoh{
  \jdg{E;L}{p_1:B}
}{
  \jdg{E;L,x:B}{p_2:B'}
}{
  \jdg{E;L}{x=p_1\ p_2:B'}
}

\dedtwoh{
  \jdg{E;L}{p_1:B}
}{
  \jdg{E;L}{p_2:B}
}{
  \jdg{E;L}{p_1\ |\ p_2:B}
}

\ded{
  \jdg{E;L}{p_i:B_i} \bigspc 1 \leq i \leq k
}{
  \jdg{E;L}{c_{(B_1, \ldots, B_k)B}(p_1, \ldots, p_k):B}
}

\dedtwoh{
  \jdg{E;L}{p_i:B_i} \bigspc 1 \leq i \leq k
}{
  x\not\in Dom(E')
}{
  \jdg{E,x:(B_1, \ldots, B_k)B,E';L}{x(p_1, \ldots, p_k):B}
}

\end{center}
\end{minipage}
\end{tabular}

Since non-terminal definitions can be recursive, the type checking of a
grammar $g$ is performed in two passes. A first pass ($\jdg{E}{g::E'}$)
collects the signatures $E'$ of all non-terminals in $g$, verifies that
each non-terminal is defined at most once in $g$, and asserts that all
grammar updates ($x:S \updatent p$) and grammar extensions ($x:S
\extendnt p$) refer to non-terminals with matching signatures in the
scope $E$ of $g$:
\begin{center}
\axiom{\jdg{E}{[]::\oslash}}

\dedtwoh{
  \jdg{E}{g::E'}
}{
  x\not\in Dom(E')
}{
  \jdg{E}{g\ x:(x_1{\HT}B_1, \ldots, x_k{\HT}B_k) B\ \newnt\ p\ ::\ 
      E',x:(B_1, \ldots, B_k) B}
}

\dedtwo{
  \jdg{E}{g::E'} \bigspc x\not\in Dom(E') \bigspc a\in\{\updatent,\extendnt\}
}{
  \jdg{E}{x:(B_1, \ldots, B_k) B}
}{
  \jdg{E}{g\ x:(x_1{\HT}B_1, \ldots, x_k{\HT}B_k)B\ a\ p\ ::\ E',x:(B_1, \ldots,B_k) B}
}
\end{center}
In a second pass ($\jdg{E}{g\ \k{ok}}$), the bodies $p$ of all
non-terminal definitions in $g$ are checked to match their signatures
in $E$. The rules for parameterized non-terminal
definitions resemble the type rules for lambda abstractions:
\begin{center}
\axiom{\jdg{E}{[]\ \k{ok}}}
\bigspc
\dedtwoh{
  \jdg{E}{g\ \k{ok}}
}{
  \jdg{E;\oslash,x_1:B_1, \ldots, x_k:B_k}{p:B} \bigspc a\in\{\newnt,\updatent,\extendnt\}
}{
  \jdg{E}{g\ x:(x_1{\HT}B_1, \ldots, x_k{\HT}B_k)B\ a\ p\ \k{ok}}
}
\end{center}
A sequence of grammars is verified by performing the above two passes on
each grammar in the sequence using the environment established by its
preceding grammars:
\begin{center}
\axiom{\jdg{}{\R \oslash}} 
\bigspc
\dedthreeh{
  \jdg{}{\gseq \R E}
}{
  \jdg{E}{g::E'}
}{
  \jdg{E,E'}{g\ \k{ok}}
}{
  \jdg{}{\gseq\ g\ \R E,E'}
}
\end{center}

It is possible to derive a simple consistency-checking algorithm from
these inference rules as follows: Starting with the proof goal
$\jdg{}{\gseq\R E'}$, the inference rules have to be applied
``backwards'' (from the conclusions to the assumptions). Since for each
syntactic construct there is exactly one applicable inference rule, the
derivation either reaches the axioms (in time proportional to the size
of the grammar) or gets stuck in a configuration where no inference rule
can be applied. In the latter case the grammar sequence is rejected as
ill-typed. In the next section we prove that parsers derived from
well-typed grammars never generate ill-formed syntax trees.

\subsection{Parsing and Term Construction}
\label{Sec:Parsing-Terms}

\noindent Each non-terminal $x$ in a grammar serves a dual purpose.  On the one
hand, it determines how to parse an input token stream and how to
construct a corresponding term of the target language. On the other
hand, it defines how to transform a pattern (a token stream inside
\p{<<>>} brackets) occurring in an incremental grammar definition into an
equivalent production.  In this section we describe the parsing of input
token streams, while pattern parsing is described in the full paper.

For the purpose of parsing it is convenient to rewrite a 
grammar sequence $\gseq$ into a single grammar $g$ 
of the form $[], x_1:S_1\newnt p_1, \ldots, x_k:S_k\newnt p_k$
$(k \geq 0)$ such that $x_i\not= x_j$ for $i\not=j$. We use the notation:
\begin{center}
\begin{tabular}{ll}
$\gseq \leadsto g$  & grammar sequence $\gseq$ normalizes to $g$
\end{tabular}
\end{center}

\begin{figure}
\figsep
\begin{center}\small
\axiom{\jd{g;\LL}{s,i}{\k{unit}}{s,i}{\k{unit}}}
\vspace{2mm}

\axiom{\jd{g;\LL}{x::s,i}{"x"}{s,i}{\k{unit}}}
\vspace{2mm}

\axiom{\jd{g;\LL}{x::s,i}{\k{ide}(B)}{s,i}{x_B} \bigspc x\not\in K(g)
\bigspc B\in\{\mbox{Binder,Var,Label}\}}
\vspace{2mm}

\axiom{\jd{g;\LL}{s,i}{\k{local}}{s,i+1}{x^i_{Binder}}}
\vspace{2mm}

\axiom{\jd{g;\LL}{s,i}{\k{global}(x)}{s,i}{x_{Var}}}
\vspace{2mm}

\axiom{\jd{g;\LL,x=t,\LL'}{s,i}{x}{s,i}{t} 
\bigspc x\not\in Dom(\LL')}
\vspace{2mm}

\axiom{\jd{g;\LL}{s,i}{x}{s,i}{\k{wrong}}
\bigspc x\not\in Dom(\LL)}
\vspace{2mm}

\dedtwo{
  \jd{g;\LL}{s,i}{p_1}{s',i'}{t} \bigspc t\not=\k{wrong}
}{
  \jd{g;\LL}{s',i'}{p_2}{s'',i''}{t'}
}{
  \jd{g;\LL}{s,i}{p_1\ p_2}{s'',i''}{t'}
} 
\dedtwo{
  \ 
}{
  \jd{g;\LL}{s,i}{p_1}{s',i'}{\k{wrong}}
}{
  \jd{g;\LL}{s,i}{p_1\ p_2}{s'',i''}{\k{wrong}}
} 
\vspace{2mm}

\dedtwo{
  \jd{g;\LL}{s,i}{p_1}{s',i'}{t} \bigspc t\not=\k{wrong}
}{
  \jd{g;\LL,x=t}{s',i'}{p_2}{s'',i''}{t'}
}{
  \jd{g;\LL}{s,i}{x=p_1\ p_2}{s'',i''}{t'}
} 
\dedtwo{
  \
}{
  \jd{g;\LL}{s,i}{p_1}{s',i'}{\k{wrong}}
}{
  \jd{g;\LL}{s,i}{x=p_1\ p_2}{s',i'}{\k{wrong}}
} 
\vspace{2mm}

\ded{
  \jd{g;\LL}{s,i}{p_1}{s',i'}{t}
}{
  \jd{g;\LL}{s,i}{p_1\ |\ p_2}{s',i'}{t}
} 
\ded{
  \jd{g;\LL}{s,i}{p_2}{s',i'}{t}
}{
  \jd{g;\LL}{s,i}{p_1\ |\ p_2}{s',i'}{t}
} 
\vspace{2mm}

\ded{
  \jd{g;\LL}{s_{j-1},i_{j-1}}{p_j}{s_j,i_j}{t_j} 
      \bigspc 1\leq j\leq k
}{
  \jd{g;\LL}{s_0,i_0}{c_{(B_1, \ldots, B_k)B}
   (p_1, \ldots, p_k)}{s_k,i_k} {c_{(B_1, \ldots, B_k)B}(t_1, \ldots, t_k)}
} 
\vspace{2mm}

\dedthree{
  \jd{g;\LL}{s_{j-1},i_{j-1}}{p_j}{s_j,i_j}{t_j} 
      \bigspc 1\leq j\leq k
}{
  (x:(x_1{\HT}B_1, \ldots, x_k{\HT}B_k) B) \newnt p \in g
}{
  \jd{g;\oslash\ x_1=t_1\  \ldots\  x_k=t_k}{s_k}{p}{s',i'}{t}
      \bigspc 
}{
  \jd{g;\LL}{s_0,i_0}{x(p_1, \ldots, p_k)}{s',i'}{t}
} 
\dedthree{
  \jd{g;\LL}{s_{j-1},i_{j-1}}{p_j}{s_j,i_j}{t_j} 
      \bigspc 1\leq j\leq k
}{
   (x:(x_1{\HT}B_1, \ldots, x_k{\HT}B_k) B \newnt p) \not\in g
}{
  \jd{g;\oslash\ x_1=t_1\  \ldots\  x_k=t_k}{s_k}{p}{s',i'}{t}
      \bigspc 
}{
  \jd{g;\LL}{s_0,i_0}{x(p_1, \ldots, p_k)}{s',i'}{\k{wrong}}
} 
\end{center}
\figsep
\caption{Parse rules for terms}
\label{Fig:Parsing-Terms}
\end{figure}

In this rewrite process, grammar updates ($x:S\updatent p$) and grammar
extensions ($x:S\extendnt p$) are eliminated by changing their
corresponding original definitions ($x:S \newnt p'$) into $x:S \newnt p$ and $x:S
\newnt p\ |\ p'$, respectively. Name conflicts between 
grammar additions $x:S\newnt\ p$ and $x:S'\newnt p'$
($p\not=p'$) in two grammars of $\gseq$ are resolved by
consistently renaming one of the non-terminals to a
fresh non-terminal $x'$ within in its local scope.  
It is easy to see that normalization preserves typing, that is, if
$\gseq \leadsto g$ and $\jdg{}{\gseq \R E}$, then $\jdg{}{g \R
E'}$, where $E'$ is equal to $E$ up to duplicate elimination.

We use the following notation to describe how a production of a grammar
$g$ applied to an input stream constructs a term $t$ of the target
language:
\[\jd{g;\LL}{s,i}{p}{s',i'}{t}\]
\noindent It states that production $p$ executed in environment $g;\LL$
starting in the initial configuration $\langle s,i \rangle$ returns a term $t$
and a final configuration $\langle s',i' \rangle$. A dynamic
environment $\LL$ contains local term variable bindings.  A configuration
$\langle s,i \rangle$ consists of the input stream $s$ and an integer
counter $i$ to generate unique fresh identifiers $x^i_B$ distinct from
user-defined identifiers of the form $x_B$. 

The parsing rules are given in figure~\ref{Fig:Parsing-Terms}. These
rules involve syntactic objects of the following categories:
\begin{center}
\begin{tabular}{rll}
$s::=$ &                   & \k{input streams} \\
       & $*$               & empty input stream\\
  $|$  & $x::s$            & identifier token\\
$b::=$ &                   & \k{terms} \\
       & $\k{unit}$        & trivial term \\
  $|$  & $x_{Binder}$      & binder identifier \\
  $|$  & $x_{Var}$         & variable identifier \\
  $|$  & $x_{Label}$       & label identifier \\
  $|$  & $x^i_B$           & fresh identifier of sort $B$ ($i\geq0$)\\
       &                   & $B\in\{\mbox{Binder},\mbox{Var},\mbox{Label}\}$\\
  $|$  & $c_{(B_1,\ldots,B_k)B}(b_1, \ldots, b_k)$ & constructed term ($k\geq0$)\\
$t::=$ &                   & \k{parse results} \\
       & $b$               & term \\
  $|$  & $\k{wrong}$       & type error \\
$\LL::=$ &                 & \k{dynamic environments}\\
       & $\oslash$         & empty environment \\
  $|$  & $\LL,x=b$         & term binding \\
\end{tabular}
\end{center}
An input stream is a sequence of identifiers, some of which may have
been declared to be keywords (e.g., \p{"if"}) in $g$.  We use the
notation $K(g)$ to denotes the set of keywords defined in productions of
$g$. The parsing rules for terminals use $K(g)$ to distinguish between
keywords and identifiers appearing in the input stream.

The sort of a term can be determined without reference to an environment:
\[  \k{unit} : \mbox{Unit} \bigspc 
    x_B :B \bigspc 
    x^i_B :B \bigspc 
    \ded{b_1:B_1 \ldots b_k:B_k}
        {c_{(B_1, \ldots, B_k)B}(b_1, \ldots, b_k) :B}
\]

A dynamic environment $\LL$ is said to match a static environment $L$
(written as $\LL\models L$) if its term bindings have names and sorts
compatible with the names and sorts in $L$.

\[ \oslash \models \oslash \bigspc 
   \dedtwoh{\LL \models L}{b:B}{\LL,x=b \models L,x:B} \]

The following theorem relates the dynamic parse rules in
figure~\ref{Fig:Parsing-Terms} with the static type rules presented in
section~\ref{Sec:Typing}.

\begin{theorem}\label{Theo:1} (parsing respects typing)
For all $g, E, L, p, M, s, s', i$ and $i'$ 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}{p:B}$
\item $\LL \models L$ 
\item $\jd{g;\LL}{s,i}{p}{s',i'}{t}$
\end{enumerate}
$t:B$ holds.
\end{theorem}
The proof of this theorem can be found in the full paper.  In
particular, if a non-parameterized ($L=\LL=\oslash$) parser with result
sort $B$ for a root production $p_0$ defined in a type-correct grammar
$g$ consumes the full input stream $s$ (returning the empty input stream
$*$), the parse result $t$ is guaranteed to be of sort $B$:
\begin{corollary}\label{Coro:1}
If 
\begin{itemize}
\item $\jdg{\oslash}{g::E}$ 
\item $\jdg{\oslash}{g\ \k{ok}}$,
\item $\jdg{E;\oslash}{p_0:B}$, and
\item $\jd{g;\oslash}{s,1}{p_0}{*,i'}{t}$
\end{itemize}
then $t:B$ and $t\not=\k{wrong}$.
\end{corollary}

\section{An Extensible Parser Package}
\label{Sec:Package}

Extensible grammars as described in this paper were developed in the
context of the Tycoon database programming environment
\cite{Matt93}. However, as sketched in figure~\ref{Fig:Grammar-Scenario},
the extensible grammar package was implemented in a way that factors out
all target-language dependencies (the base sorts $B^i$, the
abstract syntax tree constructors $c_{(B_1, \ldots, B_k)B}$, and the
renaming operation on abstract syntax trees) from the package
implementation.

A token stream $s$ is represented as an object with a local state and
methods to inspect the current input token and to advance to the next
input token.

A parser for terms of a sort $B$ is represented as a function that takes
a scanner object and returns a typed abstract syntax tree, modifying the
state of the scanner object and a variable counter to generate fresh
variable identifiers.

A grammar $g_i$ is represented as an object of an abstract data type
encapsulating information about the target language \e{TL} and the
object language \e{OL$_i$} accepted by $g_i$. The implementor of a
compiler for a language with an extensible grammar links the parser
package into the compiler. A grammar for the target language at hand is
generated via calls to the parser interface. Finally, a parser for this
grammar is generated which in turn is used to parse actual program
input.

The following steps have to be taken to generate the grammar $g_0$ and a
parser for the initial object language \e{OL$_0$}. Each of these steps
is implemented by a function call to the parser package that passes the
grammar as an explicit argument.
\begin{enumerate}\itemsep 0.5\baselineskip \parsep 0pt \topsep 0pt \parskip 0pt
\item  Creation of an initial (empty) grammar $g_0$. Arguments to this
operation provide information to the parser package about the tokens
returned by the scanner and functions to create fresh identifiers. An
initial grammar already contains the names of the builtin sorts Label,
Var, and Binder.

\item Addition of named sorts to $g_0$. These sorts correspond to
abstract-syntax-tree types in the target-language compiler. For each
newly defined sort, an AST copy routine, an AST renaming routine, and a
distinguished error value have to be supplied. The error value is
generated by the parser package in case of parse errors.

\item Addition of named constructors to $g_0$. Constructors correspond
to functions in the target-language compiler that take $k\geq 0$ typed
abstract syntax trees and return an aggregated syntax tree. For each
constructor, the list of its argument sorts and its result sort have to
be specified.

\item Addition of a concrete syntax for grammar definitions to $g_0$.
Target-language implementors can adopt either the concrete syntax used
in this paper (\k{grammar} \ldots \k{end}) or they can define their own
tailored syntax for the definition of productions $p$ that match the
abstract syntax given in section~\ref{Sec:Typing}.

\item Generation of a parser for $g_0$. Parser generation involves the
calculation of director sets to support efficient LL(1) parsing.
Furthermore, variable and non-terminal references are resolved into
direct table indices.

\item Parsing of a grammar extension $g$ using the parser generated in the
previous step. The grammar extension $g$ defines the mapping from
\e{OL$_{0}$} terms to \e{TL} terms.

\item Extension of $g_0$ by $g$.

\item Generation of a parser for the extended $g_0$. 
\end{enumerate}

A parser for \e{OL$_{i}$} derived from a grammar $g_i$ returns either a
term of the target language proper, or an abstract syntax tree for an
incremental syntax extension $g_\Delta$.  In the latter case the parser
package is invoked to check the type correctness of $g_\Delta$ in the
scope of the environment $E_i$ established by the current grammar $g_i$.
If this check succeeds, the extended grammar is obtained by normalizing
the grammar sequence $g_i, g_\Delta \leadsto g_{i+1}$. Finally, a new
parser is generated for $g_{i+1}$; this parser can then be used to parse
further input in the extended language\e{OL$_{i+1}$}.

If the parsing result is a term $t$ of the target language, the parser
package also returns a list of variable renamings. These renamings have to be
performed by the target-language compiler in $t$ to establish bindings
to global variable identifiers (see section~\ref{Keyword:Global-Vars}).

\section{Comparison with Related Work}
\label{Sec:Comparison}

Syntactic extensibility has been studied previously in the context of
programming languages and theorem provers.

Linguistic reflection \cite{SMA91,S*92,SSF92,Kirb92} in persistent
programming languages has been used to add high-level (query) notations
to strongly-typed programming languages. These extensions are achieved
by executing user-defined code at compile time to transform syntax trees
returned from the parser prior to further processing by the type checker
and code generator. Our approach differs from this work since we are
able to guarantee the termination of compilation, even when our
transformation operations are defined recursively. Furthermore, we are
not aware of work in the context of linguistic reflection to handle
correctly the problematic binding situations sketched in
section~\ref{Sec:Pattern}.


Some non-persistent language implementations, like CAML and SML,
integrate YACC or a similar parser generator that allows them to
introduce new syntax \cite{MaRa92}. If the new syntax is to be mixed
with the old one, the new syntax must be quoted in some way. Instead, we
can freely intermix new and old syntax without special quotations.

Hygienic macros \cite{K*86,Kohl86} have goals similar to those of our
extensible grammars; these macros also work on the abstract syntax and
avoid binding anomalies. However, these macros account only for explicit
(parameterized) macro calls and not for more liberal keyword-based
syntax extensions. Hygienic macros employ a multi-pass time-stamping
algorithm to prevent variable capture; this algorithm is different from
our one-pass renaming algorithm.  Furthermore, we do not handle
quotation and antiquotation in the style of Lisp.

Griffin \cite{Griff88} has enumerated desirable properties of notational
definitions and has studied their formalization. Unlike Griffin who
translates notations to combinator form, we are able to handle variables
bound to non-local binders in patterns. Moreover, while Griffin
discusses abstract translations, we provide a specific grammar
definition technique and an efficient parsing algorithm. Parsing is
efficient because it is LL(1) and because it avoids the creation of
intermediate parse trees, producing abstract syntax trees that do not
require normalization.

Bove and Arbilla \cite{BoAr92} discuss how to use explicit substitutions
to implement syntax extensions. Theirs is an elegant idea that may be
exploited in systems where the target compiler supports explicit
substitutions. As in the previous case, their work does not describe a
parsing algorithm, but presents an interesting theory.

\section{Concluding Remarks}

Extensible grammars avoid many of the problems associated with
traditional macro-expansion or program-rewrite tools by sort constraints
at grammar-definition time and by a careful handling of identifiers in
binding constructs. Furthermore, since our work extends the
well-understood parser technology by a small set of concepts, extensible
parsers can be integrated with little overhead in today's compilation
environments.

Traditional database programming languages have a bias towards a
specific data model by providing built-in syntactic support tailored to
the structures and operations of that data model.  In a programming
environment equipped with extensible grammars, such syntactic forms can
be eliminated from the core language definition and can be introduced in
application libraries shared by larger user communities. 

\bibliographystyle{florian}
\bibliography{../bib/florian}

\end{document}




