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