%% $Id$
%% \([a-zA-Z][a-zA-Z]}\.\) \([^ ]\) \1 \2
%% @\([a-z0-9]\) ^{(\1)}
\newcommand\rmindex[1]{{#1}\index{#1}\@}
\newcommand\mtt[1]{\mbox{\tt #1}}
\newcommand\ttfct[1]{\mathop{\mtt{#1}}\nolimits}
\newcommand\ttapp{\mathrel{\hbox{\tt\$}}}
\newcommand\Constant{\ttfct{Constant}}
\newcommand\Variable{\ttfct{Variable}}
\newcommand\Appl[1]{\ttfct{Appl}\mathopen{\mtt[}#1\mathclose{\mtt]}}
\newcommand\AST{{\sc ast}}
\let\rew=\longrightarrow
\chapter{Defining Logics} \label{Defining-Logics}
This chapter explains how to define new formal systems --- in particular,
their concrete syntax. While Isabelle can be regarded as a theorem prover
for set theory, higher-order logic or the sequent calculus, its
distinguishing feature is support for the definition of new logics.
Isabelle logics are hierarchies of theories, which are described and
illustrated in {\em Introduction to Isabelle}. That material, together
with the theory files provided in the examples directories, should suffice
for all simple applications. The easiest way to define a new theory is by
modifying a copy of an existing theory.
This chapter is intended for experienced Isabelle users. It documents all
aspects of theories concerned with syntax: mixfix declarations, pretty
printing, macros and translation functions. The extended examples of
\S\ref{sec:min_logics} demonstrate the logical aspects of the definition of
theories. Sections marked with * are highly technical and might be skipped
on the first reading.
\section{Priority grammars} \label{sec:priority_grammars}
\index{grammars!priority|(}
The syntax of an Isabelle logic is specified by a {\bf priority grammar}.
A context-free grammar\index{grammars!context-free} contains a set of
productions of the form $A=\gamma$, where $A$ is a nonterminal and
$\gamma$, the right-hand side, is a string of terminals and nonterminals.
Isabelle uses an extended format permitting {\bf priorities}, or
precedences. Each nonterminal is decorated by an integer priority, as
in~$A^{(p)}$. A nonterminal $A^{(p)}$ in a derivation may be replaced
using a production $A^{(q)} = \gamma$ only if $p \le q$. Any priority
grammar can be translated into a normal context free grammar by introducing
new nonterminals and productions.
Formally, a set of context free productions $G$ induces a derivation
relation $\rew@G$. Let $\alpha$ and $\beta$ denote strings of terminal or
nonterminal symbols. Then
\[ \alpha\, A^{(p)}\, \beta ~\rew@G~ \alpha\,\gamma\,\beta \]
if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$q\ge p$.
The following simple grammar for arithmetic expressions demonstrates how
binding power and associativity of operators can be enforced by priorities.
\begin{center}
\begin{tabular}{rclr}
$A^{(9)}$ & = & {\tt0} \\
$A^{(9)}$ & = & {\tt(} $A^{(0)}$ {\tt)} \\
$A^{(0)}$ & = & $A^{(0)}$ {\tt+} $A^{(1)}$ \\
$A^{(2)}$ & = & $A^{(3)}$ {\tt*} $A^{(2)}$ \\
$A^{(3)}$ & = & {\tt-} $A^{(3)}$
\end{tabular}
\end{center}
The choice of priorities determines that {\tt -} binds tighter than {\tt *},
which binds tighter than {\tt +}. Furthermore {\tt +} associates to the
left and {\tt *} to the right.
To minimize the number of subscripts, we adopt the following conventions:
\begin{itemize}
\item All priorities $p$ must be in the range $0 \leq p \leq max_pri$ for
some fixed integer $max_pri$.
\item Priority $0$ on the right-hand side and priority $max_pri$ on the
left-hand side may be omitted.
\end{itemize}
The production $A^{(p)} = \alpha$ is written as $A = \alpha~(p)$;
the priority of the left-hand side actually appears in a column on the far
right. Finally, alternatives may be separated by $|$, and repetition
indicated by \dots.
Using these conventions and assuming $max_pri=9$, the grammar takes the form
\begin{center}
\begin{tabular}{rclc}
$A$ & = & {\tt0} & \hspace*{4em} \\
& $|$ & {\tt(} $A$ {\tt)} \\
& $|$ & $A$ {\tt+} $A^{(1)}$ & (0) \\
& $|$ & $A^{(3)}$ {\tt*} $A^{(2)}$ & (2) \\
& $|$ & {\tt-} $A^{(3)}$ & (3)
\end{tabular}
\end{center}
\index{grammars!priority|)}
\begin{figure}
\begin{center}
\begin{tabular}{rclc}
$prop$ &=& \ttindex{PROP} $aprop$ ~~$|$~~ {\tt(} $prop$ {\tt)} \\
&$|$& $logic^{(3)}$ \ttindex{==} $logic^{(2)}$ & (2) \\
&$|$& $logic^{(3)}$ \ttindex{=?=} $logic^{(2)}$ & (2) \\
&$|$& $prop^{(2)}$ \ttindex{==>} $prop^{(1)}$ & (1) \\
&$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop^{(1)}$ & (1) \\
&$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\\\
$logic$ &=& $prop$ ~~$|$~~ $fun$ \\\\
$aprop$ &=& $id$ ~~$|$~~ $var$
~~$|$~~ $fun^{(max_pri)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\
$fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\
&$|$& $fun^{(max_pri)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\
&$|$& $fun^{(max_pri)}$ {\tt::} $type$ \\
&$|$& \ttindex{\%} $idts$ {\tt.} $logic$ & (0) \\\\
$idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
&$|$& $id$ \ttindex{::} $type$ & (0) \\\\
$type$ &=& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
~~$|$~~ $tvar$ {\tt::} $sort$ \\
&$|$& $id$ ~~$|$~~ $type^{(max_pri)}$ $id$
~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
&$|$& $type^{(1)}$ \ttindex{=>} $type$ & (0) \\
&$|$& {\tt[} $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0)\\
&$|$& {\tt(} $type$ {\tt)} \\\\
$sort$ &=& $id$ ~~$|$~~ {\tt\ttlbrace\ttrbrace}
~~$|$~~ {\tt\ttlbrace} $id$ {\tt,} \dots {\tt,} $id$ {\tt\ttrbrace}
\end{tabular}\index{*"!"!}\index{*"["|}\index{*"|"]}
\indexbold{type@$type$} \indexbold{sort@$sort$} \indexbold{idt@$idt$}
\indexbold{idts@$idts$} \indexbold{logic@$logic$} \indexbold{prop@$prop$}
\indexbold{fun@$fun$}
\end{center}
\caption{Meta-logic syntax}\label{fig:pure_gram}
\end{figure}
\section{The Pure syntax} \label{sec:basic_syntax}
\index{syntax!Pure|(}
At the root of all object-logics lies the Pure theory,\index{theory!Pure}
bound to the \ML{} identifier \ttindex{Pure.thy}. It contains, among many
other things, the Pure syntax. An informal account of this basic syntax
(meta-logic, types, \ldots) may be found in {\em Introduction to Isabelle}.
A more precise description using a priority grammar is shown in
Fig.\ts\ref{fig:pure_gram}. The following nonterminals are defined:
\begin{description}
\item[$prop$] Terms of type $prop$. These are formulae of the meta-logic.
\item[$aprop$] Atomic propositions. These typically include the
judgement forms of the object-logic; its definition introduces a
meta-level predicate for each judgement form.
\item[$logic$] Terms whose type belongs to class $logic$. Initially,
this category contains just $prop$. As the syntax is extended by new
object-logics, more productions for $logic$ are added automatically
(see below).
\item[$fun$] Terms potentially of function type.
\item[$type$] Types of the meta-logic.
\item[$idts$] A list of identifiers, possibly constrained by types.
\end{description}
\begin{warn}
Note that \verb|x::nat y| is parsed as \verb|x::(nat y)|, treating {\tt
y} like a type constructor applied to {\tt nat}. The likely result is
an error message. To avoid this interpretation, use parentheses and
write \verb|(x::nat) y|.
Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and
yields a syntax error. The correct form is \verb|(x::nat) (y::nat)|.
\end{warn}
\subsection{Logical types and default syntax}\label{logical-types}
Isabelle's representation of mathematical languages is based on the typed
$\lambda$-calculus. All logical types, namely those of class $logic$, are
automatically equipped with a basic syntax of types, identifiers,
variables, parentheses, $\lambda$-abstractions and applications.
More precisely, for each type constructor $ty$ with arity $(\vec{s})c$,
where $c$ is a subclass of $logic$, several productions are added:
\begin{center}
\begin{tabular}{rclc}
$ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
&$|$& $fun^{(max_pri)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\
&$|$& $ty^{(max_pri)}$ {\tt::} $type$\\\\
$logic$ &=& $ty$
\end{tabular}
\end{center}
\subsection{Lexical matters}
The parser does not process input strings directly. It operates on token
lists provided by Isabelle's \bfindex{lexer}. There are two kinds of
tokens: \bfindex{delimiters} and \bfindex{name tokens}.
Delimiters can be regarded as reserved words of the syntax. You can
add new ones when extending theories. In Fig.\ts\ref{fig:pure_gram} they
appear in typewriter font, for example {\tt ==}, {\tt =?=} and
{\tt PROP}\@.
Name tokens have a predefined syntax. The lexer distinguishes four
disjoint classes of names: \rmindex{identifiers}, \rmindex{unknowns}, type
identifiers\index{identifiers!type}, type unknowns\index{unknowns!type}.
They are denoted by $id$\index{id@$id$}, $var$\index{var@$var$},
$tid$\index{tid@$tid$}, $tvar$\index{tvar@$tvar$}, respectively. Typical
examples are {\tt x}, {\tt ?x7}, {\tt 'a}, {\tt ?'a3}. Here is the precise
syntax:
\begin{eqnarray*}
id & = & letter~quasiletter^* \\
var & = & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\
tid & = & \mbox{\tt '}id \\
tvar & = & \mbox{\tt ?}tid ~~|~~
\mbox{\tt ?}tid\mbox{\tt .}nat \\[1ex]
letter & = & \mbox{one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z}} \\
digit & = & \mbox{one of {\tt 0}\dots {\tt 9}} \\
quasiletter & = & letter ~~|~~ digit ~~|~~ \mbox{\tt _} ~~|~~ \mbox{\tt '} \\
nat & = & digit^+
\end{eqnarray*}
A $var$ or $tvar$ describes an unknown, which is internally a pair
of base name and index (\ML\ type \ttindex{indexname}). These components are
either separated by a dot as in {\tt ?x.1} or {\tt ?x7.3} or
run together as in {\tt ?x1}. The latter form is possible if the
base name does not end with digits. If the index is 0, it may be dropped
altogether: {\tt ?x} abbreviates both {\tt ?x0} and {\tt ?x.0}.
The lexer repeatedly takes the maximal prefix of the input string that
forms a valid token. A maximal prefix that is both a delimiter and a name
is treated as a delimiter. Spaces, tabs and newlines are separators; they
never occur within tokens.
Delimiters need not be separated by white space. For example, if {\tt -}
is a delimiter but {\tt --} is not, then the string {\tt --} is treated as
two consecutive occurrences of the token~{\tt -}. In contrast, \ML\
treats {\tt --} as a single symbolic name. The consequence of Isabelle's
more liberal scheme is that the same string may be parsed in different ways
after extending the syntax: after adding {\tt --} as a delimiter, the input
{\tt --} is treated as a single token.
Name tokens are terminal symbols, strictly speaking, but we can generally
regard them as nonterminals. This is because a name token carries with it
useful information, the name. Delimiters, on the other hand, are nothing
but than syntactic sugar.
\subsection{*Inspecting the syntax}
\begin{ttbox}
syn_of : theory -> Syntax.syntax
Syntax.print_syntax : Syntax.syntax -> unit
Syntax.print_gram : Syntax.syntax -> unit
Syntax.print_trans : Syntax.syntax -> unit
\end{ttbox}
The abstract type \ttindex{Syntax.syntax} allows manipulation of syntaxes
in \ML. You can display values of this type by calling the following
functions:
\begin{description}
\item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle
theory~{\it thy} as an \ML\ value.
\item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all
information contained in the syntax {\it syn}. The displayed output can
be large. The following two functions are more selective.
\item[\ttindexbold{Syntax.print_gram} {\it syn}] shows the grammar part
of~{\it syn}, namely the lexicon, roots and productions.
\item[\ttindexbold{Syntax.print_trans} {\it syn}] shows the translation
part of~{\it syn}, namely the constants, parse/print macros and
parse/print translations.
\end{description}
Let us demonstrate these functions by inspecting Pure's syntax. Even that
is too verbose to display in full.
\begin{ttbox}
Syntax.print_syntax (syn_of Pure.thy);
{\out lexicon: "!!" "\%" "(" ")" "," "." "::" ";" "==" "==>" \dots}
{\out roots: logic type fun prop}
{\out prods:}
{\out type = tid (1000)}
{\out type = tvar (1000)}
{\out type = id (1000)}
{\out type = tid "::" sort[0] => "_ofsort" (1000)}
{\out type = tvar "::" sort[0] => "_ofsort" (1000)}
{\out \vdots}
\ttbreak
{\out consts: "_K" "_appl" "_aprop" "_args" "_asms" "_bigimpl" \dots}
{\out parse_ast_translation: "_appl" "_bigimpl" "_bracket"}
{\out "_idtyp" "_lambda" "_tapp" "_tappl"}
{\out parse_rules:}
{\out parse_translation: "!!" "_K" "_abs" "_aprop"}
{\out print_translation: "all"}
{\out print_rules:}
{\out print_ast_translation: "==>" "_abs" "_idts" "fun"}
\end{ttbox}
As you can see, the output is divided into labeled sections. The grammar
is represented by {\tt lexicon}, {\tt roots} and {\tt prods}. The rest
refers to syntactic translations and macro expansion. Here is an
explanation of the various sections.
\begin{description}
\item[\ttindex{lexicon}] lists the delimiters used for lexical
analysis.\index{delimiters}
\item[\ttindex{roots}] lists the grammar's nonterminal symbols. You must
name the desired root when calling lower level functions or specifying
macros. Higher level functions usually expect a type and derive the
actual root as described in~\S\ref{sec:grammar}.
\item[\ttindex{prods}] lists the productions of the priority grammar.
The nonterminal $A^{(n)}$ is rendered in {\sc ascii} as {\tt $A$[$n$]}.
Each delimiter is quoted. Some productions are shown with {\tt =>} and
an attached string. These strings later become the heads of parse
trees; they also play a vital role when terms are printed (see
\S\ref{sec:asts}).
Productions with no strings attached are called {\bf copy
productions}\indexbold{productions!copy}. Their right-hand side must
have exactly one nonterminal symbol (or name token). The parser does
not create a new parse tree node for copy productions, but simply
returns the parse tree of the right-hand symbol.
If the right-hand side consists of a single nonterminal with no
delimiters, then the copy production is called a {\bf chain
production}\indexbold{productions!chain}. Chain productions should
be seen as abbreviations: conceptually, they are removed from the
grammar by adding new productions. Priority information
attached to chain productions is ignored, only the dummy value $-1$ is
displayed.
\item[\ttindex{consts}, \ttindex{parse_rules}, \ttindex{print_rules}]
relate to macros (see \S\ref{sec:macros}).
\item[\ttindex{parse_ast_translation}, \ttindex{print_ast_translation}]
list sets of constants that invoke translation functions for abstract
syntax trees. Section \S\ref{sec:asts} below discusses this obscure
matter.
\item[\ttindex{parse_translation}, \ttindex{print_translation}] list sets
of constants that invoke translation functions for terms (see
\S\ref{sec:tr_funs}).
\end{description}
\index{syntax!Pure|)}
\section{Mixfix declarations} \label{sec:mixfix}
\index{mixfix declaration|(}
When defining a theory, you declare new constants by giving their names,
their type, and an optional {\bf mixfix annotation}. Mixfix annotations
allow you to extend Isabelle's basic $\lambda$-calculus syntax with
readable notation. They can express any context-free priority grammar.
Isabelle syntax definitions are inspired by \OBJ~\cite{OBJ}; they are more
general than the priority declarations of \ML\ and Prolog.
A mixfix annotation defines a production of the priority grammar. It
describes the concrete syntax, the translation to abstract syntax, and the
pretty printing. Special case annotations provide a simple means of
specifying infix operators, binders and so forth.
\subsection{Grammar productions}\label{sec:grammar}
Let us examine the treatment of the production
\[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\, A@2^{(p@2)}\, \ldots\,
A@n^{(p@n)}\, w@n. \]
Here $A@i^{(p@i)}$ is a nonterminal with priority~$p@i$ for $i=1$,
\ldots,~$n$, while $w@0$, \ldots,~$w@n$ are strings of terminals.
In the corresponding mixfix annotation, the priorities are given separately
as $[p@1,\ldots,p@n]$ and~$p$. The nonterminal symbols are identified with
types~$\tau$, $\tau@1$, \ldots,~$\tau@n$ respectively, and the production's
effect on nonterminals is expressed as the function type
\[ [\tau@1, \ldots, \tau@n]\To \tau. \]
Finally, the template
\[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n \]
describes the strings of terminals.
A simple type is typically declared for each nonterminal symbol. In
first-order logic, type~$i$ stands for terms and~$o$ for formulae. Only
the outermost type constructor is taken into account. For example, any
type of the form $\sigma list$ stands for a list; productions may refer
to the symbol {\tt list} and will apply lists of any type.
The symbol associated with a type is called its {\bf root} since it may
serve as the root of a parse tree. Precisely, the root of $(\tau@1, \dots,
\tau@n)ty$ is $ty$, where $\tau@1$, \ldots, $\tau@n$ are types and $ty$ is
a type constructor. Type infixes are a special case of this; in
particular, the root of $\tau@1 \To \tau@2$ is {\tt fun}. Finally, the
root of a type variable is {\tt logic}; general productions might
refer to this nonterminal.
Identifying nonterminals with types allows a constant's type to specify
syntax as well. We can declare the function~$f$ to have type $[\tau@1,
\ldots, \tau@n]\To \tau$ and, through a mixfix annotation, specify the
layout of the function's $n$ arguments. The constant's name, in this
case~$f$, will also serve as the label in the abstract syntax tree. There
are two exceptions to this treatment of constants:
\begin{enumerate}
\item A production need not map directly to a logical function. In this
case, you must declare a constant whose purpose is purely syntactic.
By convention such constants begin with the symbol~{\tt\at},
ensuring that they can never be written in formulae.
\item A copy production has no associated constant.
\end{enumerate}
There is something artificial about this representation of productions,
but it is convenient, particularly for simple theory extensions.
\subsection{The general mixfix form}
Here is a detailed account of the general \bfindex{mixfix declaration} as
it may occur within the {\tt consts} section of a {\tt .thy} file.
\begin{center}
{\tt "$c$" ::\ "$\sigma$" ("$template$" $ps$ $p$)}
\end{center}
This constant declaration and mixfix annotation is interpreted as follows:
\begin{itemize}
\item The string {\tt "$c$"} is the name of the constant associated with
the production. If $c$ is empty (given as~{\tt ""}) then this is a copy
production.\index{productions!copy} Otherwise, parsing an instance of the
phrase $template$ generates the \AST{} {\tt ("$c$" $a@1$ $\ldots$
$a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th
argument.
\item The constant $c$, if non-empty, is declared to have type $\sigma$.
\item The string $template$ specifies the right-hand side of
the production. It has the form
\[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n, \]
where each occurrence of \ttindex{_} denotes an
argument\index{argument!mixfix} position and the~$w@i$ do not
contain~{\tt _}. (If you want a literal~{\tt _} in the concrete
syntax, you must escape it as described below.) The $w@i$ may
consist of \rmindex{delimiters}, spaces or \rmindex{pretty
printing} annotations (see below).
\item The type $\sigma$ specifies the production's nonterminal symbols (or name
tokens). If $template$ is of the form above then $\sigma$ must be a
function type with at least~$n$ argument positions, say $\sigma =
[\tau@1, \dots, \tau@n] \To \tau$. Nonterminal symbols are derived
from the type $\tau@1$, \ldots,~$\tau@n$, $\tau$ as described above.
Any of these may be function types; the corresponding root is then {\tt
fun}.
\item The optional list~$ps$ may contain at most $n$ integers, say {\tt
[$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal
priority\indexbold{priorities} required of any phrase that may appear
as the $i$-th argument. Missing priorities default to~$0$.
\item The integer $p$ is the priority of this production. If omitted, it
defaults to the maximal priority.
Priorities, or precedences, range between $0$ and
$max_pri$\indexbold{max_pri@$max_pri$} (= 1000).
\end{itemize}
The declaration {\tt $c$ ::\ "$\sigma$" ("$template$")} specifies no
priorities. The resulting production puts no priority constraints on any
of its arguments and has maximal priority itself. Omitting priorities in
this manner will introduce syntactic ambiguities unless the production's
right-hand side is fully bracketed, as in \verb|"if _ then _ else _ fi"|.
\begin{warn}
Theories must sometimes declare types for purely syntactic purposes. One
example is {\tt type}, the built-in type of types. This is a `type of
all types' in the syntactic sense only. Do not declare such types under
{\tt arities} as belonging to class $logic$, for that would allow their
use in arbitrary Isabelle expressions~(\S\ref{logical-types}).
\end{warn}
\subsection{Example: arithmetic expressions}
This theory specification contains a {\tt consts} section with mixfix
declarations encoding the priority grammar from
\S\ref{sec:priority_grammars}:
\begin{ttbox}
EXP = Pure +
types
exp
arities
exp :: logic
consts
"0" :: "exp" ("0" 9)
"+" :: "[exp, exp] => exp" ("_ + _" [0, 1] 0)
"*" :: "[exp, exp] => exp" ("_ * _" [3, 2] 2)
"-" :: "exp => exp" ("- _" [3] 3)
end
\end{ttbox}
Note that the {\tt arities} declaration causes {\tt exp} to be added to the
syntax' roots. If you put the text above into a file {\tt exp.thy} and load
it via {\tt use_thy "EXP"}, you can run some tests:
\begin{ttbox}
val read_exp = Syntax.test_read (syn_of EXP.thy) "exp";
{\out val it = fn : string -> unit}
read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";
{\out tokens: "0" "*" "0" "*" "0" "*" "0" "+" "0" "+" "0" "+" "0"}
{\out raw: ("+" ("+" ("+" ("*" "0" ("*" "0" ("*" "0" "0"))) "0") "0") "0")}
{\out \vdots}
read_exp "0 + - 0 + 0";
{\out tokens: "0" "+" "-" "0" "+" "0"}
{\out raw: ("+" ("+" "0" ("-" "0")) "0")}
{\out \vdots}
\end{ttbox}
The output of \ttindex{Syntax.test_read} includes the token list ({\tt
tokens}) and the raw \AST{} directly derived from the parse tree,
ignoring parse \AST{} translations. The rest is tracing information
provided by the macro expander (see \S\ref{sec:macros}).
Executing {\tt Syntax.print_gram} reveals the productions derived
from our mixfix declarations (lots of additional information deleted):
\begin{ttbox}
Syntax.print_gram (syn_of EXP.thy);
{\out exp = "0" => "0" (9)}
{\out exp = exp[0] "+" exp[1] => "+" (0)}
{\out exp = exp[3] "*" exp[2] => "*" (2)}
{\out exp = "-" exp[3] => "-" (3)}
\end{ttbox}
\subsection{The mixfix template}
Let us take a closer look at the string $template$ appearing in mixfix
annotations. This string specifies a list of parsing and printing
directives: delimiters\index{delimiter}, arguments\index{argument!mixfix},
spaces, blocks of indentation and line breaks. These are encoded via the
following character sequences:
\index{pretty printing|(}
\begin{description}
\item[~\ttindex_~] An argument\index{argument!mixfix} position, which
stands for a nonterminal symbol or name token.
\item[~$d$~] A \rmindex{delimiter}, namely a non-empty sequence of
non-special or escaped characters. Escaping a character\index{escape
character} means preceding it with a {\tt '} (single quote). Thus
you have to write {\tt ''} if you really want a single quote. You must
also escape {\tt _}, {\tt (}, {\tt )} and {\tt /}. Delimiters may
never contain white space, though.
\item[~$s$~] A non-empty sequence of spaces for printing. This
and the following specifications do not affect parsing at all.
\item[~{\ttindex($n$}~] Open a pretty printing block. The optional
number $n$ specifies how much indentation to add when a line break
occurs within the block. If {\tt(} is not followed by digits, the
indentation defaults to~$0$.
\item[~\ttindex)~] Close a pretty printing block.
\item[~\ttindex{//}~] Force a line break.
\item[~\ttindex/$s$~] Allow a line break. Here $s$ stands for the string
of spaces (zero or more) right after the {\tt /} character. These
spaces are printed if the break is not taken.
\end{description}
Isabelle's pretty printer resembles the one described in
Paulson~\cite{paulson91}. \index{pretty printing|)}
\subsection{Infixes}
\indexbold{infix operators}
Infix operators associating to the left or right can be declared
using {\tt infixl} or {\tt infixr}.
Roughly speaking, the form {\tt $c$ ::\ "$\sigma$" (infixl $p$)}
abbreviates the declarations
\begin{ttbox}
"op \(c\)" :: "\(\sigma\)" ("op \(c\)")
"op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
\end{ttbox}
and {\tt $c$ ::\ "$\sigma$" (infixr $p$)} abbreviates the declarations
\begin{ttbox}
"op \(c\)" :: "\(\sigma\)" ("op \(c\)")
"op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
\end{ttbox}
The infix operator is declared as a constant with the prefix {\tt op}.
Thus, prefixing infixes with \ttindex{op} makes them behave like ordinary
function symbols, as in \ML. Special characters occurring in~$c$ must be
escaped, as in delimiters, using a single quote.
The expanded forms above would be actually illegal in a {\tt .thy} file
because they declare the constant \hbox{\tt"op \(c\)"} twice.
\subsection{Binders}
\indexbold{binders}
\begingroup
\def\Q{{\cal Q}}
A {\bf binder} is a variable-binding construct such as a quantifier. The
binder declaration \indexbold{*binder}
\begin{ttbox}
\(c\) :: "\(\sigma\)" (binder "\(\Q\)" \(p\))
\end{ttbox}
introduces a constant~$c$ of type~$\sigma$, which must have the form
$(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where
$x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$
and the whole term has type~$\tau@3$. Special characters in $\Q$ must be
escaped using a single quote.
Let us declare the quantifier~$\forall$:
\begin{ttbox}
All :: "('a => o) => o" (binder "ALL " 10)
\end{ttbox}
This let us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL
$x$.$P$}. When printing, Isabelle prefers the latter form, but must fall
back on $\mtt{All}(P)$ if $P$ is not an abstraction. Both $P$ and {\tt ALL
$x$.$P$} have type~$o$, the type of formulae, while the bound variable
can be polymorphic.
The binder~$c$ of type $(\sigma \To \tau) \To \tau$ can be nested. The
external form $\Q~x@1~x@2 \ldots x@n. P$ corresponds to the internal form
\[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)) \]
\medskip
The general binder declaration
\begin{ttbox}
\(c\) :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)" (binder "\(\Q\)" \(p\))
\end{ttbox}
is internally expanded to
\begin{ttbox}
\(c\) :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"
"\(\Q\)"\hskip-3pt :: "[idts, \(\tau@2\)] => \(\tau@3\)" ("(3\(\Q\)_./ _)" \(p\))
\end{ttbox}
with $idts$ being the nonterminal symbol for a list of $id$s optionally
constrained (see Fig.\ts\ref{fig:pure_gram}). The declaration also
installs a parse translation\index{translations!parse} for~$\Q$ and a print
translation\index{translations!print} for~$c$ to translate between the
internal and external forms.
\endgroup
\index{mixfix declaration|)}
\section{Example: some minimal logics} \label{sec:min_logics}
This section presents some examples that have a simple syntax. They
demonstrate how to define new object-logics from scratch.
First we must define how an object-logic syntax embedded into the
meta-logic. Since all theorems must conform to the syntax for~$prop$ (see
Fig.\ts\ref{fig:pure_gram}), that syntax has to be extended with the
object-level syntax. Assume that the syntax of your object-logic defines a
nonterminal symbol~$o$ of formulae. These formulae can now appear in
axioms and theorems wherever $prop$ does if you add the production
\[ prop ~=~ o. \]
This is not a copy production but a coercion from formulae to propositions:
\begin{ttbox}
Base = Pure +
types
o
arities
o :: logic
consts
Trueprop :: "o => prop" ("_" 5)
end
\end{ttbox}
The constant {\tt Trueprop} (the name is arbitrary) acts as an invisible
coercion function. Assuming this definition resides in a file {\tt base.thy},
you have to load it with the command {\tt use_thy "Base"}.
One of the simplest nontrivial logics is {\bf minimal logic} of
implication. Its definition in Isabelle needs no advanced features but
illustrates the overall mechanism nicely:
\begin{ttbox}
Hilbert = Base +
consts
"-->" :: "[o, o] => o" (infixr 10)
rules
K "P --> Q --> P"
S "(P --> Q --> R) --> (P --> Q) --> P --> R"
MP "[| P --> Q; P |] ==> Q"
end
\end{ttbox}
After loading this definition from the file {\tt hilbert.thy}, you can
start to prove theorems in the logic:
\begin{ttbox}
goal Hilbert.thy "P --> P";
{\out Level 0}
{\out P --> P}
{\out 1. P --> P}
\ttbreak
by (resolve_tac [Hilbert.MP] 1);
{\out Level 1}
{\out P --> P}
{\out 1. ?P --> P --> P}
{\out 2. ?P}
\ttbreak
by (resolve_tac [Hilbert.MP] 1);
{\out Level 2}
{\out P --> P}
{\out 1. ?P1 --> ?P --> P --> P}
{\out 2. ?P1}
{\out 3. ?P}
\ttbreak
by (resolve_tac [Hilbert.S] 1);
{\out Level 3}
{\out P --> P}
{\out 1. P --> ?Q2 --> P}
{\out 2. P --> ?Q2}
\ttbreak
by (resolve_tac [Hilbert.K] 1);
{\out Level 4}
{\out P --> P}
{\out 1. P --> ?Q2}
\ttbreak
by (resolve_tac [Hilbert.K] 1);
{\out Level 5}
{\out P --> P}
{\out No subgoals!}
\end{ttbox}
As we can see, this Hilbert-style formulation of minimal logic is easy to
define but difficult to use. The following natural deduction formulation is
better:
\begin{ttbox}
MinI = Base +
consts
"-->" :: "[o, o] => o" (infixr 10)
rules
impI "(P ==> Q) ==> P --> Q"
impE "[| P --> Q; P |] ==> Q"
end
\end{ttbox}
Note, however, that although the two systems are equivalent, this fact
cannot be proved within Isabelle. Axioms {\tt S} and {\tt K} can be
derived in {\tt MinI} (exercise!), but {\tt impI} cannot be derived in {\tt
Hilbert}. The reason is that {\tt impI} is only an {\bf admissible} rule
in {\tt Hilbert}, something that can only be shown by induction over all
possible proofs in {\tt Hilbert}.
We may easily extend minimal logic with falsity:
\begin{ttbox}
MinIF = MinI +
consts
False :: "o"
rules
FalseE "False ==> P"
end
\end{ttbox}
On the other hand, we may wish to introduce conjunction only:
\begin{ttbox}
MinC = Base +
consts
"&" :: "[o, o] => o" (infixr 30)
\ttbreak
rules
conjI "[| P; Q |] ==> P & Q"
conjE1 "P & Q ==> P"
conjE2 "P & Q ==> Q"
end
\end{ttbox}
And if we want to have all three connectives together, we create and load a
theory file consisting of a single line:\footnote{We can combine the
theories without creating a theory file using the ML declaration
\begin{ttbox}
val MinIFC_thy = merge_theories(MinIF,MinC)
\end{ttbox}
\index{*merge_theories|fnote}}
\begin{ttbox}
MinIFC = MinIF + MinC
\end{ttbox}
Now we can prove mixed theorems like
\begin{ttbox}
goal MinIFC.thy "P & False --> Q";
by (resolve_tac [MinI.impI] 1);
by (dresolve_tac [MinC.conjE2] 1);
by (eresolve_tac [MinIF.FalseE] 1);
\end{ttbox}
Try this as an exercise!
\medskip
Unless you need to define macros or syntax translation functions, you may
skip the rest of this chapter.
\section{*Abstract syntax trees} \label{sec:asts}
\index{trees!abstract syntax|(} The parser, given a token list from the
lexer, applies productions to yield a parse tree\index{trees!parse}. By
applying some internal transformations the parse tree becomes an abstract
syntax tree, or \AST{}. Macro expansion, further translations and finally
type inference yields a well-typed term\index{terms!obtained from ASTs}.
The printing process is the reverse, except for some subtleties to be
discussed later.
Figure~\ref{fig:parse_print} outlines the parsing and printing process.
Much of the complexity is due to the macro mechanism. Using macros, you
can specify most forms of concrete syntax without writing any \ML{} code.
\begin{figure}
\begin{center}
\begin{tabular}{cl}
string & \\
$\downarrow$ & parser \\
parse tree & \\
$\downarrow$ & parse \AST{} translation \\
\AST{} & \\
$\downarrow$ & \AST{} rewriting (macros) \\
\AST{} & \\
$\downarrow$ & parse translation, type inference \\
--- well-typed term --- & \\
$\downarrow$ & print translation \\
\AST{} & \\
$\downarrow$ & \AST{} rewriting (macros) \\
\AST{} & \\
$\downarrow$ & print \AST{} translation, printer \\
string &
\end{tabular}
\index{translations!parse}\index{translations!parse AST}
\index{translations!print}\index{translations!print AST}
\end{center}
\caption{Parsing and printing}\label{fig:parse_print}
\end{figure}
Abstract syntax trees are an intermediate form between the raw parse trees
and the typed $\lambda$-terms. An \AST{} is either an atom (constant or
variable) or a list of {\em at least two\/} subtrees. Internally, they
have type \ttindex{Syntax.ast}: \index{*Constant} \index{*Variable}
\index{*Appl}
\begin{ttbox}
datatype ast = Constant of string
| Variable of string
| Appl of ast list
\end{ttbox}
Isabelle uses an S-expression syntax for abstract syntax trees. Constant
atoms are shown as quoted strings, variable atoms as non-quoted strings and
applications as a parenthesized list of subtrees. For example, the \AST
\begin{ttbox}
Appl [Constant "_constrain",
Appl [Constant "_abs", Variable "x", Variable "t"],
Appl [Constant "fun", Variable "'a", Variable "'b"]]
\end{ttbox}
is shown as {\tt ("_constrain" ("_abs" x t) ("fun" 'a 'b))}.
Both {\tt ()} and {\tt (f)} are illegal because they have too few
subtrees.
The resemblance of Lisp's S-expressions is intentional, but there are two
kinds of atomic symbols: $\Constant x$ and $\Variable x$. Do not take the
names ``{\tt Constant}'' and ``{\tt Variable}'' too literally; in the later
translation to terms, $\Variable x$ may become a constant, free or bound
variable, even a type constructor or class name; the actual outcome depends
on the context.
Similarly, you can think of ${\tt (} f~x@1~\ldots~x@n{\tt )}$ as the
application of~$f$ to the arguments $x@1, \ldots, x@n$. But the kind of
application is determined later by context; it could be a type constructor
applied to types.
Forms like {\tt (("_abs" x $t$) $u$)} are legal, but \AST{}s are
first-order: the {\tt "_abs"} does not bind the {\tt x} in any way. Later
at the term level, {\tt ("_abs" x $t$)} will become an {\tt Abs} node and
occurrences of {\tt x} in $t$ will be replaced by bound variables (the term
constructor \ttindex{Bound}).
\subsection{Transforming parse trees to \AST{}s}
The parse tree is the raw output of the parser. Translation functions,
called {\bf parse AST translations}\indexbold{translations!parse AST},
transform the parse tree into an abstract syntax tree.
The parse tree is constructed by nesting the right-hand sides of the
productions used to recognize the input. Such parse trees are simply lists
of tokens and constituent parse trees, the latter representing the
nonterminals of the productions. Let us refer to the actual productions in
the form displayed by {\tt Syntax.print_syntax}.
Ignoring parse \AST{} translations, parse trees are transformed to \AST{}s
by stripping out delimiters and copy productions. More precisely, the
mapping $ast_of_pt$\index{ast_of_pt@$ast_of_pt$} is derived from the
productions as follows:
\begin{itemize}
\item Name tokens: $ast_of_pt(t) = \Variable s$, where $t$ is an $id$,
$var$, $tid$ or $tvar$ token, and $s$ its associated string.
\item Copy productions: $ast_of_pt(\ldots P \ldots) = ast_of_pt(P)$.
Here $\ldots$ stands for strings of delimiters, which are
discarded. $P$ stands for the single constituent that is not a
delimiter; it is either a nonterminal symbol or a name token.
\item $0$-ary productions: $ast_of_pt(\ldots \mtt{=>} c) = \Constant c$.
Here there are no constituents other than delimiters, which are
discarded.
\item $n$-ary productions, where $n \ge 1$: delimiters are discarded and
the remaining constituents $P@1$, \ldots, $P@n$ are built into an
application whose head constant is~$c$:
\begin{eqnarray*}
\lefteqn{ast_of_pt(\ldots P@1 \ldots P@n \ldots \mtt{=>} c)} \\
&&\qquad{}= \Appl{\Constant c, ast_of_pt(P@1), \ldots, ast_of_pt(P@n)}
\end{eqnarray*}
\end{itemize}
Figure~\ref{fig:parse_ast} presents some simple examples, where {\tt ==},
{\tt _appl}, {\tt _args}, and so forth name productions of the Pure syntax.
These examples illustrate the need for further translations to make \AST{}s
closer to the typed $\lambda$-calculus. The Pure syntax provides
predefined parse \AST{} translations\index{translations!parse AST} for
ordinary applications, type applications, nested abstractions, meta
implications and function types. Figure~\ref{fig:parse_ast_tr} shows their
effect on some representative input strings.
\begin{figure}
\begin{center}
\tt\begin{tabular}{ll}
\rm input string & \rm \AST \\\hline
"f" & f \\
"'a" & 'a \\
"t == u" & ("==" t u) \\
"f(x)" & ("_appl" f x) \\
"f(x, y)" & ("_appl" f ("_args" x y)) \\
"f(x, y, z)" & ("_appl" f ("_args" x ("_args" y z))) \\
"\%x y.\ t" & ("_lambda" ("_idts" x y) t) \\
\end{tabular}
\end{center}
\caption{Parsing examples using the Pure syntax}\label{fig:parse_ast}
\end{figure}
\begin{figure}
\begin{center}
\tt\begin{tabular}{ll}
\rm input string & \rm \AST{} \\\hline
"f(x, y, z)" & (f x y z) \\
"'a ty" & (ty 'a) \\
"('a, 'b) ty" & (ty 'a 'b) \\
"\%x y z.\ t" & ("_abs" x ("_abs" y ("_abs" z t))) \\
"\%x ::\ 'a.\ t" & ("_abs" ("_constrain" x 'a) t) \\
"[| P; Q; R |] => S" & ("==>" P ("==>" Q ("==>" R S))) \\
"['a, 'b, 'c] => 'd" & ("fun" 'a ("fun" 'b ("fun" 'c 'd)))
\end{tabular}
\end{center}
\caption{Built-in parse \AST{} translations}\label{fig:parse_ast_tr}
\end{figure}
The names of constant heads in the \AST{} control the translation process.
The list of constants invoking parse \AST{} translations appears in the
output of {\tt Syntax.print_syntax} under {\tt parse_ast_translation}.
\subsection{Transforming \AST{}s to terms}
The \AST{}, after application of macros (see \S\ref{sec:macros}), is
transformed into a term. This term is probably ill-typed since type
inference has not occurred yet. The term may contain type constraints
consisting of applications with head {\tt "_constrain"}; the second
argument is a type encoded as a term. Type inference later introduces
correct types or rejects the input.
Another set of translation functions, namely parse
translations,\index{translations!parse}, may affect this process. If we
ignore parse translations for the time being, then \AST{}s are transformed
to terms by mapping \AST{} constants to constants, \AST{} variables to
schematic or free variables and \AST{} applications to applications.
More precisely, the mapping $term_of_ast$\index{term_of_ast@$term_of_ast$}
is defined by
\begin{itemize}
\item Constants: $term_of_ast(\Constant x) = \ttfct{Const} (x,
\mtt{dummyT})$.
\item Schematic variables: $term_of_ast(\Variable \mtt{"?}xi\mtt") =
\ttfct{Var} ((x, i), \mtt{dummyT})$, where $x$ is the base name and $i$
the index extracted from $xi$.
\item Free variables: $term_of_ast(\Variable x) = \ttfct{Free} (x,
\mtt{dummyT})$.
\item Function applications with $n$ arguments:
\begin{eqnarray*}
\lefteqn{term_of_ast(\Appl{f, x@1, \ldots, x@n})} \\
&&\qquad{}= term_of_ast(f) \ttapp
term_of_ast(x@1) \ttapp \ldots \ttapp term_of_ast(x@n)
\end{eqnarray*}
\end{itemize}
Here \ttindex{Const}, \ttindex{Var}, \ttindex{Free} and
\verb|$|\index{$@{\tt\$}} are constructors of the datatype {\tt term},
while \ttindex{dummyT} stands for some dummy type that is ignored during
type inference.
So far the outcome is still a first-order term. Abstractions and bound
variables (constructors \ttindex{Abs} and \ttindex{Bound}) are introduced
by parse translations. Such translations are attached to {\tt "_abs"},
{\tt "!!"} and user-defined binders.
\subsection{Printing of terms}
The output phase is essentially the inverse of the input phase. Terms are
translated via abstract syntax trees into strings. Finally the strings are
pretty printed.
Print translations (\S\ref{sec:tr_funs}) may affect the transformation of
terms into \AST{}s. Ignoring those, the transformation maps
term constants, variables and applications to the corresponding constructs
on \AST{}s. Abstractions are mapped to applications of the special
constant {\tt _abs}.
More precisely, the mapping $ast_of_term$\index{ast_of_term@$ast_of_term$}
is defined as follows:
\begin{itemize}
\item $ast_of_term(\ttfct{Const} (x, \tau)) = \Constant x$.
\item $ast_of_term(\ttfct{Free} (x, \tau)) = constrain (\Variable x,
\tau)$.
\item $ast_of_term(\ttfct{Var} ((x, i), \tau)) = constrain (\Variable
\mtt{"?}xi\mtt", \tau)$, where $\mtt?xi$ is the string representation of
the {\tt indexname} $(x, i)$.
\item For the abstraction $\lambda x::\tau.t$, let $x'$ be a variant
of~$x$ renamed to differ from all names occurring in~$t$, and let $t'$
be obtained from~$t$ by replacing all bound occurrences of~$x$ by
the free variable $x'$. This replaces corresponding occurrences of the
constructor \ttindex{Bound} by the term $\ttfct{Free} (x',
\mtt{dummyT})$:
\begin{eqnarray*}
\lefteqn{ast_of_term(\ttfct{Abs} (x, \tau, t))} \\
&&\qquad{}= \ttfct{Appl}
\mathopen{\mtt[}
\Constant \mtt{"_abs"}, constrain(\Variable x', \tau), \\
&&\qquad\qquad\qquad ast_of_term(t') \mathclose{\mtt]}.
\end{eqnarray*}
\item $ast_of_term(\ttfct{Bound} i) = \Variable \mtt{"B.}i\mtt"$.
The occurrence of constructor \ttindex{Bound} should never happen
when printing well-typed terms; it indicates a de Bruijn index with no
matching abstraction.
\item Where $f$ is not an application,
\begin{eqnarray*}
\lefteqn{ast_of_term(f \ttapp x@1 \ttapp \ldots \ttapp x@n)} \\
&&\qquad{}= \ttfct{Appl}
\mathopen{\mtt[} ast_of_term(f),
ast_of_term(x@1), \ldots,ast_of_term(x@n)
\mathclose{\mtt]}
\end{eqnarray*}
\end{itemize}
Type constraints are inserted to allow the printing of types, which is
governed by the boolean variable \ttindex{show_types}. Constraints are
treated as follows:
\begin{itemize}
\item $constrain(x, \tau) = x$, if $\tau = \mtt{dummyT}$ \index{*dummyT} or
\ttindex{show_types} not set to {\tt true}.
\item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, ty}$,
where $ty$ is the \AST{} encoding of $\tau$. That is, type constructors as
{\tt Constant}s, type identifiers as {\tt Variable}s and type applications
as {\tt Appl}s with the head type constructor as first element.
Additionally, if \ttindex{show_sorts} is set to {\tt true}, some type
variables are decorated with an \AST{} encoding of their sort.
\end{itemize}
The \AST{}, after application of macros (see \S\ref{sec:macros}), is
transformed into the final output string. The built-in {\bf print AST
translations}\indexbold{translations!print AST} effectively reverse the
parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}.
For the actual printing process, the names attached to productions
of the form $\ldots A^{(p@1)}@1 \ldots A^{(p@n)}@n \ldots \mtt{=>} c$ play
a vital role. Each \AST{} with constant head $c$, namely $\mtt"c\mtt"$ or
$(\mtt"c\mtt"~ x@1 \ldots x@n)$, is printed according to the production
for~$c$. Each argument~$x@i$ is converted to a string, and put in
parentheses if its priority~$(p@i)$ requires this. The resulting strings
and their syntactic sugar (denoted by ``\dots'' above) are joined to make a
single string.
If an application $(\mtt"c\mtt"~ x@1 \ldots x@m)$ has more arguments than the
corresponding production, it is first split into $((\mtt"c\mtt"~ x@1 \ldots
x@n) ~ x@{n+1} \ldots x@m)$. Applications with too few arguments or with
non-constant head or without a corresponding production are printed as
$f(x@1, \ldots, x@l)$ or $(\alpha@1, \ldots, \alpha@l) ty$. An occurrence of
$\Variable x$ is simply printed as~$x$.
Blanks are {\em not\/} inserted automatically. If blanks are required to
separate tokens, specify them in the mixfix declaration, possibly preceeded
by a slash~({\tt/}) to allow a line break.
\index{trees!abstract syntax|)}
\section{*Macros: Syntactic rewriting} \label{sec:macros}
\index{macros|(}\index{rewriting!syntactic|(}
Mixfix declarations alone can handle situations where there is a direct
connection between the concrete syntax and the underlying term. Sometimes
we require a more elaborate concrete syntax, such as quantifiers and list
notation. Isabelle's {\bf macros} and {\bf translation functions} can
perform translations such as
\begin{center}\tt
\begin{tabular}{r@{$\quad\protect\rightleftharpoons\quad$}l}
ALL x:A.P & Ball(A, \%x.P) \\ \relax
[x, y, z] & Cons(x, Cons(y, Cons(z, Nil)))
\end{tabular}
\end{center}
Translation functions (see \S\ref{sec:tr_funs}) must be coded in ML; they
are the most powerful translation mechanism but are difficult to read or
write. Macros are specified by first-order rewriting systems that operate
on abstract syntax trees. They are usually easy to read and write, and can
express all but the most obscure translations.
Figure~\ref{fig:set_trans} defines a fragment of first-order logic and set
theory.\footnote{This and the following theories are complete working
examples, though they specify only syntax, no axioms. The file {\tt
ZF/zf.thy} presents the full set theory definition, including many
macro rules.} Theory {\tt SET} defines constants for set comprehension
({\tt Collect}), replacement ({\tt Replace}) and bounded universal
quantification ({\tt Ball}). Each of these binds some variables. Without
additional syntax we should have to express $\forall x \in A. P$ as {\tt
Ball(A,\%x.P)}, and similarly for the others.
\begin{figure}
\begin{ttbox}
SET = Pure +
types
i, o
arities
i, o :: logic
consts
Trueprop :: "o => prop" ("_" 5)
Collect :: "[i, i => o] => i"
"{\at}Collect" :: "[idt, i, o] => i" ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
Replace :: "[i, [i, i] => o] => i"
"{\at}Replace" :: "[idt, idt, i, o] => i" ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
Ball :: "[i, i => o] => o"
"{\at}Ball" :: "[idt, i, o] => o" ("(3ALL _:_./ _)" 10)
translations
"{\ttlbrace}x:A. P{\ttrbrace}" == "Collect(A, \%x. P)"
"{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)"
"ALL x:A. P" == "Ball(A, \%x. P)"
end
\end{ttbox}
\caption{Macro example: set theory}\label{fig:set_trans}
\end{figure}
The theory specifies a variable-binding syntax through additional
productions that have mixfix declarations. Each non-copy production must
specify some constant, which is used for building \AST{}s. The additional
constants are decorated with {\tt\at} to stress their purely syntactic
purpose; they should never occur within the final well-typed terms.
Furthermore, they cannot be written in formulae because they are not legal
identifiers.
The translations cause the replacement of external forms by internal forms
after parsing, and vice versa before printing of terms. As a specification
of the set theory notation, they should be largely self-explanatory. The
syntactic constants, {\tt\at Collect}, {\tt\at Replace} and {\tt\at Ball},
appear implicitly in the macro rules via their mixfix forms.
Macros can define variable-binding syntax because they operate on \AST{}s,
which have no inbuilt notion of bound variable. The macro variables {\tt
x} and~{\tt y} have type~{\tt idt} and therefore range over identifiers,
in this case bound variables. The macro variables {\tt P} and~{\tt Q}
range over formulae containing bound variable occurrences.
Other applications of the macro system can be less straightforward, and
there are peculiarities. The rest of this section will describe in detail
how Isabelle macros are preprocessed and applied.
\subsection{Specifying macros}
Macros are basically rewrite rules on \AST{}s. But unlike other macro
systems found in programming languages, Isabelle's macros work in both
directions. Therefore a syntax contains two lists of rewrites: one for
parsing and one for printing.
The {\tt translations} section\index{translations section@{\tt translations}
section} specifies macros. The syntax for a macro is
\[ (root)\; string \quad
\left\{\begin{array}[c]{c} \mtt{=>} \\ \mtt{<=} \\ \mtt{==} \end{array}
\right\} \quad
(root)\; string
\]
%
This specifies a parse rule ({\tt =>}), a print rule ({\tt <=}), or both
({\tt ==}). The two strings specify the left and right-hand sides of the
macro rule. The $(root)$ specification is optional; it specifies the
nonterminal for parsing the $string$ and if omitted defaults to {\tt
logic}. \AST{} rewrite rules $(l, r)$ must obey certain conditions:
\begin{itemize}
\item Rules must be left linear: $l$ must not contain repeated variables.
\item Rules must have constant heads, namely $l = \mtt"c\mtt"$ or $l =
(\mtt"c\mtt" ~ x@1 \ldots x@n)$.
\item Every variable in~$r$ must also occur in~$l$.
\end{itemize}
Macro rules may refer to any syntax from the parent theories. They may
also refer to anything defined before the the {\tt .thy} file's {\tt
translations} section --- including any mixfix declarations.
Upon declaration, both sides of the macro rule undergo parsing and parse
\AST{} translations (see \S\ref{sec:asts}), but do not themselves undergo
macro expansion. The lexer runs in a different mode that additionally
accepts identifiers of the form $\_~letter~quasiletter^*$ (like {\tt _idt},
{\tt _K}). Thus, a constant whose name starts with an underscore can
appear in macro rules but not in ordinary terms.
Some atoms of the macro rule's \AST{} are designated as constants for
matching. These are all names that have been declared as classes, types or
constants.
The result of this preprocessing is two lists of macro rules, each stored
as a pair of \AST{}s. They can be viewed using {\tt Syntax.print_syntax}
(sections \ttindex{parse_rules} and \ttindex{print_rules}). For
theory~{\tt SET} of Fig.~\ref{fig:set_trans} these are
\begin{ttbox}
parse_rules:
("{\at}Collect" x A P) -> ("Collect" A ("_abs" x P))
("{\at}Replace" y x A Q) -> ("Replace" A ("_abs" x ("_abs" y Q)))
("{\at}Ball" x A P) -> ("Ball" A ("_abs" x P))
print_rules:
("Collect" A ("_abs" x P)) -> ("{\at}Collect" x A P)
("Replace" A ("_abs" x ("_abs" y Q))) -> ("{\at}Replace" y x A Q)
("Ball" A ("_abs" x P)) -> ("{\at}Ball" x A P)
\end{ttbox}
\begin{warn}
Avoid choosing variable names that have previously been used as
constants, types or type classes; the {\tt consts} section in the output
of {\tt Syntax.print_syntax} lists all such names. If a macro rule works
incorrectly, inspect its internal form as shown above, recalling that
constants appear as quoted strings and variables without quotes.
\end{warn}
\begin{warn}
If \ttindex{eta_contract} is set to {\tt true}, terms will be
$\eta$-contracted {\em before\/} the \AST{} rewriter sees them. Thus some
abstraction nodes needed for print rules to match may vanish. For example,
\verb|Ball(A, %x. P(x))| contracts {\tt Ball(A, P)}; the print rule does
not apply and the output will be {\tt Ball(A, P)}. This problem would not
occur if \ML{} translation functions were used instead of macros (as is
done for binder declarations).
\end{warn}
\begin{warn}
Another trap concerns type constraints. If \ttindex{show_types} is set to
{\tt true}, bound variables will be decorated by their meta types at the
binding place (but not at occurrences in the body). Matching with
\verb|Collect(A, %x. P)| binds {\tt x} to something like {\tt ("_constrain" y
"i")} rather than only {\tt y}. \AST{} rewriting will cause the constraint to
appear in the external form, say \verb|{y::i:A::i. P::o}|.
To allow such constraints to be re-read, your syntax should specify bound
variables using the nonterminal~\ttindex{idt}. This is the case in our
example. Choosing {\tt id} instead of {\tt idt} is a common error,
especially since it appears in former versions of most of Isabelle's
object-logics.
\end{warn}
\subsection{Applying rules}
As a term is being parsed or printed, an \AST{} is generated as an
intermediate form (recall Fig.\ts\ref{fig:parse_print}). The \AST{} is
normalized by applying macro rules in the manner of a traditional term
rewriting system. We first examine how a single rule is applied.
Let $t$ be the abstract syntax tree to be normalized and $(l, r)$ some
translation rule. A subtree~$u$ of $t$ is a {\bf redex} if it is an
instance of~$l$; in this case $l$ is said to {\bf match}~$u$. A redex
matched by $l$ may be replaced by the corresponding instance of~$r$, thus
{\bf rewriting} the \AST~$t$. Matching requires some notion of {\bf
place-holders} that may occur in rule patterns but not in ordinary
\AST{}s; {\tt Variable} atoms serve this purpose.
The matching of the object~$u$ by the pattern~$l$ is performed as follows:
\begin{itemize}
\item Every constant matches itself.
\item $\Variable x$ in the object matches $\Constant x$ in the pattern.
This point is discussed further below.
\item Every \AST{} in the object matches $\Variable x$ in the pattern,
binding~$x$ to~$u$.
\item One application matches another if they have the same number of
subtrees and corresponding subtrees match.
\item In every other case, matching fails. In particular, {\tt
Constant}~$x$ can only match itself.
\end{itemize}
A successful match yields a substitution that is applied to~$r$, generating
the instance that replaces~$u$.
The second case above may look odd. This is where {\tt Variable}s of
non-rule \AST{}s behave like {\tt Constant}s. Recall that \AST{}s are not
far removed from parse trees; at this level it is not yet known which
identifiers will become constants, bounds, frees, types or classes. As
\S\ref{sec:asts} describes, former parse tree heads appear in \AST{}s as
{\tt Constant}s, while $id$s, $var$s, $tid$s and $tvar$s become {\tt
Variable}s. On the other hand, when \AST{}s generated from terms for
printing, all constants and type constructors become {\tt Constant}s; see
\S\ref{sec:asts}. Thus \AST{}s may contain a messy mixture of {\tt
Variable}s and {\tt Constant}s. This is insignificant at macro level
because matching treats them alike.
Because of this behaviour, different kinds of atoms with the same name are
indistinguishable, which may make some rules prone to misbehaviour. Example:
\begin{ttbox}
types
Nil
consts
Nil :: "'a list"
"[]" :: "'a list" ("[]")
translations
"[]" == "Nil"
\end{ttbox}
The term {\tt Nil} will be printed as {\tt []}, just as expected. What
happens with \verb|%Nil.t| or {\tt x::Nil} is left as an exercise.
Normalizing an \AST{} involves repeatedly applying macro rules until none
is applicable. Macro rules are chosen in the order that they appear in the
{\tt translations} section. You can watch the normalization of \AST{}s
during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to
{\tt true}.\index{tracing!of macros} Alternatively, use
\ttindex{Syntax.test_read}. The information displayed when tracing
includes the \AST{} before normalization ({\tt pre}), redexes with results
({\tt rewrote}), the normal form finally reached ({\tt post}) and some
statistics ({\tt normalize}). If tracing is off,
\ttindex{Syntax.stat_norm_ast} can be set to {\tt true} in order to enable
printing of the normal form and statistics only.
\subsection{Example: the syntax of finite sets}
This example demonstrates the use of recursive macros to implement a
convenient notation for finite sets.
\begin{ttbox}
FINSET = SET +
types
is
consts
"" :: "i => is" ("_")
"{\at}Enum" :: "[i, is] => is" ("_,/ _")
empty :: "i" ("{\ttlbrace}{\ttrbrace}")
insert :: "[i, i] => i"
"{\at}Finset" :: "is => i" ("{\ttlbrace}(_){\ttrbrace}")
translations
"{\ttlbrace}x, xs{\ttrbrace}" == "insert(x, {\ttlbrace}xs{\ttrbrace})"
"{\ttlbrace}x{\ttrbrace}" == "insert(x, {\ttlbrace}{\ttrbrace})"
end
\end{ttbox}
Finite sets are internally built up by {\tt empty} and {\tt insert}. The
declarations above specify \verb|{x, y, z}| as the external representation
of
\begin{ttbox}
insert(x, insert(y, insert(z, empty)))
\end{ttbox}
The nonterminal symbol~{\tt is} stands for one or more objects of type~{\tt
i} separated by commas. The mixfix declaration \hbox{\verb|"_,/ _"|}
allows a line break after the comma for pretty printing; if no line break
is required then a space is printed instead.
The nonterminal is declared as the type~{\tt is}, but with no {\tt arities}
declaration. Hence {\tt is} is not a logical type and no default
productions are added. If we had needed enumerations of the nonterminal
{\tt logic}, which would include all the logical types, we could have used
the predefined nonterminal symbol \ttindex{args} and skipped this part
altogether. The nonterminal~{\tt is} can later be reused for other
enumerations of type~{\tt i} like lists or tuples.
Next follows {\tt empty}, which is already equipped with its syntax
\verb|{}|, and {\tt insert} without concrete syntax. The syntactic
constant {\tt\at Finset} provides concrete syntax for enumerations of~{\tt
i} enclosed in curly braces. Remember that a pair of parentheses, as in
\verb|"{(_)}"|, specifies a block of indentation for pretty printing.
The translations may look strange at first. Macro rules are best
understood in their internal forms:
\begin{ttbox}
parse_rules:
("{\at}Finset" ("{\at}Enum" x xs)) -> ("insert" x ("{\at}Finset" xs))
("{\at}Finset" x) -> ("insert" x "empty")
print_rules:
("insert" x ("{\at}Finset" xs)) -> ("{\at}Finset" ("{\at}Enum" x xs))
("insert" x "empty") -> ("{\at}Finset" x)
\end{ttbox}
This shows that \verb|{x, xs}| indeed matches any set enumeration of at least
two elements, binding the first to {\tt x} and the rest to {\tt xs}.
Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration.
The parse rules only work in the order given.
\begin{warn}
The \AST{} rewriter cannot discern constants from variables and looks
only for names of atoms. Thus the names of {\tt Constant}s occurring in
the (internal) left-hand side of translation rules should be regarded as
reserved keywords. Choose non-identifiers like {\tt\at Finset} or
sufficiently long and strange names. If a bound variable's name gets
rewritten, the result will be incorrect; for example, the term
\begin{ttbox}
\%empty insert. insert(x, empty)
\end{ttbox}
gets printed as \verb|%empty insert. {x}|.
\end{warn}
\subsection{Example: a parse macro for dependent types}\label{prod_trans}
As stated earlier, a macro rule may not introduce new {\tt Variable}s on
the right-hand side. Something like \verb|"K(B)" => "%x. B"| is illegal;
it allowed, it could cause variable capture. In such cases you usually
must fall back on translation functions. But a trick can make things
readable in some cases: {\em calling translation functions by parse
macros}:
\begin{ttbox}
PROD = FINSET +
consts
Pi :: "[i, i => i] => i"
"{\at}PROD" :: "[idt, i, i] => i" ("(3PROD _:_./ _)" 10)
"{\at}->" :: "[i, i] => i" ("(_ ->/ _)" [51, 50] 50)
\ttbreak
translations
"PROD x:A. B" => "Pi(A, \%x. B)"
"A -> B" => "Pi(A, _K(B))"
end
ML
val print_translation = [("Pi", dependent_tr' ("{\at}PROD", "{\at}->"))];
\end{ttbox}
Here {\tt Pi} is an internal constant for constructing general products.
Two external forms exist: the general case {\tt PROD x:A.B} and the
function space {\tt A -> B}, which abbreviates \verb|Pi(A, %x.B)| when {\tt B}
does not depend on~{\tt x}.
The second parse macro introduces {\tt _K(B)}, which later becomes \verb|%x.B|
due to a parse translation associated with \ttindex{_K}. The order of the
parse rules is critical. Unfortunately there is no such trick for
printing, so we have to add a {\tt ML} section for the print translation
\ttindex{dependent_tr'}.
Recall that identifiers with a leading {\tt _} are allowed in translation
rules, but not in ordinary terms. Thus we can create \AST{}s containing
names that are not directly expressible.
The parse translation for {\tt _K} is already installed in Pure, and {\tt
dependent_tr'} is exported by the syntax module for public use. See
\S\ref{sec:tr_funs} below for more of the arcane lore of translation functions.
\index{macros|)}\index{rewriting!syntactic|)}
\section{*Translation functions} \label{sec:tr_funs}
\index{translations|(}
%
This section describes the translation function mechanism. By writing
\ML{} functions, you can do almost everything with terms or \AST{}s during
parsing and printing. The logic \LK\ is a good example of sophisticated
transformations between internal and external representations of
associative sequences; here, macros would be useless.
A full understanding of translations requires some familiarity
with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
{\tt Syntax.ast} and the encodings of types and terms as such at the various
stages of the parsing or printing process. Most users should never need to
use translation functions.
\subsection{Declaring translation functions}
There are four kinds of translation functions. Each such function is
associated with a name, which triggers calls to it. Such names can be
constants (logical or syntactic) or type constructors.
{\tt Syntax.print_syntax} displays the sets of names associated with the
translation functions of a {\tt Syntax.syntax} under
\ttindex{parse_ast_translation}, \ttindex{parse_translation},
\ttindex{print_translation} and \ttindex{print_ast_translation}. You can
add new ones via the {\tt ML} section\index{ML section@{\tt ML} section} of
a {\tt .thy} file. There may never be more than one function of the same
kind per name. Conceptually, the {\tt ML} section should appear between
{\tt consts} and {\tt translations}; newly installed translation functions
are already effective when macros and logical rules are parsed.
The {\tt ML} section is copied verbatim into the \ML\ file generated from a
{\tt .thy} file. Definitions made here are accessible as components of an
\ML\ structure; to make some definitions private, use an \ML{} {\tt local}
declaration. The {\tt ML} section may install translation functions by
declaring any of the following identifiers:
\begin{ttbox}
val parse_ast_translation : (string * (ast list -> ast)) list
val print_ast_translation : (string * (ast list -> ast)) list
val parse_translation : (string * (term list -> term)) list
val print_translation : (string * (term list -> term)) list
\end{ttbox}
\subsection{The translation strategy}
All four kinds of translation functions are treated similarly. They are
called during the transformations between parse trees, \AST{}s and terms
(recall Fig.\ts\ref{fig:parse_print}). Whenever a combination of the form
$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation function
$f$ of appropriate kind exists for $c$, the result is computed by the \ML{}
function call $f \mtt[ x@1, \ldots, x@n \mtt]$.
For \AST{} translations, the arguments $x@1, \ldots, x@n$ are \AST{}s. A
combination has the form $\Constant c$ or $\Appl{\Constant c, x@1, \ldots,
x@n}$. For term translations, the arguments are terms and a combination
has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const} (c, \tau) \ttapp
x@1 \ttapp \ldots \ttapp x@n$. Terms allow more sophisticated
transformations than \AST{}s do, typically involving abstractions and bound
variables.
Regardless of whether they act on terms or \AST{}s,
parse translations differ from print translations fundamentally:
\begin{description}
\item[Parse translations] are applied bottom-up. The arguments are already
in translated form. The translations must not fail; exceptions trigger
an error message.
\item[Print translations] are applied top-down. They are supplied with
arguments that are partly still in internal form. The result again
undergoes translation; therefore a print translation should not introduce
as head the very constant that invoked it. The function may raise
exception \ttindex{Match} to indicate failure; in this event it has no
effect.
\end{description}
Only constant atoms --- constructor \ttindex{Constant} for \AST{}s and
\ttindex{Const} for terms --- can invoke translation functions. This
causes another difference between parsing and printing.
Parsing starts with a string and the constants are not yet identified.
Only parse tree heads create {\tt Constant}s in the resulting \AST; recall
$ast_of_pt$ in \S\ref{sec:asts}. Macros and parse \AST{} translations may
introduce further {\tt Constant}s. When the final \AST{} is converted to a
term, all {\tt Constant}s become {\tt Const}s; recall $term_of_ast$ in
\S\ref{sec:asts}.
Printing starts with a well-typed term and all the constants are known. So
all logical constants and type constructors may invoke print translations.
These, and macros, may introduce further constants.
\subsection{Example: a print translation for dependent types}
\indexbold{*_K}\indexbold{*dependent_tr'}
Let us continue the dependent type example (page~\pageref{prod_trans}) by
examining the parse translation for {\tt _K} and the print translation
{\tt dependent_tr'}, which are both built-in. By convention, parse
translations have names ending with {\tt _tr} and print translations have
names ending with {\tt _tr'}. Search for such names in the Isabelle
sources to locate more examples.
Here is the parse translation for {\tt _K}:
\begin{ttbox}
fun k_tr [t] = Abs ("x", dummyT, incr_boundvars 1 t)
| k_tr ts = raise TERM("k_tr",ts);
\end{ttbox}
If {\tt k_tr} is called with exactly one argument~$t$, it creates a new
{\tt Abs} node with a body derived from $t$. Since terms given to parse
translations are not yet typed, the type of the bound variable in the new
{\tt Abs} is simply {\tt dummyT}. The function increments all {\tt Bound}
nodes referring to outer abstractions by calling \ttindex{incr_boundvars},
a basic term manipulation function defined in {\tt Pure/term.ML}.
Here is the print translation for dependent types:
\begin{ttbox}
fun dependent_tr' (q,r) (A :: Abs (x, T, B) :: ts) =
if 0 mem (loose_bnos B) then
let val (x', B') = variant_abs (x, dummyT, B);
in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts)
end
else list_comb (Const (r, dummyT) $ A $ B, ts)
| dependent_tr' _ _ = raise Match;
\end{ttbox}
The argument {\tt (q,r)} is supplied to {\tt dependent_tr'} by a curried
function application during its installation. We could set up print
translations for both {\tt Pi} and {\tt Sigma} by including
\begin{ttbox}
val print_translation =
[("Pi", dependent_tr' ("{\at}PROD", "{\at}->")),
("Sigma", dependent_tr' ("{\at}SUM", "{\at}*"))];
\end{ttbox}
within the {\tt ML} section. The first of these transforms ${\tt Pi}(A,
\mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or
$\hbox{\tt{\at}->}r(A, B)$, choosing the latter form if $B$ does not depend
on~$x$. It checks this using \ttindex{loose_bnos}, yet another function
from {\tt Pure/term.ML}. Note that $x'$ is a version of $x$ renamed away
from all names in $B$, and $B'$ the body $B$ with {\tt Bound} nodes
referring to our {\tt Abs} node replaced by $\ttfct{Free} (x',
\mtt{dummyT})$.
We must be careful with types here. While types of {\tt Const}s are
ignored, type constraints may be printed for some {\tt Free}s and
{\tt Var}s if \ttindex{show_types} is set to {\tt true}. Variables of type
\ttindex{dummyT} are never printed with constraint, though. The line
\begin{ttbox}
let val (x', B') = variant_abs (x, dummyT, B);
\end{ttbox}\index{*variant_abs}
replaces bound variable occurrences in~$B$ by the free variable $x'$ with
type {\tt dummyT}. Only the binding occurrence of~$x'$ is given the
correct type~{\tt T}, so this is the only place where a type
constraint might appear.
\index{translations|)}