# HG changeset patch # User wenzelm # Date 1340029820 -7200 # Node ID 1c4500446ba479a67ac98ee9151def0f72803382 # Parent b1240319ef158fa55fcaebdfb7c0a77cb039659c more explicit section "Syntax transformations"; diff -r b1240319ef15 -r 1c4500446ba4 doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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 - "\"}-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 "\"}-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 "\"} & lexer + parser \\ + parse tree & \\ + @{text "\"} & parse AST translation \\ + AST & \\ + @{text "\"} & AST rewriting (macros) \\ + AST & \\ + @{text "\"} & parse translation \\ + --- pre-term --- & \\ + @{text "\"} & print translation \\ + AST & \\ + @{text "\"} & AST rewriting (macros) \\ + AST & \\ + @{text "\"} & 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} diff -r b1240319ef15 -r 1c4500446ba4 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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% % diff -r b1240319ef15 -r 1c4500446ba4 doc-src/Ref/syntax.tex --- 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