--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Jun 22 15:03:41 2012 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Jun 18 16:30:20 2012 +0200
@@ -24,9 +24,7 @@
Further details of the syntax engine involves the classical
distinction of lexical language versus context-free grammar (see
\secref{sec:pure-syntax}), and various mechanisms for \emph{syntax
- translations} --- either as rewrite systems on first-order ASTs
- (\secref{sec:syn-trans}) or ML functions on ASTs or @{text
- "\<lambda>"}-terms that represent parse trees (\secref{sec:tr-funs}).
+ transformations} (see \secref{sec:syntax-transformations}).
*}
@@ -1011,7 +1009,65 @@
*}
-section {* Raw syntax and translations \label{sec:syn-trans} *}
+section {* Syntax transformations \label{sec:syntax-transformations} *}
+
+text {* The inner syntax engine of Isabelle provides separate
+ mechanisms to transform parse trees either as rewrite systems on
+ first-order ASTs (\secref{sec:syn-trans}), or ML functions on ASTs
+ or syntactic @{text "\<lambda>"}-terms (\secref{sec:tr-funs}). This works
+ both for parsing and printing, as outlined in
+ \figref{fig:parse-print}.
+
+ \begin{figure}[htbp]
+ \begin{center}
+ \begin{tabular}{cl}
+ string & \\
+ @{text "\<down>"} & lexer + parser \\
+ parse tree & \\
+ @{text "\<down>"} & parse AST translation \\
+ AST & \\
+ @{text "\<down>"} & AST rewriting (macros) \\
+ AST & \\
+ @{text "\<down>"} & parse translation \\
+ --- pre-term --- & \\
+ @{text "\<down>"} & print translation \\
+ AST & \\
+ @{text "\<down>"} & AST rewriting (macros) \\
+ AST & \\
+ @{text "\<down>"} & print AST translation \\
+ string &
+ \end{tabular}
+ \end{center}
+ \caption{Parsing and printing with translations}\label{fig:parse-print}
+ \end{figure}
+
+ These intermediate syntax tree formats eventually lead to a pre-term
+ with all names and binding scopes resolved, but most type
+ information still missing. Explicit type constraints might be given by
+ the user, or implicit position information by the system --- both
+ needs to be passed-through carefully by syntax transformations.
+
+ Pre-terms are further processed by the so-called \emph{check} and
+ \emph{unckeck} phases that are intertwined with type-inference (see
+ also \cite{isabelle-implementation}). The latter allows to operate
+ on higher-order abstract syntax with proper binding and type
+ information already available.
+
+ As a rule of thumb, anything that manipulates bindings of variables
+ or constants needs to be implemented as syntax transformation (see
+ below). Anything else is better done via check/uncheck: a prominent
+ example application is the @{command abbreviation} concept of
+ Isabelle/Pure. *}
+
+
+subsection {* Abstract syntax trees *}
+
+text {*
+ FIXME
+*}
+
+
+subsection {* Raw syntax and translations \label{sec:syn-trans} *}
text {*
\begin{matharray}{rcl}
@@ -1140,7 +1196,7 @@
*}
-section {* Syntax translation functions \label{sec:tr-funs} *}
+subsection {* Syntax translation functions \label{sec:tr-funs} *}
text {*
\begin{matharray}{rcl}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Jun 22 15:03:41 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Jun 18 16:30:20 2012 +0200
@@ -41,8 +41,7 @@
Further details of the syntax engine involves the classical
distinction of lexical language versus context-free grammar (see
\secref{sec:pure-syntax}), and various mechanisms for \emph{syntax
- translations} --- either as rewrite systems on first-order ASTs
- (\secref{sec:syn-trans}) or ML functions on ASTs or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-terms that represent parse trees (\secref{sec:tr-funs}).%
+ transformations} (see \secref{sec:syntax-transformations}).%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1185,7 +1184,71 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Raw syntax and translations \label{sec:syn-trans}%
+\isamarkupsection{Syntax transformations \label{sec:syntax-transformations}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The inner syntax engine of Isabelle provides separate
+ mechanisms to transform parse trees either as rewrite systems on
+ first-order ASTs (\secref{sec:syn-trans}), or ML functions on ASTs
+ or syntactic \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-terms (\secref{sec:tr-funs}). This works
+ both for parsing and printing, as outlined in
+ \figref{fig:parse-print}.
+
+ \begin{figure}[htbp]
+ \begin{center}
+ \begin{tabular}{cl}
+ string & \\
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & lexer + parser \\
+ parse tree & \\
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & parse AST translation \\
+ AST & \\
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & AST rewriting (macros) \\
+ AST & \\
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & parse translation \\
+ --- pre-term --- & \\
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & print translation \\
+ AST & \\
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & AST rewriting (macros) \\
+ AST & \\
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & print AST translation \\
+ string &
+ \end{tabular}
+ \end{center}
+ \caption{Parsing and printing with translations}\label{fig:parse-print}
+ \end{figure}
+
+ These intermediate syntax tree formats eventually lead to a pre-term
+ with all names and binding scopes resolved, but most type
+ information still missing. Explicit type constraints might be given by
+ the user, or implicit position information by the system --- both
+ needs to be passed-through carefully by syntax transformations.
+
+ Pre-terms are further processed by the so-called \emph{check} and
+ \emph{unckeck} phases that are intertwined with type-inference (see
+ also \cite{isabelle-implementation}). The latter allows to operate
+ on higher-order abstract syntax with proper binding and type
+ information already available.
+
+ As a rule of thumb, anything that manipulates bindings of variables
+ or constants needs to be implemented as syntax transformation (see
+ below). Anything else is better done via check/uncheck: a prominent
+ example application is the \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}} concept of
+ Isabelle/Pure.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Abstract syntax trees%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Raw syntax and translations \label{sec:syn-trans}%
}
\isamarkuptrue%
%
@@ -1374,7 +1437,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Syntax translation functions \label{sec:tr-funs}%
+\isamarkupsubsection{Syntax translation functions \label{sec:tr-funs}%
}
\isamarkuptrue%
%
--- a/doc-src/Ref/syntax.tex Fri Jun 22 15:03:41 2012 +0200
+++ b/doc-src/Ref/syntax.tex Mon Jun 18 16:30:20 2012 +0200
@@ -8,49 +8,9 @@
\newcommand\Appl[1]{\ttfct{Appl}\,[#1]}
\index{syntax!transformations|(}
-This chapter is intended for experienced Isabelle users who need to define
-macros or code their own translation functions. It describes the
-transformations between parse trees, abstract syntax trees and terms.
-
-
\section{Abstract syntax trees} \label{sec:asts}
\index{ASTs|(}
-The parser, given a token list from the lexer, applies productions to yield
-a parse tree\index{parse trees}. By applying some internal transformations
-the parse tree becomes an abstract syntax tree, or \AST{}. Macro
-expansion, further translations and finally type inference yields a
-well-typed term. The printing process is the reverse, except for some
-subtleties to be discussed later.
-
-Figure~\ref{fig:parse_print} outlines the parsing and printing process.
-Much of the complexity is due to the macro mechanism. Using macros, you
-can specify most forms of concrete syntax without writing any \ML{} code.
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{cl}
-string & \\
-$\downarrow$ & lexer, parser \\
-parse tree & \\
-$\downarrow$ & parse \AST{} translation \\
-\AST{} & \\
-$\downarrow$ & \AST{} rewriting (macros) \\
-\AST{} & \\
-$\downarrow$ & parse translation, type inference \\
---- well-typed term --- & \\
-$\downarrow$ & print translation \\
-\AST{} & \\
-$\downarrow$ & \AST{} rewriting (macros) \\
-\AST{} & \\
-$\downarrow$ & print \AST{} translation \\
-string &
-\end{tabular}
-
-\end{center}
-\caption{Parsing and printing}\label{fig:parse_print}
-\end{figure}
-
Abstract syntax trees are an intermediate form between the raw parse trees
and the typed $\lambda$-terms. An \AST{} is either an atom (constant or
variable) or a list of {\em at least two\/} subtrees. Internally, they