doc-src/Ref/syntax.tex
author wenzelm
Tue, 06 May 1997 12:50:16 +0200
changeset 3108 335efc3f5632
parent 1387 9bcad9c22fd4
child 3128 d01d4c0c4b44
permissions -rw-r--r--
misc updates, tuning, cleanup;
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$
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   117
  its associated string. Note that for {\tt xstr} this does not include the
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
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   609
re-used for other enumerations of type~{\tt i} like lists or tuples. If we
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}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   659
ProdSyntax = FinSyntax +
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
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 499
diff changeset
   715
{\tt print_syntax} displays the sets of names associated with the
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   716
translation functions of a theory under
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   717
\ttindex{parse_ast_translation}, \ttindex{parse_translation},
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   718
\ttindex{print_translation} and \ttindex{print_ast_translation}.  You
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   719
can add new ones via the {\tt ML} section\index{*ML section} of a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   720
theory definition file.  There may never be more than one function of
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   721
the same kind per name.  Even though the {\tt ML} section is the very
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   722
last part of the file, newly installed translation functions are
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   723
already effective when processing all of the preceding sections.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   724
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   725
The {\tt ML} section's contents are simply copied verbatim near the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   726
beginning of the \ML\ file generated from a theory definition file.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   727
Definitions made here are accessible as components of an \ML\ 
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   728
structure; to make some parts private, use an \ML{} {\tt local}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   729
declaration.  The {\ML} code may install translation functions by
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   730
declaring any of the following identifiers:
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   731
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   732
val parse_ast_translation   : (string * (ast list -> ast)) list
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   733
val print_ast_translation   : (string * (ast list -> ast)) list
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   734
val parse_translation       : (string * (term list -> term)) list
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   735
val print_translation       : (string * (term list -> term)) list
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   736
val typed_print_translation : (string * (typ -> term list -> term)) list
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   737
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   738
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   739
\subsection{The translation strategy}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   740
The different kinds of translation functions are called during the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   741
transformations between parse trees, \AST{}s and terms (recall
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   742
Fig.\ts\ref{fig:parse_print}).  Whenever a combination of the form
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   743
$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   744
function $f$ of appropriate kind exists for $c$, the result is
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   745
computed by the \ML{} function call $f \mtt[ x@1, \ldots, x@n \mtt]$.
323
361a71713176 penultimate Springer draft
lcp
parents:
diff changeset
   746
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   747
For \AST{} translations, the arguments $x@1, \ldots, x@n$ are \AST{}s.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   748
A combination has the form $\Constant c$ or $\Appl{\Constant c, x@1,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   749
  \ldots, x@n}$.  For term translations, the arguments are terms and a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   750
combination has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   751
(c, \tau) \ttapp x@1 \ttapp \ldots \ttapp x@n$.  Terms allow more
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   752
sophisticated transformations than \AST{}s do, typically involving
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   753
abstractions and bound variables. {\em Typed} print translations may
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   754
even peek at the type $\tau$ of the constant they are invoked on.
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
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   816
            (Const (q, dummyT) $ Syntax.mark_boundT (x', T) $ A $ B', 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}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   821
The argument {\tt (q, r)} is supplied to the curried function {\tt
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
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   853
actually represent bound variables. This is achieved by
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},
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   864
{\em bound}, {\em var}. One might want to have these printed in
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
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   867
  'a}, {\tt 'aa}, {\tt 'b} for type variables. Token translations
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
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   873
its syntactic category, though. For example, consider free vs.\ bound
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   874
variables. So Isabelle's pretty printing mechanism, starting from
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
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   877
  trees appropriately. The marks are actually visible by print
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
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   881
be well-behaved in this respect. Free identifiers introduced to
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
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   893
string \times int$ the actual translation function. Assuming that $x$
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$
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   896
is output according to $f(x) = (x', len)$. Thereby $x'$ is the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   897
modified identifier name and $len$ its visual length approximated in
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1387
diff changeset
   898
terms of whole characters. Thus $x'$ may include non-printing parts
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|)}