doc-src/Logics/defining.tex
author wenzelm
Thu, 25 Nov 1993 10:44:44 +0100
changeset 142 6dfae8cddec7
parent 135 493308514ea8
child 188 6be0856cdf49
permissions -rw-r--r--
removed section 'Classes and types';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
     2
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\newcommand{\rmindex}[1]{{#1}\index{#1}\@}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
\newcommand{\mtt}[1]{\mbox{\tt #1}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
\newcommand{\ttfct}[1]{\mathop{\mtt{#1}}\nolimits}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
\newcommand{\ttrel}[1]{\mathrel{\mtt{#1}}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
\newcommand{\Constant}{\ttfct{Constant}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
\newcommand{\Variable}{\ttfct{Variable}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
\newcommand{\Appl}[1]{\ttfct{Appl}\mathopen{\mtt[}#1\mathclose{\mtt]}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
\chapter{Defining Logics} \label{Defining-Logics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
This chapter is intended for Isabelle experts. It explains how to define new
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
logical systems, Isabelle's {\em raison d'\^etre}. Isabelle logics are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
hierarchies of theories. A number of simple examples are contained in {\em
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
Introduction to Isabelle}; the full syntax of theory definition files ({\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
.thy} files) is shown in {\em The Isabelle Reference Manual}. This chapter's
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
chief purpose is a thorough description of all syntax related matters
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
concerning theories. The most important sections are \S\ref{sec:mixfix} about
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
mixfix declarations and \S\ref{sec:macros} describing the macro system. The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
concluding examples of \S\ref{sec:min_logics} are more concerned with the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
logical aspects of the definition of theories. Sections marked with * can be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
skipped on the first reading.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
\section{Precedence grammars} \label{sec:precedence_grammars}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
The precise syntax of a logic is best defined by a \rmindex{context-free
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
grammar}. In order to simplify the description of mathematical languages, we
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
introduce an extended format which permits {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
precedences}\indexbold{precedence}. This scheme generalizes precedence
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
declarations in \ML\ and {\sc prolog}. In this extended grammar format,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
nonterminals are decorated by integers, their precedence. In the sequel,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
precedences are shown as subscripts. A nonterminal $A@p$ on the right-hand
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
side of a production may only be replaced using a production $A@q = \gamma$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
where $p \le q$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
Formally, a set of context free productions $G$ induces a derivation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
relation $\rew@G$ on strings as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
\[ \alpha A@p \beta ~\rew@G~ \alpha\gamma\beta ~~~iff~~~
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
   \exists (A@q=\gamma) \in G.~q \ge p
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
Any extended grammar of this kind can be translated into a normal context
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
free grammar. However, this translation may require the introduction of a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
large number of new nonterminals and productions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
\begin{example} \label{ex:precedence}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
The following simple grammar for arithmetic expressions demonstrates how
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
binding power and associativity of operators can be enforced by precedences.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
\begin{tabular}{rclr}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
  $A@9$ & = & {\tt0} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
  $A@9$ & = & {\tt(} $A@0$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
  $A@0$ & = & $A@0$ {\tt+} $A@1$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
  $A@2$ & = & $A@3$ {\tt*} $A@2$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
  $A@3$ & = & {\tt-} $A@3$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
The choice of precedences determines that {\tt -} binds tighter than {\tt *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
which binds tighter than {\tt +}, and that {\tt +} associates to the left and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
{\tt *} to the right.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
To minimize the number of subscripts, we adopt the following conventions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
\item All precedences $p$ must be in the range $0 \leq p \leq max_pri$ for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
  some fixed $max_pri$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
\item Precedence $0$ on the right-hand side and precedence $max_pri$ on the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
  left-hand side may be omitted.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
In addition, we write the production $A@p = \alpha$ as $A = \alpha~(p)$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
i.e.\ the precedence of the left-hand side actually appears in the uttermost
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
right. Finally, alternatives may be separated by $|$, and repetition
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
indicated by \dots.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
Using these conventions and assuming $max_pri=9$, the grammar in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
Example~\ref{ex:precedence} becomes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
\begin{tabular}{rclc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
$A$ & = & {\tt0} & \hspace*{4em} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
 & $|$ & {\tt(} $A$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
 & $|$ & $A$ {\tt+} $A@1$ & (0) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
 & $|$ & $A@3$ {\tt*} $A@2$ & (2) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
 & $|$ & {\tt-} $A@3$ & (3)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
\section{Basic syntax} \label{sec:basic_syntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
The basis of all extensions by object-logics is the \rmindex{Pure theory},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
bound to the \ML-identifier \ttindex{Pure.thy}. It contains, among many other
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
things, the \rmindex{Pure syntax}. An informal account of this basic syntax
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
(meta-logic, types etc.) may be found in {\em Introduction to Isabelle}. A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
more precise description using a precedence grammar is shown in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
Figure~\ref{fig:pure_gram}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
\begin{figure}[htb]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
\begin{tabular}{rclc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
$prop$ &=& \ttindex{PROP} $aprop$ ~~$|$~~ {\tt(} $prop$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
     &$|$& $logic@3$ \ttindex{==} $logic@2$ & (2) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
     &$|$& $logic@3$ \ttindex{=?=} $logic@2$ & (2) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
     &$|$& $prop@2$ \ttindex{==>} $prop@1$ & (1) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
     &$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop@1$ & (1) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
     &$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
$logic$ &=& $prop$ ~~$|$~~ $fun$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
$aprop$ &=& $id$ ~~$|$~~ $var$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
    ~~$|$~~ $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
$fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   115
    &$|$& $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   116
    &$|$& $fun@{max_pri}$ {\tt::} $type$ \\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
    &$|$& \ttindex{\%} $idts$ {\tt.} $logic$ & (0) \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
$idts$ &=& $idt$ ~~$|$~~ $idt@1$ $idts$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
    &$|$& $id$ \ttindex{::} $type$ & (0) \\\\
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   121
$type$ &=& $tfree$ ~~$|$~~ $tvar$ ~~$|$~~ $tfree$ {\tt::} $sort$
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   122
  ~~$|$~~ $tvar$ {\tt::} $sort$ \\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
     &$|$& $id$ ~~$|$~~ $type@{max_pri}$ $id$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
                ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
     &$|$& $type@1$ \ttindex{=>} $type$ & (0) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
     &$|$& {\tt[}  $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0)\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
     &$|$& {\tt(} $type$ {\tt)} \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
$sort$ &=& $id$ ~~$|$~~ {\tt\ttlbrace\ttrbrace}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
                ~~$|$~~ {\tt\ttlbrace} $id$ {\tt,} \dots {\tt,} $id$ {\tt\ttrbrace}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
\end{tabular}\index{*"!"!}\index{*"["|}\index{*"|"]}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
\indexbold{type@$type$} \indexbold{sort@$sort$} \indexbold{idt@$idt$}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
\indexbold{idts@$idts$} \indexbold{logic@$logic$} \indexbold{prop@$prop$}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
\indexbold{fun@$fun$}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
\caption{Meta-Logic Syntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
\label{fig:pure_gram}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
The following main categories are defined:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
  \item[$prop$] Terms of type $prop$, i.e.\ formulae of the meta-logic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
  \item[$aprop$] Atomic propositions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
  \item[$logic$] Terms of types in class $logic$. Initially, $logic$ contains
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
    merely $prop$. As the syntax is extended by new object-logics, more
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   147
    productions for $logic$ are added automatically (see below).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
  \item[$fun$] Terms potentially of function type.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
  \item[$type$] Meta-types.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   153
  \item[$idts$] A list of identifiers, possibly constrained by types. Note
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
    that \verb|x :: nat y| is parsed as \verb|x :: (nat y)|, i.e.\ {\tt y}
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   155
    would be treated like a type constructor applied to {\tt nat}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
\subsection{Logical types and default syntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
Isabelle is concerned with mathematical languages which have a certain
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
minimal vocabulary: identifiers, variables, parentheses, and the lambda
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
calculus. Logical types, i.e.\ those of class $logic$, are automatically
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
equipped with this basic syntax. More precisely, for any type constructor
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   165
$ty$ with arity $(\vec{s})c$, where $c$ is a subclass of $logic$, the
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   166
following productions are added:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
\begin{tabular}{rclc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
$ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
  &$|$& $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
  &$|$& $ty@{max_pri}$ {\tt::} $type$\\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
$logic$ &=& $ty$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
\subsection{Lexical matters *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
The parser does not process input strings directly, it rather operates on
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
token lists provided by Isabelle's \rmindex{lexical analyzer} (the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
\bfindex{lexer}). There are two different kinds of tokens: {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
literals}\indexbold{literal token}\indexbold{token!literal} and {\bf valued
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
tokens}\indexbold{valued token}\indexbold{token!valued}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   185
Literals can be regarded as reserved words\index{reserved word} of the syntax
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   186
and the user can add new ones, when extending theories. In
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   187
Figure~\ref{fig:pure_gram} they appear in typewriter type, e.g.\ {\tt PROP},
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   188
{\tt ==}, {\tt =?=}, {\tt ;}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
Valued tokens on the other hand have a fixed predefined syntax. The lexer
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
distinguishes four kinds of them: identifiers\index{identifier},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
unknowns\index{unknown}\index{scheme variable|see{unknown}}, type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
variables\index{type variable}, type unknowns\index{type unknown}\index{type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
scheme variable|see{type unknown}}; they are denoted by $id$\index{id@$id$},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
$var$\index{var@$var$}, $tfree$\index{tfree@$tfree$},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
$tvar$\index{tvar@$tvar$}, respectively. Typical examples are {\tt x}, {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
?x7}, {\tt 'a}, {\tt ?'a3}, the exact syntax is:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
\begin{tabular}{rcl}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
$id$        & =   & $letter~quasiletter^*$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
$var$       & =   & ${\tt ?}id ~~|~~ {\tt ?}id{\tt .}nat$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
$tfree$     & =   & ${\tt '}id$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
$tvar$      & =   & ${\tt ?}tfree ~~|~~ {\tt ?}tfree{\tt .}nat$ \\[1ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
$letter$    & =   & one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
$digit$     & =   & one of {\tt 0}\dots {\tt 9} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
$quasiletter$ & =  & $letter ~~|~~ digit ~~|~~ {\tt _} ~~|~~ {\tt '}$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
$nat$       & =   & $digit^+$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
A string of $var$ or $tvar$ describes an \rmindex{unknown} which is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
internally a pair of base name and index (\ML\ type \ttindex{indexname}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
These components are either explicitly separated by a dot as in {\tt ?x.1} or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
{\tt ?x7.3} or directly run together as in {\tt ?x1}. The latter form is
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   215
possible, if the base name does not end with digits. And if the index is 0,
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   216
it may be dropped altogether: {\tt ?x} abbreviates {\tt ?x0} or {\tt ?x.0}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
Note that $id$, $var$, $tfree$, $tvar$ are mutually disjoint, but it is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
perfectly legal that they overlap with the set of literal tokens (e.g.\ {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
PROP}, {\tt ALL}, {\tt EX}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
The lexical analyzer translates input strings to token lists by repeatedly
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
taking the maximal prefix of the input string that forms a valid token. A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
maximal prefix that is both a literal and a valued token is treated as a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
literal. Spaces, tabs and newlines are separators; they never occur within
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
tokens.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
Note that literals need not necessarily be surrounded by white space to be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
recognized as separate. For example, if {\tt -} is a literal but {\tt --} is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
not, then the string {\tt --} is treated as two consecutive occurrences of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
{\tt -}. This is in contrast to \ML\ which would treat {\tt --} always as a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
single symbolic name. The consequence of Isabelle's more liberal scheme is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
that the same string may be parsed in different ways after extending the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
syntax: after adding {\tt --} as a literal, the input {\tt --} is treated as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
a single token.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
\subsection{Inspecting syntax *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
You may get the \ML\ representation of the syntax of any Isabelle theory by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
applying \index{*syn_of}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
  syn_of: theory -> Syntax.syntax
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
\end{ttbox}
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   245
\ttindex{Syntax.syntax} is an abstract type. Values of this type can be
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   246
displayed by the following functions: \index{*Syntax.print_syntax}
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   247
\index{*Syntax.print_gram} \index{*Syntax.print_trans}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
  Syntax.print_syntax: Syntax.syntax -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
  Syntax.print_gram: Syntax.syntax -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
  Syntax.print_trans: Syntax.syntax -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
\end{ttbox}
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   253
{\tt Syntax.print_syntax} shows virtually all information contained in a
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   254
syntax, therefore being quite verbose. Its output is divided into labeled
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   255
sections. The syntax proper is represented by {\tt lexicon}, {\tt roots} and
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
{\tt prods}. The rest refers to the manifold facilities to apply syntactic
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   257
translations (macro expansion etc.).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
To simplify coping with the verbosity of {\tt Syntax.print_syntax}, there are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
\ttindex{Syntax.print_gram} to print the syntax proper only and
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   261
\ttindex{Syntax.print_trans} to print the translation related information
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   262
only.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
Let's have a closer look at part of Pure's syntax:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
Syntax.print_syntax (syn_of Pure.thy);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
{\out lexicon: "!!" "%" "(" ")" "," "." "::" ";" "==" "==>" \dots}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
{\out roots: logic type fun prop}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
{\out prods:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
{\out   type = tfree  (1000)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
{\out   type = tvar  (1000)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
{\out   type = id  (1000)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
{\out   type = tfree "::" sort[0]  => "_ofsort" (1000)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
{\out   type = tvar "::" sort[0]  => "_ofsort" (1000)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
{\out   \vdots}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
{\out consts: "_K" "_appl" "_aprop" "_args" "_asms" "_bigimpl" \dots}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
{\out parse_ast_translation: "_appl" "_bigimpl" "_bracket"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
{\out   "_idtyp" "_lambda" "_tapp" "_tappl"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
{\out parse_rules:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
{\out parse_translation: "!!" "_K" "_abs" "_aprop"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
{\out print_translation: "all"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
{\out print_rules:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
{\out print_ast_translation: "==>" "_abs" "_idts" "fun"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
  \item[\ttindex{lexicon}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
    The set of literal tokens (i.e.\ reserved words, delimiters) used for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
    lexical analysis.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
  \item[\ttindex{roots}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
    The legal syntactic categories to start parsing with. You name the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
    desired root directly as a string when calling lower level functions or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
    specifying macros. Higher level functions usually expect a type and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
    derive the actual root as follows:\index{root_of_type@$root_of_type$}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
    \begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
      \item $root_of_type(\tau@1 \To \tau@2) = \mtt{fun}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
      \item $root_of_type(\tau@1 \mathrel{ty} \tau@2) = ty$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
      \item $root_of_type((\tau@1, \dots, \tau@n)ty) = ty$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
      \item $root_of_type(\alpha) = \mtt{logic}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
    \end{itemize}
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   305
    Thereby $\tau@1, \dots, \tau@n$ are types, $ty$ an infix or ordinary type
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   306
    constructor and $\alpha$ a type variable or unknown. Note that only the
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   307
    outermost type constructor is taken into account.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
  \item[\ttindex{prods}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
    The list of productions describing the precedence grammar. Nonterminals
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   311
    $A@n$ are rendered in {\sc ascii} as {\tt $A$[$n$]}, literal tokens are
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   312
    quoted. Some productions have strings attached after an {\tt =>}. These
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
    strings later become the heads of parse trees, but they also play a vital
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
    role when terms are printed (see \S\ref{sec:asts}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
    Productions which do not have string attached and thus do not create a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
    new parse tree node are called {\bf copy productions}\indexbold{copy
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
    production}. They must have exactly one
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
    argument\index{argument!production} (i.e.\ nonterminal or valued token)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
    on the right-hand side. The parse tree generated when parsing that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
    argument is simply passed up as the result of parsing the whole copy
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
    production.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
    A special kind of copy production is one where the argument is a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
    nonterminal and no additional syntactic sugar (literals) exists. It is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
    called a \bfindex{chain production}. Chain productions should be seen as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
    an abbreviation mechanism: conceptually, they are removed from the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
    grammar by adding appropriate new rules. Precedence information attached
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
    to chain productions is ignored, only the dummy value $-1$ is displayed.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
  \item[\ttindex{consts}, \ttindex{parse_rules}, \ttindex{print_rules}]
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   332
    This is macro related information (see \S\ref{sec:macros}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
  \item[\tt *_translation]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
    \index{*parse_ast_translation} \index{*parse_translation}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
    \index{*print_translation} \index{*print_ast_translation}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
    The sets of constants that invoke translation functions. These are more
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
    arcane matters (see \S\ref{sec:asts} and \S\ref{sec:tr_funs}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
Of course you may inspect the syntax of any theory using the above calling
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   342
sequence. Beware that, as more and more material accumulates, the output
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   343
becomes even more verbose. When extending syntaxes, new {\tt roots}, {\tt
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   344
prods}, {\tt parse_rules} and {\tt print_rules} are appended to the end. The
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   345
other lists are displayed sorted.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
\section{Abstract syntax trees} \label{sec:asts}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
Figure~\ref{fig:parse_print} shows a simplified model of the parsing and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
printing process.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
\begin{figure}[htb]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
\begin{tabular}{cl}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
string          & \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
$\downarrow$    & parser \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
parse tree      & \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
$\downarrow$    & \rmindex{parse ast translation} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
ast             & \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
$\downarrow$    & ast rewriting (macros) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
ast             & \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
$\downarrow$    & \rmindex{parse translation}, type-inference \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
--- well-typed term --- & \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
$\downarrow$    & \rmindex{print translation} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
ast             & \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
$\downarrow$    & ast rewriting (macros) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
ast             & \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
$\downarrow$    & \rmindex{print ast translation}, printer \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
string          &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
\caption{Parsing and Printing}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
\label{fig:parse_print}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   378
The parser takes an input string (more precisely the token list produced by
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   379
the lexer) and produces a \rminx{parse tree}, which is directly derived
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   380
from the productions involved. By applying some internal transformations the
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   381
parse tree becomes an \bfindex{abstract syntax tree} (\bfindex{ast}). Macro
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
expansion, further translations and finally type inference yields a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
well-typed term\index{term!well-typed}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
The printing process is the reverse, except for some subtleties to be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
discussed later.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
Asts are an intermediate form between the very raw parse trees and the typed
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
$\lambda$-terms. An ast is either an atom (constant or variable) or a list of
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   390
{\em at least two\/} subasts. Internally, they have type \ttindex{Syntax.ast}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
which is defined as: \index{*Constant} \index{*Variable} \index{*Appl}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
datatype ast =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
  Constant of string |
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
  Variable of string |
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
  Appl of ast list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
Notation: We write constant atoms as quoted strings, variable atoms as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
non-quoted strings and applications as list of subasts separated by space and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
enclosed in parentheses. For example:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
  Appl [Constant "_constrain",
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
    Appl [Constant "_abs", Variable "x", Variable "t"],
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
    Appl [Constant "fun", Variable "'a", Variable "'b"]]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
  {\rm is written as} ("_constrain" ("_abs" x t) ("fun" 'a 'b))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
Note that {\tt ()} and {\tt (f)} are both illegal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   411
The resemblance of Lisp's S-expressions is intentional, but notice the two
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
kinds of atomic symbols: $\Constant x$ and $\Variable x$. This distinction
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   413
has some more obscure reasons and you can ignore it about half of the time.
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   414
You should not take the names ``{\tt Constant}'' and ``{\tt Variable}'' too
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   415
literally. In the later translation to terms, $\Variable x$ may become a
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   416
constant, free or bound variable, even a type constructor or class name; the
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   417
actual outcome depends on the context.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
Similarly, you can think of ${\tt (} f~x@1~\ldots~x@n{\tt )}$ as some sort of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
application of $f$ to the arguments $x@1, \ldots, x@n$. But the actual kind
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
of application (say a type constructor $f$ applied to types $x@1, \ldots,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
x@n$) is determined later by context, too.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
Forms like {\tt (("_abs" x $t$) $u$)} are perfectly legal, but asts are not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
higher-order: the {\tt "_abs"} does not yet bind the {\tt x} in any way,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
though later at the term level, {\tt ("_abs" x $t$)} will become an {\tt Abs}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
node and occurrences of {\tt x} in $t$ will be replaced by {\tt Bound}s. Even
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   428
if non-constant heads of applications may seem unusual, asts should be
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   429
regarded as first-order. Purists may think of ${\tt (} f~x@1~\ldots~x@n{\tt
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   430
)}$ as a first-order application of some invisible $(n+1)$-ary constant.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
\subsection{Parse trees to asts}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
Asts are generated from parse trees by applying some translation functions,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
which are internally called {\bf parse ast translations}\indexbold{parse ast
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
translation}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
We can think of the raw output of the parser as trees built up by nesting the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
right-hand sides of those productions that were used to derive a word that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
matches the input token list. Then parse trees are simply lists of tokens and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
sub parse trees, the latter replacing the nonterminals of the productions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
Note that we refer here to the actual productions in their internal form as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
displayed by {\tt Syntax.print_syntax}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
Ignoring parse ast translations, the mapping
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
$ast_of_pt$\index{ast_of_pt@$ast_of_pt$} from parse trees to asts is derived
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
from the productions involved as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
  \item Valued tokens: $ast_of_pt(t) = \Variable s$, where $t$ is an $id$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
    $var$, $tfree$ or $tvar$ token, and $s$ its value.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
  \item Copy productions: $ast_of_pt(\ldots P \ldots) = ast_of_pt(P)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
  \item $0$-ary productions: $ast_of_pt(\ldots \mtt{=>} c) = \Constant c$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
  \item $n$-ary productions: $ast_of_pt(\ldots P@1 \ldots P@n \ldots \mtt{=>}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
    c) = \Appl{\Constant c,$ $ast_of_pt(P@1),$ $\ldots,$ $ast_of_pt(P@n)}$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
    where $n \ge 1$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
Thereby $P, P@1, \ldots, P@n$ denote sub parse trees or valued tokens and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
``\dots'' zero or more literal tokens. That means literal tokens are stripped
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
and do not appear in asts.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
The following table presents some simple examples:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
{\tt\begin{tabular}{ll}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
\rm input string    & \rm ast \\\hline
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
"f"                 & f \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
"'a"                & 'a \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
"t == u"            & ("==" t u) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
"f(x)"              & ("_appl" f x) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
"f(x, y)"           & ("_appl" f ("_args" x y)) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
"f(x, y, z)"        & ("_appl" f ("_args" x ("_args" y z))) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
"\%x y.\ t"         & ("_lambda" ("_idts" x y) t) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
\end{tabular}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
Some of these examples illustrate why further translations are desirable in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   479
order to provide some nice standard form of asts before macro expansion takes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
place. Hence the Pure syntax provides predefined parse ast
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
translations\index{parse ast translation!of Pure} for ordinary applications,
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   482
type applications, nested abstractions, meta implications and function types.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
Their net effect on some representative input strings is shown in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
Figure~\ref{fig:parse_ast_tr}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
\begin{figure}[htb]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
{\tt\begin{tabular}{ll}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
\rm string                  & \rm ast \\\hline
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
"f(x, y, z)"                & (f x y z) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
"'a ty"                     & (ty 'a) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
"('a, 'b) ty"               & (ty 'a 'b) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
"\%x y z.\ t"               & ("_abs" x ("_abs" y ("_abs" z t))) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
"\%x ::\ 'a.\ t"            & ("_abs" ("_constrain" x 'a) t) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
"[| P; Q; R |] => S"        & ("==>" P ("==>" Q ("==>" R S))) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
"['a, 'b, 'c] => 'd"        & ("fun" 'a ("fun" 'b ("fun" 'c 'd)))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
\end{tabular}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
\caption{Built-in Parse Ast Translations}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
\label{fig:parse_ast_tr}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
This translation process is guided by names of constant heads of asts. The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
list of constants invoking parse ast translations is shown in the output of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   505
{\tt Syntax.print_syntax} under {\tt parse_ast_translation}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   506
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
\subsection{Asts to terms *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
After the ast has been normalized by the macro expander (see
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
\S\ref{sec:macros}), it is transformed into a term with yet another set of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
translation functions interspersed: {\bf parse translations}\indexbold{parse
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
translation}. The result is a non-typed term\index{term!non-typed} which may
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
contain type constraints, that is 2-place applications with head {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
"_constrain"}. The second argument of a constraint is a type encoded as term.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
Real types will be introduced later during type inference, which is not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
discussed here.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
If we ignore the built-in parse translations of Pure first, then the mapping
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
$term_of_ast$\index{term_of_ast@$term_of_ast$} from asts to (non-typed) terms
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
is defined by:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
  \item $term_of_ast(\Constant x) = \ttfct{Const} (x, \mtt{dummyT})$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
  \item $term_of_ast(\Variable \mtt{"?}xi\mtt") = \ttfct{Var} ((x, i),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
    \mtt{dummyT})$, where $x$ is the base name and $i$ the index extracted
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
    from $xi$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
  \item $term_of_ast(\Variable x) = \ttfct{Free} (x, \mtt{dummyT})$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
  \item $term_of_ast(\Appl{f, x@1, \ldots, x@n}) = term_of_ast(f) ~{\tt\$}~
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
    term_of_ast(x@1)$ {\tt\$} \dots\ {\tt\$} $term_of_ast(x@n)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
Note that {\tt Const}, {\tt Var}, {\tt Free} belong to the datatype {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
term} and \ttindex{dummyT} is bound to some dummy {\tt typ}, which is ignored
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
during type-inference.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   538
So far the outcome is still a first-order term. {\tt Abs}s and {\tt Bound}s
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
are introduced by parse translations associated with {\tt "_abs"} and {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   540
"!!"} (and any other user defined binder).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   542
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
\subsection{Printing of terms *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   545
When terms are prepared for printing, they are first transformed into asts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   546
via $ast_of_term$\index{ast_of_term@$ast_of_term$} (ignoring {\bf print
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
translations}\indexbold{print translation}):
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
  \item $ast_of_term(\ttfct{Const} (x, \tau)) = \Constant x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
  \item $ast_of_term(\ttfct{Free} (x, \tau)) = constrain (\Variable x,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   552
    \tau)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   554
  \item $ast_of_term(\ttfct{Var} ((x, i), \tau)) = constrain (\Variable
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   555
    \mtt{"?}xi\mtt", \tau)$, where $\mtt?xi$ is the string representation of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   556
    the {\tt indexname} $(x, i)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
  \item $ast_of_term(\ttfct{Abs} (x, \tau, t)) = \ttfct{Appl}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
    \mathopen{\mtt[} \Constant \mtt{"_abs"}, constrain(\Variable x', \tau),$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   560
    $ast_of_term(t') \mathclose{\mtt]}$, where $x'$ is a version of $x$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
    renamed away from all names occurring in $t$, and $t'$ the body $t$ with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   562
    all {\tt Bound}s referring to this {\tt Abs} replaced by $\ttfct{Free}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
    (x', \mtt{dummyT})$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
  \item $ast_of_term(\ttfct{Bound} i) = \Variable \mtt{"B.}i\mtt"$. Note that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
    the occurrence of loose bound variables is abnormal and should never
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   567
    happen when printing well-typed terms.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
  \item $ast_of_term(f \ttrel{\$} x@1 \ttrel{\$} \ldots \ttrel{\$} x@n) =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
    \ttfct{Appl} \mathopen{\mtt[} ast_of_term(f), ast_of_term(x@1), \ldots,$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
    $ast_of_term(x@n) \mathclose{\mtt]}$, where $f$ is not an application.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   572
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
  \item $constrain(x, \tau) = x$, if $\tau = \mtt{dummyT}$ \index{*dummyT} or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
    \ttindex{show_types} not set to {\tt true}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   575
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
  \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, ty}$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
    where $ty$ is the ast encoding of $\tau$. That is: type constructors as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   578
    {\tt Constant}s, type variables as {\tt Variable}s and type applications
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   579
    as {\tt Appl}s with the head type constructor as first element.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   580
    Additionally, if \ttindex{show_sorts} is set to {\tt true}, some type
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   581
    variables are decorated with an ast encoding of their sort.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   583
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   585
After an ast has been normalized wrt.\ the print macros, it is transformed
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   586
into the final output string. The built-in {\bf print ast
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
translations}\indexbold{print ast translation} are essentially the reverse
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
ones of the parse ast translations of Figure~\ref{fig:parse_ast_tr}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
For the actual printing process, the names attached to grammar productions of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   591
the form $\ldots A@{p@1}^1 \ldots A@{p@n}^n \ldots \mtt{=>} c$ play a vital
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   592
role. Whenever an ast with constant head $c$, i.e.\ $\mtt"c\mtt"$ or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
$(\mtt"c\mtt"~ x@1 \ldots x@n)$, is encountered it is printed according to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
the production for $c$. This means that first the arguments $x@1$ \dots $x@n$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   595
are printed, then put in parentheses if necessary for reasons of precedence,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   596
and finally joined to a single string, separated by the syntactic sugar of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   597
the production (denoted by ``\dots'' above).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   598
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
If an application $(\mtt"c\mtt"~ x@1 \ldots x@m)$ has more arguments than the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   600
corresponding production, it is first split into $((\mtt"c\mtt"~ x@1 \ldots
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   601
x@n) ~ x@{n+1} \ldots x@m)$. Applications with too few arguments or with
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   602
non-constant head or without a corresponding production are printed as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   603
$f(x@1, \ldots, x@l)$ or $(\alpha@1, \ldots, \alpha@l) ty$. A single
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   604
$\Variable x$ is simply printed as $x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   605
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   606
Note that the system does {\em not\/} insert blanks automatically. They
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   607
should be part of the mixfix declaration the production has been derived
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   608
from, if they are required to separate tokens. Mixfix declarations may also
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   609
contain pretty printing annotations.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   612
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   613
\section{Mixfix declarations} \label{sec:mixfix}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   614
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   615
When defining theories, the user usually declares new constants as names
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   616
associated with a type followed by an optional \bfindex{mixfix annotation}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   617
If none of the constants are introduced with mixfix annotations, there is no
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   618
concrete syntax to speak of: terms can only be abstractions or applications
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   619
of the form $f(t@1, \dots, t@n)$. Since this notation quickly becomes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   620
unreadable, Isabelle supports syntax definitions in the form of unrestricted
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
context-free \index{context-free grammar} \index{precedence grammar}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   622
precedence grammars using mixfix annotations.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   623
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   624
Mixfix annotations describe the {\em concrete\/} syntax, a standard
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   625
translation into the abstract syntax and a pretty printing scheme, all in
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   626
one. Isabelle syntax definitions are inspired by \OBJ's~\cite{OBJ} {\em
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   627
mixfix\/} syntax. Each mixfix annotation defines a precedence grammar
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   628
production and optionally associates a constant with it.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   629
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   630
There is a general form of mixfix annotation and some shortcuts for common
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   631
cases like infix operators.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   632
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   633
The general \bfindex{mixfix declaration} as it may occur within the {\tt
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   634
consts} section\index{consts section@{\tt consts} section} of a {\tt .thy}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   635
file, specifies a constant declaration and a grammar production at the same
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   636
time. It has the form {\tt $c$ ::\ "$\tau$" ("$sy$" $ps$ $p$)} and is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   637
interpreted as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   638
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   639
  \item {\tt $c$ ::\ "$\tau$"} is the actual constant declaration without any
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   640
    syntactic significance.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   641
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   642
  \item $sy$ is the right-hand side of the production, specified as a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
    symbolic string. In general, $sy$ is of the form $\alpha@0 \_ \alpha@1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
    \dots \alpha@{n-1} \_ \alpha@n$, where each occurrence of \ttindex{_}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   645
    denotes an argument\index{argument!mixfix} position and the strings
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   646
    $\alpha@i$ do not contain (non-escaped) {\tt _}. The $\alpha@i$ may
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   647
    consist of delimiters\index{delimiter},
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   648
    spaces\index{space (pretty printing)} or \rmindex{pretty printing}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   649
    annotations (see below).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   650
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   651
  \item $\tau$ specifies the syntactic categories of the arguments on the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   652
    left-hand and of the right-hand side. Arguments may be nonterminals or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   653
    valued tokens. If $sy$ is of the form above, $\tau$ must be a nested
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   654
    function type with at least $n$ argument positions, say $\tau = [\tau@1,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   655
    \dots, \tau@n] \To \tau'$. The syntactic category of argument $i$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   656
    derived from type $\tau@i$ (see $root_of_type$ in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   657
    \S\ref{sec:basic_syntax}). The result, i.e.\ the left-hand side of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   658
    production, is derived from type $\tau'$. Note that the $\tau@i$ and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   659
    $\tau'$ may be function types.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   660
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   661
  \item $c$ is the name of the constant associated with the production. If
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   662
    $c$ is the empty string {\tt ""} then this is a \rmindex{copy
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
    production}. Otherwise, parsing an instance of the phrase $sy$ generates
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   664
    the ast {\tt ("$c$" $a@1$ $\ldots$ $a@n$)}, where $a@i$ is the ast
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   665
    generated by parsing the $i$-th argument.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   666
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   667
  \item $ps$ is an optional list of at most $n$ integers, say {\tt [$p@1$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   668
    $\ldots$, $p@m$]}, where $p@i$ is the minimal \rmindex{precedence}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   669
    required of any phrase that may appear as the $i$-th argument. Missing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   670
    precedences default to $0$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   671
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   672
  \item $p$ is the \rmindex{precedence} the of this production.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   673
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   674
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   675
Precedences\index{precedence!range of} may range between $0$ and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   676
$max_pri$\indexbold{max_pri@$max_pri$} (= 1000). If you want to ignore them,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   677
the safest way to do so is to use the declaration {\tt $c$ ::\ "$\tau$"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   678
("$sy$")}. The resulting production puts no precedence constraints on any of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   679
its arguments and has maximal precedence itself.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   680
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
\begin{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
The following theory specification contains a {\tt consts} section that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   683
encodes the precedence grammar of Example~\ref{ex:precedence} as mixfix
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   684
declarations:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   685
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
EXP = Pure +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   687
types
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   688
  exp 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   689
arities
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   690
  exp :: logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   692
  "0" :: "exp"                ("0" 9)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   693
  "+" :: "[exp, exp] => exp"  ("_ + _" [0, 1] 0)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   694
  "*" :: "[exp, exp] => exp"  ("_ * _" [3, 2] 2)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   695
  "-" :: "exp => exp"         ("- _" [3] 3)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   696
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   697
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   698
Note that the {\tt arities} declaration causes {\tt exp} to be added to the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   699
syntax' roots. If you put the above text into a file {\tt exp.thy} and load
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   700
it via {\tt use_thy "EXP"}, you can run some tests:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   701
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   702
val read_exp = Syntax.test_read (syn_of EXP.thy) "exp";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   703
read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   704
{\out tokens: "0" "*" "0" "*" "0" "*" "0" "+" "0" "+" "0" "+" "0"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   705
{\out raw: ("+" ("+" ("+" ("*" "0" ("*" "0" ("*" "0" "0"))) "0") "0") "0")}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   706
{\out \vdots}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   707
read_exp "0 + - 0 + 0";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   708
{\out tokens: "0" "+" "-" "0" "+" "0"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   709
{\out raw: ("+" ("+" "0" ("-" "0")) "0")}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   710
{\out \vdots}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   711
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   712
The output of \ttindex{Syntax.test_read} includes the token list ({\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   713
tokens}) and the raw ast directly derived from the parse tree, ignoring parse
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   714
ast translations. The rest is tracing information provided by the macro
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   715
expander (see \S\ref{sec:macros}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   716
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   717
Executing {\tt Syntax.print_gram (syn_of EXP.thy)} reveals the actual grammar
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   718
productions derived from the above mixfix declarations (lots of additional
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   719
information deleted):
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   720
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   721
exp = "0"  => "0" (9)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   722
exp = exp[0] "+" exp[1]  => "+" (0)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   723
exp = exp[3] "*" exp[2]  => "*" (2)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   724
exp = "-" exp[3]  => "-" (3)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   725
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   726
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   727
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   728
Let us now have a closer look at the structure of the string $sy$ appearing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   729
in mixfix annotations. This string specifies a list of parsing and printing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   730
directives, namely delimiters\index{delimiter},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   731
arguments\index{argument!mixfix}, spaces\index{space (pretty printing)},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   732
blocks of indentation\index{block (pretty printing)} and optional or forced
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   733
line breaks\index{break (pretty printing)}. These are encoded via the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   734
following character sequences:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   735
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   736
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   737
  \item[~\ttindex_~] An argument\index{argument!mixfix} position.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   738
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   739
  \item[~$d$~] A \rmindex{delimiter}, i.e.\ a non-empty sequence of
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   740
    non-special or escaped characters. Escaping a
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   741
    character\index{escape character} means preceding it with a {\tt '}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   742
    (quote). Thus you have to write {\tt ''} if you really want a single
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   743
    quote. Delimiters may never contain white space, though.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   744
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   745
  \item[~$s$~] A non-empty sequence of spaces\index{space (pretty printing)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   746
    for printing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   747
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   748
  \item[~{\ttindex($n$}~] Open a block\index{block (pretty printing)}. $n$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   749
    an optional sequence of digits that specifies the amount of indentation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   750
    to be added when a line break occurs within the block. If {\tt(} is not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   751
    followed by a digit, the indentation defaults to $0$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   752
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   753
  \item[~\ttindex)~] Close a block.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   754
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   755
  \item[~\ttindex{//}~] Force a line break\index{break (pretty printing)}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   756
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   757
  \item[~\ttindex/$s$~] Allow a line break\index{break (pretty printing)}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   758
    Spaces $s$ right after {\tt /} are only printed if the break is not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   759
    taken.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   760
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   761
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   762
In terms of parsing, arguments are nonterminals or valued tokens, while
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   763
delimiters are literal tokens. The other directives have only significance
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   764
for printing. The \rmindex{pretty printing} mechanisms of Isabelle is
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   765
essentially the one described in \cite{paulson91}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   766
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   767
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   768
\subsection{Infixes}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   769
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   770
Infix\index{infix} operators associating to the left or right can be declared
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   771
conveniently using \ttindex{infixl} or \ttindex{infixr}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   772
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   773
Roughly speaking, the form {\tt $c$ ::\ "$\tau$" (infixl $p$)} abbreviates:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   774
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   775
"op \(c\)" ::\ "\(\tau\)"   ("op \(c\)")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   776
"op \(c\)" ::\ "\(\tau\)"   ("(_ \(c\)/ _)" [\(p\), \(p + 1\)] \(p\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   777
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   778
and {\tt $c$ ::\ "$\tau$" (infixr $p$)} abbreviates:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   779
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   780
"op \(c\)" ::\ "\(\tau\)"   ("op \(c\)")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   781
"op \(c\)" ::\ "\(\tau\)"   ("(_ \(c\)/ _)" [\(p + 1\), \(p\)] \(p\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   782
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   783
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   784
Thus, prefixing infixes with \ttindex{op} makes them behave like ordinary
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   785
function symbols. Special characters occurring in $c$ have to be escaped as
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   786
in delimiters. Also note that the expanded forms above would be actually
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   787
illegal at the user level because of duplicate declarations of constants.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   788
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   789
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   790
\subsection{Binders}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   791
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   792
A \bfindex{binder} is a variable-binding construct, such as a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   793
\rmindex{quantifier}. The constant declaration \indexbold{*binder}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   794
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   795
\(c\) ::\ "\(\tau\)"   (binder "\(Q\)" \(p\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   796
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   797
introduces a binder $c$ of type $\tau$, which must have the form $(\tau@1 \To
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   798
\tau@2) \To \tau@3$. Its concrete syntax is $Q~x.P$. A binder is like a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   799
generalized quantifier where $\tau@1$ is the type of the bound variable $x$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   800
$\tau@2$ the type of the body $P$, and $\tau@3$ the type of the whole term.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   801
For example $\forall$ can be declared like this:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   802
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   803
All :: "('a => o) => o"   (binder "ALL " 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   804
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   805
This allows us to write $\forall x.P$ either as {\tt All(\%$x$.$P$)} or {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   806
ALL $x$.$P$}. When printing terms, Isabelle usually uses the latter form, but
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   807
has to fall back on $\mtt{All}(P)$, if $P$ is not an abstraction.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   808
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   809
Binders $c$ of type $(\sigma \To \tau) \To \tau$ can be nested; then the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   810
internal form $c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   811
\ldots))$ corresponds to external $Q~x@1~x@2 \ldots x@n. P$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   812
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   813
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   814
The general binder declaration
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   815
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   816
\(c\) ::\ "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"   (binder "\(Q\)" \(p\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   817
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   818
is internally expanded to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   819
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   820
\(c\)   ::\ "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   821
"\(Q\)" ::\ "[idts, \(\tau@2\)] => \(\tau@3\)"   ("(3\(Q\)_./ _)" \(p\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   822
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   823
with $idts$ being the syntactic category for a list of $id$s optionally
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   824
constrained (see Figure~\ref{fig:pure_gram}). Note that special characters in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   825
$Q$ have to be escaped as in delimiters.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   826
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   827
Additionally, a parse translation\index{parse translation!for binder} for $Q$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   828
and a print translation\index{print translation!for binder} for $c$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   829
installed. These perform behind the scenes the translation between the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   830
internal and external forms.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   831
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   832
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   833
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   834
\section{Syntactic translations (macros)} \label{sec:macros}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   835
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   836
So far we have pretended that there is a close enough relationship between
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   837
concrete and abstract syntax to allow an automatic translation from one to
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   838
the other using the constant name supplied with each non-copy production. In
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   839
many cases this scheme is not powerful enough. Some typical examples involve
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   840
variable binding constructs (e.g.\ {\tt ALL x:A.P} vs.\ {\tt Ball(A, \%x.P)}
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   841
or convenient notations for enumerations like finite sets, lists etc.\ (e.g.\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   842
{\tt [x, y, z]} vs.\ {\tt Cons(x, Cons(y, Cons(z, Nil)))}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   843
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   844
Isabelle offers such translation facilities at two different levels, namely
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   845
{\bf macros}\indexbold{macro} and {\bf translation functions}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   846
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   847
Macros are specified by first-order rewriting systems that operate on asts.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   848
They are usually easy to read and in most cases not very difficult to write.
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   849
Unfortunately, some more obscure translations cannot be expressed as macros
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   850
and you have to fall back on the more powerful mechanism of translation
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   851
functions written in \ML. These are quite unreadable and hard to write (see
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   852
\S\ref{sec:tr_funs}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   853
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   854
\medskip
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   855
Let us now get started with the macro system by a simple example:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   856
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   857
\begin{example}~ \label{ex:set_trans}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   858
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   859
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   860
SET = Pure +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   861
types
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   862
  i, o 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   863
arities
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   864
  i, o :: logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   865
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   866
  Trueprop      :: "o => prop"              ("_" 5)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   867
  Collect       :: "[i, i => o] => i"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   868
  "{\at}Collect"    :: "[idt, i, o] => i"       ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   869
  Replace       :: "[i, [i, i] => o] => i"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   870
  "{\at}Replace"    :: "[idt, idt, i, o] => i"  ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   871
  Ball          :: "[i, i => o] => o"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   872
  "{\at}Ball"       :: "[idt, i, o] => o"       ("(3ALL _:_./ _)" 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   873
translations
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   874
  "{\ttlbrace}x:A. P{\ttrbrace}"    == "Collect(A, %x. P)"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   875
  "{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, %x y. Q)"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   876
  "ALL x:A. P"  == "Ball(A, %x. P)"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   877
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   878
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   879
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   880
This and the following theories are complete working examples, though they
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   881
are fragmentary as they contain merely syntax. They are somewhat fashioned
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   882
after {\tt ZF/zf.thy}, where you should look for a good real-world example.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   883
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   884
{\tt SET} defines constants for set comprehension ({\tt Collect}),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   885
replacement ({\tt Replace}) and bounded universal quantification ({\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   886
Ball}). Without additional syntax you would have to express $\forall x \in A.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   887
P(x)$ as {\tt Ball(A, P)}. Since this is quite awkward, we define additional
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   888
constants with appropriate concrete syntax. These constants are decorated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   889
with {\tt\at} to stress their pure syntactic purpose; they should never occur
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   890
within the final well-typed terms. Another consequence is that the user
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   891
cannot refer to such names directly, since they are not legal identifiers.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   892
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   893
The translations cause the replacement of external forms by internal forms
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   894
after parsing, and vice versa before printing of terms.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   895
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   896
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   897
This is only a very simple but common instance of a more powerful mechanism.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   898
As a specification of what is to be translated, it should be comprehensible
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   899
without further explanations. But there are also some snags and other
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   900
peculiarities that are typical for macro systems in general. The purpose of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   901
this section is to explain how Isabelle's macro system really works.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   902
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   903
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   904
\subsection{Specifying macros}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   905
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   906
Basically macros are rewrite rules on asts. But unlike other macro systems of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   907
various programming languages, Isabelle's macros work two way. Therefore a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   908
syntax contains two lists of rules: one for parsing and one for printing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   909
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   910
The {\tt translations} section\index{translations section@{\tt translations}
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   911
section} consists of a list of rule specifications of the form:
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   912
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   913
\begin{center}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   914
{\tt $[$ ($root$) $]$ $string$ $[$ => $|$ <= $|$ == $]$ $[$ ($root$) $]$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   915
$string$}.
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   916
\end{center}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   917
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   918
This specifies a \rmindex{parse rule} ({\tt =>}) a \rmindex{print rule} ({\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   919
<=}) or both ({\tt ==}). The two $string$s preceded by optional parenthesized
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   920
$root$s denote the left-hand and right-hand side of the rule as `source
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   921
code', i.e.\ in the usual syntax of terms.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   922
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   923
Rules are internalized wrt.\ an intermediate signature that is obtained from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   924
the parent theories' ones by adding all material of all sections preceding
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   925
{\tt translations} in the {\tt .thy} file. Especially, new syntax defined in
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   926
{\tt consts} is already effective.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   927
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   928
Then part of the process that transforms input strings into terms is applied:
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   929
lexing, parsing and parse ast translations (see \S\ref{sec:asts}). Macros
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   930
specified in the parents are {\em not\/} expanded. Also note that the lexer
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   931
runs in a different mode that additionally accepts identifiers of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   932
$\_~letter~quasiletter^*$ (like {\tt _idt}, {\tt _K}). The syntactic category
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   933
to parse is specified by $root$, which defaults to {\tt logic}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   934
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   935
Finally, Isabelle tries to guess which atoms of the resulting ast of the rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   936
should be treated as constants during matching (see below). These names are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   937
extracted from all class, type and constant declarations made so far.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   938
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   939
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   940
The result are two lists of translation rules in internal form, that is pairs
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   941
of asts. They can be viewed using {\tt Syntax.print_syntax} (sections
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   942
\ttindex{parse_rules} and \ttindex{print_rules}). For {\tt SET} of
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   943
Example~\ref{ex:set_trans} these are:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   944
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   945
parse_rules:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   946
  ("{\at}Collect" x A P)  ->  ("Collect" A ("_abs" x P))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   947
  ("{\at}Replace" y x A Q)  ->  ("Replace" A ("_abs" x ("_abs" y Q)))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   948
  ("{\at}Ball" x A P)  ->  ("Ball" A ("_abs" x P))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   949
print_rules:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   950
  ("Collect" A ("_abs" x P))  ->  ("{\at}Collect" x A P)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   951
  ("Replace" A ("_abs" x ("_abs" y Q)))  ->  ("{\at}Replace" y x A Q)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   952
  ("Ball" A ("_abs" x P))  ->  ("{\at}Ball" x A P)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   953
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   954
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   955
Note that in this notation all rules are oriented left to right. In the {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   956
translations} section, which has been split into two parts, print rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   957
appeared right to left.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   958
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   959
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   960
Be careful not to choose names for variables in rules that are actually
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   961
treated as constant. If in doubt, check the rules in their internal form or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   962
the section labeled {\tt consts} in the output of {\tt Syntax.print_syntax}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   963
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   964
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   965
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   966
\subsection{Applying rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   967
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   968
In the course of parsing and printing terms, asts are generated as an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   969
intermediate form as pictured in Figure~\ref{fig:parse_print}. These asts are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   970
normalized wrt.\ the given lists of translation rules in a uniform manner. As
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   971
stated earlier, asts are supposed to be first-order `terms'. The rewriting
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   972
systems derived from {\tt translations} sections essentially resemble
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   973
traditional first-order term rewriting systems. We first examine how a single
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   974
rule is applied.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   975
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   976
Let $t$ be the ast to be normalized and $(l, r)$ some translation rule. A
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   977
subast $u$ of $t$ is called {\bf redex}\indexbold{redex (ast)} (reducible
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   978
expression), if it is an instance of $l$. In this case $l$ is said to {\bf
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   979
match}\indexbold{match (ast)} $u$. A redex matched by $l$ may be replaced by
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   980
the corresponding instance of $r$, thus {\bf rewriting}\index{rewrite (ast)}
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
   981
the ast $t$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   982
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   983
Matching requires some notion of {\bf place-holders}\indexbold{place-holder
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   984
(ast)} that may occur in rule patterns but not in ordinary asts, which are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   985
considered ground. Here we simply use {\tt Variable}s for this purpose.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   986
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   987
More formally, the matching of $u$ by $l$ is performed as follows (the rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   988
pattern is the second argument): \index{match (ast)@$match$ (ast)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   989
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   990
  \item $match(\Constant x, \Constant x) = \mbox{OK}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   991
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   992
  \item $match(\Variable x, \Constant x) = \mbox{OK}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   993
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   994
  \item $match(u, \Variable x) = \mbox{OK, bind}~x~\mbox{to}~u$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   995
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   996
  \item $match(\Appl{u@1, \ldots, u@n}, \Appl{l@1, \ldots, l@n}) = match(u@1,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   997
    l@1), \ldots, match(u@n, l@n)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   998
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   999
  \item $match(u, l) = \mbox{FAIL}$ in any other case.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1000
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1001
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1002
This means that a {\tt Constant} pattern matches any atomic asts of the same
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1003
name, while a {\tt Variable} matches any ast. If successful, $match$ yields a
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1004
substitution $\sigma$ that is applied to $r$, generating the appropriate
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1005
instance that replaces $u$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1006
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1007
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1008
In order to make things simple and fast, ast rewrite rules $(l, r)$ are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1009
restricted by the following conditions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1010
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1011
  \item Rules have to be left linear, i.e.\ $l$ must not contain any {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1012
    Variable} more than once.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1013
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1014
  \item Rules must have constant heads, i.e.\ $l = \mtt"c\mtt"$ or $l =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1015
    (\mtt"c\mtt" ~ x@1 \ldots x@n)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1016
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1017
  \item The set of variables contained in $r$ has to be a subset of those of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1018
    $l$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1019
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1020
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1021
\medskip
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1022
Having first-order matching in mind, the second case of $match$ may look a
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1023
bit odd. But this is exactly the place, where {\tt Variable}s of non-rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1024
asts behave like {\tt Constant}s. The deeper meaning of this is related with
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1025
asts being very `primitive' in some sense, ignorant of the underlying
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1026
`semantics', not far removed from parse trees. At this level it is not yet
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1027
known, which $id$s will become constants, bounds, frees, types or classes. As
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1028
$ast_of_pt$ (see \S\ref{sec:asts}) shows, former parse tree heads appear in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1029
asts as {\tt Constant}s, while $id$s, $var$s, $tfree$s and $tvar$s become
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1030
{\tt Variable}s.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1031
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1032
This is at variance with asts generated from terms before printing (see
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1033
$ast_of_term$ in \S\ref{sec:asts}), where all constants and type constructors
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1034
become {\tt Constant}s.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1035
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1036
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1037
This means asts may contain quite a messy mixture of {\tt Variable}s and {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1038
Constant}s, which is insignificant at macro level because $match$ treats them
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1039
alike.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1040
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1041
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1042
Because of this behaviour, different kinds of atoms with the same name are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1043
indistinguishable, which may make some rules prone to misbehaviour. Regard
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1044
the following fragmentary example:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1045
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1046
types
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1047
  Nil 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1048
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1049
  Nil     :: "'a list"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1050
  "[]"    :: "'a list"    ("[]")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1051
translations
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1052
  "[]"    == "Nil"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1053
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1054
Then the term {\tt Nil} will be printed as {\tt []}, just as expected. What
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1055
happens with \verb|%Nil.t| or {\tt x::Nil} is left as an exercise.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1056
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1057
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1058
\subsection{Rewriting strategy}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1059
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1060
When normalizing an ast by repeatedly applying translation rules until no
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1061
more rule is applicable, there are in each step two choices: which rule to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1062
apply next, and which redex to reduce.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1063
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1064
We could assume that the user always supplies terminating and confluent
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1065
rewriting systems, but this would often complicate things unnecessarily.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1066
Therefore, we reveal part of the actual rewriting strategy: The normalizer
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1067
always applies the first matching rule reducing an unspecified redex chosen
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1068
first.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1069
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1070
Thereby, `first rule' is roughly speaking meant wrt.\ the appearance of the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1071
rules in the {\tt translations} sections. But this is more tricky than it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1072
seems: If a given theory is {\em extended}, new rules are simply appended to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1073
the end. But if theories are {\em merged}, it is not clear which list of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1074
rules has priority over the other. In fact the merge order is left
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1075
unspecified. This shouldn't cause any problems in practice, since
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1076
translations of different theories usually do not overlap. {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1077
Syntax.print_syntax} shows the rules in their internal order.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1078
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1079
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1080
You can watch the normalization of asts during parsing and printing by
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1081
setting \ttindex{Syntax.trace_norm_ast} to {\tt true}. An alternative is the
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1082
use of \ttindex{Syntax.test_read}, which is always in trace mode. The
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1083
information displayed when tracing\index{tracing (ast)} includes: the ast
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1084
before normalization ({\tt pre}), redexes with results ({\tt rewrote}), the
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1085
normal form finally reached ({\tt post}) and some statistics ({\tt
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1086
normalize}). If tracing is off, \ttindex{Syntax.stat_norm_ast} can be set to
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1087
{\tt true} in order to enable printing of the normal form and statistics
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1088
only.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1089
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1090
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1091
\subsection{More examples}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1092
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1093
Let us first reconsider Example~\ref{ex:set_trans}, which is concerned with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1094
variable binding constructs.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1095
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1096
There is a minor disadvantage over an implementation via translation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1097
functions (as done for binders):
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1098
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1099
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1100
If \ttindex{eta_contract} is set to {\tt true}, terms will be
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1101
$\eta$-contracted {\em before\/} the ast rewriter sees them. Thus some
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1102
abstraction nodes needed for print rules to match may get lost. E.g.\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1103
\verb|Ball(A, %x. P(x))| is contracted to {\tt Ball(A, P)}, the print rule is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1104
no longer applicable and the output will be {\tt Ball(A, P)}. Note that
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1105
$\eta$-expansion via macros is {\em not\/} possible.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1106
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1107
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1108
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1109
Another common trap are meta constraints. If \ttindex{show_types} is set to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1110
{\tt true}, bound variables will be decorated by their meta types at the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1111
binding place (but not at occurrences in the body). E.g.\ matching with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1112
\verb|Collect(A, %x. P)| binds {\tt x} to something like {\tt ("_constrain" y
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1113
"i")} rather than only {\tt y}. Ast rewriting will cause the constraint to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1114
appear in the external form, say \verb|{y::i:A::i. P::o}|. Therefore your
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1115
syntax should be ready for such constraints to be re-read. This is the case
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1116
in our example, because of the category {\tt idt} of the first argument.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1117
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1118
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1119
Choosing {\tt id} instead of {\tt idt} is a very common error, especially
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1120
since it appears in former versions of most of Isabelle's object-logics.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1121
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1122
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1123
\begin{example} \label{ex:finset_trans}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1124
This example demonstrates the use of recursive macros to implement a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1125
convenient notation for finite sets.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1126
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1127
FINSET = SET +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1128
types
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1129
  is 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1130
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1131
  ""            :: "i => is"                ("_")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1132
  "{\at}Enum"       :: "[i, is] => is"          ("_,/ _")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1133
  empty         :: "i"                      ("{\ttlbrace}{\ttrbrace}")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1134
  insert        :: "[i, i] => i"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1135
  "{\at}Finset"     :: "is => i"                ("{\ttlbrace}(_){\ttrbrace}")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1136
translations
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1137
  "{\ttlbrace}x, xs{\ttrbrace}"     == "insert(x, {\ttlbrace}xs{\ttrbrace})"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1138
  "{\ttlbrace}x{\ttrbrace}"         == "insert(x, {\ttlbrace}{\ttrbrace})"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1139
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1140
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1141
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1142
Finite sets are internally built up by {\tt empty} and {\tt insert}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1143
Externally we would like to see \verb|{x, y, z}| rather than {\tt insert(x,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1144
insert(y, insert(z, empty)))}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1145
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1146
First we define the generic syntactic category {\tt is} for one or more
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1147
objects of type {\tt i} separated by commas (including breaks for pretty
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1148
printing). The category has to be declared as a 0-place type constructor, but
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1149
without {\tt arities} declaration. Hence {\tt is} is not a logical type, no
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1150
default productions will be added, and we can cook our own syntax for {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1151
is} (first two lines of {\tt consts} section). If we had needed generic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1152
enumerations of type $\alpha$ (i.e.\ {\tt logic}), we could have used the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1153
predefined category \ttindex{args} and skipped this part altogether.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1154
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1155
Next follows {\tt empty}, which is already equipped with its syntax
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1156
\verb|{}|, and {\tt insert} without concrete syntax. The syntactic constant
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1157
{\tt\at Finset} provides concrete syntax for enumerations of {\tt i} enclosed
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1158
in curly braces. Remember that a pair of parentheses specifies a block of
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1159
indentation for pretty printing. The category {\tt is} can later be reused
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1160
for other enumerations like lists or tuples.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1161
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1162
The translations may look a bit odd at first sight, but rules can only be
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1163
fully understood in their internal forms, which are:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1164
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1165
parse_rules:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1166
  ("{\at}Finset" ("{\at}Enum" x xs))  ->  ("insert" x ("{\at}Finset" xs))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1167
  ("{\at}Finset" x)  ->  ("insert" x "empty")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1168
print_rules:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1169
  ("insert" x ("{\at}Finset" xs))  ->  ("{\at}Finset" ("{\at}Enum" x xs))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1170
  ("insert" x "empty")  ->  ("{\at}Finset" x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1171
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1172
This shows that \verb|{x, xs}| indeed matches any set enumeration of at least
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1173
two elements, binding the first to {\tt x} and the rest to {\tt xs}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1174
Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration. Note that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1175
the parse rules only work in this order.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1176
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1177
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1178
Some rules are prone to misbehaviour, as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1179
\verb|%empty insert. insert(x, empty)| shows, which is printed as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1180
\verb|%empty insert. {x}|. This problem arises, because the ast rewriter
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1181
cannot discern constants, frees, bounds etc.\ and looks only for names of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1182
atoms.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1183
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1184
Thus the names of {\tt Constant}s occurring in the (internal) left-hand side
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1185
of translation rules should be regarded as `reserved keywords'. It is good
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1186
practice to choose non-identifiers here like {\tt\at Finset} or sufficiently
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1187
long and strange names.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1188
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1189
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1190
\begin{example} \label{ex:prod_trans}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1191
One of the well-formedness conditions for ast rewrite rules stated earlier
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1192
implies that you can never introduce new {\tt Variable}s on the right-hand
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1193
side. Something like \verb|"K(B)" => "%x. B"| is illegal and could cause
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1194
variable capturing, if it were allowed. In such cases you usually have to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1195
fall back on translation functions. But there is a trick that makes things
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1196
quite readable in some cases: {\em calling parse translations by parse
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1197
rules}. This is demonstrated here.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1198
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1199
PROD = FINSET +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1200
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1201
  Pi            :: "[i, i => i] => i"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1202
  "{\at}PROD"       :: "[idt, i, i] => i"     ("(3PROD _:_./ _)" 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1203
  "{\at}->"         :: "[i, i] => i"          ("(_ ->/ _)" [51, 50] 50)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1204
translations
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1205
  "PROD x:A. B" => "Pi(A, %x. B)"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1206
  "A -> B"      => "Pi(A, _K(B))"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1207
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1208
ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1209
  val print_translation = [("Pi", dependent_tr' ("{\at}PROD", "{\at}->"))];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1210
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1211
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1212
{\tt Pi} is an internal constant for constructing dependent products. Two
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1213
external forms exist: {\tt PROD x:A.B}, the general case, and {\tt A -> B},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1214
an abbreviation for \verb|Pi(A, %x.B)| with {\tt B} not actually depending on
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1215
{\tt x}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1216
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1217
Now the second parse rule is where the trick comes in: {\tt _K(B)} is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1218
introduced during ast rewriting, which later becomes \verb|%x.B| due to a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1219
parse translation associated with \ttindex{_K}. Note that a leading {\tt _}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1220
in $id$s is allowed in translation rules, but not in ordinary terms. This
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1221
special behaviour of the lexer is very useful for `forging' asts containing
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1222
names that are not directly accessible normally.
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1223
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1224
Unfortunately, there is no such trick for printing, so we have to add a {\tt
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1225
ML} section for the print translation \ttindex{dependent_tr'}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1226
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1227
The parse translation for {\tt _K} is already installed in Pure, and {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1228
dependent_tr'} is exported by the syntax module for public use. See
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1229
\S\ref{sec:tr_funs} for more of the arcane lore of translation functions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1230
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1231
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1232
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1233
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1234
\section{Translation functions *} \label{sec:tr_funs}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1235
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1236
This section is about the remaining translation mechanism which enables the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1237
designer of theories to do almost everything with terms or asts during the
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1238
parsing or printing process, by writing \ML-functions. The logic \LK\ is a
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1239
good example of a quite sophisticated use of this to transform between
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1240
internal and external representations of associative sequences. The high
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1241
level macro system described in \S\ref{sec:macros} fails here completely.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1242
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1243
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1244
A full understanding of the matters presented here requires some familiarity
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1245
with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1246
{\tt Syntax.ast} and the encodings of types and terms as such at the various
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1247
stages of the parsing or printing process. You probably do not really want to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1248
use translation functions at all!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1249
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1250
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1251
As already mentioned in \S\ref{sec:asts}, there are four kinds of translation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1252
functions. All such functions are associated with a name which specifies an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1253
ast's or term's head invoking that function. Such names can be (logical or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1254
syntactic) constants or type constructors.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1255
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1256
{\tt Syntax.print_syntax} displays the sets of names associated with the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1257
translation functions of a {\tt Syntax.syntax} under
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1258
\ttindex{parse_ast_translation}, \ttindex{parse_translation},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1259
\ttindex{print_translation} and \ttindex{print_ast_translation}. The user can
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1260
add new ones via the {\tt ML} section\index{ML section@{\tt ML} section} of a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1261
{\tt .thy} file. But there may never be more than one function of the same
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1262
kind per name.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1263
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1264
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1265
Conceptually, the {\tt ML} section should appear between {\tt consts} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1266
{\tt translations}, i.e.\ newly installed translation functions are already
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1267
effective when macros and logical rules are parsed. {\tt ML} has to be the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1268
last section because the {\tt .thy} file parser is unable to detect the end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1269
of \ML\ code in another way than by end-of-file.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1270
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1271
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1272
All text of the {\tt ML} section is simply copied verbatim into the \ML\ file
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1273
generated from a {\tt .thy} file. Definitions made here by the user become
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1274
components of a \ML\ structure of the same name as the theory to be created.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1275
Therefore local things should be declared within {\tt local}. The following
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1276
special \ML\ values, which are all optional, serve as the interface for the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1277
installation of user defined translation functions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1278
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1279
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1280
val parse_ast_translation: (string * (ast list -> ast)) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1281
val parse_translation: (string * (term list -> term)) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1282
val print_translation: (string * (term list -> term)) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1283
val print_ast_translation: (string * (ast list -> ast)) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1284
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1285
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1286
The basic idea behind all four kinds of functions is relatively simple (see
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1287
also Figure~\ref{fig:parse_print}): Whenever --- during the transformations
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1288
between parse trees, asts and terms --- a combination of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1289
$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation function $f$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1290
of appropriate kind exists for $c$, the result will be $f \mtt[ x@1, \ldots,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1291
x@n \mtt]$. Thereby, $x@1, \ldots, x@n$ (with $n \ge 0$) are asts for ast
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1292
translations and terms for term translations. A `combination' at ast level is
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1293
of the form $\Constant c$ or $\Appl{\Constant c, x@1, \ldots, x@n}$, and at
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1294
term level $\ttfct{Const} (c, \tau)$ or $\ttfct{Const} (c, \tau) \ttrel{\$}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1295
x@1 \ttrel{\$} \dots \ttrel{\$} x@n$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1296
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1297
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1298
Translation functions at ast level differ from those at term level only in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1299
the same way, as asts and terms differ. Terms, being more complex and more
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1300
specific, allow more sophisticated transformations (typically involving
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1301
abstractions and bound variables).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1302
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1303
On the other hand, {\em parse\/} (ast) translations differ from {\em print\/}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1304
(ast) translations more fundamentally:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1305
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1306
  \item[Parse (ast) translations] are applied bottom-up, i.e.\ the arguments
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1307
    supplied ($x@1, \ldots, x@n$ above) are already in translated form.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1308
    Additionally, they may not fail, exceptions are re-raised after printing
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1309
    an error message.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1310
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1311
  \item[Print (ast) translations] are applied top-down, i.e.\ supplied with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1312
    arguments that are partly still in internal form. The result is again fed
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1313
    into the translation machinery as a whole. Therefore a print (ast)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1314
    translation should not introduce as head a constant of the same name that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1315
    invoked it in the first place. Alternatively, exception \ttindex{Match}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1316
    may be raised, indicating failure of translation.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1317
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1318
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1319
Another difference between the parsing and the printing process is, which
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1320
atoms are {\tt Constant}s or {\tt Const}s, i.e.\ able to invoke translation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1321
functions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1322
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1323
For parse ast translations only former parse tree heads are {\tt Constant}s
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1324
(see also $ast_of_pt$ in \S\ref{sec:asts}). These and additionally introduced
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1325
{\tt Constant}s (e.g.\ by macros), become {\tt Const}s for parse translations
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1326
(see also $term_of_ast$ in \S\ref{sec:asts}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1327
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1328
The situation is slightly different, when terms are prepared for printing,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1329
since the role of atoms is known. Initially, all logical constants and type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1330
constructors may invoke print translations. New constants may be introduced
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1331
by these or by macros, able to invoke parse ast translations.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1332
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1333
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1334
\subsection{A simple example *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1335
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1336
Presenting a simple and useful example of translation functions is not that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1337
easy, since the macro system is sufficient for most simple applications. By
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1338
convention, translation functions always have names ending with {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1339
_ast_tr}, {\tt _tr}, {\tt _tr'} or {\tt _ast_tr'}. You may look for such
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1340
names in the sources of Pure Isabelle for more examples.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1341
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1342
\begin{example} \label{ex:tr_funs}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1343
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1344
We continue Example~\ref{ex:prod_trans} by presenting the \ML\ sources of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1345
parse translation for \ttindex{_K} and the print translation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1346
\ttindex{dependent_tr'}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1347
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1348
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1349
(* nondependent abstraction *)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1350
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1351
fun k_tr (*"_K"*) [t] = Abs ("x", dummyT, incr_boundvars 1 t)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1352
  | k_tr (*"_K"*) ts = raise_term "k_tr" ts;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1353
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1354
(* dependent / nondependent quantifiers *)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1355
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1356
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1357
      if 0 mem (loose_bnos B) then
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1358
        let val (x', B') = variant_abs (x, dummyT, B);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1359
        in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1360
        end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1361
      else list_comb (Const (r, dummyT) $ A $ B, ts)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1362
  | dependent_tr' _ _ = raise Match;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1363
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1364
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1365
This text is taken from the Pure sources, ordinary user translations would
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1366
typically appear within the {\tt ML} section of the {\tt .thy} file.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1367
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1368
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1369
If {\tt k_tr} is called with exactly one argument $t$, it creates a new {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1370
Abs} node with a body derived from $t$: loose {\tt Bound}s, i.e.\ those
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1371
referring to outer {\tt Abs}s, are incremented using
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1372
\ttindex{incr_boundvars}. This and many other basic term manipulation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1373
functions are defined in {\tt Pure/term.ML}, the comments there being in most
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1374
cases the only documentation.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1375
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1376
Since terms fed into parse translations are not yet typed, the type of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1377
bound variable in the new {\tt Abs} is simply {\tt dummyT}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1378
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1379
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1380
The argument $(q, r)$ for {\tt dependent_tr'} is supplied already during the
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1381
installation within an {\tt ML} section. This yields a parse translation that
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1382
transforms something like $c(A, \mtt{Abs}(x, T, B), t@1, \ldots, t@n)$ into
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1383
$q(x', A, B', t@1, \ldots, t@n)$ or $r(A, B, t@1, \ldots, t@n)$. The latter
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1384
form, if $B$ does not actually depend on $x$. This is checked using
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1385
\ttindex{loose_bnos}, yet another function of {\tt Pure/term.ML}. Note that
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1386
$x'$ is a version of $x$ renamed away from all names in $B$, and $B'$ the
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1387
body $B$ with {\tt Bound}s referring to our {\tt Abs} node replaced by
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1388
$\ttfct{Free} (x', \mtt{dummyT})$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1389
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1390
We have to be more careful with types here. While types of {\tt Const}s are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1391
completely ignored, type constraints may be printed for some {\tt Free}s and
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1392
{\tt Var}s (if \ttindex{show_types} is set to {\tt true}). Variables of type
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1393
\ttindex{dummyT} are never printed with constraint, though. Thus, a
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1394
constraint of $x'$ may only appear at its binding place, since {\tt Free}s of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1395
$B'$ replacing the appropriate {\tt Bound}s of $B$ via \ttindex{variant_abs}
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1396
have all type {\tt dummyT}. \end{example}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1397
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1398
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1399
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1400
\section{Example: some minimal logics} \label{sec:min_logics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1401
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1402
This concluding section presents some examples that are very simple from a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1403
syntactic point of view. They should rather demonstrate how to define new
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1404
object-logics from scratch. In particular we need to say how an object-logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1405
syntax is hooked up to the meta-logic. Since all theorems must conform to the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1406
syntax for $prop$ (see Figure~\ref{fig:pure_gram}), that syntax has to be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1407
extended with the object-level syntax. Assume that the syntax of your
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1408
object-logic defines a category $o$ of formulae. These formulae can now
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1409
appear in axioms and theorems wherever $prop$ does if you add the production
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1410
\[ prop ~=~ o. \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1411
More precisely, you need a coercion from formulae to propositions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1412
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1413
Base = Pure +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1414
types
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1415
  o 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1416
arities
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1417
  o :: logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1418
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1419
  Trueprop :: "o => prop"   ("_" 5)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1420
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1421
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1422
The constant {\tt Trueprop} (the name is arbitrary) acts as an invisible
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1423
coercion function. Assuming this definition resides in a file {\tt base.thy},
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
  1424
you have to load it with the command {\tt use_thy "Base"}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1425
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1426
One of the simplest nontrivial logics is {\em minimal logic\/} of
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1427
implication. Its definition in Isabelle needs no advanced features but
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1428
illustrates the overall mechanism quite nicely:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1429
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1430
Hilbert = Base +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1431
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1432
  "-->" :: "[o, o] => o"   (infixr 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1433
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1434
  K     "P --> Q --> P"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1435
  S     "(P --> Q --> R) --> (P --> Q) --> P --> R"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1436
  MP    "[| P --> Q; P |] ==> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1437
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1438
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1439
After loading this definition you can start to prove theorems in this logic:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1440
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1441
goal Hilbert.thy "P --> P";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1442
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1443
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1444
{\out  1.  P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1445
by (resolve_tac [Hilbert.MP] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1446
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1447
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1448
{\out  1.  ?P --> P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1449
{\out  2.  ?P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1450
by (resolve_tac [Hilbert.MP] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1451
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1452
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1453
{\out  1.  ?P1 --> ?P --> P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1454
{\out  2.  ?P1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1455
{\out  3.  ?P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1456
by (resolve_tac [Hilbert.S] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1457
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1458
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1459
{\out  1.  P --> ?Q2 --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1460
{\out  2.  P --> ?Q2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1461
by (resolve_tac [Hilbert.K] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1462
{\out Level 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1463
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1464
{\out  1.  P --> ?Q2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1465
by (resolve_tac [Hilbert.K] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1466
{\out Level 5}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1467
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1468
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1469
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1470
As you can see, this Hilbert-style formulation of minimal logic is easy to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1471
define but difficult to use. The following natural deduction formulation is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1472
far preferable:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1473
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1474
MinI = Base +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1475
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1476
  "-->" :: "[o, o] => o"   (infixr 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1477
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1478
  impI  "(P ==> Q) ==> P --> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1479
  impE  "[| P --> Q; P |] ==> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1480
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1481
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1482
Note, however, that although the two systems are equivalent, this fact cannot
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1483
be proved within Isabelle: {\tt S} and {\tt K} can be derived in {\tt MinI}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1484
(exercise!), but {\tt impI} cannot be derived in {\tt Hilbert}. The reason is
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1485
that {\tt impI} is only an {\em admissible\/} rule in {\tt Hilbert},
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1486
something that can only be shown by induction over all possible proofs in
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
  1487
{\tt Hilbert}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1488
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1489
It is a very simple matter to extend minimal logic with falsity:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1490
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1491
MinIF = MinI +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1492
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1493
  False :: "o"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1494
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1495
  FalseE "False ==> P"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1496
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1497
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1498
On the other hand, we may wish to introduce conjunction only:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1499
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1500
MinC = Base +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1501
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1502
  "&" :: "[o, o] => o"   (infixr 30)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1503
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1504
  conjI  "[| P; Q |] ==> P & Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1505
  conjE1 "P & Q ==> P"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1506
  conjE2 "P & Q ==> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1507
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1508
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1509
And if we want to have all three connectives together, we define:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1510
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1511
MinIFC = MinIF + MinC
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1512
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1513
Now we can prove mixed theorems like
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1514
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1515
goal MinIFC.thy "P & False --> Q";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1516
by (resolve_tac [MinI.impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1517
by (dresolve_tac [MinC.conjE2] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1518
by (eresolve_tac [MinIF.FalseE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1519
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1520
Try this as an exercise!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1521