# HG changeset patch # User wenzelm # Date 1340218204 -7200 # Node ID 8537313dd26110da99217587434db172683165dc # Parent e21f4d5b9636f637e38fc64620d5284a90050f24 more on "Syntax translation functions"; diff -r e21f4d5b9636 -r 8537313dd261 doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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 \ 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 \ 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, \, x\<^sub>n]"} in ML. + + For AST translations, the arguments @{text "x\<^sub>1, \, 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, \, x\<^sub>n]"}. + For term translations, the arguments are terms and a combination has + the form @{ML Const}~@{text "(c, \)"} or @{ML Const}~@{text "(c, \) + $ x\<^sub>1 $ \ $ 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 "\"} 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 diff -r e21f4d5b9636 -r 8537313dd261 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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% % diff -r e21f4d5b9636 -r 8537313dd261 doc-src/Ref/syntax.tex --- 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"