--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue Jun 19 22:06:08 2012 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Jun 20 20:50:04 2012 +0200
@@ -1410,7 +1410,7 @@
\begin{warn}
If syntax translation rules work incorrectly, the output of
- @{command print_syntax} with its \emph{rules} sections reveals the
+ @{command_ref print_syntax} with its \emph{rules} sections reveals the
actual internal forms of AST pattern, without potentially confusing
concrete syntax. Recall that AST constants appear as quoted strings
and variables without quotes.
@@ -1440,49 +1440,98 @@
@{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
+ Syntax translation functions written in ML admit almost arbitrary
+ manipulations of inner syntax, at the expense of some complexity and
+ obscurity in the implementation.
+
@{rail "
( @@{command parse_ast_translation} | @@{command parse_translation} |
@@{command print_translation} | @@{command typed_print_translation} |
@@{command print_ast_translation}) ('(' @'advanced' ')')? @{syntax text}
"}
- Syntax translation functions written in ML admit almost arbitrary
- manipulations of Isabelle's inner syntax. Any of the above commands
- have a single @{syntax text} argument that refers to an ML
- expression of appropriate type, which are as follows by default:
+ Any of the above commands have a single @{syntax text} argument that
+ refers to an ML expression of appropriate type, which are as follows
+ by default:
+
+ \medskip
+ {\small
+ \begin{tabular}{ll}
+ @{command parse_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
+ @{command parse_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
+ @{command print_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
+ @{command typed_print_translation} & : @{ML_type "(string * (typ -> term list -> term)) list"} \\
+ @{command print_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
+ \end{tabular}}
+ \medskip
-%FIXME proper antiquotations
-\begin{ttbox}
-val parse_ast_translation : (string * (ast list -> ast)) list
-val parse_translation : (string * (term list -> term)) list
-val print_translation : (string * (term list -> term)) list
-val typed_print_translation : (string * (typ -> term list -> term)) list
-val print_ast_translation : (string * (ast list -> ast)) list
-\end{ttbox}
+ The argument list consist of @{text "(c, tr)"} pairs, where @{text
+ "c"} is the syntax name of the syntax constant, term constant or
+ type constructor involved, and @{text "tr"} a function that
+ translates a syntax form @{text "c args"} into @{text "tr args"}.
+ For print translations, the naming convention for such functions is
+ @{text "tr'"} instead of @{text "tr"}.
+
+ The @{command_ref print_syntax} command displays the sets of names
+ associated with the translation functions of a theory under @{text
+ "parse_ast_translation"} etc.
+
+ If the @{verbatim "("}@{keyword "advanced"}@{verbatim ")"} option is
+ given, the corresponding translation functions depend on the current
+ theory or proof context as additional argument. This allows to
+ implement advanced syntax mechanisms, as translations functions may
+ refer to specific theory declarations or auxiliary proof data.
+*}
+
+subsubsection {* The translation strategy *}
- If the @{text "(advanced)"} option is given, the corresponding
- translation functions may depend on the current theory or proof
- context. This allows to implement advanced syntax mechanisms, as
- translations functions may refer to specific theory declarations or
- auxiliary proof data.
+text {* The different kinds of translation functions are called during
+ the transformations between parse trees, ASTs and syntactic terms
+ (cf.\ \figref{fig:parse-print}). Whenever a combination of the form
+ @{text "c x\<^sub>1 \<dots> x\<^sub>n"} is encountered, and a translation function
+ @{text "f"} of appropriate kind is declared for @{text "c"}, the
+ result is produced by evaluation of @{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"} in ML.
+
+ For AST translations, the arguments @{text "x\<^sub>1, \<dots>, x\<^sub>n"} are ASTs. A
+ combination has the form @{ML "Ast.Constant"}~@{text "c"} or @{ML
+ "Ast.Appl"}~@{text "["}@{ML Ast.Constant}~@{text "c, x\<^sub>1, \<dots>, x\<^sub>n]"}.
+ For term translations, the arguments are terms and a combination has
+ the form @{ML Const}~@{text "(c, \<tau>)"} or @{ML Const}~@{text "(c, \<tau>)
+ $ x\<^sub>1 $ \<dots> $ x\<^sub>n"}. Terms allow more sophisticated transformations
+ than ASTs do, typically involving abstractions and bound
+ variables. \emph{Typed} print translations may even peek at the type
+ @{text "\<tau>"} of the constant they are invoked on.
+
+ Regardless of whether they act on ASTs or terms, translation
+ functions called during the parsing process differ from those for
+ printing in their overall behaviour:
+
+ \begin{description}
-%FIXME proper antiquotations
-\begin{ttbox}
-val parse_ast_translation:
- (string * (Proof.context -> ast list -> ast)) list
-val parse_translation:
- (string * (Proof.context -> term list -> term)) list
-val print_translation:
- (string * (Proof.context -> term list -> term)) list
-val typed_print_translation:
- (string * (Proof.context -> typ -> term list -> term)) list
-val print_ast_translation:
- (string * (Proof.context -> ast list -> ast)) list
-\end{ttbox}
+ \item [Parse translations] are applied bottom-up. The arguments are
+ already in translated form. The translations must not fail;
+ exceptions trigger an error message. There may be at most one
+ function associated with any syntactic name.
- \medskip See also the chapter on ``Syntax Transformations'' in old
- \cite{isabelle-ref} for further details on translations on parse
- trees.
+ \item [Print translations] are applied top-down. They are supplied
+ with arguments that are partly still in internal form. The result
+ again undergoes translation; therefore a print translation should
+ not introduce as head the very constant that invoked it. The
+ function may raise exception @{ML Match} to indicate failure; in
+ this event it has no effect. Multiple functions associated with
+ some syntactic name are tried in the order of declaration in the
+ theory.
+
+ \end{description}
+
+ Only constant atoms --- constructor @{ML Ast.Constant} for ASTs and
+ @{ML Const} for terms --- can invoke translation functions. This
+ means that parse translations can only be associated with parse tree
+ heads of concrete syntax, or syntactic constants introduced via
+ other translations. For plain identifiers within the term language,
+ the status of constant versus variable is not yet know during
+ parsing. This is in contrast to print translations, where constants
+ are explicitly known from the given term in its fully internal form.
*}
end
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue Jun 19 22:06:08 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Jun 20 20:50:04 2012 +0200
@@ -1653,7 +1653,7 @@
\begin{warn}
If syntax translation rules work incorrectly, the output of
- \hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}syntax}}}} with its \emph{rules} sections reveals the
+ \indexref{}{command}{print\_syntax}\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}syntax}}}} with its \emph{rules} sections reveals the
actual internal forms of AST pattern, without potentially confusing
concrete syntax. Recall that AST constants appear as quoted strings
and variables without quotes.
@@ -1685,6 +1685,10 @@
\indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\end{matharray}
+ Syntax translation functions written in ML admit almost arbitrary
+ manipulations of inner syntax, at the expense of some complexity and
+ obscurity in the implementation.
+
\begin{railoutput}
\rail@begin{5}{}
\rail@bar
@@ -1709,43 +1713,88 @@
\end{railoutput}
- Syntax translation functions written in ML admit almost arbitrary
- manipulations of Isabelle's inner syntax. Any of the above commands
- have a single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument that refers to an ML
- expression of appropriate type, which are as follows by default:
+ Any of the above commands have a single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument that
+ refers to an ML expression of appropriate type, which are as follows
+ by default:
-%FIXME proper antiquotations
-\begin{ttbox}
-val parse_ast_translation : (string * (ast list -> ast)) list
-val parse_translation : (string * (term list -> term)) list
-val print_translation : (string * (term list -> term)) list
-val typed_print_translation : (string * (typ -> term list -> term)) list
-val print_ast_translation : (string * (ast list -> ast)) list
-\end{ttbox}
+ \medskip
+ {\small
+ \begin{tabular}{ll}
+ \hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (Ast.ast list -> Ast.ast)) list| \\
+ \hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (term list -> term)) list| \\
+ \hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (term list -> term)) list| \\
+ \hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isaliteral{5F}{\isacharunderscore}}print{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (typ -> term list -> term)) list| \\
+ \hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (Ast.ast list -> Ast.ast)) list| \\
+ \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 \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.
- If the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}advanced{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option is given, the corresponding
- translation functions may depend on the current theory or proof
- context. This allows to implement advanced syntax mechanisms, as
- translations functions may refer to specific theory declarations or
- auxiliary proof data.
+ If the \verb|(|\hyperlink{keyword.advanced}{\mbox{\isa{\isakeyword{advanced}}}}\verb|)| option is
+ given, the corresponding translation functions depend on the current
+ theory or proof context as additional argument. This allows to
+ implement advanced syntax mechanisms, as translations functions may
+ refer to specific theory declarations or auxiliary proof data.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{The translation strategy%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The different kinds of translation functions are called 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
+ \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} of appropriate kind is declared for \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}}, the
+ result is produced by evaluation of \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5B}{\isacharbrackleft}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} in ML.
+
+ For AST translations, the arguments \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are ASTs. A
+ combination has the form \verb|Ast.Constant|~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} or \verb|Ast.Appl|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}}\verb|Ast.Constant|~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}.
+ For term translations, the arguments are terms and a combination has
+ 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.
-%FIXME proper antiquotations
-\begin{ttbox}
-val parse_ast_translation:
- (string * (Proof.context -> ast list -> ast)) list
-val parse_translation:
- (string * (Proof.context -> term list -> term)) list
-val print_translation:
- (string * (Proof.context -> term list -> term)) list
-val typed_print_translation:
- (string * (Proof.context -> typ -> term list -> term)) list
-val print_ast_translation:
- (string * (Proof.context -> ast list -> ast)) list
-\end{ttbox}
+ Regardless of whether they act on ASTs or terms, translation
+ functions called during the parsing process differ from those for
+ printing in their overall behaviour:
+
+ \begin{description}
+
+ \item [Parse translations] are applied bottom-up. The arguments are
+ already in translated form. The translations must not fail;
+ exceptions trigger an error message. There may be at most one
+ function associated with any syntactic name.
- \medskip See also the chapter on ``Syntax Transformations'' in old
- \cite{isabelle-ref} for further details on translations on parse
- trees.%
+ \item [Print translations] are applied top-down. They are supplied
+ with arguments that are partly still in internal form. The result
+ again undergoes translation; therefore a print translation should
+ not introduce as head the very constant that invoked it. The
+ function may raise exception \verb|Match| to indicate failure; in
+ this event it has no effect. Multiple functions associated with
+ some syntactic name are tried in the order of declaration in the
+ theory.
+
+ \end{description}
+
+ Only constant atoms --- constructor \verb|Ast.Constant| for ASTs and
+ \verb|Const| for terms --- can invoke translation functions. This
+ means that parse translations can only be associated with parse tree
+ heads of concrete syntax, or syntactic constants introduced via
+ other translations. For plain identifiers within the term language,
+ the status of constant versus variable is not yet know during
+ parsing. This is in contrast to print translations, where constants
+ are explicitly known from the given term in its fully internal form.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Ref/syntax.tex Tue Jun 19 22:06:08 2012 +0200
+++ b/doc-src/Ref/syntax.tex Wed Jun 20 20:50:04 2012 +0200
@@ -234,101 +234,6 @@
by a slash~({\tt/}) to allow a line break.
\index{ASTs|)}
-
-\section{Translation functions} \label{sec:tr_funs}
-\index{translations|(}
-%
-This section describes the translation function mechanism. By writing \ML{}
-functions, you can do almost everything to terms or \AST{}s during parsing and
-printing. The logic LK is a good example of sophisticated transformations
-between internal and external representations of sequents; here, macros would
-be useless.
-
-A full understanding of translations requires some familiarity
-with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
-{\tt Syntax.ast} and the encodings of types and terms as such at the various
-stages of the parsing or printing process. Most users should never need to
-use translation functions.
-
-\subsection{Declaring translation functions}
-There are four kinds of translation functions, with one of these
-coming in two variants. Each such function is associated with a name,
-which triggers calls to it. Such names can be constants (logical or
-syntactic) or type constructors.
-
-Function {\tt print_syntax} displays the sets of names associated with the
-translation functions of a theory under \texttt{parse_ast_translation}, etc.
-You can add new ones via the {\tt ML} section\index{*ML section} of a theory
-definition file. Even though the {\tt ML} section is the very last part of
-the file, newly installed translation functions are already effective when
-processing all of the preceding sections.
-
-The {\tt ML} section's contents are simply copied verbatim near the
-beginning of the \ML\ file generated from a theory definition file.
-Definitions made here are accessible as components of an \ML\
-structure; to make some parts private, use an \ML{} {\tt local}
-declaration. The {\ML} code may install translation functions by
-declaring any of the following identifiers:
-\begin{ttbox}
-val parse_ast_translation : (string * (ast list -> ast)) list
-val print_ast_translation : (string * (ast list -> ast)) list
-val parse_translation : (string * (term list -> term)) list
-val print_translation : (string * (term list -> term)) list
-val typed_print_translation :
- (string * (bool -> typ -> term list -> term)) list
-\end{ttbox}
-
-\subsection{The translation strategy}
-The different kinds of translation functions are called during the
-transformations between parse trees, \AST{}s and terms (recall
-Fig.\ts\ref{fig:parse_print}). Whenever a combination of the form
-$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation
-function $f$ of appropriate kind exists for $c$, the result is
-computed by the \ML{} function call $f \mtt[ x@1, \ldots, x@n \mtt]$.
-
-For \AST{} translations, the arguments $x@1, \ldots, x@n$ are \AST{}s.
-A combination has the form $\Constant c$ or $\Appl{\Constant c, x@1,
- \ldots, x@n}$. For term translations, the arguments are terms and a
-combination has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const}
-(c, \tau) \ttapp x@1 \ttapp \ldots \ttapp x@n$. Terms allow more
-sophisticated transformations than \AST{}s do, typically involving
-abstractions and bound variables. {\em Typed} print translations may
-even peek at the type $\tau$ of the constant they are invoked on; they
-are also passed the current value of the \ttindex{show_sorts} flag.
-
-Regardless of whether they act on terms or \AST{}s, translation
-functions called during the parsing process differ from those for
-printing more fundamentally in their overall behaviour:
-\begin{description}
-\item[Parse translations] are applied bottom-up. The arguments are already in
- translated form. The translations must not fail; exceptions trigger an
- error message. There may never be more than one function associated with
- any syntactic name.
-
-\item[Print translations] are applied top-down. They are supplied with
- arguments that are partly still in internal form. The result again
- undergoes translation; therefore a print translation should not introduce as
- head the very constant that invoked it. The function may raise exception
- \xdx{Match} to indicate failure; in this event it has no effect. Multiple
- functions associated with some syntactic name are tried in an unspecified
- order.
-\end{description}
-
-Only constant atoms --- constructor \ttindex{Constant} for \AST{}s and
-\ttindex{Const} for terms --- can invoke translation functions. This
-causes another difference between parsing and printing.
-
-Parsing starts with a string and the constants are not yet identified.
-Only parse tree heads create {\tt Constant}s in the resulting \AST, as
-described in \S\ref{sec:astofpt}. Macros and parse \AST{} translations may
-introduce further {\tt Constant}s. When the final \AST{} is converted to a
-term, all {\tt Constant}s become {\tt Const}s, as described in
-\S\ref{sec:termofast}.
-
-Printing starts with a well-typed term and all the constants are known. So
-all logical constants and type constructors may invoke print translations.
-These, and macros, may introduce further constants.
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"