doc-src/Ref/syntax.tex
author paulson
Thu, 05 Feb 1998 10:26:59 +0100
changeset 4597 a0bdee64194c
parent 4375 ef2a7b589004
child 5371 e27558a68b8d
permissions -rw-r--r--
Fixed a lot of overfull and underfull lines (hboxes)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
     1
%% $Id$
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
     2
\chapter{Syntax Transformations} \label{chap:syntax}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
     3
\newcommand\ttapp{\mathrel{\hbox{\tt\$}}}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
     4
\newcommand\mtt[1]{\mbox{\tt #1}}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
     5
\newcommand\ttfct[1]{\mathop{\mtt{#1}}\nolimits}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
     6
\newcommand\Constant{\ttfct{Constant}}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
     7
\newcommand\Variable{\ttfct{Variable}}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
     8
\newcommand\Appl[1]{\ttfct{Appl}\,[#1]}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
     9
\index{syntax!transformations|(}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    10
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    11
This chapter is intended for experienced Isabelle users who need to define
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    12
macros or code their own translation functions.  It describes the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    13
transformations between parse trees, abstract syntax trees and terms.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    14
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    15
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    16
\section{Abstract syntax trees} \label{sec:asts}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
    17
\index{ASTs|(}
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    18
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    19
The parser, given a token list from the lexer, applies productions to yield
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    20
a parse tree\index{parse trees}.  By applying some internal transformations
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    21
the parse tree becomes an abstract syntax tree, or \AST{}.  Macro
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    22
expansion, further translations and finally type inference yields a
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    23
well-typed term.  The printing process is the reverse, except for some
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    24
subtleties to be discussed later.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    25
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    26
Figure~\ref{fig:parse_print} outlines the parsing and printing process.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    27
Much of the complexity is due to the macro mechanism.  Using macros, you
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    28
can specify most forms of concrete syntax without writing any \ML{} code.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    29
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    30
\begin{figure}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    31
\begin{center}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    32
\begin{tabular}{cl}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    33
string          & \\
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
    34
$\downarrow$    & lexer, parser \\
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    35
parse tree      & \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    36
$\downarrow$    & parse \AST{} translation \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    37
\AST{}             & \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    38
$\downarrow$    & \AST{} rewriting (macros) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    39
\AST{}             & \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    40
$\downarrow$    & parse translation, type inference \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    41
--- well-typed term --- & \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    42
$\downarrow$    & print translation \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    43
\AST{}             & \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    44
$\downarrow$    & \AST{} rewriting (macros) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    45
\AST{}             & \\
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
    46
$\downarrow$    & print \AST{} translation, token translation \\
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    47
string          &
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    48
\end{tabular}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    49
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    50
\end{center}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    51
\caption{Parsing and printing}\label{fig:parse_print}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    52
\end{figure}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    53
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    54
Abstract syntax trees are an intermediate form between the raw parse trees
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    55
and the typed $\lambda$-terms.  An \AST{} is either an atom (constant or
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    56
variable) or a list of {\em at least two\/} subtrees.  Internally, they
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    57
have type \mltydx{Syntax.ast}: \index{*Constant} \index{*Variable}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    58
\index{*Appl}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    59
\begin{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    60
datatype ast = Constant of string
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    61
             | Variable of string
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    62
             | Appl of ast list
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    63
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    64
%
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    65
Isabelle uses an S-expression syntax for abstract syntax trees.  Constant
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    66
atoms are shown as quoted strings, variable atoms as non-quoted strings and
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
    67
applications as a parenthesised list of subtrees.  For example, the \AST
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    68
\begin{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    69
Appl [Constant "_constrain",
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    70
      Appl [Constant "_abs", Variable "x", Variable "t"],
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    71
      Appl [Constant "fun", Variable "'a", Variable "'b"]]
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    72
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    73
is shown as {\tt ("_constrain" ("_abs" x t) ("fun" 'a 'b))}.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    74
Both {\tt ()} and {\tt (f)} are illegal because they have too few
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
    75
subtrees.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    76
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    77
The resemblance to Lisp's S-expressions is intentional, but there are two
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    78
kinds of atomic symbols: $\Constant x$ and $\Variable x$.  Do not take the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    79
names {\tt Constant} and {\tt Variable} too literally; in the later
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    80
translation to terms, $\Variable x$ may become a constant, free or bound
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    81
variable, even a type constructor or class name; the actual outcome depends
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    82
on the context.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    83
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    84
Similarly, you can think of ${\tt (} f~x@1~\ldots~x@n{\tt )}$ as the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    85
application of~$f$ to the arguments $x@1, \ldots, x@n$.  But the kind of
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    86
application is determined later by context; it could be a type constructor
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    87
applied to types.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    88
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    89
Forms like {\tt (("_abs" x $t$) $u$)} are legal, but \AST{}s are
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    90
first-order: the {\tt "_abs"} does not bind the {\tt x} in any way.  Later
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    91
at the term level, {\tt ("_abs" x $t$)} will become an {\tt Abs} node and
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    92
occurrences of {\tt x} in $t$ will be replaced by bound variables (the term
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    93
constructor \ttindex{Bound}).
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    94
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    95
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    96
\section{Transforming parse trees to \AST{}s}\label{sec:astofpt}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    97
\index{ASTs!made from parse trees}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    98
\newcommand\astofpt[1]{\lbrakk#1\rbrakk}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
    99
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   100
The parse tree is the raw output of the parser.  Translation functions,
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   101
called {\bf parse AST translations}\indexbold{translations!parse AST},
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   102
transform the parse tree into an abstract syntax tree.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   103
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   104
The parse tree is constructed by nesting the right-hand sides of the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   105
productions used to recognize the input.  Such parse trees are simply lists
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   106
of tokens and constituent parse trees, the latter representing the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   107
nonterminals of the productions.  Let us refer to the actual productions in
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   108
the form displayed by {\tt print_syntax} (see \S\ref{sec:inspct-thy} for an
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   109
example).
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   110
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   111
Ignoring parse \AST{} translations, parse trees are transformed to \AST{}s
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   112
by stripping out delimiters and copy productions.  More precisely, the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   113
mapping $\astofpt{-}$ is derived from the productions as follows:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   114
\begin{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   115
\item Name tokens: $\astofpt{t} = \Variable s$, where $t$ is an \ndx{id},
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   116
  \ndx{var}, \ndx{tid}, \ndx{tvar}, \ndx{xnum} or \ndx{xstr} token, and $s$
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   117
  its associated string.  Note that for {\tt xstr} this does not include the
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   118
  quotes.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   119
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   120
\item Copy productions:\index{productions!copy}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   121
  $\astofpt{\ldots P \ldots} = \astofpt{P}$.  Here $\ldots$ stands for
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   122
  strings of delimiters, which are discarded.  $P$ stands for the single
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   123
  constituent that is not a delimiter; it is either a nonterminal symbol or
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   124
  a name token.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   125
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   126
  \item 0-ary productions: $\astofpt{\ldots \mtt{=>} c} = \Constant c$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   127
    Here there are no constituents other than delimiters, which are
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   128
    discarded.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   129
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   130
  \item $n$-ary productions, where $n \ge 1$: delimiters are discarded and
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   131
    the remaining constituents $P@1$, \ldots, $P@n$ are built into an
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   132
    application whose head constant is~$c$:
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   133
    \[ \astofpt{\ldots P@1 \ldots P@n \ldots \mtt{=>} c} =
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   134
       \Appl{\Constant c, \astofpt{P@1}, \ldots, \astofpt{P@n}}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   135
    \]
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   136
\end{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   137
Figure~\ref{fig:parse_ast} presents some simple examples, where {\tt ==},
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   138
{\tt _appl}, {\tt _args}, and so forth name productions of the Pure syntax.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   139
These examples illustrate the need for further translations to make \AST{}s
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   140
closer to the typed $\lambda$-calculus.  The Pure syntax provides
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   141
predefined parse \AST{} translations\index{translations!parse AST} for
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   142
ordinary applications, type applications, nested abstractions, meta
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   143
implications and function types.  Figure~\ref{fig:parse_ast_tr} shows their
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   144
effect on some representative input strings.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   145
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   146
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   147
\begin{figure}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   148
\begin{center}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   149
\tt\begin{tabular}{ll}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   150
\rm input string    & \rm \AST \\\hline
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   151
"f"                 & f \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   152
"'a"                & 'a \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   153
"t == u"            & ("==" t u) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   154
"f(x)"              & ("_appl" f x) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   155
"f(x, y)"           & ("_appl" f ("_args" x y)) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   156
"f(x, y, z)"        & ("_appl" f ("_args" x ("_args" y z))) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   157
"\%x y.\ t"         & ("_lambda" ("_idts" x y) t) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   158
\end{tabular}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   159
\end{center}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   160
\caption{Parsing examples using the Pure syntax}\label{fig:parse_ast}
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   161
\end{figure}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   162
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   163
\begin{figure}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   164
\begin{center}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   165
\tt\begin{tabular}{ll}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   166
\rm input string            & \rm \AST{} \\\hline
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   167
"f(x, y, z)"                & (f x y z) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   168
"'a ty"                     & (ty 'a) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   169
"('a, 'b) ty"               & (ty 'a 'b) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   170
"\%x y z.\ t"               & ("_abs" x ("_abs" y ("_abs" z t))) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   171
"\%x ::\ 'a.\ t"            & ("_abs" ("_constrain" x 'a) t) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   172
"[| P; Q; R |] => S"        & ("==>" P ("==>" Q ("==>" R S))) \\
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   173
"['a, 'b, 'c] => 'd"        & ("fun" 'a ("fun" 'b ("fun" 'c 'd)))
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   174
\end{tabular}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   175
\end{center}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   176
\caption{Built-in parse \AST{} translations}\label{fig:parse_ast_tr}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   177
\end{figure}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   178
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   179
The names of constant heads in the \AST{} control the translation process.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   180
The list of constants invoking parse \AST{} translations appears in the
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   181
output of {\tt print_syntax} under {\tt parse_ast_translation}.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   182
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   183
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   184
\section{Transforming \AST{}s to terms}\label{sec:termofast}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   185
\index{terms!made from ASTs}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   186
\newcommand\termofast[1]{\lbrakk#1\rbrakk}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   187
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   188
The \AST{}, after application of macros (see \S\ref{sec:macros}), is
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   189
transformed into a term.  This term is probably ill-typed since type
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   190
inference has not occurred yet.  The term may contain type constraints
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   191
consisting of applications with head {\tt "_constrain"}; the second
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   192
argument is a type encoded as a term.  Type inference later introduces
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   193
correct types or rejects the input.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   194
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   195
Another set of translation functions, namely parse
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   196
translations\index{translations!parse}, may affect this process.  If we
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   197
ignore parse translations for the time being, then \AST{}s are transformed
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   198
to terms by mapping \AST{} constants to constants, \AST{} variables to
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   199
schematic or free variables and \AST{} applications to applications.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   200
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   201
More precisely, the mapping $\termofast{-}$ is defined by
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   202
\begin{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   203
\item Constants: $\termofast{\Constant x} = \ttfct{Const} (x,
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   204
  \mtt{dummyT})$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   205
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   206
\item Schematic variables: $\termofast{\Variable \mtt{"?}xi\mtt"} =
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   207
  \ttfct{Var} ((x, i), \mtt{dummyT})$, where $x$ is the base name and $i$
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   208
  the index extracted from~$xi$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   209
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   210
\item Free variables: $\termofast{\Variable x} = \ttfct{Free} (x,
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   211
  \mtt{dummyT})$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   212
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   213
\item Function applications with $n$ arguments:
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   214
    \[ \termofast{\Appl{f, x@1, \ldots, x@n}} =
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   215
       \termofast{f} \ttapp
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   216
         \termofast{x@1} \ttapp \ldots \ttapp \termofast{x@n}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   217
    \]
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   218
\end{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   219
Here \ttindex{Const}, \ttindex{Var}, \ttindex{Free} and
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   220
\verb|$|\index{$@{\tt\$}} are constructors of the datatype \mltydx{term},
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   221
while \ttindex{dummyT} stands for some dummy type that is ignored during
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   222
type inference.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   223
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   224
So far the outcome is still a first-order term.  Abstractions and bound
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   225
variables (constructors \ttindex{Abs} and \ttindex{Bound}) are introduced
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   226
by parse translations.  Such translations are attached to {\tt "_abs"},
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   227
{\tt "!!"} and user-defined binders.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   228
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   229
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   230
\section{Printing of terms}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   231
\newcommand\astofterm[1]{\lbrakk#1\rbrakk}\index{ASTs!made from terms}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   232
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   233
The output phase is essentially the inverse of the input phase.  Terms are
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   234
translated via abstract syntax trees into strings.  Finally the strings are
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   235
pretty printed.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   236
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   237
Print translations (\S\ref{sec:tr_funs}) may affect the transformation of
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   238
terms into \AST{}s.  Ignoring those, the transformation maps
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   239
term constants, variables and applications to the corresponding constructs
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   240
on \AST{}s.  Abstractions are mapped to applications of the special
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   241
constant {\tt _abs}.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   242
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   243
More precisely, the mapping $\astofterm{-}$ is defined as follows:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   244
\begin{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   245
  \item $\astofterm{\ttfct{Const} (x, \tau)} = \Constant x$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   246
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   247
  \item $\astofterm{\ttfct{Free} (x, \tau)} = constrain (\Variable x,
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   248
    \tau)$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   249
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   250
  \item $\astofterm{\ttfct{Var} ((x, i), \tau)} = constrain (\Variable
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   251
    \mtt{"?}xi\mtt", \tau)$, where $\mtt?xi$ is the string representation of
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   252
    the {\tt indexname} $(x, i)$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   253
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   254
  \item For the abstraction $\lambda x::\tau.t$, let $x'$ be a variant
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   255
    of~$x$ renamed to differ from all names occurring in~$t$, and let $t'$
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   256
    be obtained from~$t$ by replacing all bound occurrences of~$x$ by
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   257
    the free variable $x'$.  This replaces corresponding occurrences of the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   258
    constructor \ttindex{Bound} by the term $\ttfct{Free} (x',
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   259
    \mtt{dummyT})$:
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   260
   \[ \astofterm{\ttfct{Abs} (x, \tau, t)} =
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   261
      \Appl{\Constant \mtt{"_abs"},
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   262
        constrain(\Variable x', \tau), \astofterm{t'}}.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   263
    \]
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   264
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   265
  \item $\astofterm{\ttfct{Bound} i} = \Variable \mtt{"B.}i\mtt"$.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   266
    The occurrence of constructor \ttindex{Bound} should never happen
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   267
    when printing well-typed terms; it indicates a de Bruijn index with no
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   268
    matching abstraction.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   269
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   270
  \item Where $f$ is not an application,
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   271
    \[ \astofterm{f \ttapp x@1 \ttapp \ldots \ttapp x@n} =
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   272
       \Appl{\astofterm{f}, \astofterm{x@1}, \ldots,\astofterm{x@n}}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   273
    \]
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   274
\end{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   275
%
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   276
Type constraints\index{type constraints} are inserted to allow the printing
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   277
of types.  This is governed by the boolean variable \ttindex{show_types}:
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   278
\begin{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   279
  \item $constrain(x, \tau) = x$ \ if $\tau = \mtt{dummyT}$ \index{*dummyT} or
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   280
    \ttindex{show_types} is set to {\tt false}.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   281
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   282
  \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x,
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   283
         \astofterm{\tau}}$ \ otherwise.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   284
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   285
    Here, $\astofterm{\tau}$ is the \AST{} encoding of $\tau$: type
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   286
    constructors go to {\tt Constant}s; type identifiers go to {\tt
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   287
      Variable}s; type applications go to {\tt Appl}s with the type
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   288
    constructor as the first element.  If \ttindex{show_sorts} is set to
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   289
    {\tt true}, some type variables are decorated with an \AST{} encoding
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   290
    of their sort.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   291
\end{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   292
%
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   293
The \AST{}, after application of macros (see \S\ref{sec:macros}), is
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   294
transformed into the final output string.  The built-in {\bf print AST
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   295
  translations}\indexbold{translations!print AST} reverse the
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   296
parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   297
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   298
For the actual printing process, the names attached to productions
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   299
of the form $\ldots A^{(p@1)}@1 \ldots A^{(p@n)}@n \ldots \mtt{=>} c$ play
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   300
a vital role.  Each \AST{} with constant head $c$, namely $\mtt"c\mtt"$ or
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   301
$(\mtt"c\mtt"~ x@1 \ldots x@n)$, is printed according to the production
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   302
for~$c$.  Each argument~$x@i$ is converted to a string, and put in
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   303
parentheses if its priority~$(p@i)$ requires this.  The resulting strings
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   304
and their syntactic sugar (denoted by \dots{} above) are joined to make a
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   305
single string.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   306
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   307
If an application $(\mtt"c\mtt"~ x@1 \ldots x@m)$ has more arguments
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   308
than the corresponding production, it is first split into
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   309
$((\mtt"c\mtt"~ x@1 \ldots x@n) ~ x@{n+1} \ldots x@m)$.  Applications
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   310
with too few arguments or with non-constant head or without a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   311
corresponding production are printed as $f(x@1, \ldots, x@l)$ or
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   312
$(\alpha@1, \ldots, \alpha@l) ty$.  Multiple productions associated
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   313
with some name $c$ are tried in order of appearance.  An occurrence of
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   314
$\Variable x$ is simply printed as~$x$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   315
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   316
Blanks are {\em not\/} inserted automatically.  If blanks are required to
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   317
separate tokens, specify them in the mixfix declaration, possibly preceded
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   318
by a slash~({\tt/}) to allow a line break.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   319
\index{ASTs|)}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   320
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   321
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   322
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   323
\section{Macros: syntactic rewriting} \label{sec:macros}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   324
\index{macros|(}\index{rewriting!syntactic|(}
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   325
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   326
Mixfix declarations alone can handle situations where there is a direct
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   327
connection between the concrete syntax and the underlying term.  Sometimes
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   328
we require a more elaborate concrete syntax, such as quantifiers and list
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   329
notation.  Isabelle's {\bf macros} and {\bf translation functions} can
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   330
perform translations such as
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   331
\begin{center}\tt
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   332
  \begin{tabular}{r@{$\quad\protect\rightleftharpoons\quad$}l}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   333
    ALL x:A.P   & Ball(A, \%x.P)        \\ \relax
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   334
    [x, y, z]   & Cons(x, Cons(y, Cons(z, Nil)))
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   335
  \end{tabular}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   336
\end{center}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   337
Translation functions (see \S\ref{sec:tr_funs}) must be coded in ML; they
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   338
are the most powerful translation mechanism but are difficult to read or
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   339
write.  Macros are specified by first-order rewriting systems that operate
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   340
on abstract syntax trees.  They are usually easy to read and write, and can
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   341
express all but the most obscure translations.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   342
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   343
Figure~\ref{fig:set_trans} defines a fragment of first-order logic and
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   344
set theory.\footnote{This and the following theories are complete
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   345
  working examples, though they specify only syntax, no axioms.  The
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   346
  file {\tt ZF/ZF.thy} presents a full set theory definition,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   347
  including many macro rules.} Theory {\tt SetSyntax} declares
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   348
constants for set comprehension ({\tt Collect}), replacement ({\tt
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   349
  Replace}) and bounded universal quantification ({\tt Ball}).  Each
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   350
of these binds some variables.  Without additional syntax we should
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   351
have to write $\forall x \in A.  P$ as {\tt Ball(A,\%x.P)}, and
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   352
similarly for the others.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   353
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   354
\begin{figure}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   355
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   356
SetSyntax = Pure +
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   357
types
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   358
  i o
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   359
arities
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   360
  i, o :: logic
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   361
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   362
  Trueprop      :: o => prop                ("_" 5)
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   363
  Collect       :: [i, i => o] => i
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   364
  Replace       :: [i, [i, i] => o] => i
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   365
  Ball          :: [i, i => o] => o
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   366
syntax
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   367
  "{\at}Collect"    :: [idt, i, o] => i         ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   368
  "{\at}Replace"    :: [idt, idt, i, o] => i    ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   369
  "{\at}Ball"       :: [idt, i, o] => o         ("(3ALL _:_./ _)" 10)
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   370
translations
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   371
  "{\ttlbrace}x:A. P{\ttrbrace}"    == "Collect(A, \%x. P)"
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   372
  "{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)"
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   373
  "ALL x:A. P"  == "Ball(A, \%x. P)"
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   374
end
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   375
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   376
\caption{Macro example: set theory}\label{fig:set_trans}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   377
\end{figure}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   378
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   379
The theory specifies a variable-binding syntax through additional productions
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   380
that have mixfix declarations.  Each non-copy production must specify some
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   381
constant, which is used for building \AST{}s. \index{constants!syntactic} The
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   382
additional constants are decorated with {\tt\at} to stress their purely
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   383
syntactic purpose; they may not occur within the final well-typed terms,
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   384
being declared as {\tt syntax} rather than {\tt consts}.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   385
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   386
The translations cause the replacement of external forms by internal forms
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   387
after parsing, and vice versa before printing of terms.  As a specification
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   388
of the set theory notation, they should be largely self-explanatory.  The
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   389
syntactic constants, {\tt\at Collect}, {\tt\at Replace} and {\tt\at Ball},
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   390
appear implicitly in the macro rules via their mixfix forms.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   391
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   392
Macros can define variable-binding syntax because they operate on \AST{}s,
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   393
which have no inbuilt notion of bound variable.  The macro variables {\tt
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   394
  x} and~{\tt y} have type~{\tt idt} and therefore range over identifiers,
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   395
in this case bound variables.  The macro variables {\tt P} and~{\tt Q}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   396
range over formulae containing bound variable occurrences.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   397
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   398
Other applications of the macro system can be less straightforward, and
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   399
there are peculiarities.  The rest of this section will describe in detail
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   400
how Isabelle macros are preprocessed and applied.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   401
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   402
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   403
\subsection{Specifying macros}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   404
Macros are basically rewrite rules on \AST{}s.  But unlike other macro
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   405
systems found in programming languages, Isabelle's macros work in both
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   406
directions.  Therefore a syntax contains two lists of rewrites: one for
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   407
parsing and one for printing.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   408
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   409
\index{*translations section}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   410
The {\tt translations} section specifies macros.  The syntax for a macro is
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   411
\[ (root)\; string \quad
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   412
   \left\{\begin{array}[c]{c} \mtt{=>} \\ \mtt{<=} \\ \mtt{==} \end{array}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   413
   \right\} \quad
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   414
   (root)\; string
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   415
\]
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   416
%
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   417
This specifies a parse rule ({\tt =>}), a print rule ({\tt <=}), or both
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   418
({\tt ==}).  The two strings specify the left and right-hand sides of the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   419
macro rule.  The $(root)$ specification is optional; it specifies the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   420
nonterminal for parsing the $string$ and if omitted defaults to {\tt
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   421
  logic}.  \AST{} rewrite rules $(l, r)$ must obey certain conditions:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   422
\begin{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   423
\item Rules must be left linear: $l$ must not contain repeated variables.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   424
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   425
\item Rules must have constant heads, namely $l = \mtt"c\mtt"$ or $l =
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   426
  (\mtt"c\mtt" ~ x@1 \ldots x@n)$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   427
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   428
\item Every variable in~$r$ must also occur in~$l$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   429
\end{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   430
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   431
Macro rules may refer to any syntax from the parent theories.  They
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   432
may also refer to anything defined before the current {\tt
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   433
  translations} section --- including any mixfix declarations.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   434
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   435
Upon declaration, both sides of the macro rule undergo parsing and parse
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   436
\AST{} translations (see \S\ref{sec:asts}), but do not themselves undergo
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   437
macro expansion.  The lexer runs in a different mode that additionally
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   438
accepts identifiers of the form $\_~letter~quasiletter^*$ (like {\tt _idt},
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   439
{\tt _K}).  Thus, a constant whose name starts with an underscore can
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   440
appear in macro rules but not in ordinary terms.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   441
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   442
Some atoms of the macro rule's \AST{} are designated as constants for
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   443
matching.  These are all names that have been declared as classes, types or
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   444
constants (logical and syntactic).
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   445
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   446
The result of this preprocessing is two lists of macro rules, each
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   447
stored as a pair of \AST{}s.  They can be viewed using {\tt
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   448
  print_syntax} (sections \ttindex{parse_rules} and
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   449
\ttindex{print_rules}).  For theory~{\tt SetSyntax} of
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   450
Fig.~\ref{fig:set_trans} these are
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   451
\begin{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   452
parse_rules:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   453
  ("{\at}Collect" x A P)  ->  ("Collect" A ("_abs" x P))
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   454
  ("{\at}Replace" y x A Q)  ->  ("Replace" A ("_abs" x ("_abs" y Q)))
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   455
  ("{\at}Ball" x A P)  ->  ("Ball" A ("_abs" x P))
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   456
print_rules:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   457
  ("Collect" A ("_abs" x P))  ->  ("{\at}Collect" x A P)
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   458
  ("Replace" A ("_abs" x ("_abs" y Q)))  ->  ("{\at}Replace" y x A Q)
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   459
  ("Ball" A ("_abs" x P))  ->  ("{\at}Ball" x A P)
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   460
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   461
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   462
\begin{warn}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   463
  Avoid choosing variable names that have previously been used as
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   464
  constants, types or type classes; the {\tt consts} section in the output
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   465
  of {\tt print_syntax} lists all such names.  If a macro rule works
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   466
  incorrectly, inspect its internal form as shown above, recalling that
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   467
  constants appear as quoted strings and variables without quotes.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   468
\end{warn}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   469
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   470
\begin{warn}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   471
If \ttindex{eta_contract} is set to {\tt true}, terms will be
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   472
$\eta$-contracted {\em before\/} the \AST{} rewriter sees them.  Thus some
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   473
abstraction nodes needed for print rules to match may vanish.  For example,
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   474
\verb|Ball(A, %x. P(x))| contracts to {\tt Ball(A, P)}; the print rule does
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   475
not apply and the output will be {\tt Ball(A, P)}.  This problem would not
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   476
occur if \ML{} translation functions were used instead of macros (as is
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   477
done for binder declarations).
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   478
\end{warn}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   479
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   480
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   481
\begin{warn}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   482
Another trap concerns type constraints.  If \ttindex{show_types} is set to
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   483
{\tt true}, bound variables will be decorated by their meta types at the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   484
binding place (but not at occurrences in the body).  Matching with
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   485
\verb|Collect(A, %x. P)| binds {\tt x} to something like {\tt ("_constrain" y
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   486
"i")} rather than only {\tt y}.  \AST{} rewriting will cause the constraint to
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   487
appear in the external form, say \verb|{y::i:A::i. P::o}|.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   488
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   489
To allow such constraints to be re-read, your syntax should specify bound
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   490
variables using the nonterminal~\ndx{idt}.  This is the case in our
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   491
example.  Choosing {\tt id} instead of {\tt idt} is a common error.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   492
\end{warn}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   493
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   494
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   495
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   496
\subsection{Applying rules}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   497
As a term is being parsed or printed, an \AST{} is generated as an
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   498
intermediate form (recall Fig.\ts\ref{fig:parse_print}).  The \AST{} is
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   499
normalised by applying macro rules in the manner of a traditional term
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   500
rewriting system.  We first examine how a single rule is applied.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   501
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   502
Let $t$ be the abstract syntax tree to be normalised and $(l, r)$ some
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   503
translation rule.  A subtree~$u$ of $t$ is a {\bf redex} if it is an
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   504
instance of~$l$; in this case $l$ is said to {\bf match}~$u$.  A redex
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   505
matched by $l$ may be replaced by the corresponding instance of~$r$, thus
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   506
{\bf rewriting} the \AST~$t$.  Matching requires some notion of {\bf
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   507
  place-holders} that may occur in rule patterns but not in ordinary
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   508
\AST{}s; {\tt Variable} atoms serve this purpose.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   509
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   510
The matching of the object~$u$ by the pattern~$l$ is performed as follows:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   511
\begin{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   512
  \item Every constant matches itself.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   513
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   514
  \item $\Variable x$ in the object matches $\Constant x$ in the pattern.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   515
    This point is discussed further below.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   516
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   517
  \item Every \AST{} in the object matches $\Variable x$ in the pattern,
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   518
    binding~$x$ to~$u$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   519
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   520
  \item One application matches another if they have the same number of
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   521
    subtrees and corresponding subtrees match.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   522
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   523
  \item In every other case, matching fails.  In particular, {\tt
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   524
      Constant}~$x$ can only match itself.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   525
\end{itemize}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   526
A successful match yields a substitution that is applied to~$r$, generating
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   527
the instance that replaces~$u$.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   528
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   529
The second case above may look odd.  This is where {\tt Variable}s of
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   530
non-rule \AST{}s behave like {\tt Constant}s.  Recall that \AST{}s are not
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   531
far removed from parse trees; at this level it is not yet known which
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   532
identifiers will become constants, bounds, frees, types or classes.  As
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   533
\S\ref{sec:asts} describes, former parse tree heads appear in \AST{}s as
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   534
{\tt Constant}s, while the name tokens \ndx{id}, \ndx{var}, \ndx{tid},
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   535
\ndx{tvar}, \ndx{xnum} and \ndx{xstr} become {\tt Variable}s.  On the other
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   536
hand, when \AST{}s generated from terms for printing, all constants and type
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   537
constructors become {\tt Constant}s; see \S\ref{sec:asts}.  Thus \AST{}s may
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   538
contain a messy mixture of {\tt Variable}s and {\tt Constant}s.  This is
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   539
insignificant at macro level because matching treats them alike.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   540
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   541
Because of this behaviour, different kinds of atoms with the same name are
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   542
indistinguishable, which may make some rules prone to misbehaviour.  Example:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   543
\begin{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   544
types
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   545
  Nil
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   546
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   547
  Nil     :: 'a list
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   548
syntax
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   549
  "[]"    :: 'a list    ("[]")
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   550
translations
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   551
  "[]"    == "Nil"
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   552
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   553
The term {\tt Nil} will be printed as {\tt []}, just as expected.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   554
The term \verb|%Nil.t| will be printed as \verb|%[].t|, which might not be
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   555
expected!  Guess how type~{\tt Nil} is printed?
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   556
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   557
Normalizing an \AST{} involves repeatedly applying macro rules until
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   558
none are applicable.  Macro rules are chosen in order of appearance in
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   559
the theory definitions.  You can watch the normalization of \AST{}s
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   560
during parsing and printing by setting \ttindex{Syntax.trace_norm_ast}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   561
to {\tt true}.\index{tracing!of macros} Alternatively, use
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   562
\ttindex{Syntax.test_read}.  The information displayed when tracing
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   563
includes the \AST{} before normalization ({\tt pre}), redexes with
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   564
results ({\tt rewrote}), the normal form finally reached ({\tt post})
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   565
and some statistics ({\tt normalize}).  If tracing is off,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   566
\ttindex{Syntax.stat_norm_ast} can be set to {\tt true} in order to
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   567
enable printing of the normal form and statistics only.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   568
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   569
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   570
\subsection{Example: the syntax of finite sets}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   571
\index{examples!of macros}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   572
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   573
This example demonstrates the use of recursive macros to implement a
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   574
convenient notation for finite sets.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   575
\index{*empty constant}\index{*insert constant}\index{{}@\verb'{}' symbol}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   576
\index{"@Enum@{\tt\at Enum} constant}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   577
\index{"@Finset@{\tt\at Finset} constant}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   578
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   579
FinSyntax = SetSyntax +
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   580
types
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   581
  is
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   582
syntax
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   583
  ""            :: i => is                  ("_")
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   584
  "{\at}Enum"       :: [i, is] => is            ("_,/ _")
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   585
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   586
  empty         :: i                        ("{\ttlbrace}{\ttrbrace}")
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   587
  insert        :: [i, i] => i
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   588
syntax
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   589
  "{\at}Finset"     :: is => i                  ("{\ttlbrace}(_){\ttrbrace}")
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   590
translations
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   591
  "{\ttlbrace}x, xs{\ttrbrace}"     == "insert(x, {\ttlbrace}xs{\ttrbrace})"
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   592
  "{\ttlbrace}x{\ttrbrace}"         == "insert(x, {\ttlbrace}{\ttrbrace})"
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   593
end
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   594
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   595
Finite sets are internally built up by {\tt empty} and {\tt insert}.  The
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   596
declarations above specify \verb|{x, y, z}| as the external representation
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   597
of
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   598
\begin{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   599
insert(x, insert(y, insert(z, empty)))
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   600
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   601
The nonterminal symbol~\ndx{is} stands for one or more objects of type~{\tt
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   602
  i} separated by commas.  The mixfix declaration \hbox{\verb|"_,/ _"|}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   603
allows a line break after the comma for \rmindex{pretty printing}; if no
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   604
line break is required then a space is printed instead.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   605
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   606
The nonterminal is declared as the type~{\tt is}, but with no {\tt arities}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   607
declaration.  Hence {\tt is} is not a logical type and may be used safely as
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   608
a new nonterminal for custom syntax.  The nonterminal~{\tt is} can later be
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   609
re-used for other enumerations of type~{\tt i} like lists or tuples.  If we
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   610
had needed polymorphic enumerations, we could have used the predefined
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   611
nonterminal symbol \ndx{args} and skipped this part altogether.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   612
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   613
\index{"@Finset@{\tt\at Finset} constant}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   614
Next follows {\tt empty}, which is already equipped with its syntax
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   615
\verb|{}|, and {\tt insert} without concrete syntax.  The syntactic
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   616
constant {\tt\at Finset} provides concrete syntax for enumerations of~{\tt
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   617
  i} enclosed in curly braces.  Remember that a pair of parentheses, as in
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   618
\verb|"{(_)}"|, specifies a block of indentation for pretty printing.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   619
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   620
The translations may look strange at first.  Macro rules are best
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   621
understood in their internal forms:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   622
\begin{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   623
parse_rules:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   624
  ("{\at}Finset" ("{\at}Enum" x xs))  ->  ("insert" x ("{\at}Finset" xs))
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   625
  ("{\at}Finset" x)  ->  ("insert" x "empty")
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   626
print_rules:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   627
  ("insert" x ("{\at}Finset" xs))  ->  ("{\at}Finset" ("{\at}Enum" x xs))
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   628
  ("insert" x "empty")  ->  ("{\at}Finset" x)
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   629
\end{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   630
This shows that \verb|{x,xs}| indeed matches any set enumeration of at least
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   631
two elements, binding the first to {\tt x} and the rest to {\tt xs}.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   632
Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   633
The parse rules only work in the order given.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   634
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   635
\begin{warn}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   636
  The \AST{} rewriter cannot distinguish constants from variables and looks
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   637
  only for names of atoms.  Thus the names of {\tt Constant}s occurring in
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   638
  the (internal) left-hand side of translation rules should be regarded as
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   639
  \rmindex{reserved words}.  Choose non-identifiers like {\tt\at Finset} or
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   640
  sufficiently long and strange names.  If a bound variable's name gets
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   641
  rewritten, the result will be incorrect; for example, the term
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   642
\begin{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   643
\%empty insert. insert(x, empty)
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   644
\end{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   645
\par\noindent is incorrectly printed as \verb|%empty insert. {x}|.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   646
\end{warn}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   647
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   648
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   649
\subsection{Example: a parse macro for dependent types}\label{prod_trans}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   650
\index{examples!of macros}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   651
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   652
As stated earlier, a macro rule may not introduce new {\tt Variable}s on
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   653
the right-hand side.  Something like \verb|"K(B)" => "%x.B"| is illegal;
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   654
if allowed, it could cause variable capture.  In such cases you usually
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   655
must fall back on translation functions.  But a trick can make things
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   656
readable in some cases: {\em calling\/} translation functions by parse
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   657
macros:
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   658
\begin{ttbox}
3135
233aba197bf2 tuned spaces;
wenzelm
parents: 3128
diff changeset
   659
ProdSyntax = SetSyntax +
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   660
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   661
  Pi            :: [i, i => i] => i
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   662
syntax
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   663
  "{\at}PROD"       :: [idt, i, i] => i       ("(3PROD _:_./ _)" 10)
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 864
diff changeset
   664
  "{\at}->"         :: [i, i] => i            ("(_ ->/ _)" [51, 50] 50)
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   665
\ttbreak
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   666
translations
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   667
  "PROD x:A. B" => "Pi(A, \%x. B)"
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   668
  "A -> B"      => "Pi(A, _K(B))"
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   669
end
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   670
ML
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   671
  val print_translation = [("Pi", dependent_tr' ("{\at}PROD", "{\at}->"))];
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   672
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   673
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   674
Here {\tt Pi} is a logical constant for constructing general products.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   675
Two external forms exist: the general case {\tt PROD x:A.B} and the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   676
function space {\tt A -> B}, which abbreviates \verb|Pi(A, %x.B)| when {\tt B}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   677
does not depend on~{\tt x}.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   678
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   679
The second parse macro introduces {\tt _K(B)}, which later becomes
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   680
\verb|%x.B| due to a parse translation associated with \cdx{_K}.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   681
Unfortunately there is no such trick for printing, so we have to add a {\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   682
ML} section for the print translation \ttindex{dependent_tr'}.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   683
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   684
Recall that identifiers with a leading {\tt _} are allowed in translation
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   685
rules, but not in ordinary terms.  Thus we can create \AST{}s containing
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   686
names that are not directly expressible.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   687
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   688
The parse translation for {\tt _K} is already installed in Pure, and {\tt
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   689
dependent_tr'} is exported by the syntax module for public use.  See
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   690
\S\ref{sec:tr_funs} below for more of the arcane lore of translation functions.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   691
\index{macros|)}\index{rewriting!syntactic|)}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   692
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   693
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   694
\section{Translation functions} \label{sec:tr_funs}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   695
\index{translations|(}
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   696
%
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   697
This section describes the translation function mechanism.  By writing
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   698
\ML{} functions, you can do almost everything to terms or \AST{}s
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   699
during parsing and printing.  The logic \LK\ is a good example of
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   700
sophisticated transformations between internal and external
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   701
representations of sequents; here, macros would be useless.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   702
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   703
A full understanding of translations requires some familiarity
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   704
with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   705
{\tt Syntax.ast} and the encodings of types and terms as such at the various
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   706
stages of the parsing or printing process.  Most users should never need to
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   707
use translation functions.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   708
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   709
\subsection{Declaring translation functions}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   710
There are four kinds of translation functions, with one of these
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   711
coming in two variants.  Each such function is associated with a name,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   712
which triggers calls to it.  Such names can be constants (logical or
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   713
syntactic) or type constructors.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   714
4597
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4375
diff changeset
   715
{\tt print_syntax} displays the sets of names associated with the translation
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4375
diff changeset
   716
functions of a theory under \texttt{parse_ast_translation}, etc.  You can add
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4375
diff changeset
   717
new ones via the {\tt ML} section\index{*ML section} of a theory definition
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4375
diff changeset
   718
file.  There may never be more than one function of the same kind per name.
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4375
diff changeset
   719
Even though the {\tt ML} section is the very last part of the file, newly
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4375
diff changeset
   720
installed translation functions are already effective when processing all of
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4375
diff changeset
   721
the preceding sections.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   722
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   723
The {\tt ML} section's contents are simply copied verbatim near the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   724
beginning of the \ML\ file generated from a theory definition file.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   725
Definitions made here are accessible as components of an \ML\ 
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   726
structure; to make some parts private, use an \ML{} {\tt local}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   727
declaration.  The {\ML} code may install translation functions by
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   728
declaring any of the following identifiers:
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   729
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   730
val parse_ast_translation   : (string * (ast list -> ast)) list
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   731
val print_ast_translation   : (string * (ast list -> ast)) list
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   732
val parse_translation       : (string * (term list -> term)) list
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   733
val print_translation       : (string * (term list -> term)) list
4375
ef2a7b589004 changed typed_print_translation;
wenzelm
parents: 3485
diff changeset
   734
val typed_print_translation :
ef2a7b589004 changed typed_print_translation;
wenzelm
parents: 3485
diff changeset
   735
    (string * (bool -> typ -> term list -> term)) list
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   736
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   737
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   738
\subsection{The translation strategy}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   739
The different kinds of translation functions are called during the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   740
transformations between parse trees, \AST{}s and terms (recall
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   741
Fig.\ts\ref{fig:parse_print}).  Whenever a combination of the form
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   742
$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   743
function $f$ of appropriate kind exists for $c$, the result is
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   744
computed by the \ML{} function call $f \mtt[ x@1, \ldots, x@n \mtt]$.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   745
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   746
For \AST{} translations, the arguments $x@1, \ldots, x@n$ are \AST{}s.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   747
A combination has the form $\Constant c$ or $\Appl{\Constant c, x@1,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   748
  \ldots, x@n}$.  For term translations, the arguments are terms and a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   749
combination has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   750
(c, \tau) \ttapp x@1 \ttapp \ldots \ttapp x@n$.  Terms allow more
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   751
sophisticated transformations than \AST{}s do, typically involving
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   752
abstractions and bound variables. {\em Typed} print translations may
4375
ef2a7b589004 changed typed_print_translation;
wenzelm
parents: 3485
diff changeset
   753
even peek at the type $\tau$ of the constant they are invoked on; they
ef2a7b589004 changed typed_print_translation;
wenzelm
parents: 3485
diff changeset
   754
are also passed the current value of the \ttindex{show_sorts} flag.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   755
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   756
Regardless of whether they act on terms or \AST{}s, translation
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   757
functions called during the parsing process differ from those for
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   758
printing more fundamentally in their overall behaviour:
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   759
\begin{description}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   760
\item[Parse translations] are applied bottom-up.  The arguments are already
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   761
  in translated form.  The translations must not fail; exceptions trigger
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   762
  an error message.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   763
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   764
\item[Print translations] are applied top-down.  They are supplied with
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   765
  arguments that are partly still in internal form.  The result again
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   766
  undergoes translation; therefore a print translation should not introduce
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   767
  as head the very constant that invoked it.  The function may raise
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   768
  exception \xdx{Match} to indicate failure; in this event it has no
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   769
  effect.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   770
\end{description}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   771
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   772
Only constant atoms --- constructor \ttindex{Constant} for \AST{}s and
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   773
\ttindex{Const} for terms --- can invoke translation functions.  This
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   774
causes another difference between parsing and printing.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   775
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   776
Parsing starts with a string and the constants are not yet identified.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   777
Only parse tree heads create {\tt Constant}s in the resulting \AST, as
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   778
described in \S\ref{sec:astofpt}.  Macros and parse \AST{} translations may
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   779
introduce further {\tt Constant}s.  When the final \AST{} is converted to a
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   780
term, all {\tt Constant}s become {\tt Const}s, as described in
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   781
\S\ref{sec:termofast}.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   782
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   783
Printing starts with a well-typed term and all the constants are known.  So
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   784
all logical constants and type constructors may invoke print translations.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   785
These, and macros, may introduce further constants.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   786
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   787
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   788
\subsection{Example: a print translation for dependent types}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   789
\index{examples!of translations}\indexbold{*dependent_tr'}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   790
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   791
Let us continue the dependent type example (page~\pageref{prod_trans}) by
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   792
examining the parse translation for~\cdx{_K} and the print translation
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   793
{\tt dependent_tr'}, which are both built-in.  By convention, parse
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   794
translations have names ending with {\tt _tr} and print translations have
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   795
names ending with {\tt _tr'}.  Search for such names in the Isabelle
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   796
sources to locate more examples.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   797
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   798
Here is the parse translation for {\tt _K}:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   799
\begin{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   800
fun k_tr [t] = Abs ("x", dummyT, incr_boundvars 1 t)
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   801
  | k_tr ts = raise TERM ("k_tr", ts);
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   802
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   803
If {\tt k_tr} is called with exactly one argument~$t$, it creates a new
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   804
{\tt Abs} node with a body derived from $t$.  Since terms given to parse
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   805
translations are not yet typed, the type of the bound variable in the new
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   806
{\tt Abs} is simply {\tt dummyT}.  The function increments all {\tt Bound}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   807
nodes referring to outer abstractions by calling \ttindex{incr_boundvars},
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   808
a basic term manipulation function defined in {\tt Pure/term.ML}.
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   809
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   810
Here is the print translation for dependent types:
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   811
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   812
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   813
      if 0 mem (loose_bnos B) then
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   814
        let val (x', B') = Syntax.variant_abs' (x, dummyT, B) in
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   815
          list_comb
3135
233aba197bf2 tuned spaces;
wenzelm
parents: 3128
diff changeset
   816
            (Const (q,{\thinspace}dummyT) $ Syntax.mark_boundT (x',{\thinspace}T) $ A $ B',{\thinspace}ts)
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   817
        end
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   818
      else list_comb (Const (r, dummyT) $ A $ B, ts)
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   819
  | dependent_tr' _ _ = raise Match;
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   820
\end{ttbox}
3135
233aba197bf2 tuned spaces;
wenzelm
parents: 3128
diff changeset
   821
The argument {\tt (q,{\thinspace}r)} is supplied to the curried function {\tt
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   822
  dependent_tr'} by a partial application during its installation.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   823
For example, we could set up print translations for both {\tt Pi} and
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   824
{\tt Sigma} by including
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   825
\begin{ttbox}\index{*ML section}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   826
val print_translation =
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   827
  [("Pi",    dependent_tr' ("{\at}PROD", "{\at}->")),
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   828
   ("Sigma", dependent_tr' ("{\at}SUM", "{\at}*"))];
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   829
\end{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   830
within the {\tt ML} section.  The first of these transforms ${\tt
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   831
  Pi}(A, \mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   832
$\hbox{\tt{\at}->}(A, B)$, choosing the latter form if $B$ does not
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   833
depend on~$x$.  It checks this using \ttindex{loose_bnos}, yet another
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   834
function from {\tt Pure/term.ML}.  Note that $x'$ is a version of $x$
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   835
renamed away from all names in $B$, and $B'$ is the body $B$ with {\tt
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   836
  Bound} nodes referring to the {\tt Abs} node replaced by
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   837
$\ttfct{Free} (x', \mtt{dummyT})$ (but marked as representing a bound
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   838
variable).
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   839
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   840
We must be careful with types here.  While types of {\tt Const}s are
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   841
ignored, type constraints may be printed for some {\tt Free}s and
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   842
{\tt Var}s if \ttindex{show_types} is set to {\tt true}.  Variables of type
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   843
\ttindex{dummyT} are never printed with constraint, though.  The line
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   844
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   845
        let val (x', B') = Syntax.variant_abs' (x, dummyT, B);
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   846
\end{ttbox}\index{*Syntax.variant_abs'}
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   847
replaces bound variable occurrences in~$B$ by the free variable $x'$ with
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   848
type {\tt dummyT}.  Only the binding occurrence of~$x'$ is given the
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   849
correct type~{\tt T}, so this is the only place where a type
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   850
constraint might appear.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   851
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   852
Also note that we are responsible to mark free identifiers that
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   853
actually represent bound variables.  This is achieved by
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   854
\ttindex{Syntax.variant_abs'} and \ttindex{Syntax.mark_boundT} above.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   855
Failing to do so may cause these names to be printed in the wrong
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   856
style.  \index{translations|)} \index{syntax!transformations|)}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   857
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   858
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   859
\section{Token translations} \label{sec:tok_tr}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   860
\index{token translations|(}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   861
%
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   862
Isabelle's meta-logic features quite a lot of different kinds of
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   863
identifiers, namely {\em class}, {\em tfree}, {\em tvar}, {\em free},
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   864
{\em bound}, {\em var}.  One might want to have these printed in
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   865
different styles, e.g.\ in bold or italic, or even transcribed into
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   866
something more readable like $\alpha, \alpha', \beta$ instead of {\tt
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   867
  'a}, {\tt 'aa}, {\tt 'b} for type variables.  Token translations
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   868
provide a means to such ends, enabling the user to install certain
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   869
\ML{} functions associated with any logical \rmindex{token class} and
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   870
depending on some \rmindex{print mode}.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   871
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   872
The logical class of identifiers can not necessarily be determined by
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   873
its syntactic category, though.  For example, consider free vs.\ bound
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   874
variables.  So Isabelle's pretty printing mechanism, starting from
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   875
fully typed terms, has to be careful to preserve this additional
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   876
information\footnote{This is done by marking atoms in abstract syntax
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   877
  trees appropriately.  The marks are actually visible by print
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   878
  translation functions -- they are just special constants applied to
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   879
  atomic asts, for example \texttt{("_bound" x)}.}.  In particular,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   880
user-supplied print translation functions operating on terms have to
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   881
be well-behaved in this respect.  Free identifiers introduced to
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   882
represent bound variables have to be marked appropriately (cf.\ the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   883
example at the end of \S\ref{sec:tr_funs}).
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   884
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   885
\medskip Token translations may be installed by declaring the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   886
\ttindex{token_translation} value within the \texttt{ML} section of a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   887
theory definition file:
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   888
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   889
val token_translation: (string * string * (string -> string * int)) list
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   890
\end{ttbox}\index{token_translation}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   891
The elements of this list are of the form $(m, c, f)$, where $m$ is a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   892
print mode identifier, $c$ a token class, and $f\colon string \to
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   893
string \times int$ the actual translation function.  Assuming that $x$
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   894
is of identifier class $c$, and print mode $m$ is the first one of all
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   895
currently active modes that provide some translation for $c$, then $x$
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   896
is output according to $f(x) = (x', len)$.  Thereby $x'$ is the
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   897
modified identifier name and $len$ its visual length approximated in
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3135
diff changeset
   898
terms of whole characters.  Thus $x'$ may include non-printing parts
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   899
like control sequences or markup information for typesetting systems.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   900
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   901
%FIXME example (?)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   902
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   903
\index{token translations|)}