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