author | wenzelm |
Tue, 19 Jun 2012 20:43:09 +0200 | |
changeset 48115 | d868e4f7905b |
parent 48114 | 428e55887f24 |
child 48116 | fd773574cb81 |
permissions | -rw-r--r-- |
30184
37969710e61f
removed parts of the manual that are clearly obsolete, or covered by
wenzelm
parents:
14947
diff
changeset
|
1 |
|
323 | 2 |
\chapter{Syntax Transformations} \label{chap:syntax} |
3 |
\newcommand\ttapp{\mathrel{\hbox{\tt\$}}} |
|
4 |
\newcommand\mtt[1]{\mbox{\tt #1}} |
|
5 |
\newcommand\ttfct[1]{\mathop{\mtt{#1}}\nolimits} |
|
6 |
\newcommand\Constant{\ttfct{Constant}} |
|
7 |
\newcommand\Variable{\ttfct{Variable}} |
|
8 |
\newcommand\Appl[1]{\ttfct{Appl}\,[#1]} |
|
9 |
\index{syntax!transformations|(} |
|
10 |
||
11 |
||
6618 | 12 |
\section{Transforming parse trees to ASTs}\label{sec:astofpt} |
323 | 13 |
\index{ASTs!made from parse trees} |
14 |
\newcommand\astofpt[1]{\lbrakk#1\rbrakk} |
|
15 |
||
16 |
The parse tree is the raw output of the parser. Translation functions, |
|
17 |
called {\bf parse AST translations}\indexbold{translations!parse AST}, |
|
18 |
transform the parse tree into an abstract syntax tree. |
|
19 |
||
20 |
The parse tree is constructed by nesting the right-hand sides of the |
|
21 |
productions used to recognize the input. Such parse trees are simply lists |
|
22 |
of tokens and constituent parse trees, the latter representing the |
|
23 |
nonterminals of the productions. Let us refer to the actual productions in |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
24 |
the form displayed by {\tt print_syntax} (see \S\ref{sec:inspct-thy} for an |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
25 |
example). |
323 | 26 |
|
27 |
Ignoring parse \AST{} translations, parse trees are transformed to \AST{}s |
|
28 |
by stripping out delimiters and copy productions. More precisely, the |
|
29 |
mapping $\astofpt{-}$ is derived from the productions as follows: |
|
30 |
\begin{itemize} |
|
31 |
\item Name tokens: $\astofpt{t} = \Variable s$, where $t$ is an \ndx{id}, |
|
14947 | 32 |
\ndx{var}, \ndx{tid}, \ndx{tvar}, \ndx{num}, \ndx{xnum} or \ndx{xstr} token, |
33 |
and $s$ its associated string. Note that for {\tt xstr} this does not |
|
34 |
include the quotes. |
|
323 | 35 |
|
36 |
\item Copy productions:\index{productions!copy} |
|
37 |
$\astofpt{\ldots P \ldots} = \astofpt{P}$. Here $\ldots$ stands for |
|
38 |
strings of delimiters, which are discarded. $P$ stands for the single |
|
39 |
constituent that is not a delimiter; it is either a nonterminal symbol or |
|
40 |
a name token. |
|
41 |
||
42 |
\item 0-ary productions: $\astofpt{\ldots \mtt{=>} c} = \Constant c$. |
|
43 |
Here there are no constituents other than delimiters, which are |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
44 |
discarded. |
323 | 45 |
|
46 |
\item $n$-ary productions, where $n \ge 1$: delimiters are discarded and |
|
47 |
the remaining constituents $P@1$, \ldots, $P@n$ are built into an |
|
48 |
application whose head constant is~$c$: |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
49 |
\[ \astofpt{\ldots P@1 \ldots P@n \ldots \mtt{=>} c} = |
323 | 50 |
\Appl{\Constant c, \astofpt{P@1}, \ldots, \astofpt{P@n}} |
51 |
\] |
|
52 |
\end{itemize} |
|
53 |
Figure~\ref{fig:parse_ast} presents some simple examples, where {\tt ==}, |
|
54 |
{\tt _appl}, {\tt _args}, and so forth name productions of the Pure syntax. |
|
55 |
These examples illustrate the need for further translations to make \AST{}s |
|
56 |
closer to the typed $\lambda$-calculus. The Pure syntax provides |
|
57 |
predefined parse \AST{} translations\index{translations!parse AST} for |
|
58 |
ordinary applications, type applications, nested abstractions, meta |
|
59 |
implications and function types. Figure~\ref{fig:parse_ast_tr} shows their |
|
60 |
effect on some representative input strings. |
|
61 |
||
62 |
||
63 |
\begin{figure} |
|
64 |
\begin{center} |
|
65 |
\tt\begin{tabular}{ll} |
|
66 |
\rm input string & \rm \AST \\\hline |
|
67 |
"f" & f \\ |
|
68 |
"'a" & 'a \\ |
|
69 |
"t == u" & ("==" t u) \\ |
|
70 |
"f(x)" & ("_appl" f x) \\ |
|
71 |
"f(x, y)" & ("_appl" f ("_args" x y)) \\ |
|
72 |
"f(x, y, z)" & ("_appl" f ("_args" x ("_args" y z))) \\ |
|
73 |
"\%x y.\ t" & ("_lambda" ("_idts" x y) t) \\ |
|
74 |
\end{tabular} |
|
75 |
\end{center} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
76 |
\caption{Parsing examples using the Pure syntax}\label{fig:parse_ast} |
323 | 77 |
\end{figure} |
78 |
||
79 |
\begin{figure} |
|
80 |
\begin{center} |
|
81 |
\tt\begin{tabular}{ll} |
|
82 |
\rm input string & \rm \AST{} \\\hline |
|
83 |
"f(x, y, z)" & (f x y z) \\ |
|
84 |
"'a ty" & (ty 'a) \\ |
|
85 |
"('a, 'b) ty" & (ty 'a 'b) \\ |
|
86 |
"\%x y z.\ t" & ("_abs" x ("_abs" y ("_abs" z t))) \\ |
|
87 |
"\%x ::\ 'a.\ t" & ("_abs" ("_constrain" x 'a) t) \\ |
|
88 |
"[| P; Q; R |] => S" & ("==>" P ("==>" Q ("==>" R S))) \\ |
|
89 |
"['a, 'b, 'c] => 'd" & ("fun" 'a ("fun" 'b ("fun" 'c 'd))) |
|
90 |
\end{tabular} |
|
91 |
\end{center} |
|
92 |
\caption{Built-in parse \AST{} translations}\label{fig:parse_ast_tr} |
|
93 |
\end{figure} |
|
94 |
||
95 |
The names of constant heads in the \AST{} control the translation process. |
|
96 |
The list of constants invoking parse \AST{} translations appears in the |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
97 |
output of {\tt print_syntax} under {\tt parse_ast_translation}. |
323 | 98 |
|
99 |
||
6618 | 100 |
\section{Transforming ASTs to terms}\label{sec:termofast} |
323 | 101 |
\index{terms!made from ASTs} |
102 |
\newcommand\termofast[1]{\lbrakk#1\rbrakk} |
|
103 |
||
104 |
The \AST{}, after application of macros (see \S\ref{sec:macros}), is |
|
105 |
transformed into a term. This term is probably ill-typed since type |
|
106 |
inference has not occurred yet. The term may contain type constraints |
|
107 |
consisting of applications with head {\tt "_constrain"}; the second |
|
108 |
argument is a type encoded as a term. Type inference later introduces |
|
109 |
correct types or rejects the input. |
|
110 |
||
111 |
Another set of translation functions, namely parse |
|
112 |
translations\index{translations!parse}, may affect this process. If we |
|
113 |
ignore parse translations for the time being, then \AST{}s are transformed |
|
114 |
to terms by mapping \AST{} constants to constants, \AST{} variables to |
|
115 |
schematic or free variables and \AST{} applications to applications. |
|
116 |
||
117 |
More precisely, the mapping $\termofast{-}$ is defined by |
|
118 |
\begin{itemize} |
|
119 |
\item Constants: $\termofast{\Constant x} = \ttfct{Const} (x, |
|
120 |
\mtt{dummyT})$. |
|
121 |
||
122 |
\item Schematic variables: $\termofast{\Variable \mtt{"?}xi\mtt"} = |
|
123 |
\ttfct{Var} ((x, i), \mtt{dummyT})$, where $x$ is the base name and $i$ |
|
124 |
the index extracted from~$xi$. |
|
125 |
||
126 |
\item Free variables: $\termofast{\Variable x} = \ttfct{Free} (x, |
|
127 |
\mtt{dummyT})$. |
|
128 |
||
129 |
\item Function applications with $n$ arguments: |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
130 |
\[ \termofast{\Appl{f, x@1, \ldots, x@n}} = |
323 | 131 |
\termofast{f} \ttapp |
132 |
\termofast{x@1} \ttapp \ldots \ttapp \termofast{x@n} |
|
133 |
\] |
|
134 |
\end{itemize} |
|
135 |
Here \ttindex{Const}, \ttindex{Var}, \ttindex{Free} and |
|
136 |
\verb|$|\index{$@{\tt\$}} are constructors of the datatype \mltydx{term}, |
|
137 |
while \ttindex{dummyT} stands for some dummy type that is ignored during |
|
138 |
type inference. |
|
139 |
||
140 |
So far the outcome is still a first-order term. Abstractions and bound |
|
141 |
variables (constructors \ttindex{Abs} and \ttindex{Bound}) are introduced |
|
142 |
by parse translations. Such translations are attached to {\tt "_abs"}, |
|
143 |
{\tt "!!"} and user-defined binders. |
|
144 |
||
145 |
||
146 |
\section{Printing of terms} |
|
147 |
\newcommand\astofterm[1]{\lbrakk#1\rbrakk}\index{ASTs!made from terms} |
|
148 |
||
149 |
The output phase is essentially the inverse of the input phase. Terms are |
|
150 |
translated via abstract syntax trees into strings. Finally the strings are |
|
151 |
pretty printed. |
|
152 |
||
153 |
Print translations (\S\ref{sec:tr_funs}) may affect the transformation of |
|
154 |
terms into \AST{}s. Ignoring those, the transformation maps |
|
155 |
term constants, variables and applications to the corresponding constructs |
|
156 |
on \AST{}s. Abstractions are mapped to applications of the special |
|
157 |
constant {\tt _abs}. |
|
158 |
||
159 |
More precisely, the mapping $\astofterm{-}$ is defined as follows: |
|
160 |
\begin{itemize} |
|
161 |
\item $\astofterm{\ttfct{Const} (x, \tau)} = \Constant x$. |
|
162 |
||
163 |
\item $\astofterm{\ttfct{Free} (x, \tau)} = constrain (\Variable x, |
|
164 |
\tau)$. |
|
165 |
||
166 |
\item $\astofterm{\ttfct{Var} ((x, i), \tau)} = constrain (\Variable |
|
167 |
\mtt{"?}xi\mtt", \tau)$, where $\mtt?xi$ is the string representation of |
|
168 |
the {\tt indexname} $(x, i)$. |
|
169 |
||
170 |
\item For the abstraction $\lambda x::\tau.t$, let $x'$ be a variant |
|
171 |
of~$x$ renamed to differ from all names occurring in~$t$, and let $t'$ |
|
172 |
be obtained from~$t$ by replacing all bound occurrences of~$x$ by |
|
173 |
the free variable $x'$. This replaces corresponding occurrences of the |
|
174 |
constructor \ttindex{Bound} by the term $\ttfct{Free} (x', |
|
175 |
\mtt{dummyT})$: |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
176 |
\[ \astofterm{\ttfct{Abs} (x, \tau, t)} = |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
177 |
\Appl{\Constant \mtt{"_abs"}, |
8136 | 178 |
constrain(\Variable x', \tau), \astofterm{t'}} |
323 | 179 |
\] |
180 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
181 |
\item $\astofterm{\ttfct{Bound} i} = \Variable \mtt{"B.}i\mtt"$. |
323 | 182 |
The occurrence of constructor \ttindex{Bound} should never happen |
183 |
when printing well-typed terms; it indicates a de Bruijn index with no |
|
184 |
matching abstraction. |
|
185 |
||
186 |
\item Where $f$ is not an application, |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
187 |
\[ \astofterm{f \ttapp x@1 \ttapp \ldots \ttapp x@n} = |
323 | 188 |
\Appl{\astofterm{f}, \astofterm{x@1}, \ldots,\astofterm{x@n}} |
189 |
\] |
|
190 |
\end{itemize} |
|
191 |
% |
|
332 | 192 |
Type constraints\index{type constraints} are inserted to allow the printing |
193 |
of types. This is governed by the boolean variable \ttindex{show_types}: |
|
323 | 194 |
\begin{itemize} |
195 |
\item $constrain(x, \tau) = x$ \ if $\tau = \mtt{dummyT}$ \index{*dummyT} or |
|
332 | 196 |
\ttindex{show_types} is set to {\tt false}. |
323 | 197 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
198 |
\item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
199 |
\astofterm{\tau}}$ \ otherwise. |
323 | 200 |
|
201 |
Here, $\astofterm{\tau}$ is the \AST{} encoding of $\tau$: type |
|
202 |
constructors go to {\tt Constant}s; type identifiers go to {\tt |
|
203 |
Variable}s; type applications go to {\tt Appl}s with the type |
|
204 |
constructor as the first element. If \ttindex{show_sorts} is set to |
|
205 |
{\tt true}, some type variables are decorated with an \AST{} encoding |
|
206 |
of their sort. |
|
207 |
\end{itemize} |
|
208 |
% |
|
209 |
The \AST{}, after application of macros (see \S\ref{sec:macros}), is |
|
210 |
transformed into the final output string. The built-in {\bf print AST |
|
332 | 211 |
translations}\indexbold{translations!print AST} reverse the |
323 | 212 |
parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}. |
213 |
||
214 |
For the actual printing process, the names attached to productions |
|
215 |
of the form $\ldots A^{(p@1)}@1 \ldots A^{(p@n)}@n \ldots \mtt{=>} c$ play |
|
216 |
a vital role. Each \AST{} with constant head $c$, namely $\mtt"c\mtt"$ or |
|
217 |
$(\mtt"c\mtt"~ x@1 \ldots x@n)$, is printed according to the production |
|
218 |
for~$c$. Each argument~$x@i$ is converted to a string, and put in |
|
219 |
parentheses if its priority~$(p@i)$ requires this. The resulting strings |
|
220 |
and their syntactic sugar (denoted by \dots{} above) are joined to make a |
|
221 |
single string. |
|
222 |
||
3108 | 223 |
If an application $(\mtt"c\mtt"~ x@1 \ldots x@m)$ has more arguments |
224 |
than the corresponding production, it is first split into |
|
225 |
$((\mtt"c\mtt"~ x@1 \ldots x@n) ~ x@{n+1} \ldots x@m)$. Applications |
|
226 |
with too few arguments or with non-constant head or without a |
|
227 |
corresponding production are printed as $f(x@1, \ldots, x@l)$ or |
|
228 |
$(\alpha@1, \ldots, \alpha@l) ty$. Multiple productions associated |
|
229 |
with some name $c$ are tried in order of appearance. An occurrence of |
|
323 | 230 |
$\Variable x$ is simply printed as~$x$. |
231 |
||
232 |
Blanks are {\em not\/} inserted automatically. If blanks are required to |
|
233 |
separate tokens, specify them in the mixfix declaration, possibly preceded |
|
234 |
by a slash~({\tt/}) to allow a line break. |
|
235 |
\index{ASTs|)} |
|
236 |
||
237 |
||
238 |
||
3108 | 239 |
\section{Macros: syntactic rewriting} \label{sec:macros} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
240 |
\index{macros|(}\index{rewriting!syntactic|(} |
323 | 241 |
|
3108 | 242 |
Figure~\ref{fig:set_trans} defines a fragment of first-order logic and |
243 |
set theory.\footnote{This and the following theories are complete |
|
244 |
working examples, though they specify only syntax, no axioms. The |
|
245 |
file {\tt ZF/ZF.thy} presents a full set theory definition, |
|
246 |
including many macro rules.} Theory {\tt SetSyntax} declares |
|
247 |
constants for set comprehension ({\tt Collect}), replacement ({\tt |
|
248 |
Replace}) and bounded universal quantification ({\tt Ball}). Each |
|
249 |
of these binds some variables. Without additional syntax we should |
|
250 |
have to write $\forall x \in A. P$ as {\tt Ball(A,\%x.P)}, and |
|
251 |
similarly for the others. |
|
323 | 252 |
|
253 |
\begin{figure} |
|
254 |
\begin{ttbox} |
|
3108 | 255 |
SetSyntax = Pure + |
323 | 256 |
types |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
257 |
i o |
323 | 258 |
arities |
259 |
i, o :: logic |
|
260 |
consts |
|
1387 | 261 |
Trueprop :: o => prop ("_" 5) |
262 |
Collect :: [i, i => o] => i |
|
263 |
Replace :: [i, [i, i] => o] => i |
|
264 |
Ball :: [i, i => o] => o |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
265 |
syntax |
1387 | 266 |
"{\at}Collect" :: [idt, i, o] => i ("(1{\ttlbrace}_:_./ _{\ttrbrace})") |
267 |
"{\at}Replace" :: [idt, idt, i, o] => i ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})") |
|
268 |
"{\at}Ball" :: [idt, i, o] => o ("(3ALL _:_./ _)" 10) |
|
323 | 269 |
translations |
270 |
"{\ttlbrace}x:A. P{\ttrbrace}" == "Collect(A, \%x. P)" |
|
271 |
"{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)" |
|
272 |
"ALL x:A. P" == "Ball(A, \%x. P)" |
|
273 |
end |
|
274 |
\end{ttbox} |
|
275 |
\caption{Macro example: set theory}\label{fig:set_trans} |
|
276 |
\end{figure} |
|
277 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
278 |
The theory specifies a variable-binding syntax through additional productions |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
279 |
that have mixfix declarations. Each non-copy production must specify some |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
280 |
constant, which is used for building \AST{}s. \index{constants!syntactic} The |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
281 |
additional constants are decorated with {\tt\at} to stress their purely |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
282 |
syntactic purpose; they may not occur within the final well-typed terms, |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
283 |
being declared as {\tt syntax} rather than {\tt consts}. |
323 | 284 |
|
285 |
The translations cause the replacement of external forms by internal forms |
|
286 |
after parsing, and vice versa before printing of terms. As a specification |
|
287 |
of the set theory notation, they should be largely self-explanatory. The |
|
288 |
syntactic constants, {\tt\at Collect}, {\tt\at Replace} and {\tt\at Ball}, |
|
289 |
appear implicitly in the macro rules via their mixfix forms. |
|
290 |
||
291 |
Macros can define variable-binding syntax because they operate on \AST{}s, |
|
292 |
which have no inbuilt notion of bound variable. The macro variables {\tt |
|
293 |
x} and~{\tt y} have type~{\tt idt} and therefore range over identifiers, |
|
294 |
in this case bound variables. The macro variables {\tt P} and~{\tt Q} |
|
295 |
range over formulae containing bound variable occurrences. |
|
296 |
||
297 |
Other applications of the macro system can be less straightforward, and |
|
298 |
there are peculiarities. The rest of this section will describe in detail |
|
299 |
how Isabelle macros are preprocessed and applied. |
|
300 |
||
301 |
||
302 |
\subsection{Specifying macros} |
|
303 |
||
48115 | 304 |
For theory~{\tt SetSyntax} of Fig.~\ref{fig:set_trans} these are |
323 | 305 |
\begin{ttbox} |
306 |
parse_rules: |
|
307 |
("{\at}Collect" x A P) -> ("Collect" A ("_abs" x P)) |
|
308 |
("{\at}Replace" y x A Q) -> ("Replace" A ("_abs" x ("_abs" y Q))) |
|
309 |
("{\at}Ball" x A P) -> ("Ball" A ("_abs" x P)) |
|
310 |
print_rules: |
|
311 |
("Collect" A ("_abs" x P)) -> ("{\at}Collect" x A P) |
|
312 |
("Replace" A ("_abs" x ("_abs" y Q))) -> ("{\at}Replace" y x A Q) |
|
313 |
("Ball" A ("_abs" x P)) -> ("{\at}Ball" x A P) |
|
314 |
\end{ttbox} |
|
315 |
||
316 |
\begin{warn} |
|
317 |
Avoid choosing variable names that have previously been used as |
|
318 |
constants, types or type classes; the {\tt consts} section in the output |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
319 |
of {\tt print_syntax} lists all such names. If a macro rule works |
323 | 320 |
incorrectly, inspect its internal form as shown above, recalling that |
321 |
constants appear as quoted strings and variables without quotes. |
|
322 |
\end{warn} |
|
323 |
||
324 |
\begin{warn} |
|
325 |
If \ttindex{eta_contract} is set to {\tt true}, terms will be |
|
326 |
$\eta$-contracted {\em before\/} the \AST{} rewriter sees them. Thus some |
|
327 |
abstraction nodes needed for print rules to match may vanish. For example, |
|
332 | 328 |
\verb|Ball(A, %x. P(x))| contracts to {\tt Ball(A, P)}; the print rule does |
323 | 329 |
not apply and the output will be {\tt Ball(A, P)}. This problem would not |
330 |
occur if \ML{} translation functions were used instead of macros (as is |
|
331 |
done for binder declarations). |
|
332 |
\end{warn} |
|
333 |
||
334 |
||
335 |
\begin{warn} |
|
336 |
Another trap concerns type constraints. If \ttindex{show_types} is set to |
|
337 |
{\tt true}, bound variables will be decorated by their meta types at the |
|
338 |
binding place (but not at occurrences in the body). Matching with |
|
339 |
\verb|Collect(A, %x. P)| binds {\tt x} to something like {\tt ("_constrain" y |
|
340 |
"i")} rather than only {\tt y}. \AST{} rewriting will cause the constraint to |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
341 |
appear in the external form, say \verb|{y::i:A::i. P::o}|. |
323 | 342 |
|
343 |
To allow such constraints to be re-read, your syntax should specify bound |
|
344 |
variables using the nonterminal~\ndx{idt}. This is the case in our |
|
3108 | 345 |
example. Choosing {\tt id} instead of {\tt idt} is a common error. |
323 | 346 |
\end{warn} |
347 |
||
348 |
||
349 |
||
350 |
\subsection{Applying rules} |
|
351 |
As a term is being parsed or printed, an \AST{} is generated as an |
|
352 |
intermediate form (recall Fig.\ts\ref{fig:parse_print}). The \AST{} is |
|
332 | 353 |
normalised by applying macro rules in the manner of a traditional term |
323 | 354 |
rewriting system. We first examine how a single rule is applied. |
355 |
||
332 | 356 |
Let $t$ be the abstract syntax tree to be normalised and $(l, r)$ some |
323 | 357 |
translation rule. A subtree~$u$ of $t$ is a {\bf redex} if it is an |
358 |
instance of~$l$; in this case $l$ is said to {\bf match}~$u$. A redex |
|
359 |
matched by $l$ may be replaced by the corresponding instance of~$r$, thus |
|
360 |
{\bf rewriting} the \AST~$t$. Matching requires some notion of {\bf |
|
361 |
place-holders} that may occur in rule patterns but not in ordinary |
|
362 |
\AST{}s; {\tt Variable} atoms serve this purpose. |
|
363 |
||
364 |
The matching of the object~$u$ by the pattern~$l$ is performed as follows: |
|
365 |
\begin{itemize} |
|
366 |
\item Every constant matches itself. |
|
367 |
||
368 |
\item $\Variable x$ in the object matches $\Constant x$ in the pattern. |
|
369 |
This point is discussed further below. |
|
370 |
||
371 |
\item Every \AST{} in the object matches $\Variable x$ in the pattern, |
|
372 |
binding~$x$ to~$u$. |
|
373 |
||
374 |
\item One application matches another if they have the same number of |
|
375 |
subtrees and corresponding subtrees match. |
|
376 |
||
377 |
\item In every other case, matching fails. In particular, {\tt |
|
378 |
Constant}~$x$ can only match itself. |
|
379 |
\end{itemize} |
|
380 |
A successful match yields a substitution that is applied to~$r$, generating |
|
381 |
the instance that replaces~$u$. |
|
382 |
||
383 |
The second case above may look odd. This is where {\tt Variable}s of |
|
384 |
non-rule \AST{}s behave like {\tt Constant}s. Recall that \AST{}s are not |
|
385 |
far removed from parse trees; at this level it is not yet known which |
|
386 |
identifiers will become constants, bounds, frees, types or classes. As |
|
387 |
\S\ref{sec:asts} describes, former parse tree heads appear in \AST{}s as |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
388 |
{\tt Constant}s, while the name tokens \ndx{id}, \ndx{var}, \ndx{tid}, |
14947 | 389 |
\ndx{tvar}, \ndx{num}, \ndx{xnum} and \ndx{xstr} become {\tt Variable}s. On the other |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
390 |
hand, when \AST{}s generated from terms for printing, all constants and type |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
391 |
constructors become {\tt Constant}s; see \S\ref{sec:asts}. Thus \AST{}s may |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
392 |
contain a messy mixture of {\tt Variable}s and {\tt Constant}s. This is |
323 | 393 |
insignificant at macro level because matching treats them alike. |
394 |
||
395 |
Because of this behaviour, different kinds of atoms with the same name are |
|
396 |
indistinguishable, which may make some rules prone to misbehaviour. Example: |
|
397 |
\begin{ttbox} |
|
398 |
types |
|
399 |
Nil |
|
400 |
consts |
|
1387 | 401 |
Nil :: 'a list |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
402 |
syntax |
1387 | 403 |
"[]" :: 'a list ("[]") |
323 | 404 |
translations |
405 |
"[]" == "Nil" |
|
406 |
\end{ttbox} |
|
407 |
The term {\tt Nil} will be printed as {\tt []}, just as expected. |
|
408 |
The term \verb|%Nil.t| will be printed as \verb|%[].t|, which might not be |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
409 |
expected! Guess how type~{\tt Nil} is printed? |
323 | 410 |
|
14893 | 411 |
Normalizing an \AST{} involves repeatedly applying macro rules until none are |
412 |
applicable. Macro rules are chosen in order of appearance in the theory |
|
413 |
definitions. You can watch the normalization of \AST{}s during parsing and |
|
414 |
printing by setting \ttindex{Syntax.trace_ast} to {\tt true}.\index{tracing!of |
|
415 |
macros} The information displayed when tracing includes the \AST{} before |
|
416 |
normalization ({\tt pre}), redexes with results ({\tt rewrote}), the normal |
|
417 |
form finally reached ({\tt post}) and some statistics ({\tt normalize}). |
|
323 | 418 |
|
419 |
\subsection{Example: the syntax of finite sets} |
|
420 |
\index{examples!of macros} |
|
421 |
||
422 |
This example demonstrates the use of recursive macros to implement a |
|
423 |
convenient notation for finite sets. |
|
424 |
\begin{ttbox} |
|
3108 | 425 |
FinSyntax = SetSyntax + |
323 | 426 |
types |
427 |
is |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
428 |
syntax |
1387 | 429 |
"" :: i => is ("_") |
430 |
"{\at}Enum" :: [i, is] => is ("_,/ _") |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
431 |
consts |
1387 | 432 |
empty :: i ("{\ttlbrace}{\ttrbrace}") |
433 |
insert :: [i, i] => i |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
434 |
syntax |
1387 | 435 |
"{\at}Finset" :: is => i ("{\ttlbrace}(_){\ttrbrace}") |
323 | 436 |
translations |
437 |
"{\ttlbrace}x, xs{\ttrbrace}" == "insert(x, {\ttlbrace}xs{\ttrbrace})" |
|
438 |
"{\ttlbrace}x{\ttrbrace}" == "insert(x, {\ttlbrace}{\ttrbrace})" |
|
439 |
end |
|
440 |
\end{ttbox} |
|
441 |
Finite sets are internally built up by {\tt empty} and {\tt insert}. The |
|
442 |
declarations above specify \verb|{x, y, z}| as the external representation |
|
443 |
of |
|
444 |
\begin{ttbox} |
|
445 |
insert(x, insert(y, insert(z, empty))) |
|
446 |
\end{ttbox} |
|
447 |
The nonterminal symbol~\ndx{is} stands for one or more objects of type~{\tt |
|
448 |
i} separated by commas. The mixfix declaration \hbox{\verb|"_,/ _"|} |
|
449 |
allows a line break after the comma for \rmindex{pretty printing}; if no |
|
450 |
line break is required then a space is printed instead. |
|
451 |
||
452 |
The nonterminal is declared as the type~{\tt is}, but with no {\tt arities} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
453 |
declaration. Hence {\tt is} is not a logical type and may be used safely as |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
454 |
a new nonterminal for custom syntax. The nonterminal~{\tt is} can later be |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3135
diff
changeset
|
455 |
re-used for other enumerations of type~{\tt i} like lists or tuples. If we |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
456 |
had needed polymorphic enumerations, we could have used the predefined |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
457 |
nonterminal symbol \ndx{args} and skipped this part altogether. |
323 | 458 |
|
459 |
Next follows {\tt empty}, which is already equipped with its syntax |
|
460 |
\verb|{}|, and {\tt insert} without concrete syntax. The syntactic |
|
461 |
constant {\tt\at Finset} provides concrete syntax for enumerations of~{\tt |
|
462 |
i} enclosed in curly braces. Remember that a pair of parentheses, as in |
|
463 |
\verb|"{(_)}"|, specifies a block of indentation for pretty printing. |
|
464 |
||
465 |
The translations may look strange at first. Macro rules are best |
|
466 |
understood in their internal forms: |
|
467 |
\begin{ttbox} |
|
468 |
parse_rules: |
|
469 |
("{\at}Finset" ("{\at}Enum" x xs)) -> ("insert" x ("{\at}Finset" xs)) |
|
470 |
("{\at}Finset" x) -> ("insert" x "empty") |
|
471 |
print_rules: |
|
472 |
("insert" x ("{\at}Finset" xs)) -> ("{\at}Finset" ("{\at}Enum" x xs)) |
|
473 |
("insert" x "empty") -> ("{\at}Finset" x) |
|
474 |
\end{ttbox} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
475 |
This shows that \verb|{x,xs}| indeed matches any set enumeration of at least |
323 | 476 |
two elements, binding the first to {\tt x} and the rest to {\tt xs}. |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
477 |
Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration. |
323 | 478 |
The parse rules only work in the order given. |
479 |
||
480 |
\begin{warn} |
|
332 | 481 |
The \AST{} rewriter cannot distinguish constants from variables and looks |
323 | 482 |
only for names of atoms. Thus the names of {\tt Constant}s occurring in |
483 |
the (internal) left-hand side of translation rules should be regarded as |
|
484 |
\rmindex{reserved words}. Choose non-identifiers like {\tt\at Finset} or |
|
485 |
sufficiently long and strange names. If a bound variable's name gets |
|
486 |
rewritten, the result will be incorrect; for example, the term |
|
487 |
\begin{ttbox} |
|
488 |
\%empty insert. insert(x, empty) |
|
489 |
\end{ttbox} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
490 |
\par\noindent is incorrectly printed as \verb|%empty insert. {x}|. |
323 | 491 |
\end{warn} |
492 |
||
493 |
||
494 |
\subsection{Example: a parse macro for dependent types}\label{prod_trans} |
|
495 |
\index{examples!of macros} |
|
496 |
||
497 |
As stated earlier, a macro rule may not introduce new {\tt Variable}s on |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
498 |
the right-hand side. Something like \verb|"K(B)" => "%x.B"| is illegal; |
323 | 499 |
if allowed, it could cause variable capture. In such cases you usually |
500 |
must fall back on translation functions. But a trick can make things |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
501 |
readable in some cases: {\em calling\/} translation functions by parse |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
502 |
macros: |
323 | 503 |
\begin{ttbox} |
3135 | 504 |
ProdSyntax = SetSyntax + |
323 | 505 |
consts |
1387 | 506 |
Pi :: [i, i => i] => i |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
507 |
syntax |
1387 | 508 |
"{\at}PROD" :: [idt, i, i] => i ("(3PROD _:_./ _)" 10) |
509 |
"{\at}->" :: [i, i] => i ("(_ ->/ _)" [51, 50] 50) |
|
323 | 510 |
\ttbreak |
511 |
translations |
|
512 |
"PROD x:A. B" => "Pi(A, \%x. B)" |
|
513 |
"A -> B" => "Pi(A, _K(B))" |
|
514 |
end |
|
515 |
ML |
|
516 |
val print_translation = [("Pi", dependent_tr' ("{\at}PROD", "{\at}->"))]; |
|
517 |
\end{ttbox} |
|
518 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
519 |
Here {\tt Pi} is a logical constant for constructing general products. |
323 | 520 |
Two external forms exist: the general case {\tt PROD x:A.B} and the |
521 |
function space {\tt A -> B}, which abbreviates \verb|Pi(A, %x.B)| when {\tt B} |
|
522 |
does not depend on~{\tt x}. |
|
523 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
524 |
The second parse macro introduces {\tt _K(B)}, which later becomes |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
525 |
\verb|%x.B| due to a parse translation associated with \cdx{_K}. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
526 |
Unfortunately there is no such trick for printing, so we have to add a {\tt |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
527 |
ML} section for the print translation \ttindex{dependent_tr'}. |
323 | 528 |
|
529 |
Recall that identifiers with a leading {\tt _} are allowed in translation |
|
530 |
rules, but not in ordinary terms. Thus we can create \AST{}s containing |
|
531 |
names that are not directly expressible. |
|
532 |
||
8136 | 533 |
The parse translation for {\tt _K} is already installed in Pure, and the |
534 |
function {\tt dependent_tr'} is exported by the syntax module for public use. |
|
535 |
See \S\ref{sec:tr_funs} below for more of the arcane lore of translation |
|
536 |
functions. \index{macros|)}\index{rewriting!syntactic|)} |
|
323 | 537 |
|
538 |
||
539 |
\section{Translation functions} \label{sec:tr_funs} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
540 |
\index{translations|(} |
323 | 541 |
% |
9695 | 542 |
This section describes the translation function mechanism. By writing \ML{} |
543 |
functions, you can do almost everything to terms or \AST{}s during parsing and |
|
544 |
printing. The logic LK is a good example of sophisticated transformations |
|
545 |
between internal and external representations of sequents; here, macros would |
|
546 |
be useless. |
|
323 | 547 |
|
548 |
A full understanding of translations requires some familiarity |
|
549 |
with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ}, |
|
550 |
{\tt Syntax.ast} and the encodings of types and terms as such at the various |
|
551 |
stages of the parsing or printing process. Most users should never need to |
|
552 |
use translation functions. |
|
553 |
||
554 |
\subsection{Declaring translation functions} |
|
3108 | 555 |
There are four kinds of translation functions, with one of these |
556 |
coming in two variants. Each such function is associated with a name, |
|
557 |
which triggers calls to it. Such names can be constants (logical or |
|
558 |
syntactic) or type constructors. |
|
323 | 559 |
|
6343 | 560 |
Function {\tt print_syntax} displays the sets of names associated with the |
561 |
translation functions of a theory under \texttt{parse_ast_translation}, etc. |
|
562 |
You can add new ones via the {\tt ML} section\index{*ML section} of a theory |
|
563 |
definition file. Even though the {\tt ML} section is the very last part of |
|
564 |
the file, newly installed translation functions are already effective when |
|
565 |
processing all of the preceding sections. |
|
323 | 566 |
|
3108 | 567 |
The {\tt ML} section's contents are simply copied verbatim near the |
568 |
beginning of the \ML\ file generated from a theory definition file. |
|
569 |
Definitions made here are accessible as components of an \ML\ |
|
570 |
structure; to make some parts private, use an \ML{} {\tt local} |
|
571 |
declaration. The {\ML} code may install translation functions by |
|
572 |
declaring any of the following identifiers: |
|
323 | 573 |
\begin{ttbox} |
3108 | 574 |
val parse_ast_translation : (string * (ast list -> ast)) list |
575 |
val print_ast_translation : (string * (ast list -> ast)) list |
|
576 |
val parse_translation : (string * (term list -> term)) list |
|
577 |
val print_translation : (string * (term list -> term)) list |
|
4375 | 578 |
val typed_print_translation : |
579 |
(string * (bool -> typ -> term list -> term)) list |
|
323 | 580 |
\end{ttbox} |
581 |
||
582 |
\subsection{The translation strategy} |
|
3108 | 583 |
The different kinds of translation functions are called during the |
584 |
transformations between parse trees, \AST{}s and terms (recall |
|
585 |
Fig.\ts\ref{fig:parse_print}). Whenever a combination of the form |
|
586 |
$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation |
|
587 |
function $f$ of appropriate kind exists for $c$, the result is |
|
588 |
computed by the \ML{} function call $f \mtt[ x@1, \ldots, x@n \mtt]$. |
|
323 | 589 |
|
3108 | 590 |
For \AST{} translations, the arguments $x@1, \ldots, x@n$ are \AST{}s. |
591 |
A combination has the form $\Constant c$ or $\Appl{\Constant c, x@1, |
|
592 |
\ldots, x@n}$. For term translations, the arguments are terms and a |
|
593 |
combination has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const} |
|
594 |
(c, \tau) \ttapp x@1 \ttapp \ldots \ttapp x@n$. Terms allow more |
|
595 |
sophisticated transformations than \AST{}s do, typically involving |
|
596 |
abstractions and bound variables. {\em Typed} print translations may |
|
4375 | 597 |
even peek at the type $\tau$ of the constant they are invoked on; they |
598 |
are also passed the current value of the \ttindex{show_sorts} flag. |
|
323 | 599 |
|
3108 | 600 |
Regardless of whether they act on terms or \AST{}s, translation |
601 |
functions called during the parsing process differ from those for |
|
602 |
printing more fundamentally in their overall behaviour: |
|
323 | 603 |
\begin{description} |
6343 | 604 |
\item[Parse translations] are applied bottom-up. The arguments are already in |
605 |
translated form. The translations must not fail; exceptions trigger an |
|
606 |
error message. There may never be more than one function associated with |
|
607 |
any syntactic name. |
|
608 |
||
323 | 609 |
\item[Print translations] are applied top-down. They are supplied with |
610 |
arguments that are partly still in internal form. The result again |
|
6343 | 611 |
undergoes translation; therefore a print translation should not introduce as |
612 |
head the very constant that invoked it. The function may raise exception |
|
613 |
\xdx{Match} to indicate failure; in this event it has no effect. Multiple |
|
614 |
functions associated with some syntactic name are tried in an unspecified |
|
615 |
order. |
|
323 | 616 |
\end{description} |
617 |
||
618 |
Only constant atoms --- constructor \ttindex{Constant} for \AST{}s and |
|
619 |
\ttindex{Const} for terms --- can invoke translation functions. This |
|
620 |
causes another difference between parsing and printing. |
|
621 |
||
622 |
Parsing starts with a string and the constants are not yet identified. |
|
623 |
Only parse tree heads create {\tt Constant}s in the resulting \AST, as |
|
624 |
described in \S\ref{sec:astofpt}. Macros and parse \AST{} translations may |
|
625 |
introduce further {\tt Constant}s. When the final \AST{} is converted to a |
|
626 |
term, all {\tt Constant}s become {\tt Const}s, as described in |
|
627 |
\S\ref{sec:termofast}. |
|
628 |
||
629 |
Printing starts with a well-typed term and all the constants are known. So |
|
630 |
all logical constants and type constructors may invoke print translations. |
|
631 |
These, and macros, may introduce further constants. |
|
632 |
||
633 |
||
634 |
\subsection{Example: a print translation for dependent types} |
|
635 |
\index{examples!of translations}\indexbold{*dependent_tr'} |
|
636 |
||
637 |
Let us continue the dependent type example (page~\pageref{prod_trans}) by |
|
638 |
examining the parse translation for~\cdx{_K} and the print translation |
|
639 |
{\tt dependent_tr'}, which are both built-in. By convention, parse |
|
640 |
translations have names ending with {\tt _tr} and print translations have |
|
641 |
names ending with {\tt _tr'}. Search for such names in the Isabelle |
|
642 |
sources to locate more examples. |
|
643 |
||
644 |
Here is the parse translation for {\tt _K}: |
|
645 |
\begin{ttbox} |
|
646 |
fun k_tr [t] = Abs ("x", dummyT, incr_boundvars 1 t) |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
647 |
| k_tr ts = raise TERM ("k_tr", ts); |
323 | 648 |
\end{ttbox} |
649 |
If {\tt k_tr} is called with exactly one argument~$t$, it creates a new |
|
650 |
{\tt Abs} node with a body derived from $t$. Since terms given to parse |
|
651 |
translations are not yet typed, the type of the bound variable in the new |
|
652 |
{\tt Abs} is simply {\tt dummyT}. The function increments all {\tt Bound} |
|
653 |
nodes referring to outer abstractions by calling \ttindex{incr_boundvars}, |
|
654 |
a basic term manipulation function defined in {\tt Pure/term.ML}. |
|
655 |
||
656 |
Here is the print translation for dependent types: |
|
657 |
\begin{ttbox} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
658 |
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = |
323 | 659 |
if 0 mem (loose_bnos B) then |
3108 | 660 |
let val (x', B') = Syntax.variant_abs' (x, dummyT, B) in |
661 |
list_comb |
|
8136 | 662 |
(Const (q,dummyT) $ |
663 |
Syntax.mark_boundT (x',{\thinspace}T) $ A $ B', ts) |
|
323 | 664 |
end |
665 |
else list_comb (Const (r, dummyT) $ A $ B, ts) |
|
666 |
| dependent_tr' _ _ = raise Match; |
|
667 |
\end{ttbox} |
|
3135 | 668 |
The argument {\tt (q,{\thinspace}r)} is supplied to the curried function {\tt |
3108 | 669 |
dependent_tr'} by a partial application during its installation. |
670 |
For example, we could set up print translations for both {\tt Pi} and |
|
671 |
{\tt Sigma} by including |
|
323 | 672 |
\begin{ttbox}\index{*ML section} |
673 |
val print_translation = |
|
674 |
[("Pi", dependent_tr' ("{\at}PROD", "{\at}->")), |
|
675 |
("Sigma", dependent_tr' ("{\at}SUM", "{\at}*"))]; |
|
676 |
\end{ttbox} |
|
3108 | 677 |
within the {\tt ML} section. The first of these transforms ${\tt |
678 |
Pi}(A, \mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or |
|
679 |
$\hbox{\tt{\at}->}(A, B)$, choosing the latter form if $B$ does not |
|
680 |
depend on~$x$. It checks this using \ttindex{loose_bnos}, yet another |
|
681 |
function from {\tt Pure/term.ML}. Note that $x'$ is a version of $x$ |
|
682 |
renamed away from all names in $B$, and $B'$ is the body $B$ with {\tt |
|
683 |
Bound} nodes referring to the {\tt Abs} node replaced by |
|
684 |
$\ttfct{Free} (x', \mtt{dummyT})$ (but marked as representing a bound |
|
685 |
variable). |
|
323 | 686 |
|
687 |
We must be careful with types here. While types of {\tt Const}s are |
|
688 |
ignored, type constraints may be printed for some {\tt Free}s and |
|
689 |
{\tt Var}s if \ttindex{show_types} is set to {\tt true}. Variables of type |
|
690 |
\ttindex{dummyT} are never printed with constraint, though. The line |
|
691 |
\begin{ttbox} |
|
3108 | 692 |
let val (x', B') = Syntax.variant_abs' (x, dummyT, B); |
693 |
\end{ttbox}\index{*Syntax.variant_abs'} |
|
323 | 694 |
replaces bound variable occurrences in~$B$ by the free variable $x'$ with |
695 |
type {\tt dummyT}. Only the binding occurrence of~$x'$ is given the |
|
696 |
correct type~{\tt T}, so this is the only place where a type |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
499
diff
changeset
|
697 |
constraint might appear. |
3108 | 698 |
|
699 |
Also note that we are responsible to mark free identifiers that |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3135
diff
changeset
|
700 |
actually represent bound variables. This is achieved by |
3108 | 701 |
\ttindex{Syntax.variant_abs'} and \ttindex{Syntax.mark_boundT} above. |
702 |
Failing to do so may cause these names to be printed in the wrong |
|
703 |
style. \index{translations|)} \index{syntax!transformations|)} |
|
704 |
||
705 |
||
5371 | 706 |
%%% Local Variables: |
707 |
%%% mode: latex |
|
708 |
%%% TeX-master: "ref" |
|
709 |
%%% End: |