62  Appl of ast list 
62  Appl of ast list 
63 \end{ttbox} 
63 \end{ttbox} 
64 % 
64 % 
65 Isabelle uses an Sexpression syntax for abstract syntax trees. Constant 
65 Isabelle uses an Sexpression syntax for abstract syntax trees. Constant 
66 atoms are shown as quoted strings, variable atoms as nonquoted strings and 
66 atoms are shown as quoted strings, variable atoms as nonquoted strings and 
67 applications as a parenthesized list of subtrees. For example, the \AST 
67 applications as a parenthesised list of subtrees. For example, the \AST 
68 \begin{ttbox} 
68 \begin{ttbox} 
69 Appl [Constant "_constrain", 
69 Appl [Constant "_constrain", 
70 Appl [Constant "_abs", Variable "x", Variable "t"], 
70 Appl [Constant "_abs", Variable "x", Variable "t"], 
71 Appl [Constant "fun", Variable "'a", Variable "'b"]] 
71 Appl [Constant "fun", Variable "'a", Variable "'b"]] 
72 \end{ttbox} 
72 \end{ttbox} 
268 \[ \astofterm{f \ttapp x@1 \ttapp \ldots \ttapp x@n} = 
268 \[ \astofterm{f \ttapp x@1 \ttapp \ldots \ttapp x@n} = 
269 \Appl{\astofterm{f}, \astofterm{x@1}, \ldots,\astofterm{x@n}} 
269 \Appl{\astofterm{f}, \astofterm{x@1}, \ldots,\astofterm{x@n}} 
270 \] 
270 \] 
271 \end{itemize} 
271 \end{itemize} 
272 % 
272 % 
273 Type constraints are inserted to allow the printing of types. This is 
273 Type constraints\index{type constraints} are inserted to allow the printing 
274 governed by the boolean variable \ttindex{show_types}: 
274 of types. This is governed by the boolean variable \ttindex{show_types}: 
275 \begin{itemize} 
275 \begin{itemize} 
276 \item $constrain(x, \tau) = x$ \ if $\tau = \mtt{dummyT}$ \index{*dummyT} or 
276 \item $constrain(x, \tau) = x$ \ if $\tau = \mtt{dummyT}$ \index{*dummyT} or 
277 \ttindex{show_types} not set to {\tt true}. 
277 \ttindex{show_types} is set to {\tt false}. 
278 
278 
279 \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, 
279 \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, 
280 \astofterm{\tau}}$ \ otherwise. 
280 \astofterm{\tau}}$ \ otherwise. 
281 
281 
282 Here, $\astofterm{\tau}$ is the \AST{} encoding of $\tau$: type 
282 Here, $\astofterm{\tau}$ is the \AST{} encoding of $\tau$: type 
287 of their sort. 
287 of their sort. 
288 \end{itemize} 
288 \end{itemize} 
289 % 
289 % 
290 The \AST{}, after application of macros (see \S\ref{sec:macros}), is 
290 The \AST{}, after application of macros (see \S\ref{sec:macros}), is 
291 transformed into the final output string. The builtin {\bf print AST 
291 transformed into the final output string. The builtin {\bf print AST 
292 translations}\indexbold{translations!print AST} effectively reverse the 
292 translations}\indexbold{translations!print AST} reverse the 
293 parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}. 
293 parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}. 
294 
294 
295 For the actual printing process, the names attached to productions 
295 For the actual printing process, the names attached to productions 
296 of the form $\ldots A^{(p@1)}@1 \ldots A^{(p@n)}@n \ldots \mtt{=>} c$ play 
296 of the form $\ldots A^{(p@1)}@1 \ldots A^{(p@n)}@n \ldots \mtt{=>} c$ play 
297 a vital role. Each \AST{} with constant head $c$, namely $\mtt"c\mtt"$ or 
297 a vital role. Each \AST{} with constant head $c$, namely $\mtt"c\mtt"$ or 
336 express all but the most obscure translations. 
336 express all but the most obscure translations. 
337 
337 
338 Figure~\ref{fig:set_trans} defines a fragment of firstorder logic and set 
338 Figure~\ref{fig:set_trans} defines a fragment of firstorder logic and set 
339 theory.\footnote{This and the following theories are complete working 
339 theory.\footnote{This and the following theories are complete working 
340 examples, though they specify only syntax, no axioms. The file {\tt 
340 examples, though they specify only syntax, no axioms. The file {\tt 
341 ZF/zf.thy} presents the full set theory definition, including many 
341 ZF/ZF.thy} presents the full set theory definition, including many 
342 macro rules.} Theory {\tt SET} defines constants for set comprehension 
342 macro rules.} Theory {\tt SET} defines constants for set comprehension 
343 ({\tt Collect}), replacement ({\tt Replace}) and bounded universal 
343 ({\tt Collect}), replacement ({\tt Replace}) and bounded universal 
344 quantification ({\tt Ball}). Each of these binds some variables. Without 
344 quantification ({\tt Ball}). Each of these binds some variables. Without 
345 additional syntax we should have to express $\forall x \in A. P$ as {\tt 
345 additional syntax we should have to write $\forall x \in A. P$ as {\tt 
346 Ball(A,\%x.P)}, and similarly for the others. 
346 Ball(A,\%x.P)}, and similarly for the others. 
347 
347 
348 \begin{figure} 
348 \begin{figure} 
349 \begin{ttbox} 
349 \begin{ttbox} 
350 SET = Pure + 
350 SET = Pure + 
462 
462 
463 \begin{warn} 
463 \begin{warn} 
464 If \ttindex{eta_contract} is set to {\tt true}, terms will be 
464 If \ttindex{eta_contract} is set to {\tt true}, terms will be 
465 $\eta$contracted {\em before\/} the \AST{} rewriter sees them. Thus some 
465 $\eta$contracted {\em before\/} the \AST{} rewriter sees them. Thus some 
466 abstraction nodes needed for print rules to match may vanish. For example, 
466 abstraction nodes needed for print rules to match may vanish. For example, 
467 \verbBall(A, %x. P(x)) contracts {\tt Ball(A, P)}; the print rule does 
467 \verbBall(A, %x. P(x)) contracts to {\tt Ball(A, P)}; the print rule does 
468 not apply and the output will be {\tt Ball(A, P)}. This problem would not 
468 not apply and the output will be {\tt Ball(A, P)}. This problem would not 
469 occur if \ML{} translation functions were used instead of macros (as is 
469 occur if \ML{} translation functions were used instead of macros (as is 
470 done for binder declarations). 
470 done for binder declarations). 
471 \end{warn} 
471 \end{warn} 
472 
472 
489 
489 
490 
490 
491 \subsection{Applying rules} 
491 \subsection{Applying rules} 
492 As a term is being parsed or printed, an \AST{} is generated as an 
492 As a term is being parsed or printed, an \AST{} is generated as an 
493 intermediate form (recall Fig.\ts\ref{fig:parse_print}). The \AST{} is 
493 intermediate form (recall Fig.\ts\ref{fig:parse_print}). The \AST{} is 
494 normalized by applying macro rules in the manner of a traditional term 
494 normalised by applying macro rules in the manner of a traditional term 
495 rewriting system. We first examine how a single rule is applied. 
495 rewriting system. We first examine how a single rule is applied. 
496 
496 
497 Let $t$ be the abstract syntax tree to be normalized and $(l, r)$ some 
497 Let $t$ be the abstract syntax tree to be normalised and $(l, r)$ some 
498 translation rule. A subtree~$u$ of $t$ is a {\bf redex} if it is an 
498 translation rule. A subtree~$u$ of $t$ is a {\bf redex} if it is an 
499 instance of~$l$; in this case $l$ is said to {\bf match}~$u$. A redex 
499 instance of~$l$; in this case $l$ is said to {\bf match}~$u$. A redex 
500 matched by $l$ may be replaced by the corresponding instance of~$r$, thus 
500 matched by $l$ may be replaced by the corresponding instance of~$r$, thus 
501 {\bf rewriting} the \AST~$t$. Matching requires some notion of {\bf 
501 {\bf rewriting} the \AST~$t$. Matching requires some notion of {\bf 
502 placeholders} that may occur in rule patterns but not in ordinary 
502 placeholders} that may occur in rule patterns but not in ordinary 
544 translations 
544 translations 
545 "[]" == "Nil" 
545 "[]" == "Nil" 
546 \end{ttbox} 
546 \end{ttbox} 
547 The term {\tt Nil} will be printed as {\tt []}, just as expected. 
547 The term {\tt Nil} will be printed as {\tt []}, just as expected. 
548 The term \verb%Nil.t will be printed as \verb%[].t, which might not be 
548 The term \verb%Nil.t will be printed as \verb%[].t, which might not be 
549 expected! 
549 expected! How is the type~{\tt Nil} printed? 
550 
550 
551 Normalizing an \AST{} involves repeatedly applying macro rules until none 
551 Normalizing an \AST{} involves repeatedly applying macro rules until none 
552 is applicable. Macro rules are chosen in the order that they appear in the 
552 are applicable. Macro rules are chosen in the order that they appear in the 
553 {\tt translations} section. You can watch the normalization of \AST{}s 
553 {\tt translations} section. You can watch the normalization of \AST{}s 
554 during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to 
554 during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to 
555 {\tt true}.\index{tracing!of macros} Alternatively, use 
555 {\tt true}.\index{tracing!of macros} Alternatively, use 
556 \ttindex{Syntax.test_read}. The information displayed when tracing 
556 \ttindex{Syntax.test_read}. The information displayed when tracing 
557 includes the \AST{} before normalization ({\tt pre}), redexes with results 
557 includes the \AST{} before normalization ({\tt pre}), redexes with results 
624 two elements, binding the first to {\tt x} and the rest to {\tt xs}. 
624 two elements, binding the first to {\tt x} and the rest to {\tt xs}. 
625 Likewise, \verb{xs} and \verb{x} represent any set enumeration. 
625 Likewise, \verb{xs} and \verb{x} represent any set enumeration. 
626 The parse rules only work in the order given. 
626 The parse rules only work in the order given. 
627 
627 
628 \begin{warn} 
628 \begin{warn} 
629 The \AST{} rewriter cannot discern constants from variables and looks 
629 The \AST{} rewriter cannot distinguish constants from variables and looks 
630 only for names of atoms. Thus the names of {\tt Constant}s occurring in 
630 only for names of atoms. Thus the names of {\tt Constant}s occurring in 
631 the (internal) lefthand side of translation rules should be regarded as 
631 the (internal) lefthand side of translation rules should be regarded as 
632 \rmindex{reserved words}. Choose nonidentifiers like {\tt\at Finset} or 
632 \rmindex{reserved words}. Choose nonidentifiers like {\tt\at Finset} or 
633 sufficiently long and strange names. If a bound variable's name gets 
633 sufficiently long and strange names. If a bound variable's name gets 
634 rewritten, the result will be incorrect; for example, the term 
634 rewritten, the result will be incorrect; for example, the term 
635 \begin{ttbox} 
635 \begin{ttbox} 
636 \%empty insert. insert(x, empty) 
636 \%empty insert. insert(x, empty) 
637 \end{ttbox} 
637 \end{ttbox} 
638 gets printed as \verb%empty insert. {x}. 
638 \par\noindent is printed as \verb%empty insert. {x}. 
639 \end{warn} 
639 \end{warn} 
640 
640 
641 
641 
642 \subsection{Example: a parse macro for dependent types}\label{prod_trans} 
642 \subsection{Example: a parse macro for dependent types}\label{prod_trans} 
643 \index{examples!of macros} 
643 \index{examples!of macros} 
688 \index{translations(} 
688 \index{translations(} 
689 % 
689 % 
690 This section describes the translation function mechanism. By writing 
690 This section describes the translation function mechanism. By writing 
691 \ML{} functions, you can do almost everything with terms or \AST{}s during 
691 \ML{} functions, you can do almost everything with terms or \AST{}s during 
692 parsing and printing. The logic \LK\ is a good example of sophisticated 
692 parsing and printing. The logic \LK\ is a good example of sophisticated 
693 transformations between internal and external representations of 
693 transformations between internal and external representations of sequents; 
694 associative sequences; here, macros would be useless. 
694 here, macros would be useless. 
695 
695 
696 A full understanding of translations requires some familiarity 
696 A full understanding of translations requires some familiarity 
697 with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ}, 
697 with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ}, 
698 {\tt Syntax.ast} and the encodings of types and terms as such at the various 
698 {\tt Syntax.ast} and the encodings of types and terms as such at the various 
699 stages of the parsing or printing process. Most users should never need to 
699 stages of the parsing or printing process. Most users should never need to 
803 in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts) 
803 in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts) 
804 end 
804 end 
805 else list_comb (Const (r, dummyT) $ A $ B, ts) 
805 else list_comb (Const (r, dummyT) $ A $ B, ts) 
806  dependent_tr' _ _ = raise Match; 
806  dependent_tr' _ _ = raise Match; 
807 \end{ttbox} 
807 \end{ttbox} 
808 The argument {\tt (q,r)} is supplied to {\tt dependent_tr'} by a curried 
808 The argument {\tt (q,r)} is supplied to the curried function {\tt 
809 function application during its installation. We could set up print 
809 dependent_tr'} by a partial application during its installation. We 
810 translations for both {\tt Pi} and {\tt Sigma} by including 
810 can set up print translations for both {\tt Pi} and {\tt Sigma} by 

811 including 
811 \begin{ttbox}\index{*ML section} 
812 \begin{ttbox}\index{*ML section} 
812 val print_translation = 
813 val print_translation = 
813 [("Pi", dependent_tr' ("{\at}PROD", "{\at}>")), 
814 [("Pi", dependent_tr' ("{\at}PROD", "{\at}>")), 
814 ("Sigma", dependent_tr' ("{\at}SUM", "{\at}*"))]; 
815 ("Sigma", dependent_tr' ("{\at}SUM", "{\at}*"))]; 
815 \end{ttbox} 
816 \end{ttbox} 
816 within the {\tt ML} section. The first of these transforms ${\tt Pi}(A, 
817 within the {\tt ML} section. The first of these transforms ${\tt Pi}(A, 
817 \mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or 
818 \mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or 
818 $\hbox{\tt{\at}>}r(A, B)$, choosing the latter form if $B$ does not depend 
819 $\hbox{\tt{\at}>}(A, B)$, choosing the latter form if $B$ does not depend 
819 on~$x$. It checks this using \ttindex{loose_bnos}, yet another function 
820 on~$x$. It checks this using \ttindex{loose_bnos}, yet another function 
820 from {\tt Pure/term.ML}. Note that $x'$ is a version of $x$ renamed away 
821 from {\tt Pure/term.ML}. Note that $x'$ is a version of $x$ renamed away 
821 from all names in $B$, and $B'$ the body $B$ with {\tt Bound} nodes 
822 from all names in $B$, and $B'$ is the body $B$ with {\tt Bound} nodes 
822 referring to our {\tt Abs} node replaced by $\ttfct{Free} (x', 
823 referring to the {\tt Abs} node replaced by $\ttfct{Free} (x', 
823 \mtt{dummyT})$. 
824 \mtt{dummyT})$. 
824 
825 
825 We must be careful with types here. While types of {\tt Const}s are 
826 We must be careful with types here. While types of {\tt Const}s are 
826 ignored, type constraints may be printed for some {\tt Free}s and 
827 ignored, type constraints may be printed for some {\tt Free}s and 
827 {\tt Var}s if \ttindex{show_types} is set to {\tt true}. Variables of type 
828 {\tt Var}s if \ttindex{show_types} is set to {\tt true}. Variables of type 