7 chapter {* Inner syntax --- the term language *}
9 section {* Printing logical entities *}
11 subsection {* Diagnostic commands *}
14 \begin{matharray}{rcl}
15 @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
16 @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
17 @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
18 @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
19 @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
20 @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
21 @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
24 These diagnostic commands assist interactive development by printing
25 internal logical entities in a human-readable fashion.
36 ( 'prf' | 'full\_prf' ) modes? thmrefs?
38 'pr' modes? nat? (',' nat)?
41 modes: '(' (name + ) ')'
47 \item @{command "typ"}~@{text \<tau>} reads and prints types of the
48 meta-logic according to the current theory or proof context.
50 \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
51 read, type-check and print terms or propositions according to the
52 current theory or proof context; the inferred type of @{text t} is
53 output as well. Note that these commands are also useful in
54 inspecting the current environment of term abbreviations.
56 \item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves
57 theorems from the current theory or proof context. Note that any
58 attributes included in the theorem specifications are applied to a
59 temporary context derived from the current theory or proof; the
60 result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
61 \<dots>, a\<^sub>n"} do not have any permanent effect.
63 \item @{command "prf"} displays the (compact) proof term of the
64 current proof state (if present), or of the given theorems. Note
65 that this requires proof terms to be switched on for the current
66 object logic (see the ``Proof terms'' section of the Isabelle
67 reference manual for information on how to do this).
69 \item @{command "full_prf"} is like @{command "prf"}, but displays
70 the full proof term, i.e.\ also displays information omitted in the
71 compact proof term, which is denoted by ``@{text _}'' placeholders
74 \item @{command "pr"}~@{text "goals, prems"} prints the current
75 proof state (if present), including the proof context, current facts
76 and goals. The optional limit arguments affect the number of goals
77 and premises to be displayed, which is initially 10 for both.
78 Omitting limit values leaves the current setting unchanged.
82 All of the diagnostic commands above admit a list of @{text modes}
83 to be specified, which is appended to the current print mode (see
84 also \cite{isabelle-ref}). Thus the output behavior may be modified
85 according particular print mode features. For example, @{command
86 "pr"}~@{text "(latex xsymbols)"} would print the current proof state
87 with mathematical symbols and special characters represented in
88 {\LaTeX} source, according to the Isabelle style
91 Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
92 systematic way to include formal items into the printed text
97 subsection {* Details of printed content *}
101 @{index_ML show_types: "bool ref"} & default @{ML false} \\
102 @{index_ML show_sorts: "bool ref"} & default @{ML false} \\
103 @{index_ML show_consts: "bool ref"} & default @{ML false} \\
104 @{index_ML long_names: "bool ref"} & default @{ML false} \\
105 @{index_ML short_names: "bool ref"} & default @{ML false} \\
106 @{index_ML unique_names: "bool ref"} & default @{ML true} \\
107 @{index_ML show_brackets: "bool ref"} & default @{ML false} \\
108 @{index_ML eta_contract: "bool ref"} & default @{ML true} \\
109 @{index_ML goals_limit: "int ref"} & default @{ML 10} \\
110 @{index_ML Proof.show_main_goal: "bool ref"} & default @{ML false} \\
111 @{index_ML show_hyps: "bool ref"} & default @{ML false} \\
112 @{index_ML show_tags: "bool ref"} & default @{ML false} \\
113 @{index_ML show_question_marks: "bool ref"} & default @{ML true} \\
116 These global ML variables control the detail of information that is
117 displayed for types, terms, theorems, goals etc.
119 In interactive sessions, the user interface usually manages these
120 global parameters of the Isabelle process, even with some concept of
121 persistence. Nonetheless it is occasionally useful to manipulate ML
122 variables directly, e.g.\ using @{command "ML_val"} or @{command
125 Batch-mode logic sessions may be configured by putting appropriate
126 ML text directly into the @{verbatim ROOT.ML} file.
130 \item @{ML show_types} and @{ML show_sorts} control printing of type
131 constraints for term variables, and sort constraints for type
132 variables. By default, neither of these are shown in output. If
133 @{ML show_sorts} is set to @{ML true}, types are always shown as
136 Note that displaying types and sorts may explain why a polymorphic
137 inference rule fails to resolve with some goal, or why a rewrite
138 rule does not apply as expected.
140 \item @{ML show_consts} controls printing of types of constants when
141 displaying a goal state.
143 Note that the output can be enormous, because polymorphic constants
144 often occur at several different type instances.
146 \item @{ML long_names}, @{ML short_names}, and @{ML unique_names}
147 control the way of printing fully qualified internal names in
148 external form. See also \secref{sec:antiq} for the document
149 antiquotation options of the same names.
151 \item @{ML show_brackets} controls bracketing in pretty printed
152 output. If set to @{ML true}, all sub-expressions of the pretty
153 printing tree will be parenthesized, even if this produces malformed
154 term syntax! This crude way of showing the internal structure of
155 pretty printed entities may occasionally help to diagnose problems
156 with operator priorities, for example.
158 \item @{ML eta_contract} controls @{text "\<eta>"}-contracted printing of
161 The @{text \<eta>}-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"},
162 provided @{text x} is not free in @{text f}. It asserts
163 \emph{extensionality} of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv>
164 g x"} for all @{text x}. Higher-order unification frequently puts
165 terms into a fully @{text \<eta>}-expanded form. For example, if @{text
166 F} has type @{text "(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>"} then its expanded form is @{term
167 "\<lambda>h. F (\<lambda>x. h x)"}.
169 Setting @{ML eta_contract} makes Isabelle perform @{text
170 \<eta>}-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"}
171 appears simply as @{text F}.
173 Note that the distinction between a term and its @{text \<eta>}-expanded
174 form occasionally matters. While higher-order resolution and
175 rewriting operate modulo @{text "\<alpha>\<beta>\<eta>"}-conversion, some other tools
176 might look at terms more discretely.
178 \item @{ML goals_limit} controls the maximum number of subgoals to
179 be shown in goal output.
181 \item @{ML Proof.show_main_goal} controls whether the main result to
182 be proven should be displayed. This information might be relevant
183 for schematic goals, to inspect the current claim that has been
186 \item @{ML show_hyps} controls printing of implicit hypotheses of
187 local facts. Normally, only those hypotheses are displayed that are
188 \emph{not} covered by the assumptions of the current context: this
189 situation indicates a fault in some tool being used.
191 By setting @{ML show_hyps} to @{ML true}, output of \emph{all}
192 hypotheses can be enforced, which is occasionally useful for
195 \item @{ML show_tags} controls printing of extra annotations within
196 theorems, such as internal position information, or the case names
197 being attached by the attribute @{attribute case_names}.
199 Note that the @{attribute tagged} and @{attribute untagged}
200 attributes provide low-level access to the collection of tags
201 associated with a theorem.
203 \item @{ML show_question_marks} controls printing of question marks
204 for schematic variables, such as @{text ?x}. Only the leading
205 question mark is affected, the remaining text is unchanged
206 (including proper markup for schematic variables that might be
207 relevant for user interfaces).
213 subsection {* Printing limits *}
217 @{index_ML Pretty.setdepth: "int -> unit"} \\
218 @{index_ML Pretty.setmargin: "int -> unit"} \\
219 @{index_ML print_depth: "int -> unit"} \\
222 These ML functions set limits for pretty printed text.
226 \item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to
227 limit the printing depth to @{text d}. This affects the display of
228 types, terms, theorems etc. The default value is 0, which permits
229 printing to an arbitrary depth. Other useful values for @{text d}
232 \item @{ML Pretty.setmargin}~@{text m} tells the pretty printer to
233 assume a right margin (page width) of @{text m}. The initial margin
234 is 76, but user interfaces might adapt the margin automatically when
237 \item @{ML print_depth}~@{text n} limits the printing depth of the
238 ML toplevel pretty printer; the precise effect depends on the ML
239 compiler and run-time system. Typically @{text n} should be less
240 than 10. Bigger values such as 100--1000 are useful for debugging.
246 section {* Mixfix annotations *}
248 text {* Mixfix annotations specify concrete \emph{inner syntax} of
249 Isabelle types and terms. Some commands such as @{command
250 "typedecl"} admit infixes only, while @{command "definition"} etc.\
251 support the full range of general mixfixes and binders. Fixed
252 parameters in toplevel theorem statements, locale specifications
253 also admit mixfix annotations.
255 \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
257 infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
259 mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
261 structmixfix: mixfix | '(' 'structure' ')'
264 prios: '[' (nat + ',') ']'
268 Here the \railtok{string} specifications refer to the actual mixfix
269 template, which may include literal text, spacing, blocks, and
270 arguments (denoted by ``@{text _}''); the special symbol
271 ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index
272 argument that specifies an implicit structure reference (see also
273 \secref{sec:locale}). Infix and binder declarations provide common
274 abbreviations for particular mixfix declarations. So in practice,
275 mixfix templates mostly degenerate to literal text for concrete
276 syntax, such as ``@{verbatim "++"}'' for an infix symbol.
278 \medskip In full generality, mixfix declarations work as follows.
279 Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is
280 annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text
281 "mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of
282 delimiters that surround argument positions as indicated by
285 Altogether this determines a production for a context-free priority
286 grammar, where for each argument @{text "i"} the syntactic category
287 is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and
288 the result category is determined from @{text "\<tau>"} (with
289 priority @{text "p"}). Priority specifications are optional, with
290 default 0 for arguments and 1000 for the result.
292 Since @{text "\<tau>"} may be again a function type, the constant
293 type scheme may have more argument positions than the mixfix
294 pattern. Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
295 @{text "m > n"} works by attaching concrete notation only to the
296 innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
297 instead. If a term has fewer arguments than specified in the mixfix
298 template, the concrete syntax is ignored.
300 \medskip A mixfix template may also contain additional directives
301 for pretty printing, notably spaces, blocks, and breaks. The
302 general template format is a sequence over any of the following
307 \item @{text "d"} is a delimiter, namely a non-empty sequence of
308 characters other than the following special characters:
312 @{verbatim "'"} & single quote \\
313 @{verbatim "_"} & underscore \\
314 @{text "\<index>"} & index symbol \\
315 @{verbatim "("} & open parenthesis \\
316 @{verbatim ")"} & close parenthesis \\
317 @{verbatim "/"} & slash \\
321 \item @{verbatim "'"} escapes the special meaning of these
322 meta-characters, producing a literal version of the following
323 character, unless that is a blank.
325 A single quote followed by a blank separates delimiters, without
326 affecting printing, but input tokens may have additional white space
329 \item @{verbatim "_"} is an argument position, which stands for a
330 certain syntactic category in the underlying grammar.
332 \item @{text "\<index>"} is an indexed argument position; this is the place
333 where implicit structure arguments can be attached.
335 \item @{text "s"} is a non-empty sequence of spaces for printing.
336 This and the following specifications do not affect parsing at all.
338 \item @{verbatim "("}@{text n} opens a pretty printing block. The
339 optional number specifies how much indentation to add when a line
340 break occurs within the block. If the parenthesis is not followed
341 by digits, the indentation defaults to 0. A block specified via
342 @{verbatim "(00"} is unbreakable.
344 \item @{verbatim ")"} closes a pretty printing block.
346 \item @{verbatim "//"} forces a line break.
348 \item @{verbatim "/"}@{text s} allows a line break. Here @{text s}
349 stands for the string of spaces (zero or more) right after the
350 slash. These spaces are printed if the break is \emph{not} taken.
354 For example, the template @{verbatim "(_ +/ _)"} specifies an infix
355 operator. There are two argument positions; the delimiter
356 @{verbatim "+"} is preceded by a space and followed by a space or
357 line break; the entire phrase is a pretty printing block.
359 The general idea of pretty printing with blocks and breaks is also
360 described in \cite{paulson-ml2}.
364 section {* Explicit term notation *}
367 \begin{matharray}{rcll}
368 @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
369 @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
373 ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
379 \item @{command "notation"}~@{text "c (mx)"} associates mixfix
380 syntax with an existing constant or fixed variable. This is a
381 robust interface to the underlying @{command "syntax"} primitive
382 (\secref{sec:syn-trans}). Type declaration and internal syntactic
383 representation of the given entity is retrieved from the context.
385 \item @{command "no_notation"} is similar to @{command "notation"},
386 but removes the specified syntax annotation from the present
392 section {* The Pure syntax *}
394 subsection {* Priority grammars *}
396 text {* A context-free grammar consists of a set of \emph{terminal
397 symbols}, a set of \emph{nonterminal symbols} and a set of
398 \emph{productions}. Productions have the form @{text "A = \<gamma>"},
399 where @{text A} is a nonterminal and @{text \<gamma>} is a string of
400 terminals and nonterminals. One designated nonterminal is called
401 the \emph{root symbol}. The language defined by the grammar
402 consists of all strings of terminals that can be derived from the
403 root symbol by applying productions as rewrite rules.
405 The standard Isabelle parser for inner syntax uses a \emph{priority
406 grammar}. Each nonterminal is decorated by an integer priority:
407 @{text "A\<^sup>(\<^sup>p\<^sup>)"}. In a derivation, @{text "A\<^sup>(\<^sup>p\<^sup>)"} may be rewritten
408 using a production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} only if @{text "p \<le> q"}. Any
409 priority grammar can be translated into a normal context-free
410 grammar by introducing new nonterminals and productions.
412 \medskip Formally, a set of context free productions @{text G}
413 induces a derivation relation @{text "\<longrightarrow>\<^sub>G"} as follows. Let @{text
414 \<alpha>} and @{text \<beta>} denote strings of terminal or nonterminal symbols.
417 @{text "\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>"}
419 if and only if @{text G} contains some production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"}
420 for @{text "p \<le> q"}.
422 \medskip The following grammar for arithmetic expressions
423 demonstrates how binding power and associativity of operators can be
424 enforced by priorities.
427 \begin{tabular}{rclr}
428 @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim 0} \\
429 @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim "("} @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim ")"} \\
430 @{text "A\<^sup>(\<^sup>0\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} \\
431 @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} \\
432 @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "="} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} \\
435 The choice of priorities determines that @{verbatim "-"} binds
436 tighter than @{verbatim "*"}, which binds tighter than @{verbatim
437 "+"}. Furthermore @{verbatim "+"} associates to the left and
438 @{verbatim "*"} to the right.
440 \medskip For clarity, grammars obey these conventions:
443 \item All priorities must lie between 0 and 1000.
445 \item Priority 0 on the right-hand side and priority 1000 on the
446 left-hand side may be omitted.
448 \item The production @{text "A\<^sup>(\<^sup>p\<^sup>) = \<alpha>"} is written as @{text "A = \<alpha>
449 (p)"}, i.e.\ the priority of the left-hand side actually appears in
450 a column on the far right.
452 \item Alternatives are separated by @{text "|"}.
454 \item Repetition is indicated by dots @{text "(\<dots>)"} in an informal
459 Using these conventions, the example grammar specification above
462 \begin{tabular}{rclc}
463 @{text A} & @{text "="} & @{verbatim 0} & \qquad\qquad \\
464 & @{text "|"} & @{verbatim "("} @{text A} @{verbatim ")"} \\
465 & @{text "|"} & @{text A} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} & @{text "(0)"} \\
466 & @{text "|"} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
467 & @{text "|"} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
473 subsection {* The Pure grammar *}
476 \begin{figure}[htb]\small
478 \begin{tabular}{rclc}
480 @{text any} & = & @{text "prop | logic"} \\\\
485 \caption{The Pure grammar}\label{fig:pure-grammar}
488 The priority grammar of the @{text "Pure"} theory is defined in
489 \figref{fig:pure-grammar}. The following nonterminals are
494 \item @{text "any"} denotes any term.
496 \item @{text "prop"} denotes meta-level propositions, which are
497 terms of type @{typ prop}. The syntax of such formulae of the
498 meta-logic is carefully distinguished from usual conventions for
499 object-logics. In particular, plain @{text "\<lambda>"}-term
500 notation is \emph{not} recognized as @{text "prop"}.
502 \item @{text aprop} denotes atomic propositions, which are embedded
503 into regular @{typ prop} by means of an explicit @{text "PROP"}
506 Terms of type @{typ prop} with non-constant head, e.g.\ a plain
507 variable, are printed in this form. Constants that yield type @{typ
508 prop} are expected to provide their own concrete syntax; otherwise
509 the printed version will appear like @{typ logic} and cannot be
510 parsed again as @{typ prop}.
512 \item @{text logic} denotes arbitrary terms of a logical type,
513 excluding type @{typ prop}. This is the main syntactic category of
514 object-logic entities, covering plain @{text \<lambda>}-term notation
515 (variables, abstraction, application), plus anything defined by the
518 When specifying notation for logical entities, all logical types
519 (excluding @{typ prop}) are \emph{collapsed} to this single category
522 \item @{text idt} denotes identifiers, possibly constrained by
525 \item @{text idts} denotes a sequence of @{text idt}. This is the
526 most basic category for variables in iterated binders, such as
527 @{text "\<lambda>"} or @{text "\<And>"}.
529 \item @{text pttrn} and @{text pttrns} denote patterns for
530 abstraction, cases bindings etc. In Pure, these categories start as
531 a merely copy of @{text idt} and @{text idts}, respectively.
532 Object-logics may add additional productions for binding forms.
534 \item @{text type} denotes types of the meta-logic.
536 \item @{text sort} denotes meta-level sorts.
541 In @{text idts}, note that @{text "x :: nat y"} is parsed as @{text
542 "x :: (nat y)"}, treating @{text y} like a type constructor applied
543 to @{text nat}. To avoid this interpretation, write @{text "(x ::
544 nat) y"} with explicit parentheses.
546 Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x ::
547 (nat y :: nat)"}. The correct form is @{text "(x :: nat) (y ::
548 nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the
549 sequence of identifiers.
553 Type constraints for terms bind very weakly. For example, @{text "x
554 < y :: nat"} is normally parsed as @{text "(x < y) :: nat"}, unless
555 @{text "<"} has a very low priority, in which case the input is
556 likely to be ambiguous. The correct form is @{text "x < (y :: nat)"}.
561 section {* Syntax and translations \label{sec:syn-trans} *}
564 \begin{matharray}{rcl}
565 @{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
566 @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
567 @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
568 @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
569 @{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
573 'nonterminals' (name +)
575 ('syntax' | 'no\_syntax') mode? (constdecl +)
577 ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
580 mode: ('(' ( name | 'output' | name 'output' ) ')')
582 transpat: ('(' nameref ')')? string
588 \item @{command "nonterminals"}~@{text c} declares a type
589 constructor @{text c} (without arguments) to act as purely syntactic
590 type: a nonterminal symbol of the inner syntax.
592 \item @{command "syntax"}~@{text "(mode) decls"} is similar to
593 @{command "consts"}~@{text decls}, except that the actual logical
594 signature extension is omitted. Thus the context free grammar of
595 Isabelle's inner syntax may be augmented in arbitrary ways,
596 independently of the logic. The @{text mode} argument refers to the
597 print mode that the grammar rules belong; unless the @{keyword_ref
598 "output"} indicator is given, all productions are added both to the
599 input and output grammar.
601 \item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar
602 declarations (and translations) resulting from @{text decls}, which
603 are interpreted in the same manner as for @{command "syntax"} above.
605 \item @{command "translations"}~@{text rules} specifies syntactic
606 translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
607 parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
608 Translation patterns may be prefixed by the syntactic category to be
609 used for parsing; the default is @{text logic}.
611 \item @{command "no_translations"}~@{text rules} removes syntactic
612 translation rules, which are interpreted in the same manner as for
613 @{command "translations"} above.
619 section {* Syntax translation functions *}
622 \begin{matharray}{rcl}
623 @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
624 @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
625 @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
626 @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
627 @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
631 ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
632 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
636 Syntax translation functions written in ML admit almost arbitrary
637 manipulations of Isabelle's inner syntax. Any of the above commands
638 have a single \railqtok{text} argument that refers to an ML
639 expression of appropriate type, which are as follows by default:
641 %FIXME proper antiquotations
643 val parse_ast_translation : (string * (ast list -> ast)) list
644 val parse_translation : (string * (term list -> term)) list
645 val print_translation : (string * (term list -> term)) list
646 val typed_print_translation :
647 (string * (bool -> typ -> term list -> term)) list
648 val print_ast_translation : (string * (ast list -> ast)) list
651 If the @{text "(advanced)"} option is given, the corresponding
652 translation functions may depend on the current theory or proof
653 context. This allows to implement advanced syntax mechanisms, as
654 translations functions may refer to specific theory declarations or
655 auxiliary proof data.
657 See also \cite[\S8]{isabelle-ref} for more information on the
658 general concept of syntax transformations in Isabelle.
660 %FIXME proper antiquotations
662 val parse_ast_translation:
663 (string * (Proof.context -> ast list -> ast)) list
664 val parse_translation:
665 (string * (Proof.context -> term list -> term)) list
666 val print_translation:
667 (string * (Proof.context -> term list -> term)) list
668 val typed_print_translation:
669 (string * (Proof.context -> bool -> typ -> term list -> term)) list
670 val print_ast_translation:
671 (string * (Proof.context -> ast list -> ast)) list