--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Aug 15 12:54:25 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Aug 15 13:07:24 2012 +0200
@@ -1235,7 +1235,7 @@
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.
+ need 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
@@ -1363,7 +1363,7 @@
correspondence of a particular grammar production to some known term
entity is preserved.
- \item Input type constants (constructors) and type classes ---
+ \item Input of type constants (constructors) and type classes ---
thanks to explicit syntactic distinction independently on the
context.
@@ -1374,9 +1374,10 @@
\end{itemize}
In other words, syntax transformations that operate on input terms
- written as prefix applications are difficult to achieve. Luckily,
- this case rarely occurs in practice, because syntax forms to be
- translated usually correspond to some bits of concrete notation.%
+ written as prefix applications are difficult to make robust.
+ Luckily, this case rarely occurs in practice, because syntax forms
+ to be translated usually correspond to some bits of concrete
+ notation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1528,7 +1529,7 @@
Such syntactic constants are invented on the spot, without formal
check wrt.\ existing declarations. It is conventional to use plain
identifiers prefixed by a single underscore (e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}foobar{\isaliteral{22}{\isachardoublequote}}}). Names should be chosen with care, to avoid clashes
- with unrelated syntax declarations.
+ with other syntax declarations.
\medskip The special case of copy production is specified by \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|""| (empty string). It means that the
resulting parse tree \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is copied directly, without any
@@ -1540,7 +1541,7 @@
\item \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules} specifies syntactic
translation rules (i.e.\ macros) as first-order rewrite rules on
- ASTs (see also \secref{sec:ast}). The theory context maintains two
+ ASTs (\secref{sec:ast}). The theory context maintains two
independent lists translation rules: parse rules (\verb|=>|
or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7269676874686172706F6F6E75703E}{\isasymrightharpoonup}}{\isaliteral{22}{\isachardoublequote}}}) and print rules (\verb|<=| or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C656674686172706F6F6E646F776E3E}{\isasymleftharpoondown}}{\isaliteral{22}{\isachardoublequote}}}).
For convenience, both can be specified simultaneously as parse~/
@@ -1660,7 +1661,7 @@
chosen in order of appearance in the theory definitions.
The configuration options \hyperlink{attribute.syntax-ast-trace}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}trace}}} and
- \hyperlink{attribute.syntax-ast-stats}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}stats}}} might help understand this process
+ \hyperlink{attribute.syntax-ast-stats}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}stats}}} might help to understand this process
and diagnose problems.
\begin{warn}
@@ -1759,11 +1760,9 @@
\end{tabular}}
\medskip
- The argument list consist of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ tr{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} pairs, where \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} is the syntax name of the syntax constant, term constant or
- type constructor involved, and \isa{{\isaliteral{22}{\isachardoublequote}}tr{\isaliteral{22}{\isachardoublequote}}} a function that
- translates a syntax form \isa{{\isaliteral{22}{\isachardoublequote}}c\ args{\isaliteral{22}{\isachardoublequote}}} into \isa{{\isaliteral{22}{\isachardoublequote}}tr\ args{\isaliteral{22}{\isachardoublequote}}}.
- For print translations, the naming convention for such functions is
- \isa{{\isaliteral{22}{\isachardoublequote}}tr{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} instead of \isa{{\isaliteral{22}{\isachardoublequote}}tr{\isaliteral{22}{\isachardoublequote}}}.
+ The argument list consists of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ tr{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} pairs, where \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} is the syntax name of the formal entity involved, and \isa{{\isaliteral{22}{\isachardoublequote}}tr{\isaliteral{22}{\isachardoublequote}}} a function that translates a syntax form \isa{{\isaliteral{22}{\isachardoublequote}}c\ args{\isaliteral{22}{\isachardoublequote}}} into
+ \isa{{\isaliteral{22}{\isachardoublequote}}tr\ args{\isaliteral{22}{\isachardoublequote}}}. The ML naming convention for parse translations
+ is \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}tr{\isaliteral{22}{\isachardoublequote}}} and for print translations \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}tr{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}}.
The \indexref{}{command}{print\_syntax}\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}syntax}}}} command displays the sets of names
associated with the translation functions of a theory under \isa{{\isaliteral{22}{\isachardoublequote}}parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation{\isaliteral{22}{\isachardoublequote}}} etc.
@@ -1797,7 +1796,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The different kinds of translation functions are called during
+The different kinds of translation functions are invoked during
the transformations between parse trees, ASTs and syntactic terms
(cf.\ \figref{fig:parse-print}). Whenever a combination of the form
\isa{{\isaliteral{22}{\isachardoublequote}}c\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} is encountered, and a translation function
@@ -1810,7 +1809,8 @@
the form \verb|Const|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} or \verb|Const|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{24}{\isachardollar}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}. Terms allow more sophisticated transformations
than ASTs do, typically involving abstractions and bound
variables. \emph{Typed} print translations may even peek at the type
- \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} of the constant they are invoked on.
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} of the constant they are invoked on, although that information
+ may be inaccurate.
Regardless of whether they act on ASTs or terms, translation
functions called during the parsing process differ from those for