added section "The Pure grammar" (incomplete version, based on old ref manual);
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 "\<^bold>d"} is a delimiter, namely a non-empty
308 sequence of characters other than the special characters @{text "'"}
309 (single quote), @{text "_"} (underscore), @{text "\<index>"} (index
310 symbol), @{text "/"} (slash), @{text "("} and @{text ")"}
313 A single quote escapes the special meaning of these meta-characters,
314 producing a literal version of the following character, unless that
315 is a blank. A single quote followed by a blank separates
316 delimiters, without affecting printing, but input tokens may have
317 additional white space here.
319 \item @{text "_"} is an argument position, which stands for a
320 certain syntactic category in the underlying grammar.
322 \item @{text "\<index>"} is an indexed argument position; this is
323 the place where implicit structure arguments can be attached.
325 \item @{text "\<^bold>s"} is a non-empty sequence of spaces for
326 printing. This and the following specifications do not affect
329 \item @{text "(\<^bold>n"} opens a pretty printing block. The
330 optional number specifies how much indentation to add when a line
331 break occurs within the block. If the parenthesis is not followed
332 by digits, the indentation defaults to 0. A block specified via
333 @{text "(00"} is unbreakable.
335 \item @{text ")"} closes a pretty printing block.
337 \item @{text "//"} forces a line break.
339 \item @{text "/\<^bold>s"} allows a line break. Here @{text
340 "\<^bold>s"} stands for the string of spaces (zero or more) right
341 after the slash. These spaces are printed if the break is
346 For example, the template @{text "(_ +/ _)"} specifies an infix
347 operator. There are two argument positions; the delimiter @{text
348 "+"} is preceded by a space and followed by a space or line break;
349 the entire phrase is a pretty printing block.
351 The general idea of pretty printing with blocks and breaks is also
352 described in \cite{paulson-ml2}.
356 section {* Explicit term notation *}
359 \begin{matharray}{rcll}
360 @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
361 @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
365 ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
371 \item @{command "notation"}~@{text "c (mx)"} associates mixfix
372 syntax with an existing constant or fixed variable. This is a
373 robust interface to the underlying @{command "syntax"} primitive
374 (\secref{sec:syn-trans}). Type declaration and internal syntactic
375 representation of the given entity is retrieved from the context.
377 \item @{command "no_notation"} is similar to @{command "notation"},
378 but removes the specified syntax annotation from the present
384 section {* The Pure syntax *}
386 subsection {* Priority grammars *}
388 text {* A context-free grammar consists of a set of \emph{terminal
389 symbols}, a set of \emph{nonterminal symbols} and a set of
390 \emph{productions}. Productions have the form @{text "A = \<gamma>"},
391 where @{text A} is a nonterminal and @{text \<gamma>} is a string of
392 terminals and nonterminals. One designated nonterminal is called
393 the \emph{root symbol}. The language defined by the grammar
394 consists of all strings of terminals that can be derived from the
395 root symbol by applying productions as rewrite rules.
397 The standard Isabelle parser for inner syntax uses a \emph{priority
398 grammar}. Each nonterminal is decorated by an integer priority:
399 @{text "A\<^sup>(\<^sup>p\<^sup>)"}. In a derivation, @{text "A\<^sup>(\<^sup>p\<^sup>)"} may be rewritten
400 using a production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} only if @{text "p \<le> q"}. Any
401 priority grammar can be translated into a normal context-free
402 grammar by introducing new nonterminals and productions.
404 \medskip Formally, a set of context free productions @{text G}
405 induces a derivation relation @{text "\<longrightarrow>\<^sub>G"} as follows. Let @{text
406 \<alpha>} and @{text \<beta>} denote strings of terminal or nonterminal symbols.
409 @{text "\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>"}
411 if and only if @{text G} contains some production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"}
412 for @{text "p \<le> q"}.
414 \medskip The following grammar for arithmetic expressions
415 demonstrates how binding power and associativity of operators can be
416 enforced by priorities.
419 \begin{tabular}{rclr}
420 @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim 0} \\
421 @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim "("} @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim ")"} \\
422 @{text "A\<^sup>(\<^sup>0\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} \\
423 @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} \\
424 @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "="} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} \\
427 The choice of priorities determines that @{verbatim "-"} binds
428 tighter than @{verbatim "*"}, which binds tighter than @{verbatim
429 "+"}. Furthermore @{verbatim "+"} associates to the left and
430 @{verbatim "*"} to the right.
432 \medskip For clarity, grammars obey these conventions:
435 \item All priorities must lie between 0 and 1000.
437 \item Priority 0 on the right-hand side and priority 1000 on the
438 left-hand side may be omitted.
440 \item The production @{text "A\<^sup>(\<^sup>p\<^sup>) = \<alpha>"} is written as @{text "A = \<alpha>
441 (p)"}, i.e.\ the priority of the left-hand side actually appears in
442 a column on the far right.
444 \item Alternatives are separated by @{text "|"}.
446 \item Repetition is indicated by dots @{text "(\<dots>)"} in an informal
451 Using these conventions, the example grammar specification above
454 \begin{tabular}{rclc}
455 @{text A} & @{text "="} & @{verbatim 0} & \qquad\qquad \\
456 & @{text "|"} & @{verbatim "("} @{text A} @{verbatim ")"} \\
457 & @{text "|"} & @{text A} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} & @{text "(0)"} \\
458 & @{text "|"} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
459 & @{text "|"} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
465 subsection {* The Pure grammar *}
468 \begin{figure}[htb]\small
470 \begin{tabular}{rclc}
472 @{text any} & = & @{text "prop | logic"} \\\\
477 \caption{The Pure grammar}\label{fig:pure-grammar}
480 The priority grammar of the @{text "Pure"} theory is defined in
481 \figref{fig:pure-grammar}. The following nonterminals are
486 \item @{text "any"} denotes any term.
488 \item @{text "prop"} denotes meta-level propositions, which are
489 terms of type @{typ prop}. The syntax of such formulae of the
490 meta-logic is carefully distinguished from usual conventions for
491 object-logics. In particular, plain @{text "\<lambda>"}-term
492 notation is \emph{not} recognized as @{text "prop"}.
494 \item @{text aprop} denotes atomic propositions, which are embedded
495 into regular @{typ prop} by means of an explicit @{text "PROP"}
498 Terms of type @{typ prop} with non-constant head, e.g.\ a plain
499 variable, are printed in this form. Constants that yield type @{typ
500 prop} are expected to provide their own concrete syntax; otherwise
501 the printed version will appear like @{typ logic} and cannot be
502 parsed again as @{typ prop}.
504 \item @{text logic} denotes arbitrary terms of a logical type,
505 excluding type @{typ prop}. This is the main syntactic category of
506 object-logic entities, covering plain @{text \<lambda>}-term notation
507 (variables, abstraction, application), plus anything defined by the
510 When specifying notation for logical entities, all logical types
511 (excluding @{typ prop}) are \emph{collapsed} to this single category
514 \item @{text idt} denotes identifiers, possibly constrained by
517 \item @{text idts} denotes a sequence of @{text idt}. This is the
518 most basic category for variables in iterated binders, such as
519 @{text "\<lambda>"} or @{text "\<And>"}.
521 \item @{text pttrn} and @{text pttrns} denote patterns for
522 abstraction, cases bindings etc. In Pure, these categories start as
523 a merely copy of @{text idt} and @{text idts}, respectively.
524 Object-logics may add additional productions for binding forms.
526 \item @{text type} denotes types of the meta-logic.
528 \item @{text sort} denotes meta-level sorts.
533 In @{text idts}, note that @{text "x :: nat y"} is parsed as @{text
534 "x :: (nat y)"}, treating @{text y} like a type constructor applied
535 to @{text nat}. To avoid this interpretation, write @{text "(x ::
536 nat) y"} with explicit parentheses.
538 Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x ::
539 (nat y :: nat)"}. The correct form is @{text "(x :: nat) (y ::
540 nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the
541 sequence of identifiers.
545 Type constraints for terms bind very weakly. For example, @{text "x
546 < y :: nat"} is normally parsed as @{text "(x < y) :: nat"}, unless
547 @{text "<"} has a very low priority, in which case the input is
548 likely to be ambiguous. The correct form is @{text "x < (y :: nat)"}.
553 section {* Syntax and translations \label{sec:syn-trans} *}
556 \begin{matharray}{rcl}
557 @{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
558 @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
559 @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
560 @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
561 @{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
565 'nonterminals' (name +)
567 ('syntax' | 'no\_syntax') mode? (constdecl +)
569 ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
572 mode: ('(' ( name | 'output' | name 'output' ) ')')
574 transpat: ('(' nameref ')')? string
580 \item @{command "nonterminals"}~@{text c} declares a type
581 constructor @{text c} (without arguments) to act as purely syntactic
582 type: a nonterminal symbol of the inner syntax.
584 \item @{command "syntax"}~@{text "(mode) decls"} is similar to
585 @{command "consts"}~@{text decls}, except that the actual logical
586 signature extension is omitted. Thus the context free grammar of
587 Isabelle's inner syntax may be augmented in arbitrary ways,
588 independently of the logic. The @{text mode} argument refers to the
589 print mode that the grammar rules belong; unless the @{keyword_ref
590 "output"} indicator is given, all productions are added both to the
591 input and output grammar.
593 \item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar
594 declarations (and translations) resulting from @{text decls}, which
595 are interpreted in the same manner as for @{command "syntax"} above.
597 \item @{command "translations"}~@{text rules} specifies syntactic
598 translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
599 parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
600 Translation patterns may be prefixed by the syntactic category to be
601 used for parsing; the default is @{text logic}.
603 \item @{command "no_translations"}~@{text rules} removes syntactic
604 translation rules, which are interpreted in the same manner as for
605 @{command "translations"} above.
611 section {* Syntax translation functions *}
614 \begin{matharray}{rcl}
615 @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
616 @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
617 @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
618 @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
619 @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
623 ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
624 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
628 Syntax translation functions written in ML admit almost arbitrary
629 manipulations of Isabelle's inner syntax. Any of the above commands
630 have a single \railqtok{text} argument that refers to an ML
631 expression of appropriate type, which are as follows by default:
633 %FIXME proper antiquotations
635 val parse_ast_translation : (string * (ast list -> ast)) list
636 val parse_translation : (string * (term list -> term)) list
637 val print_translation : (string * (term list -> term)) list
638 val typed_print_translation :
639 (string * (bool -> typ -> term list -> term)) list
640 val print_ast_translation : (string * (ast list -> ast)) list
643 If the @{text "(advanced)"} option is given, the corresponding
644 translation functions may depend on the current theory or proof
645 context. This allows to implement advanced syntax mechanisms, as
646 translations functions may refer to specific theory declarations or
647 auxiliary proof data.
649 See also \cite[\S8]{isabelle-ref} for more information on the
650 general concept of syntax transformations in Isabelle.
652 %FIXME proper antiquotations
654 val parse_ast_translation:
655 (string * (Proof.context -> ast list -> ast)) list
656 val parse_translation:
657 (string * (Proof.context -> term list -> term)) list
658 val print_translation:
659 (string * (Proof.context -> term list -> term)) list
660 val typed_print_translation:
661 (string * (Proof.context -> bool -> typ -> term list -> term)) list
662 val print_ast_translation:
663 (string * (Proof.context -> ast list -> ast)) list