doc-src/Logics/defining.tex
author wenzelm
Sat, 01 Jul 2000 19:49:20 +0200
changeset 9226 cbe6144f0f15
parent 291 a615050a7494
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
     2
%%  \([a-zA-Z][a-zA-Z]}\.\) \([^ ]\)             \1  \2
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
     3
%%  @\([a-z0-9]\)       ^{(\1)}
108
e332c5bf9e1f replaced by current version;
wenzelm
parents: 104
diff changeset
     4
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
     5
\newcommand\rmindex[1]{{#1}\index{#1}\@}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
     6
\newcommand\mtt[1]{\mbox{\tt #1}}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
     7
\newcommand\ttfct[1]{\mathop{\mtt{#1}}\nolimits}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
     8
\newcommand\ttapp{\mathrel{\hbox{\tt\$}}}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
     9
\newcommand\Constant{\ttfct{Constant}}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    10
\newcommand\Variable{\ttfct{Variable}}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    11
\newcommand\Appl[1]{\ttfct{Appl}\mathopen{\mtt[}#1\mathclose{\mtt]}}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    12
\newcommand\AST{{\sc ast}}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    13
\let\rew=\longrightarrow
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
\chapter{Defining Logics} \label{Defining-Logics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    18
This chapter explains how to define new formal systems --- in particular,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    19
their concrete syntax.  While Isabelle can be regarded as a theorem prover
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    20
for set theory, higher-order logic or the sequent calculus, its
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    21
distinguishing feature is support for the definition of new logics.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    23
Isabelle logics are hierarchies of theories, which are described and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    24
illustrated in {\em Introduction to Isabelle}.  That material, together
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    25
with the theory files provided in the examples directories, should suffice
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    26
for all simple applications.  The easiest way to define a new theory is by
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    27
modifying a copy of an existing theory.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    28
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    29
This chapter is intended for experienced Isabelle users.  It documents all
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    30
aspects of theories concerned with syntax: mixfix declarations, pretty
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    31
printing, macros and translation functions.  The extended examples of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    32
\S\ref{sec:min_logics} demonstrate the logical aspects of the definition of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    33
theories.  Sections marked with * are highly technical and might be skipped
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    34
on the first reading.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    37
\section{Priority grammars} \label{sec:priority_grammars}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    38
\index{grammars!priority|(} 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    40
The syntax of an Isabelle logic is specified by a {\bf priority grammar}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    41
A context-free grammar\index{grammars!context-free} contains a set of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    42
productions of the form $A=\gamma$, where $A$ is a nonterminal and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    43
$\gamma$, the right-hand side, is a string of terminals and nonterminals.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    44
Isabelle uses an extended format permitting {\bf priorities}, or
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    45
precedences.  Each nonterminal is decorated by an integer priority, as
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    46
in~$A^{(p)}$.  A nonterminal $A^{(p)}$ in a derivation may be replaced
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    47
using a production $A^{(q)} = \gamma$ only if $p \le q$.  Any priority
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    48
grammar can be translated into a normal context free grammar by introducing
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    49
new nonterminals and productions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
Formally, a set of context free productions $G$ induces a derivation
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    52
relation $\rew@G$.  Let $\alpha$ and $\beta$ denote strings of terminal or
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    53
nonterminal symbols.  Then
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    54
\[ \alpha\, A^{(p)}\, \beta ~\rew@G~ \alpha\,\gamma\,\beta \] 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    55
if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$q\ge p$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
The following simple grammar for arithmetic expressions demonstrates how
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    58
binding power and associativity of operators can be enforced by priorities.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
\begin{tabular}{rclr}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    61
  $A^{(9)}$ & = & {\tt0} \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    62
  $A^{(9)}$ & = & {\tt(} $A^{(0)}$ {\tt)} \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    63
  $A^{(0)}$ & = & $A^{(0)}$ {\tt+} $A^{(1)}$ \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    64
  $A^{(2)}$ & = & $A^{(3)}$ {\tt*} $A^{(2)}$ \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    65
  $A^{(3)}$ & = & {\tt-} $A^{(3)}$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
\end{center}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    68
The choice of priorities determines that {\tt -} binds tighter than {\tt *},
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    69
which binds tighter than {\tt +}.  Furthermore {\tt +} associates to the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    70
left and {\tt *} to the right.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
To minimize the number of subscripts, we adopt the following conventions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
\begin{itemize}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    74
\item All priorities $p$ must be in the range $0 \leq p \leq max_pri$ for
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    75
  some fixed integer $max_pri$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    76
\item Priority $0$ on the right-hand side and priority $max_pri$ on the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
  left-hand side may be omitted.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
\end{itemize}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    79
The production $A^{(p)} = \alpha$ is written as $A = \alpha~(p)$;
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    80
the priority of the left-hand side actually appears in a column on the far
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    81
right.  Finally, alternatives may be separated by $|$, and repetition
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
indicated by \dots.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    84
Using these conventions and assuming $max_pri=9$, the grammar takes the form
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
\begin{tabular}{rclc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
$A$ & = & {\tt0} & \hspace*{4em} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
 & $|$ & {\tt(} $A$ {\tt)} \\
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    89
 & $|$ & $A$ {\tt+} $A^{(1)}$ & (0) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    90
 & $|$ & $A^{(3)}$ {\tt*} $A^{(2)}$ & (2) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    91
 & $|$ & {\tt-} $A^{(3)}$ & (3)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
\end{center}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    94
\index{grammars!priority|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
    97
\begin{figure}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
\begin{tabular}{rclc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
$prop$ &=& \ttindex{PROP} $aprop$ ~~$|$~~ {\tt(} $prop$ {\tt)} \\
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   101
     &$|$& $logic^{(3)}$ \ttindex{==} $logic^{(2)}$ & (2) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   102
     &$|$& $logic^{(3)}$ \ttindex{=?=} $logic^{(2)}$ & (2) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   103
     &$|$& $prop^{(2)}$ \ttindex{==>} $prop^{(1)}$ & (1) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   104
     &$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop^{(1)}$ & (1) \\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
     &$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
$logic$ &=& $prop$ ~~$|$~~ $fun$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
$aprop$ &=& $id$ ~~$|$~~ $var$
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   108
    ~~$|$~~ $fun^{(max_pri)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
$fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   110
    &$|$& $fun^{(max_pri)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   111
    &$|$& $fun^{(max_pri)}$ {\tt::} $type$ \\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
    &$|$& \ttindex{\%} $idts$ {\tt.} $logic$ & (0) \\\\
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   113
$idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
    &$|$& $id$ \ttindex{::} $type$ & (0) \\\\
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   116
$type$ &=& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   117
  ~~$|$~~ $tvar$ {\tt::} $sort$ \\
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   118
     &$|$& $id$ ~~$|$~~ $type^{(max_pri)}$ $id$
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
                ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   120
     &$|$& $type^{(1)}$ \ttindex{=>} $type$ & (0) \\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
     &$|$& {\tt[}  $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0)\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
     &$|$& {\tt(} $type$ {\tt)} \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
$sort$ &=& $id$ ~~$|$~~ {\tt\ttlbrace\ttrbrace}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
                ~~$|$~~ {\tt\ttlbrace} $id$ {\tt,} \dots {\tt,} $id$ {\tt\ttrbrace}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
\end{tabular}\index{*"!"!}\index{*"["|}\index{*"|"]}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
\indexbold{type@$type$} \indexbold{sort@$sort$} \indexbold{idt@$idt$}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
\indexbold{idts@$idts$} \indexbold{logic@$logic$} \indexbold{prop@$prop$}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
\indexbold{fun@$fun$}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
\end{center}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   130
\caption{Meta-logic syntax}\label{fig:pure_gram}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   133
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   134
\section{The Pure syntax} \label{sec:basic_syntax}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   135
\index{syntax!Pure|(}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   137
At the root of all object-logics lies the Pure theory,\index{theory!Pure}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   138
bound to the \ML{} identifier \ttindex{Pure.thy}.  It contains, among many
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   139
other things, the Pure syntax. An informal account of this basic syntax
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   140
(meta-logic, types, \ldots) may be found in {\em Introduction to Isabelle}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   141
A more precise description using a priority grammar is shown in
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   142
Fig.\ts\ref{fig:pure_gram}.  The following nonterminals are defined:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   143
\begin{description}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   144
  \item[$prop$] Terms of type $prop$.  These are formulae of the meta-logic.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   146
  \item[$aprop$] Atomic propositions.  These typically include the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   147
    judgement forms of the object-logic; its definition introduces a
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   148
    meta-level predicate for each judgement form.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   149
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   150
  \item[$logic$] Terms whose type belongs to class $logic$.  Initially,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   151
    this category contains just $prop$.  As the syntax is extended by new
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   152
    object-logics, more productions for $logic$ are added automatically
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   153
    (see below).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
  \item[$fun$] Terms potentially of function type.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   157
  \item[$type$] Types of the meta-logic.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   159
  \item[$idts$] A list of identifiers, possibly constrained by types.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   162
\begin{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   163
  Note that \verb|x::nat y| is parsed as \verb|x::(nat y)|, treating {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   164
    y} like a type constructor applied to {\tt nat}.  The likely result is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   165
  an error message.  To avoid this interpretation, use parentheses and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   166
  write \verb|(x::nat) y|.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   168
  Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   169
  yields a syntax error.  The correct form is \verb|(x::nat) (y::nat)|.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   170
\end{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   171
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   172
\subsection{Logical types and default syntax}\label{logical-types}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   173
Isabelle's representation of mathematical languages is based on the typed
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   174
$\lambda$-calculus.  All logical types, namely those of class $logic$, are
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   175
automatically equipped with a basic syntax of types, identifiers,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   176
variables, parentheses, $\lambda$-abstractions and applications.  
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   177
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   178
More precisely, for each type constructor $ty$ with arity $(\vec{s})c$,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   179
where $c$ is a subclass of $logic$, several productions are added:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
\begin{tabular}{rclc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
$ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   183
  &$|$& $fun^{(max_pri)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   184
  &$|$& $ty^{(max_pri)}$ {\tt::} $type$\\\\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
$logic$ &=& $ty$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   190
\subsection{Lexical matters}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   191
The parser does not process input strings directly.  It operates on token
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   192
lists provided by Isabelle's \bfindex{lexer}.  There are two kinds of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   193
tokens: \bfindex{delimiters} and \bfindex{name tokens}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   195
Delimiters can be regarded as reserved words of the syntax.  You can
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   196
add new ones when extending theories.  In Fig.\ts\ref{fig:pure_gram} they
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   197
appear in typewriter font, for example {\tt ==}, {\tt =?=} and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   198
{\tt PROP}\@.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   200
Name tokens have a predefined syntax.  The lexer distinguishes four
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   201
disjoint classes of names: \rmindex{identifiers}, \rmindex{unknowns}, type
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   202
identifiers\index{identifiers!type}, type unknowns\index{unknowns!type}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   203
They are denoted by $id$\index{id@$id$}, $var$\index{var@$var$},
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   204
$tid$\index{tid@$tid$}, $tvar$\index{tvar@$tvar$}, respectively.  Typical
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   205
examples are {\tt x}, {\tt ?x7}, {\tt 'a}, {\tt ?'a3}.  Here is the precise
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   206
syntax:
188
6be0856cdf49 last minute changes, eg literal tokens -> delimiters and valued tokens ->
nipkow
parents: 142
diff changeset
   207
\begin{eqnarray*}
6be0856cdf49 last minute changes, eg literal tokens -> delimiters and valued tokens ->
nipkow
parents: 142
diff changeset
   208
id        & =   & letter~quasiletter^* \\
6be0856cdf49 last minute changes, eg literal tokens -> delimiters and valued tokens ->
nipkow
parents: 142
diff changeset
   209
var       & =   & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   210
tid     & =   & \mbox{\tt '}id \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   211
tvar      & =   & \mbox{\tt ?}tid ~~|~~
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   212
                  \mbox{\tt ?}tid\mbox{\tt .}nat \\[1ex]
188
6be0856cdf49 last minute changes, eg literal tokens -> delimiters and valued tokens ->
nipkow
parents: 142
diff changeset
   213
letter    & =   & \mbox{one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z}} \\
6be0856cdf49 last minute changes, eg literal tokens -> delimiters and valued tokens ->
nipkow
parents: 142
diff changeset
   214
digit     & =   & \mbox{one of {\tt 0}\dots {\tt 9}} \\
6be0856cdf49 last minute changes, eg literal tokens -> delimiters and valued tokens ->
nipkow
parents: 142
diff changeset
   215
quasiletter & =  & letter ~~|~~ digit ~~|~~ \mbox{\tt _} ~~|~~ \mbox{\tt '} \\
6be0856cdf49 last minute changes, eg literal tokens -> delimiters and valued tokens ->
nipkow
parents: 142
diff changeset
   216
nat       & =   & digit^+
6be0856cdf49 last minute changes, eg literal tokens -> delimiters and valued tokens ->
nipkow
parents: 142
diff changeset
   217
\end{eqnarray*}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   218
A $var$ or $tvar$ describes an unknown, which is internally a pair
188
6be0856cdf49 last minute changes, eg literal tokens -> delimiters and valued tokens ->
nipkow
parents: 142
diff changeset
   219
of base name and index (\ML\ type \ttindex{indexname}).  These components are
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   220
either separated by a dot as in {\tt ?x.1} or {\tt ?x7.3} or
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   221
run together as in {\tt ?x1}.  The latter form is possible if the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   222
base name does not end with digits.  If the index is 0, it may be dropped
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   223
altogether: {\tt ?x} abbreviates both {\tt ?x0} and {\tt ?x.0}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   225
The lexer repeatedly takes the maximal prefix of the input string that
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   226
forms a valid token.  A maximal prefix that is both a delimiter and a name
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   227
is treated as a delimiter.  Spaces, tabs and newlines are separators; they
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   228
never occur within tokens.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   230
Delimiters need not be separated by white space.  For example, if {\tt -}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   231
is a delimiter but {\tt --} is not, then the string {\tt --} is treated as
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   232
two consecutive occurrences of the token~{\tt -}.  In contrast, \ML\ 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   233
treats {\tt --} as a single symbolic name.  The consequence of Isabelle's
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   234
more liberal scheme is that the same string may be parsed in different ways
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   235
after extending the syntax: after adding {\tt --} as a delimiter, the input
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   236
{\tt --} is treated as a single token.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   238
Name tokens are terminal symbols, strictly speaking, but we can generally
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   239
regard them as nonterminals.  This is because a name token carries with it
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   240
useful information, the name.  Delimiters, on the other hand, are nothing
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   241
but than syntactic sugar.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   244
\subsection{*Inspecting the syntax}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
\begin{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   246
syn_of              : theory -> Syntax.syntax
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   247
Syntax.print_syntax : Syntax.syntax -> unit
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   248
Syntax.print_gram   : Syntax.syntax -> unit
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   249
Syntax.print_trans  : Syntax.syntax -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
\end{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   251
The abstract type \ttindex{Syntax.syntax} allows manipulation of syntaxes
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   252
in \ML.  You can display values of this type by calling the following
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   253
functions:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   254
\begin{description}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   255
\item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   256
  theory~{\it thy} as an \ML\ value.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   257
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   258
\item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   259
  information contained in the syntax {\it syn}.  The displayed output can
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   260
  be large.  The following two functions are more selective.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   262
\item[\ttindexbold{Syntax.print_gram} {\it syn}] shows the grammar part
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   263
  of~{\it syn}, namely the lexicon, roots and productions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   265
\item[\ttindexbold{Syntax.print_trans} {\it syn}] shows the translation
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   266
  part of~{\it syn}, namely the constants, parse/print macros and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   267
  parse/print translations.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   268
\end{description}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   269
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   270
Let us demonstrate these functions by inspecting Pure's syntax.  Even that
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   271
is too verbose to display in full.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
Syntax.print_syntax (syn_of Pure.thy);
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   274
{\out lexicon: "!!" "\%" "(" ")" "," "." "::" ";" "==" "==>" \dots}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
{\out roots: logic type fun prop}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
{\out prods:}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   277
{\out   type = tid  (1000)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
{\out   type = tvar  (1000)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
{\out   type = id  (1000)}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   280
{\out   type = tid "::" sort[0]  => "_ofsort" (1000)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
{\out   type = tvar "::" sort[0]  => "_ofsort" (1000)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
{\out   \vdots}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   283
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
{\out consts: "_K" "_appl" "_aprop" "_args" "_asms" "_bigimpl" \dots}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
{\out parse_ast_translation: "_appl" "_bigimpl" "_bracket"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
{\out   "_idtyp" "_lambda" "_tapp" "_tappl"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
{\out parse_rules:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
{\out parse_translation: "!!" "_K" "_abs" "_aprop"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
{\out print_translation: "all"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
{\out print_rules:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
{\out print_ast_translation: "==>" "_abs" "_idts" "fun"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   294
As you can see, the output is divided into labeled sections.  The grammar
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   295
is represented by {\tt lexicon}, {\tt roots} and {\tt prods}.  The rest
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   296
refers to syntactic translations and macro expansion.  Here is an
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   297
explanation of the various sections.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
\begin{description}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   299
  \item[\ttindex{lexicon}] lists the delimiters used for lexical
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   300
    analysis.\index{delimiters} 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   302
  \item[\ttindex{roots}] lists the grammar's nonterminal symbols.  You must
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   303
    name the desired root when calling lower level functions or specifying
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   304
    macros.  Higher level functions usually expect a type and derive the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   305
    actual root as described in~\S\ref{sec:grammar}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   307
  \item[\ttindex{prods}] lists the productions of the priority grammar.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   308
    The nonterminal $A^{(n)}$ is rendered in {\sc ascii} as {\tt $A$[$n$]}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   309
    Each delimiter is quoted.  Some productions are shown with {\tt =>} and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   310
    an attached string.  These strings later become the heads of parse
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   311
    trees; they also play a vital role when terms are printed (see
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   312
    \S\ref{sec:asts}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   314
    Productions with no strings attached are called {\bf copy
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   315
      productions}\indexbold{productions!copy}.  Their right-hand side must
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   316
    have exactly one nonterminal symbol (or name token).  The parser does
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   317
    not create a new parse tree node for copy productions, but simply
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   318
    returns the parse tree of the right-hand symbol.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   320
    If the right-hand side consists of a single nonterminal with no
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   321
    delimiters, then the copy production is called a {\bf chain
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   322
      production}\indexbold{productions!chain}.  Chain productions should
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   323
    be seen as abbreviations: conceptually, they are removed from the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   324
    grammar by adding new productions.  Priority information
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   325
    attached to chain productions is ignored, only the dummy value $-1$ is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   326
    displayed.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
  \item[\ttindex{consts}, \ttindex{parse_rules}, \ttindex{print_rules}]
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   329
    relate to macros (see \S\ref{sec:macros}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   331
  \item[\ttindex{parse_ast_translation}, \ttindex{print_ast_translation}]
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   332
    list sets of constants that invoke translation functions for abstract
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   333
    syntax trees.  Section \S\ref{sec:asts} below discusses this obscure
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   334
    matter. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   336
  \item[\ttindex{parse_translation}, \ttindex{print_translation}] list sets
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   337
    of constants that invoke translation functions for terms (see
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   338
    \S\ref{sec:tr_funs}).
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   339
\end{description}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   340
\index{syntax!Pure|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
\section{Mixfix declarations} \label{sec:mixfix}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   344
\index{mixfix declaration|(} 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   346
When defining a theory, you declare new constants by giving their names,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   347
their type, and an optional {\bf mixfix annotation}.  Mixfix annotations
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   348
allow you to extend Isabelle's basic $\lambda$-calculus syntax with
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   349
readable notation.  They can express any context-free priority grammar.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   350
Isabelle syntax definitions are inspired by \OBJ~\cite{OBJ}; they are more
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   351
general than the priority declarations of \ML\ and Prolog.  
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   352
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   353
A mixfix annotation defines a production of the priority grammar.  It
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   354
describes the concrete syntax, the translation to abstract syntax, and the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   355
pretty printing.  Special case annotations provide a simple means of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   356
specifying infix operators, binders and so forth.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   358
\subsection{Grammar productions}\label{sec:grammar}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   359
Let us examine the treatment of the production
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   360
\[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\, A@2^{(p@2)}\, \ldots\,  
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   361
                  A@n^{(p@n)}\, w@n. \]
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   362
Here $A@i^{(p@i)}$ is a nonterminal with priority~$p@i$ for $i=1$,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   363
\ldots,~$n$, while $w@0$, \ldots,~$w@n$ are strings of terminals.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   364
In the corresponding mixfix annotation, the priorities are given separately
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   365
as $[p@1,\ldots,p@n]$ and~$p$.  The nonterminal symbols are identified with
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   366
types~$\tau$, $\tau@1$, \ldots,~$\tau@n$ respectively, and the production's
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   367
effect on nonterminals is expressed as the function type
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   368
\[ [\tau@1, \ldots, \tau@n]\To \tau. \]
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   369
Finally, the template
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   370
\[ w@0  \;_\; w@1 \;_\; \ldots \;_\; w@n \]
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   371
describes the strings of terminals.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   373
A simple type is typically declared for each nonterminal symbol.  In
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   374
first-order logic, type~$i$ stands for terms and~$o$ for formulae.  Only
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   375
the outermost type constructor is taken into account.  For example, any
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   376
type of the form $\sigma list$ stands for a list;  productions may refer
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   377
to the symbol {\tt list} and will apply lists of any type.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   378
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   379
The symbol associated with a type is called its {\bf root} since it may
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   380
serve as the root of a parse tree.  Precisely, the root of $(\tau@1, \dots,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   381
\tau@n)ty$ is $ty$, where $\tau@1$, \ldots, $\tau@n$ are types and $ty$ is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   382
a type constructor.  Type infixes are a special case of this; in
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   383
particular, the root of $\tau@1 \To \tau@2$ is {\tt fun}.  Finally, the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   384
root of a type variable is {\tt logic}; general productions might
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   385
refer to this nonterminal.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   387
Identifying nonterminals with types allows a constant's type to specify
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   388
syntax as well.  We can declare the function~$f$ to have type $[\tau@1,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   389
\ldots, \tau@n]\To \tau$ and, through a mixfix annotation, specify the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   390
layout of the function's $n$ arguments.  The constant's name, in this
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   391
case~$f$, will also serve as the label in the abstract syntax tree.  There
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   392
are two exceptions to this treatment of constants:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   393
\begin{enumerate}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   394
  \item A production need not map directly to a logical function.  In this
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   395
    case, you must declare a constant whose purpose is purely syntactic.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   396
    By convention such constants begin with the symbol~{\tt\at}, 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   397
    ensuring that they can never be written in formulae.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   398
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   399
  \item A copy production has no associated constant.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   400
\end{enumerate}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   401
There is something artificial about this representation of productions,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   402
but it is convenient, particularly for simple theory extensions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   404
\subsection{The general mixfix form}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   405
Here is a detailed account of the general \bfindex{mixfix declaration} as
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   406
it may occur within the {\tt consts} section of a {\tt .thy} file.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   407
\begin{center}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   408
  {\tt "$c$" ::\ "$\sigma$" ("$template$" $ps$ $p$)}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   409
\end{center}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   410
This constant declaration and mixfix annotation is interpreted as follows:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   411
\begin{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   412
\item The string {\tt "$c$"} is the name of the constant associated with
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   413
  the production.  If $c$ is empty (given as~{\tt ""}) then this is a copy
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   414
  production.\index{productions!copy} Otherwise, parsing an instance of the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   415
  phrase $template$ generates the \AST{} {\tt ("$c$" $a@1$ $\ldots$
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   416
    $a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   417
  argument.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   418
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   419
  \item The constant $c$, if non-empty, is declared to have type $\sigma$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   421
  \item The string $template$ specifies the right-hand side of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   422
    the production.  It has the form
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   423
    \[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n, \] 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   424
    where each occurrence of \ttindex{_} denotes an
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   425
    argument\index{argument!mixfix} position and the~$w@i$ do not
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   426
    contain~{\tt _}.  (If you want a literal~{\tt _} in the concrete
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   427
    syntax, you must escape it as described below.)  The $w@i$ may
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   428
    consist of \rmindex{delimiters}, spaces or \rmindex{pretty
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   429
      printing} annotations (see below).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   431
  \item The type $\sigma$ specifies the production's nonterminal symbols (or name
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   432
    tokens).  If $template$ is of the form above then $\sigma$ must be a
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   433
    function type with at least~$n$ argument positions, say $\sigma =
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   434
    [\tau@1, \dots, \tau@n] \To \tau$.  Nonterminal symbols are derived
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   435
    from the type $\tau@1$, \ldots,~$\tau@n$, $\tau$ as described above.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   436
    Any of these may be function types; the corresponding root is then {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   437
      fun}. 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   439
  \item The optional list~$ps$ may contain at most $n$ integers, say {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   440
      [$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   441
    priority\indexbold{priorities} required of any phrase that may appear
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   442
    as the $i$-th argument.  Missing priorities default to~$0$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   443
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   444
  \item The integer $p$ is the priority of this production.  If omitted, it
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   445
    defaults to the maximal priority.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   446
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   447
    Priorities, or precedences, range between $0$ and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   448
    $max_pri$\indexbold{max_pri@$max_pri$} (= 1000).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   451
The declaration {\tt $c$ ::\ "$\sigma$" ("$template$")} specifies no
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   452
priorities.  The resulting production puts no priority constraints on any
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   453
of its arguments and has maximal priority itself.  Omitting priorities in
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   454
this manner will introduce syntactic ambiguities unless the production's
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   455
right-hand side is fully bracketed, as in \verb|"if _ then _ else _ fi"|.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   457
\begin{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   458
  Theories must sometimes declare types for purely syntactic purposes.  One
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   459
  example is {\tt type}, the built-in type of types.  This is a `type of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   460
  all types' in the syntactic sense only.  Do not declare such types under
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   461
  {\tt arities} as belonging to class $logic$, for that would allow their
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   462
  use in arbitrary Isabelle expressions~(\S\ref{logical-types}).
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   463
\end{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   464
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   465
\subsection{Example: arithmetic expressions}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   466
This theory specification contains a {\tt consts} section with mixfix
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   467
declarations encoding the priority grammar from
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   468
\S\ref{sec:priority_grammars}:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
EXP = Pure +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
types
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   472
  exp
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
arities
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
  exp :: logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
consts
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   476
  "0" :: "exp"                ("0"      9)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   477
  "+" :: "[exp, exp] => exp"  ("_ + _"  [0, 1] 0)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   478
  "*" :: "[exp, exp] => exp"  ("_ * _"  [3, 2] 2)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   479
  "-" :: "exp => exp"         ("- _"    [3] 3)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
Note that the {\tt arities} declaration causes {\tt exp} to be added to the
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   483
syntax' roots.  If you put the text above into a file {\tt exp.thy} and load
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   484
it via {\tt use_thy "EXP"}, you can run some tests:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
val read_exp = Syntax.test_read (syn_of EXP.thy) "exp";
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   487
{\out val it = fn : string -> unit}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
{\out tokens: "0" "*" "0" "*" "0" "*" "0" "+" "0" "+" "0" "+" "0"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
{\out raw: ("+" ("+" ("+" ("*" "0" ("*" "0" ("*" "0" "0"))) "0") "0") "0")}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
{\out \vdots}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
read_exp "0 + - 0 + 0";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
{\out tokens: "0" "+" "-" "0" "+" "0"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
{\out raw: ("+" ("+" "0" ("-" "0")) "0")}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
{\out \vdots}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
The output of \ttindex{Syntax.test_read} includes the token list ({\tt
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   498
  tokens}) and the raw \AST{} directly derived from the parse tree,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   499
ignoring parse \AST{} translations.  The rest is tracing information
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   500
provided by the macro expander (see \S\ref{sec:macros}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   502
Executing {\tt Syntax.print_gram} reveals the productions derived
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   503
from our mixfix declarations (lots of additional information deleted):
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
\begin{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   505
Syntax.print_gram (syn_of EXP.thy);
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   506
{\out exp = "0"  => "0" (9)}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   507
{\out exp = exp[0] "+" exp[1]  => "+" (0)}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   508
{\out exp = exp[3] "*" exp[2]  => "*" (2)}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   509
{\out exp = "-" exp[3]  => "-" (3)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   512
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   513
\subsection{The mixfix template}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   514
Let us take a closer look at the string $template$ appearing in mixfix
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   515
annotations.  This string specifies a list of parsing and printing
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   516
directives: delimiters\index{delimiter}, arguments\index{argument!mixfix},
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   517
spaces, blocks of indentation and line breaks.  These are encoded via the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
following character sequences:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   520
\index{pretty printing|(}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
\begin{description}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   522
  \item[~\ttindex_~] An argument\index{argument!mixfix} position, which
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   523
    stands for a nonterminal symbol or name token.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   525
  \item[~$d$~] A \rmindex{delimiter}, namely a non-empty sequence of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   526
    non-special or escaped characters.  Escaping a character\index{escape
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   527
      character} means preceding it with a {\tt '} (single quote).  Thus
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   528
    you have to write {\tt ''} if you really want a single quote.  You must
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   529
    also escape {\tt _}, {\tt (}, {\tt )} and {\tt /}.  Delimiters may
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   530
    never contain white space, though.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   532
  \item[~$s$~] A non-empty sequence of spaces for printing.  This
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   533
    and the following specifications do not affect parsing at all.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   535
  \item[~{\ttindex($n$}~] Open a pretty printing block.  The optional
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   536
    number $n$ specifies how much indentation to add when a line break
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   537
    occurs within the block.  If {\tt(} is not followed by digits, the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   538
    indentation defaults to~$0$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   540
  \item[~\ttindex)~] Close a pretty printing block.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   542
  \item[~\ttindex{//}~] Force a line break.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   544
  \item[~\ttindex/$s$~] Allow a line break.  Here $s$ stands for the string
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   545
    of spaces (zero or more) right after the {\tt /} character.  These
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   546
    spaces are printed if the break is not taken.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   547
\end{description}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   548
Isabelle's pretty printer resembles the one described in
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   549
Paulson~\cite{paulson91}.  \index{pretty printing|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   552
\subsection{Infixes}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   553
\indexbold{infix operators}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   554
Infix operators associating to the left or right can be declared
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   555
using {\tt infixl} or {\tt infixr}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   556
Roughly speaking, the form {\tt $c$ ::\ "$\sigma$" (infixl $p$)}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   557
abbreviates the declarations
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
\begin{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   559
"op \(c\)" :: "\(\sigma\)"   ("op \(c\)")
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   560
"op \(c\)" :: "\(\sigma\)"   ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
\end{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   562
and {\tt $c$ ::\ "$\sigma$" (infixr $p$)} abbreviates the declarations
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
\begin{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   564
"op \(c\)" :: "\(\sigma\)"   ("op \(c\)")
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   565
"op \(c\)" :: "\(\sigma\)"   ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
\end{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   567
The infix operator is declared as a constant with the prefix {\tt op}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
Thus, prefixing infixes with \ttindex{op} makes them behave like ordinary
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   569
function symbols, as in \ML.  Special characters occurring in~$c$ must be
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   570
escaped, as in delimiters, using a single quote.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   571
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   572
The expanded forms above would be actually illegal in a {\tt .thy} file
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   573
because they declare the constant \hbox{\tt"op \(c\)"} twice.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   575
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
\subsection{Binders}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   577
\indexbold{binders}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   578
\begingroup
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   579
\def\Q{{\cal Q}}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   580
A {\bf binder} is a variable-binding construct such as a quantifier.  The
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   581
binder declaration \indexbold{*binder}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
\begin{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   583
\(c\) :: "\(\sigma\)"   (binder "\(\Q\)" \(p\))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
\end{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   585
introduces a constant~$c$ of type~$\sigma$, which must have the form
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   586
$(\tau@1 \To \tau@2) \To \tau@3$.  Its concrete syntax is $\Q~x.P$, where
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   587
$x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   588
and the whole term has type~$\tau@3$.  Special characters in $\Q$ must be
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   589
escaped using a single quote.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   590
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   591
Let us declare the quantifier~$\forall$:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   592
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
All :: "('a => o) => o"   (binder "ALL " 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
\end{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   595
This let us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   596
  $x$.$P$}.  When printing, Isabelle prefers the latter form, but must fall
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   597
back on $\mtt{All}(P)$ if $P$ is not an abstraction.  Both $P$ and {\tt ALL
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   598
  $x$.$P$} have type~$o$, the type of formulae, while the bound variable
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   599
can be polymorphic.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   600
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   601
The binder~$c$ of type $(\sigma \To \tau) \To \tau$ can be nested.  The
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   602
external form $\Q~x@1~x@2 \ldots x@n. P$ corresponds to the internal form
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   603
\[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)) \]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   604
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   605
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   606
The general binder declaration
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
\begin{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   608
\(c\)    :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"   (binder "\(\Q\)" \(p\))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   609
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
is internally expanded to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
\begin{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   612
\(c\)    :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   613
"\(\Q\)"\hskip-3pt  :: "[idts, \(\tau@2\)] => \(\tau@3\)"   ("(3\(\Q\)_./ _)" \(p\))
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   614
\end{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   615
with $idts$ being the nonterminal symbol for a list of $id$s optionally
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   616
constrained (see Fig.\ts\ref{fig:pure_gram}).  The declaration also
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   617
installs a parse translation\index{translations!parse} for~$\Q$ and a print
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   618
translation\index{translations!print} for~$c$ to translate between the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   619
internal and external forms.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   620
\endgroup
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   622
\index{mixfix declaration|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   623
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   624
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   625
\section{Example: some minimal logics} \label{sec:min_logics}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   626
This section presents some examples that have a simple syntax.  They
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   627
demonstrate how to define new object-logics from scratch.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   628
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   629
First we must define how an object-logic syntax embedded into the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   630
meta-logic.  Since all theorems must conform to the syntax for~$prop$ (see
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   631
Fig.\ts\ref{fig:pure_gram}), that syntax has to be extended with the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   632
object-level syntax.  Assume that the syntax of your object-logic defines a
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   633
nonterminal symbol~$o$ of formulae.  These formulae can now appear in
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   634
axioms and theorems wherever $prop$ does if you add the production
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   635
\[ prop ~=~ o. \]
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   636
This is not a copy production but a coercion from formulae to propositions:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   637
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   638
Base = Pure +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   639
types
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   640
  o
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   641
arities
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   642
  o :: logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
  Trueprop :: "o => prop"   ("_" 5)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   645
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   646
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   647
The constant {\tt Trueprop} (the name is arbitrary) acts as an invisible
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   648
coercion function.  Assuming this definition resides in a file {\tt base.thy},
135
493308514ea8 various minor changes;
wenzelm
parents: 108
diff changeset
   649
you have to load it with the command {\tt use_thy "Base"}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   650
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   651
One of the simplest nontrivial logics is {\bf minimal logic} of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   652
implication.  Its definition in Isabelle needs no advanced features but
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   653
illustrates the overall mechanism nicely:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   654
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   655
Hilbert = Base +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   656
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   657
  "-->" :: "[o, o] => o"   (infixr 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   658
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   659
  K     "P --> Q --> P"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   660
  S     "(P --> Q --> R) --> (P --> Q) --> P --> R"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   661
  MP    "[| P --> Q; P |] ==> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   662
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
\end{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   664
After loading this definition from the file {\tt hilbert.thy}, you can
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   665
start to prove theorems in the logic:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   666
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   667
goal Hilbert.thy "P --> P";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   668
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   669
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   670
{\out  1.  P --> P}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   671
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   672
by (resolve_tac [Hilbert.MP] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   673
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   674
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   675
{\out  1.  ?P --> P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   676
{\out  2.  ?P}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   677
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   678
by (resolve_tac [Hilbert.MP] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   679
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   680
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
{\out  1.  ?P1 --> ?P --> P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
{\out  2.  ?P1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   683
{\out  3.  ?P}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   684
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   685
by (resolve_tac [Hilbert.S] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   687
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   688
{\out  1.  P --> ?Q2 --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   689
{\out  2.  P --> ?Q2}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   690
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
by (resolve_tac [Hilbert.K] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   692
{\out Level 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   693
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   694
{\out  1.  P --> ?Q2}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   695
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   696
by (resolve_tac [Hilbert.K] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   697
{\out Level 5}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   698
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   699
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   700
\end{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   701
As we can see, this Hilbert-style formulation of minimal logic is easy to
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   702
define but difficult to use.  The following natural deduction formulation is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   703
better:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   704
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   705
MinI = Base +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   706
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   707
  "-->" :: "[o, o] => o"   (infixr 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   708
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   709
  impI  "(P ==> Q) ==> P --> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   710
  impE  "[| P --> Q; P |] ==> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   711
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   712
\end{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   713
Note, however, that although the two systems are equivalent, this fact
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   714
cannot be proved within Isabelle.  Axioms {\tt S} and {\tt K} can be
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   715
derived in {\tt MinI} (exercise!), but {\tt impI} cannot be derived in {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   716
  Hilbert}.  The reason is that {\tt impI} is only an {\bf admissible} rule
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   717
in {\tt Hilbert}, something that can only be shown by induction over all
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   718
possible proofs in {\tt Hilbert}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   719
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   720
We may easily extend minimal logic with falsity:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   721
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   722
MinIF = MinI +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   723
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   724
  False :: "o"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   725
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   726
  FalseE "False ==> P"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   727
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   728
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   729
On the other hand, we may wish to introduce conjunction only:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   730
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   731
MinC = Base +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   732
consts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   733
  "&" :: "[o, o] => o"   (infixr 30)
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   734
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   735
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   736
  conjI  "[| P; Q |] ==> P & Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   737
  conjE1 "P & Q ==> P"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   738
  conjE2 "P & Q ==> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   739
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   740
\end{ttbox}
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   741
And if we want to have all three connectives together, we create and load a
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   742
theory file consisting of a single line:\footnote{We can combine the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   743
  theories without creating a theory file using the ML declaration
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   744
\begin{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   745
val MinIFC_thy = merge_theories(MinIF,MinC)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   746
\end{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   747
\index{*merge_theories|fnote}}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   748
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   749
MinIFC = MinIF + MinC
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   750
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   751
Now we can prove mixed theorems like
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   752
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   753
goal MinIFC.thy "P & False --> Q";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   754
by (resolve_tac [MinI.impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   755
by (dresolve_tac [MinC.conjE2] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   756
by (eresolve_tac [MinIF.FalseE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   757
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   758
Try this as an exercise!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   759
291
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   760
\medskip
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   761
Unless you need to define macros or syntax translation functions, you may
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   762
skip the rest of this chapter.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   763
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   764
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   765
\section{*Abstract syntax trees} \label{sec:asts}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   766
\index{trees!abstract syntax|(} The parser, given a token list from the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   767
lexer, applies productions to yield a parse tree\index{trees!parse}.  By
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   768
applying some internal transformations the parse tree becomes an abstract
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   769
syntax tree, or \AST{}.  Macro expansion, further translations and finally
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   770
type inference yields a well-typed term\index{terms!obtained from ASTs}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   771
The printing process is the reverse, except for some subtleties to be
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   772
discussed later.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   773
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   774
Figure~\ref{fig:parse_print} outlines the parsing and printing process.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   775
Much of the complexity is due to the macro mechanism.  Using macros, you
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   776
can specify most forms of concrete syntax without writing any \ML{} code.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   777
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   778
\begin{figure}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   779
\begin{center}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   780
\begin{tabular}{cl}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   781
string          & \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   782
$\downarrow$    & parser \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   783
parse tree      & \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   784
$\downarrow$    & parse \AST{} translation \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   785
\AST{}             & \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   786
$\downarrow$    & \AST{} rewriting (macros) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   787
\AST{}             & \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   788
$\downarrow$    & parse translation, type inference \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   789
--- well-typed term --- & \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   790
$\downarrow$    & print translation \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   791
\AST{}             & \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   792
$\downarrow$    & \AST{} rewriting (macros) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   793
\AST{}             & \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   794
$\downarrow$    & print \AST{} translation, printer \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   795
string          &
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   796
\end{tabular}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   797
\index{translations!parse}\index{translations!parse AST}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   798
\index{translations!print}\index{translations!print AST}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   799
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   800
\end{center}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   801
\caption{Parsing and printing}\label{fig:parse_print}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   802
\end{figure}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   803
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   804
Abstract syntax trees are an intermediate form between the raw parse trees
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   805
and the typed $\lambda$-terms.  An \AST{} is either an atom (constant or
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   806
variable) or a list of {\em at least two\/} subtrees.  Internally, they
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   807
have type \ttindex{Syntax.ast}: \index{*Constant} \index{*Variable}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   808
\index{*Appl}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   809
\begin{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   810
datatype ast = Constant of string
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   811
             | Variable of string
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   812
             | Appl of ast list
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   813
\end{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   814
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   815
Isabelle uses an S-expression syntax for abstract syntax trees.  Constant
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   816
atoms are shown as quoted strings, variable atoms as non-quoted strings and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   817
applications as a parenthesized list of subtrees.  For example, the \AST
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   818
\begin{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   819
Appl [Constant "_constrain",
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   820
  Appl [Constant "_abs", Variable "x", Variable "t"],
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   821
  Appl [Constant "fun", Variable "'a", Variable "'b"]]
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   822
\end{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   823
is shown as {\tt ("_constrain" ("_abs" x t) ("fun" 'a 'b))}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   824
Both {\tt ()} and {\tt (f)} are illegal because they have too few
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   825
subtrees. 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   826
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   827
The resemblance of Lisp's S-expressions is intentional, but there are two
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   828
kinds of atomic symbols: $\Constant x$ and $\Variable x$.  Do not take the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   829
names ``{\tt Constant}'' and ``{\tt Variable}'' too literally; in the later
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   830
translation to terms, $\Variable x$ may become a constant, free or bound
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   831
variable, even a type constructor or class name; the actual outcome depends
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   832
on the context.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   833
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   834
Similarly, you can think of ${\tt (} f~x@1~\ldots~x@n{\tt )}$ as the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   835
application of~$f$ to the arguments $x@1, \ldots, x@n$.  But the kind of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   836
application is determined later by context; it could be a type constructor
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   837
applied to types.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   838
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   839
Forms like {\tt (("_abs" x $t$) $u$)} are legal, but \AST{}s are
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   840
first-order: the {\tt "_abs"} does not bind the {\tt x} in any way.  Later
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   841
at the term level, {\tt ("_abs" x $t$)} will become an {\tt Abs} node and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   842
occurrences of {\tt x} in $t$ will be replaced by bound variables (the term
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   843
constructor \ttindex{Bound}).
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   844
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   845
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   846
\subsection{Transforming parse trees to \AST{}s}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   847
The parse tree is the raw output of the parser.  Translation functions,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   848
called {\bf parse AST translations}\indexbold{translations!parse AST},
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   849
transform the parse tree into an abstract syntax tree.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   850
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   851
The parse tree is constructed by nesting the right-hand sides of the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   852
productions used to recognize the input.  Such parse trees are simply lists
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   853
of tokens and constituent parse trees, the latter representing the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   854
nonterminals of the productions.  Let us refer to the actual productions in
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   855
the form displayed by {\tt Syntax.print_syntax}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   856
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   857
Ignoring parse \AST{} translations, parse trees are transformed to \AST{}s
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   858
by stripping out delimiters and copy productions.  More precisely, the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   859
mapping $ast_of_pt$\index{ast_of_pt@$ast_of_pt$} is derived from the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   860
productions as follows:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   861
\begin{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   862
  \item Name tokens: $ast_of_pt(t) = \Variable s$, where $t$ is an $id$,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   863
    $var$, $tid$ or $tvar$ token, and $s$ its associated string.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   864
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   865
  \item Copy productions: $ast_of_pt(\ldots P \ldots) = ast_of_pt(P)$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   866
    Here $\ldots$ stands for strings of delimiters, which are
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   867
    discarded.  $P$ stands for the single constituent that is not a
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   868
    delimiter; it is either a nonterminal symbol or a name token.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   869
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   870
  \item $0$-ary productions: $ast_of_pt(\ldots \mtt{=>} c) = \Constant c$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   871
    Here there are no constituents other than delimiters, which are
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   872
    discarded. 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   873
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   874
  \item $n$-ary productions, where $n \ge 1$: delimiters are discarded and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   875
    the remaining constituents $P@1$, \ldots, $P@n$ are built into an
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   876
    application whose head constant is~$c$:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   877
    \begin{eqnarray*}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   878
      \lefteqn{ast_of_pt(\ldots P@1 \ldots P@n \ldots \mtt{=>} c)} \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   879
      &&\qquad{}= \Appl{\Constant c, ast_of_pt(P@1), \ldots, ast_of_pt(P@n)}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   880
    \end{eqnarray*}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   881
\end{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   882
Figure~\ref{fig:parse_ast} presents some simple examples, where {\tt ==},
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   883
{\tt _appl}, {\tt _args}, and so forth name productions of the Pure syntax.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   884
These examples illustrate the need for further translations to make \AST{}s
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   885
closer to the typed $\lambda$-calculus.  The Pure syntax provides
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   886
predefined parse \AST{} translations\index{translations!parse AST} for
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   887
ordinary applications, type applications, nested abstractions, meta
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   888
implications and function types.  Figure~\ref{fig:parse_ast_tr} shows their
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   889
effect on some representative input strings.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   890
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   891
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   892
\begin{figure}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   893
\begin{center}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   894
\tt\begin{tabular}{ll}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   895
\rm input string    & \rm \AST \\\hline
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   896
"f"                 & f \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   897
"'a"                & 'a \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   898
"t == u"            & ("==" t u) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   899
"f(x)"              & ("_appl" f x) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   900
"f(x, y)"           & ("_appl" f ("_args" x y)) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   901
"f(x, y, z)"        & ("_appl" f ("_args" x ("_args" y z))) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   902
"\%x y.\ t"         & ("_lambda" ("_idts" x y) t) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   903
\end{tabular}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   904
\end{center}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   905
\caption{Parsing examples using the Pure syntax}\label{fig:parse_ast} 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   906
\end{figure}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   907
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   908
\begin{figure}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   909
\begin{center}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   910
\tt\begin{tabular}{ll}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   911
\rm input string            & \rm \AST{} \\\hline
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   912
"f(x, y, z)"                & (f x y z) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   913
"'a ty"                     & (ty 'a) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   914
"('a, 'b) ty"               & (ty 'a 'b) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   915
"\%x y z.\ t"               & ("_abs" x ("_abs" y ("_abs" z t))) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   916
"\%x ::\ 'a.\ t"            & ("_abs" ("_constrain" x 'a) t) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   917
"[| P; Q; R |] => S"        & ("==>" P ("==>" Q ("==>" R S))) \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   918
"['a, 'b, 'c] => 'd"        & ("fun" 'a ("fun" 'b ("fun" 'c 'd)))
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   919
\end{tabular}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   920
\end{center}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   921
\caption{Built-in parse \AST{} translations}\label{fig:parse_ast_tr}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   922
\end{figure}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   923
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   924
The names of constant heads in the \AST{} control the translation process.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   925
The list of constants invoking parse \AST{} translations appears in the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   926
output of {\tt Syntax.print_syntax} under {\tt parse_ast_translation}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   927
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   928
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   929
\subsection{Transforming \AST{}s to terms}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   930
The \AST{}, after application of macros (see \S\ref{sec:macros}), is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   931
transformed into a term.  This term is probably ill-typed since type
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   932
inference has not occurred yet.  The term may contain type constraints
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   933
consisting of applications with head {\tt "_constrain"}; the second
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   934
argument is a type encoded as a term.  Type inference later introduces
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   935
correct types or rejects the input.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   936
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   937
Another set of translation functions, namely parse
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   938
translations,\index{translations!parse}, may affect this process.  If we
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   939
ignore parse translations for the time being, then \AST{}s are transformed
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   940
to terms by mapping \AST{} constants to constants, \AST{} variables to
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   941
schematic or free variables and \AST{} applications to applications.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   942
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   943
More precisely, the mapping $term_of_ast$\index{term_of_ast@$term_of_ast$}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   944
is defined by
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   945
\begin{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   946
\item Constants: $term_of_ast(\Constant x) = \ttfct{Const} (x,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   947
  \mtt{dummyT})$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   948
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   949
\item Schematic variables: $term_of_ast(\Variable \mtt{"?}xi\mtt") =
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   950
  \ttfct{Var} ((x, i), \mtt{dummyT})$, where $x$ is the base name and $i$
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   951
  the index extracted from $xi$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   952
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   953
\item Free variables: $term_of_ast(\Variable x) = \ttfct{Free} (x,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   954
  \mtt{dummyT})$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   955
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   956
\item Function applications with $n$ arguments:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   957
    \begin{eqnarray*}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   958
      \lefteqn{term_of_ast(\Appl{f, x@1, \ldots, x@n})} \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   959
      &&\qquad{}= term_of_ast(f) \ttapp
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   960
         term_of_ast(x@1) \ttapp \ldots \ttapp term_of_ast(x@n)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   961
    \end{eqnarray*}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   962
\end{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   963
Here \ttindex{Const}, \ttindex{Var}, \ttindex{Free} and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   964
\verb|$|\index{$@{\tt\$}} are constructors of the datatype {\tt term},
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   965
while \ttindex{dummyT} stands for some dummy type that is ignored during
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   966
type inference.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   967
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   968
So far the outcome is still a first-order term.  Abstractions and bound
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   969
variables (constructors \ttindex{Abs} and \ttindex{Bound}) are introduced
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   970
by parse translations.  Such translations are attached to {\tt "_abs"},
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   971
{\tt "!!"} and user-defined binders.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   972
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   973
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   974
\subsection{Printing of terms}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   975
The output phase is essentially the inverse of the input phase.  Terms are
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   976
translated via abstract syntax trees into strings.  Finally the strings are
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   977
pretty printed.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   978
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   979
Print translations (\S\ref{sec:tr_funs}) may affect the transformation of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   980
terms into \AST{}s.  Ignoring those, the transformation maps
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   981
term constants, variables and applications to the corresponding constructs
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   982
on \AST{}s.  Abstractions are mapped to applications of the special
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   983
constant {\tt _abs}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   984
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   985
More precisely, the mapping $ast_of_term$\index{ast_of_term@$ast_of_term$}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   986
is defined as follows:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   987
\begin{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   988
  \item $ast_of_term(\ttfct{Const} (x, \tau)) = \Constant x$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   989
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   990
  \item $ast_of_term(\ttfct{Free} (x, \tau)) = constrain (\Variable x,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   991
    \tau)$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   992
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   993
  \item $ast_of_term(\ttfct{Var} ((x, i), \tau)) = constrain (\Variable
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   994
    \mtt{"?}xi\mtt", \tau)$, where $\mtt?xi$ is the string representation of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   995
    the {\tt indexname} $(x, i)$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   996
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   997
  \item For the abstraction $\lambda x::\tau.t$, let $x'$ be a variant
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   998
    of~$x$ renamed to differ from all names occurring in~$t$, and let $t'$
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
   999
    be obtained from~$t$ by replacing all bound occurrences of~$x$ by
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1000
    the free variable $x'$.  This replaces corresponding occurrences of the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1001
    constructor \ttindex{Bound} by the term $\ttfct{Free} (x',
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1002
    \mtt{dummyT})$:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1003
   \begin{eqnarray*}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1004
      \lefteqn{ast_of_term(\ttfct{Abs} (x, \tau, t))} \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1005
      &&\qquad{}=   \ttfct{Appl}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1006
                  \mathopen{\mtt[} 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1007
                  \Constant \mtt{"_abs"}, constrain(\Variable x', \tau), \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1008
      &&\qquad\qquad\qquad ast_of_term(t') \mathclose{\mtt]}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1009
    \end{eqnarray*}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1010
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1011
  \item $ast_of_term(\ttfct{Bound} i) = \Variable \mtt{"B.}i\mtt"$.  
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1012
    The occurrence of constructor \ttindex{Bound} should never happen
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1013
    when printing well-typed terms; it indicates a de Bruijn index with no
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1014
    matching abstraction.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1015
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1016
  \item Where $f$ is not an application,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1017
    \begin{eqnarray*}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1018
      \lefteqn{ast_of_term(f \ttapp x@1 \ttapp \ldots \ttapp x@n)} \\
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1019
      &&\qquad{}= \ttfct{Appl} 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1020
                  \mathopen{\mtt[} ast_of_term(f), 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1021
                  ast_of_term(x@1), \ldots,ast_of_term(x@n) 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1022
                  \mathclose{\mtt]}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1023
    \end{eqnarray*}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1024
\end{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1025
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1026
Type constraints are inserted to allow the printing of types, which is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1027
governed by the boolean variable \ttindex{show_types}.  Constraints are
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1028
treated as follows:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1029
\begin{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1030
  \item $constrain(x, \tau) = x$, if $\tau = \mtt{dummyT}$ \index{*dummyT} or
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1031
    \ttindex{show_types} not set to {\tt true}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1032
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1033
  \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, ty}$,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1034
    where $ty$ is the \AST{} encoding of $\tau$.  That is, type constructors as
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1035
    {\tt Constant}s, type identifiers as {\tt Variable}s and type applications
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1036
    as {\tt Appl}s with the head type constructor as first element.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1037
    Additionally, if \ttindex{show_sorts} is set to {\tt true}, some type
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1038
    variables are decorated with an \AST{} encoding of their sort.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1039
\end{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1040
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1041
The \AST{}, after application of macros (see \S\ref{sec:macros}), is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1042
transformed into the final output string.  The built-in {\bf print AST
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1043
  translations}\indexbold{translations!print AST} effectively reverse the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1044
parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1045
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1046
For the actual printing process, the names attached to productions
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1047
of the form $\ldots A^{(p@1)}@1 \ldots A^{(p@n)}@n \ldots \mtt{=>} c$ play
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1048
a vital role.  Each \AST{} with constant head $c$, namely $\mtt"c\mtt"$ or
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1049
$(\mtt"c\mtt"~ x@1 \ldots x@n)$, is printed according to the production
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1050
for~$c$.  Each argument~$x@i$ is converted to a string, and put in
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1051
parentheses if its priority~$(p@i)$ requires this.  The resulting strings
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1052
and their syntactic sugar (denoted by ``\dots'' above) are joined to make a
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1053
single string.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1054
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1055
If an application $(\mtt"c\mtt"~ x@1 \ldots x@m)$ has more arguments than the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1056
corresponding production, it is first split into $((\mtt"c\mtt"~ x@1 \ldots
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1057
x@n) ~ x@{n+1} \ldots x@m)$. Applications with too few arguments or with
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1058
non-constant head or without a corresponding production are printed as
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1059
$f(x@1, \ldots, x@l)$ or $(\alpha@1, \ldots, \alpha@l) ty$.  An occurrence of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1060
$\Variable x$ is simply printed as~$x$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1061
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1062
Blanks are {\em not\/} inserted automatically.  If blanks are required to
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1063
separate tokens, specify them in the mixfix declaration, possibly preceeded
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1064
by a slash~({\tt/}) to allow a line break.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1065
\index{trees!abstract syntax|)}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1066
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1067
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1068
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1069
\section{*Macros: Syntactic rewriting} \label{sec:macros}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1070
\index{macros|(}\index{rewriting!syntactic|(} 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1071
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1072
Mixfix declarations alone can handle situations where there is a direct
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1073
connection between the concrete syntax and the underlying term.  Sometimes
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1074
we require a more elaborate concrete syntax, such as quantifiers and list
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1075
notation.  Isabelle's {\bf macros} and {\bf translation functions} can
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1076
perform translations such as
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1077
\begin{center}\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1078
  \begin{tabular}{r@{$\quad\protect\rightleftharpoons\quad$}l}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1079
    ALL x:A.P   & Ball(A, \%x.P)        \\ \relax
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1080
    [x, y, z]   & Cons(x, Cons(y, Cons(z, Nil)))
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1081
  \end{tabular}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1082
\end{center}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1083
Translation functions (see \S\ref{sec:tr_funs}) must be coded in ML; they
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1084
are the most powerful translation mechanism but are difficult to read or
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1085
write.  Macros are specified by first-order rewriting systems that operate
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1086
on abstract syntax trees.  They are usually easy to read and write, and can
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1087
express all but the most obscure translations.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1088
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1089
Figure~\ref{fig:set_trans} defines a fragment of first-order logic and set
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1090
theory.\footnote{This and the following theories are complete working
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1091
  examples, though they specify only syntax, no axioms.  The file {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1092
    ZF/zf.thy} presents the full set theory definition, including many
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1093
  macro rules.}  Theory {\tt SET} defines constants for set comprehension
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1094
({\tt Collect}), replacement ({\tt Replace}) and bounded universal
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1095
quantification ({\tt Ball}).  Each of these binds some variables.  Without
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1096
additional syntax we should have to express $\forall x \in A.  P$ as {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1097
  Ball(A,\%x.P)}, and similarly for the others.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1098
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1099
\begin{figure}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1100
\begin{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1101
SET = Pure +
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1102
types
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1103
  i, o
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1104
arities
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1105
  i, o :: logic
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1106
consts
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1107
  Trueprop      :: "o => prop"              ("_" 5)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1108
  Collect       :: "[i, i => o] => i"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1109
  "{\at}Collect"    :: "[idt, i, o] => i"       ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1110
  Replace       :: "[i, [i, i] => o] => i"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1111
  "{\at}Replace"    :: "[idt, idt, i, o] => i"  ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1112
  Ball          :: "[i, i => o] => o"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1113
  "{\at}Ball"       :: "[idt, i, o] => o"       ("(3ALL _:_./ _)" 10)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1114
translations
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1115
  "{\ttlbrace}x:A. P{\ttrbrace}"    == "Collect(A, \%x. P)"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1116
  "{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1117
  "ALL x:A. P"  == "Ball(A, \%x. P)"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1118
end
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1119
\end{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1120
\caption{Macro example: set theory}\label{fig:set_trans}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1121
\end{figure}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1122
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1123
The theory specifies a variable-binding syntax through additional
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1124
productions that have mixfix declarations.  Each non-copy production must
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1125
specify some constant, which is used for building \AST{}s.  The additional
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1126
constants are decorated with {\tt\at} to stress their purely syntactic
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1127
purpose; they should never occur within the final well-typed terms.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1128
Furthermore, they cannot be written in formulae because they are not legal
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1129
identifiers.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1130
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1131
The translations cause the replacement of external forms by internal forms
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1132
after parsing, and vice versa before printing of terms.  As a specification
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1133
of the set theory notation, they should be largely self-explanatory.  The
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1134
syntactic constants, {\tt\at Collect}, {\tt\at Replace} and {\tt\at Ball},
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1135
appear implicitly in the macro rules via their mixfix forms.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1136
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1137
Macros can define variable-binding syntax because they operate on \AST{}s,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1138
which have no inbuilt notion of bound variable.  The macro variables {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1139
  x} and~{\tt y} have type~{\tt idt} and therefore range over identifiers,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1140
in this case bound variables.  The macro variables {\tt P} and~{\tt Q}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1141
range over formulae containing bound variable occurrences.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1142
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1143
Other applications of the macro system can be less straightforward, and
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1144
there are peculiarities.  The rest of this section will describe in detail
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1145
how Isabelle macros are preprocessed and applied.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1146
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1147
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1148
\subsection{Specifying macros}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1149
Macros are basically rewrite rules on \AST{}s.  But unlike other macro
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1150
systems found in programming languages, Isabelle's macros work in both
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1151
directions.  Therefore a syntax contains two lists of rewrites: one for
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1152
parsing and one for printing.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1153
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1154
The {\tt translations} section\index{translations section@{\tt translations}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1155
section} specifies macros.  The syntax for a macro is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1156
\[ (root)\; string \quad
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1157
   \left\{\begin{array}[c]{c} \mtt{=>} \\ \mtt{<=} \\ \mtt{==} \end{array}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1158
   \right\} \quad
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1159
   (root)\; string 
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1160
\]
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1161
%
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1162
This specifies a parse rule ({\tt =>}), a print rule ({\tt <=}), or both
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1163
({\tt ==}).  The two strings specify the left and right-hand sides of the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1164
macro rule.  The $(root)$ specification is optional; it specifies the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1165
nonterminal for parsing the $string$ and if omitted defaults to {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1166
  logic}.  \AST{} rewrite rules $(l, r)$ must obey certain conditions:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1167
\begin{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1168
\item Rules must be left linear: $l$ must not contain repeated variables.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1169
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1170
\item Rules must have constant heads, namely $l = \mtt"c\mtt"$ or $l =
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1171
  (\mtt"c\mtt" ~ x@1 \ldots x@n)$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1172
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1173
\item Every variable in~$r$ must also occur in~$l$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1174
\end{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1175
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1176
Macro rules may refer to any syntax from the parent theories.  They may
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1177
also refer to anything defined before the the {\tt .thy} file's {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1178
  translations} section --- including any mixfix declarations.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1179
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1180
Upon declaration, both sides of the macro rule undergo parsing and parse
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1181
\AST{} translations (see \S\ref{sec:asts}), but do not themselves undergo
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1182
macro expansion.  The lexer runs in a different mode that additionally
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1183
accepts identifiers of the form $\_~letter~quasiletter^*$ (like {\tt _idt},
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1184
{\tt _K}).  Thus, a constant whose name starts with an underscore can
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1185
appear in macro rules but not in ordinary terms.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1186
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1187
Some atoms of the macro rule's \AST{} are designated as constants for
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1188
matching.  These are all names that have been declared as classes, types or
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1189
constants.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1190
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1191
The result of this preprocessing is two lists of macro rules, each stored
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1192
as a pair of \AST{}s.  They can be viewed using {\tt Syntax.print_syntax}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1193
(sections \ttindex{parse_rules} and \ttindex{print_rules}).  For
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1194
theory~{\tt SET} of Fig.~\ref{fig:set_trans} these are
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1195
\begin{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1196
parse_rules:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1197
  ("{\at}Collect" x A P)  ->  ("Collect" A ("_abs" x P))
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1198
  ("{\at}Replace" y x A Q)  ->  ("Replace" A ("_abs" x ("_abs" y Q)))
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1199
  ("{\at}Ball" x A P)  ->  ("Ball" A ("_abs" x P))
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1200
print_rules:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1201
  ("Collect" A ("_abs" x P))  ->  ("{\at}Collect" x A P)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1202
  ("Replace" A ("_abs" x ("_abs" y Q)))  ->  ("{\at}Replace" y x A Q)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1203
  ("Ball" A ("_abs" x P))  ->  ("{\at}Ball" x A P)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1204
\end{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1205
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1206
\begin{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1207
  Avoid choosing variable names that have previously been used as
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1208
  constants, types or type classes; the {\tt consts} section in the output
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1209
  of {\tt Syntax.print_syntax} lists all such names.  If a macro rule works
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1210
  incorrectly, inspect its internal form as shown above, recalling that
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1211
  constants appear as quoted strings and variables without quotes.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1212
\end{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1213
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1214
\begin{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1215
If \ttindex{eta_contract} is set to {\tt true}, terms will be
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1216
$\eta$-contracted {\em before\/} the \AST{} rewriter sees them.  Thus some
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1217
abstraction nodes needed for print rules to match may vanish.  For example,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1218
\verb|Ball(A, %x. P(x))| contracts {\tt Ball(A, P)}; the print rule does
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1219
not apply and the output will be {\tt Ball(A, P)}.  This problem would not
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1220
occur if \ML{} translation functions were used instead of macros (as is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1221
done for binder declarations).
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1222
\end{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1223
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1224
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1225
\begin{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1226
Another trap concerns type constraints.  If \ttindex{show_types} is set to
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1227
{\tt true}, bound variables will be decorated by their meta types at the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1228
binding place (but not at occurrences in the body).  Matching with
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1229
\verb|Collect(A, %x. P)| binds {\tt x} to something like {\tt ("_constrain" y
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1230
"i")} rather than only {\tt y}.  \AST{} rewriting will cause the constraint to
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1231
appear in the external form, say \verb|{y::i:A::i. P::o}|.  
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1232
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1233
To allow such constraints to be re-read, your syntax should specify bound
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1234
variables using the nonterminal~\ttindex{idt}.  This is the case in our
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1235
example.  Choosing {\tt id} instead of {\tt idt} is a common error,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1236
especially since it appears in former versions of most of Isabelle's
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1237
object-logics.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1238
\end{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1239
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1240
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1241
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1242
\subsection{Applying rules}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1243
As a term is being parsed or printed, an \AST{} is generated as an
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1244
intermediate form (recall Fig.\ts\ref{fig:parse_print}).  The \AST{} is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1245
normalized by applying macro rules in the manner of a traditional term
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1246
rewriting system.  We first examine how a single rule is applied.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1247
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1248
Let $t$ be the abstract syntax tree to be normalized and $(l, r)$ some
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1249
translation rule.  A subtree~$u$ of $t$ is a {\bf redex} if it is an
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1250
instance of~$l$; in this case $l$ is said to {\bf match}~$u$.  A redex
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1251
matched by $l$ may be replaced by the corresponding instance of~$r$, thus
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1252
{\bf rewriting} the \AST~$t$.  Matching requires some notion of {\bf
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1253
  place-holders} that may occur in rule patterns but not in ordinary
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1254
\AST{}s; {\tt Variable} atoms serve this purpose.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1255
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1256
The matching of the object~$u$ by the pattern~$l$ is performed as follows:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1257
\begin{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1258
  \item Every constant matches itself.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1259
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1260
  \item $\Variable x$ in the object matches $\Constant x$ in the pattern.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1261
    This point is discussed further below.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1262
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1263
  \item Every \AST{} in the object matches $\Variable x$ in the pattern,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1264
    binding~$x$ to~$u$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1265
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1266
  \item One application matches another if they have the same number of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1267
    subtrees and corresponding subtrees match.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1268
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1269
  \item In every other case, matching fails.  In particular, {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1270
      Constant}~$x$ can only match itself.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1271
\end{itemize}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1272
A successful match yields a substitution that is applied to~$r$, generating
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1273
the instance that replaces~$u$.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1274
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1275
The second case above may look odd.  This is where {\tt Variable}s of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1276
non-rule \AST{}s behave like {\tt Constant}s.  Recall that \AST{}s are not
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1277
far removed from parse trees; at this level it is not yet known which
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1278
identifiers will become constants, bounds, frees, types or classes.  As
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1279
\S\ref{sec:asts} describes, former parse tree heads appear in \AST{}s as
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1280
{\tt Constant}s, while $id$s, $var$s, $tid$s and $tvar$s become {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1281
  Variable}s.  On the other hand, when \AST{}s generated from terms for
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1282
printing, all constants and type constructors become {\tt Constant}s; see
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1283
\S\ref{sec:asts}.  Thus \AST{}s may contain a messy mixture of {\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1284
  Variable}s and {\tt Constant}s.  This is insignificant at macro level
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1285
because matching treats them alike.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1286
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1287
Because of this behaviour, different kinds of atoms with the same name are
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1288
indistinguishable, which may make some rules prone to misbehaviour.  Example:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1289
\begin{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1290
types
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1291
  Nil
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1292
consts
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1293
  Nil     :: "'a list"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1294
  "[]"    :: "'a list"    ("[]")
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1295
translations
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1296
  "[]"    == "Nil"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1297
\end{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1298
The term {\tt Nil} will be printed as {\tt []}, just as expected.  What
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1299
happens with \verb|%Nil.t| or {\tt x::Nil} is left as an exercise.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1300
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1301
Normalizing an \AST{} involves repeatedly applying macro rules until none
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1302
is applicable.  Macro rules are chosen in the order that they appear in the
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1303
{\tt translations} section.  You can watch the normalization of \AST{}s
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1304
during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1305
{\tt true}.\index{tracing!of macros} Alternatively, use
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1306
\ttindex{Syntax.test_read}.  The information displayed when tracing
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1307
includes the \AST{} before normalization ({\tt pre}), redexes with results
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1308
({\tt rewrote}), the normal form finally reached ({\tt post}) and some
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1309
statistics ({\tt normalize}).  If tracing is off,
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1310
\ttindex{Syntax.stat_norm_ast} can be set to {\tt true} in order to enable
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1311
printing of the normal form and statistics only.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1312
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1313
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1314
\subsection{Example: the syntax of finite sets}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1315
This example demonstrates the use of recursive macros to implement a
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1316
convenient notation for finite sets.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1317
\begin{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1318
FINSET = SET +
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1319
types
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1320
  is
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1321
consts
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1322
  ""            :: "i => is"                ("_")
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1323
  "{\at}Enum"       :: "[i, is] => is"          ("_,/ _")
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1324
  empty         :: "i"                      ("{\ttlbrace}{\ttrbrace}")
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1325
  insert        :: "[i, i] => i"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1326
  "{\at}Finset"     :: "is => i"                ("{\ttlbrace}(_){\ttrbrace}")
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1327
translations
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1328
  "{\ttlbrace}x, xs{\ttrbrace}"     == "insert(x, {\ttlbrace}xs{\ttrbrace})"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1329
  "{\ttlbrace}x{\ttrbrace}"         == "insert(x, {\ttlbrace}{\ttrbrace})"
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1330
end
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1331
\end{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1332
Finite sets are internally built up by {\tt empty} and {\tt insert}.  The
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1333
declarations above specify \verb|{x, y, z}| as the external representation
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1334
of
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1335
\begin{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1336
insert(x, insert(y, insert(z, empty)))
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1337
\end{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1338
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1339
The nonterminal symbol~{\tt is} stands for one or more objects of type~{\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1340
  i} separated by commas.  The mixfix declaration \hbox{\verb|"_,/ _"|}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1341
allows a line break after the comma for pretty printing; if no line break
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1342
is required then a space is printed instead.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1343
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1344
The nonterminal is declared as the type~{\tt is}, but with no {\tt arities}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1345
declaration.  Hence {\tt is} is not a logical type and no default
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1346
productions are added.  If we had needed enumerations of the nonterminal
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1347
{\tt logic}, which would include all the logical types, we could have used
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1348
the predefined nonterminal symbol \ttindex{args} and skipped this part
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1349
altogether.  The nonterminal~{\tt is} can later be reused for other
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1350
enumerations of type~{\tt i} like lists or tuples.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1351
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1352
Next follows {\tt empty}, which is already equipped with its syntax
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1353
\verb|{}|, and {\tt insert} without concrete syntax.  The syntactic
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1354
constant {\tt\at Finset} provides concrete syntax for enumerations of~{\tt
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1355
  i} enclosed in curly braces.  Remember that a pair of parentheses, as in
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1356
\verb|"{(_)}"|, specifies a block of indentation for pretty printing.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1357
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1358
The translations may look strange at first.  Macro rules are best
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1359
understood in their internal forms:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1360
\begin{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1361
parse_rules:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1362
  ("{\at}Finset" ("{\at}Enum" x xs))  ->  ("insert" x ("{\at}Finset" xs))
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1363
  ("{\at}Finset" x)  ->  ("insert" x "empty")
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1364
print_rules:
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1365
  ("insert" x ("{\at}Finset" xs))  ->  ("{\at}Finset" ("{\at}Enum" x xs))
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1366
  ("insert" x "empty")  ->  ("{\at}Finset" x)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1367
\end{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1368
This shows that \verb|{x, xs}| indeed matches any set enumeration of at least
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1369
two elements, binding the first to {\tt x} and the rest to {\tt xs}.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1370
Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration.  
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1371
The parse rules only work in the order given.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1372
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1373
\begin{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1374
  The \AST{} rewriter cannot discern constants from variables and looks
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1375
  only for names of atoms.  Thus the names of {\tt Constant}s occurring in
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1376
  the (internal) left-hand side of translation rules should be regarded as
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1377
  reserved keywords.  Choose non-identifiers like {\tt\at Finset} or
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1378
  sufficiently long and strange names.  If a bound variable's name gets
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1379
  rewritten, the result will be incorrect; for example, the term
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1380
\begin{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1381
\%empty insert. insert(x, empty)
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1382
\end{ttbox}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1383
  gets printed as \verb|%empty insert. {x}|.
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1384
\end{warn}
a615050a7494 first draft of Springer volume
lcp
parents: 188
diff changeset
  1385