src/Doc/Isar_Ref/Inner_Syntax.thy
author wenzelm
Sun Feb 25 12:59:08 2018 +0100 (20 months ago)
changeset 67718 17874d43d3b3
parent 67513 731b1ad6759a
child 68249 949d93804740
permissions -rw-r--r--
notation for dummy sort;
     1 (*:maxLineLen=78:*)
     2 
     3 theory Inner_Syntax
     4   imports Main Base
     5 begin
     6 
     7 chapter \<open>Inner syntax --- the term language \label{ch:inner-syntax}\<close>
     8 
     9 text \<open>
    10   The inner syntax of Isabelle provides concrete notation for the main
    11   entities of the logical framework, notably \<open>\<lambda>\<close>-terms with types and type
    12   classes. Applications may either extend existing syntactic categories by
    13   additional notation, or define new sub-languages that are linked to the
    14   standard term language via some explicit markers. For example \<^verbatim>\<open>FOO\<close>~\<open>foo\<close>
    15   could embed the syntax corresponding for some user-defined nonterminal \<open>foo\<close>
    16   --- within the bounds of the given lexical syntax of Isabelle/Pure.
    17 
    18   The most basic way to specify concrete syntax for logical entities works via
    19   mixfix annotations (\secref{sec:mixfix}), which may be usually given as part
    20   of the original declaration or via explicit notation commands later on
    21   (\secref{sec:notation}). This already covers many needs of concrete syntax
    22   without having to understand the full complexity of inner syntax layers.
    23 
    24   Further details of the syntax engine involves the classical distinction of
    25   lexical language versus context-free grammar (see \secref{sec:pure-syntax}),
    26   and various mechanisms for \<^emph>\<open>syntax transformations\<close> (see
    27   \secref{sec:syntax-transformations}).
    28 \<close>
    29 
    30 
    31 section \<open>Printing logical entities\<close>
    32 
    33 subsection \<open>Diagnostic commands \label{sec:print-diag}\<close>
    34 
    35 text \<open>
    36   \begin{matharray}{rcl}
    37     @{command_def "typ"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
    38     @{command_def "term"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
    39     @{command_def "prop"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
    40     @{command_def "thm"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
    41     @{command_def "prf"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
    42     @{command_def "full_prf"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
    43     @{command_def "print_state"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
    44   \end{matharray}
    45 
    46   These diagnostic commands assist interactive development by printing
    47   internal logical entities in a human-readable fashion.
    48 
    49   @{rail \<open>
    50     @@{command typ} @{syntax modes}? @{syntax type} ('::' @{syntax sort})?
    51     ;
    52     @@{command term} @{syntax modes}? @{syntax term}
    53     ;
    54     @@{command prop} @{syntax modes}? @{syntax prop}
    55     ;
    56     @@{command thm} @{syntax modes}? @{syntax thms}
    57     ;
    58     ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thms}?
    59     ;
    60     @@{command print_state} @{syntax modes}?
    61     ;
    62     @{syntax_def modes}: '(' (@{syntax name} + ) ')'
    63   \<close>}
    64 
    65   \<^descr> @{command "typ"}~\<open>\<tau>\<close> reads and prints a type expression according to the
    66   current context.
    67 
    68   \<^descr> @{command "typ"}~\<open>\<tau> :: s\<close> uses type-inference to determine the most
    69   general way to make \<open>\<tau>\<close> conform to sort \<open>s\<close>. For concrete \<open>\<tau>\<close> this checks if
    70   the type belongs to that sort. Dummy type parameters ``\<open>_\<close>'' (underscore)
    71   are assigned to fresh type variables with most general sorts, according the
    72   the principles of type-inference.
    73 
    74     \<^descr> @{command "term"}~\<open>t\<close> and @{command "prop"}~\<open>\<phi>\<close> read, type-check and
    75     print terms or propositions according to the current theory or proof
    76     context; the inferred type of \<open>t\<close> is output as well. Note that these
    77     commands are also useful in inspecting the current environment of term
    78     abbreviations.
    79 
    80     \<^descr> @{command "thm"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> retrieves theorems from the current theory
    81     or proof context. Note that any attributes included in the theorem
    82     specifications are applied to a temporary context derived from the current
    83     theory or proof; the result is discarded, i.e.\ attributes involved in
    84     \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> do not have any permanent effect.
    85 
    86     \<^descr> @{command "prf"} displays the (compact) proof term of the current proof
    87     state (if present), or of the given theorems. Note that this requires an
    88     underlying logic image with proof terms enabled, e.g. \<open>HOL-Proofs\<close>.
    89 
    90     \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays the full
    91     proof term, i.e.\ also displays information omitted in the compact proof
    92     term, which is denoted by ``\<open>_\<close>'' placeholders there.
    93 
    94     \<^descr> @{command "print_state"} prints the current proof state (if present),
    95     including current facts and goals.
    96 
    97   All of the diagnostic commands above admit a list of \<open>modes\<close> to be
    98   specified, which is appended to the current print mode; see also
    99   \secref{sec:print-modes}. Thus the output behavior may be modified according
   100   particular print mode features. For example, @{command
   101   "print_state"}~\<open>(latex)\<close> prints the current proof state with mathematical
   102   symbols and special characters represented in {\LaTeX} source, according to
   103   the Isabelle style @{cite "isabelle-system"}.
   104 
   105   Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic
   106   way to include formal items into the printed text document.
   107 \<close>
   108 
   109 
   110 subsection \<open>Details of printed content\<close>
   111 
   112 text \<open>
   113   \begin{tabular}{rcll}
   114     @{attribute_def show_markup} & : & \<open>attribute\<close> \\
   115     @{attribute_def show_types} & : & \<open>attribute\<close> & default \<open>false\<close> \\
   116     @{attribute_def show_sorts} & : & \<open>attribute\<close> & default \<open>false\<close> \\
   117     @{attribute_def show_consts} & : & \<open>attribute\<close> & default \<open>false\<close> \\
   118     @{attribute_def show_abbrevs} & : & \<open>attribute\<close> & default \<open>true\<close> \\
   119     @{attribute_def show_brackets} & : & \<open>attribute\<close> & default \<open>false\<close> \\
   120     @{attribute_def names_long} & : & \<open>attribute\<close> & default \<open>false\<close> \\
   121     @{attribute_def names_short} & : & \<open>attribute\<close> & default \<open>false\<close> \\
   122     @{attribute_def names_unique} & : & \<open>attribute\<close> & default \<open>true\<close> \\
   123     @{attribute_def eta_contract} & : & \<open>attribute\<close> & default \<open>true\<close> \\
   124     @{attribute_def goals_limit} & : & \<open>attribute\<close> & default \<open>10\<close> \\
   125     @{attribute_def show_main_goal} & : & \<open>attribute\<close> & default \<open>false\<close> \\
   126     @{attribute_def show_hyps} & : & \<open>attribute\<close> & default \<open>false\<close> \\
   127     @{attribute_def show_tags} & : & \<open>attribute\<close> & default \<open>false\<close> \\
   128     @{attribute_def show_question_marks} & : & \<open>attribute\<close> & default \<open>true\<close> \\
   129   \end{tabular}
   130   \<^medskip>
   131 
   132   These configuration options control the detail of information that is
   133   displayed for types, terms, theorems, goals etc. See also
   134   \secref{sec:config}.
   135 
   136   \<^descr> @{attribute show_markup} controls direct inlining of markup into the
   137   printed representation of formal entities --- notably type and sort
   138   constraints. This enables Prover IDE users to retrieve that information via
   139   tooltips or popups while hovering with the mouse over the output window, for
   140   example. Consequently, this option is enabled by default for Isabelle/jEdit.
   141 
   142   \<^descr> @{attribute show_types} and @{attribute show_sorts} control printing of
   143   type constraints for term variables, and sort constraints for type
   144   variables. By default, neither of these are shown in output. If @{attribute
   145   show_sorts} is enabled, types are always shown as well. In Isabelle/jEdit,
   146   manual setting of these options is normally not required thanks to
   147   @{attribute show_markup} above.
   148 
   149   Note that displaying types and sorts may explain why a polymorphic inference
   150   rule fails to resolve with some goal, or why a rewrite rule does not apply
   151   as expected.
   152 
   153   \<^descr> @{attribute show_consts} controls printing of types of constants when
   154   displaying a goal state.
   155 
   156   Note that the output can be enormous, because polymorphic constants often
   157   occur at several different type instances.
   158 
   159   \<^descr> @{attribute show_abbrevs} controls folding of constant abbreviations.
   160 
   161   \<^descr> @{attribute show_brackets} controls bracketing in pretty printed output.
   162   If enabled, all sub-expressions of the pretty printing tree will be
   163   parenthesized, even if this produces malformed term syntax! This crude way
   164   of showing the internal structure of pretty printed entities may
   165   occasionally help to diagnose problems with operator priorities, for
   166   example.
   167 
   168   \<^descr> @{attribute names_long}, @{attribute names_short}, and @{attribute
   169   names_unique} control the way of printing fully qualified internal names in
   170   external form. See also \secref{sec:antiq} for the document antiquotation
   171   options of the same names.
   172 
   173   \<^descr> @{attribute eta_contract} controls \<open>\<eta>\<close>-contracted printing of terms.
   174 
   175   The \<open>\<eta>\<close>-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"}, provided \<open>x\<close> is not
   176   free in \<open>f\<close>. It asserts \<^emph>\<open>extensionality\<close> of functions: @{prop "f \<equiv> g"} if
   177   @{prop "f x \<equiv> g x"} for all \<open>x\<close>. Higher-order unification frequently puts
   178   terms into a fully \<open>\<eta>\<close>-expanded form. For example, if \<open>F\<close> has type \<open>(\<tau> \<Rightarrow> \<tau>)
   179   \<Rightarrow> \<tau>\<close> then its expanded form is @{term "\<lambda>h. F (\<lambda>x. h x)"}.
   180 
   181   Enabling @{attribute eta_contract} makes Isabelle perform \<open>\<eta>\<close>-contractions
   182   before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"} appears simply as \<open>F\<close>.
   183 
   184   Note that the distinction between a term and its \<open>\<eta>\<close>-expanded form
   185   occasionally matters. While higher-order resolution and rewriting operate
   186   modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion, some other tools might look at terms more
   187   discretely.
   188 
   189   \<^descr> @{attribute goals_limit} controls the maximum number of subgoals to be
   190   printed.
   191 
   192   \<^descr> @{attribute show_main_goal} controls whether the main result to be proven
   193   should be displayed. This information might be relevant for schematic goals,
   194   to inspect the current claim that has been synthesized so far.
   195 
   196   \<^descr> @{attribute show_hyps} controls printing of implicit hypotheses of local
   197   facts. Normally, only those hypotheses are displayed that are \<^emph>\<open>not\<close> covered
   198   by the assumptions of the current context: this situation indicates a fault
   199   in some tool being used.
   200 
   201   By enabling @{attribute show_hyps}, output of \<^emph>\<open>all\<close> hypotheses can be
   202   enforced, which is occasionally useful for diagnostic purposes.
   203 
   204   \<^descr> @{attribute show_tags} controls printing of extra annotations within
   205   theorems, such as internal position information, or the case names being
   206   attached by the attribute @{attribute case_names}.
   207 
   208   Note that the @{attribute tagged} and @{attribute untagged} attributes
   209   provide low-level access to the collection of tags associated with a
   210   theorem.
   211 
   212   \<^descr> @{attribute show_question_marks} controls printing of question marks for
   213   schematic variables, such as \<open>?x\<close>. Only the leading question mark is
   214   affected, the remaining text is unchanged (including proper markup for
   215   schematic variables that might be relevant for user interfaces).
   216 \<close>
   217 
   218 
   219 subsection \<open>Alternative print modes \label{sec:print-modes}\<close>
   220 
   221 text \<open>
   222   \begin{mldecls}
   223     @{index_ML print_mode_value: "unit -> string list"} \\
   224     @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\
   225   \end{mldecls}
   226 
   227   The \<^emph>\<open>print mode\<close> facility allows to modify various operations for printing.
   228   Commands like @{command typ}, @{command term}, @{command thm} (see
   229   \secref{sec:print-diag}) take additional print modes as optional argument.
   230   The underlying ML operations are as follows.
   231 
   232     \<^descr> @{ML "print_mode_value ()"} yields the list of currently active print
   233     mode names. This should be understood as symbolic representation of
   234     certain individual features for printing (with precedence from left to
   235     right).
   236 
   237     \<^descr> @{ML Print_Mode.with_modes}~\<open>modes f x\<close> evaluates \<open>f x\<close> in an execution
   238     context where the print mode is prepended by the given \<open>modes\<close>. This
   239     provides a thread-safe way to augment print modes. It is also monotonic in
   240     the set of mode names: it retains the default print mode that certain
   241     user-interfaces might have installed for their proper functioning!
   242 
   243   \<^medskip>
   244   The pretty printer for inner syntax maintains alternative mixfix productions
   245   for any print mode name invented by the user, say in commands like @{command
   246   notation} or @{command abbreviation}. Mode names can be arbitrary, but the
   247   following ones have a specific meaning by convention:
   248 
   249     \<^item> \<^verbatim>\<open>""\<close> (the empty string): default mode; implicitly active as last
   250     element in the list of modes.
   251 
   252     \<^item> \<^verbatim>\<open>input\<close>: dummy print mode that is never active; may be used to specify
   253     notation that is only available for input.
   254 
   255     \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active; used internally in
   256     Isabelle/Pure.
   257 
   258     \<^item> \<^verbatim>\<open>ASCII\<close>: prefer ASCII art over mathematical symbols.
   259 
   260     \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX} document
   261     preparation of Isabelle theory sources; allows to provide alternative
   262     output notation.
   263 \<close>
   264 
   265 
   266 section \<open>Mixfix annotations \label{sec:mixfix}\<close>
   267 
   268 text \<open>
   269   Mixfix annotations specify concrete \<^emph>\<open>inner syntax\<close> of Isabelle types and
   270   terms. Locally fixed parameters in toplevel theorem statements, locale and
   271   class specifications also admit mixfix annotations in a fairly uniform
   272   manner. A mixfix annotation describes the concrete syntax, the translation
   273   to abstract syntax, and the pretty printing. Special case annotations
   274   provide a simple means of specifying infix operators and binders.
   275 
   276   Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}. It allows to
   277   specify any context-free priority grammar, which is more general than the
   278   fixity declarations of ML and Prolog.
   279 
   280   @{rail \<open>
   281     @{syntax_def mixfix}: '('
   282       (@{syntax template} prios? @{syntax nat}? |
   283         (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
   284         @'binder' @{syntax template} prios? @{syntax nat} |
   285         @'structure') ')'
   286     ;
   287     @{syntax template}: string
   288     ;
   289     prios: '[' (@{syntax nat} + ',') ']'
   290   \<close>}
   291 
   292   The string given as \<open>template\<close> may include literal text, spacing, blocks,
   293   and arguments (denoted by ``\<open>_\<close>''); the special symbol ``\<^verbatim>\<open>\<index>\<close>'' (printed as
   294   ``\<open>\<index>\<close>'') represents an index argument that specifies an implicit @{keyword
   295   "structure"} reference (see also \secref{sec:locale}). Only locally fixed
   296   variables may be declared as @{keyword "structure"}.
   297 
   298   Infix and binder declarations provide common abbreviations for particular
   299   mixfix declarations. So in practice, mixfix templates mostly degenerate to
   300   literal text for concrete syntax, such as ``\<^verbatim>\<open>++\<close>'' for an infix symbol.
   301 \<close>
   302 
   303 
   304 subsection \<open>The general mixfix form\<close>
   305 
   306 text \<open>
   307   In full generality, mixfix declarations work as follows. Suppose a constant
   308   \<open>c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> is annotated by \<open>(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)\<close>, where
   309   \<open>mixfix\<close> is a string \<open>d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n\<close> consisting of delimiters that
   310   surround argument positions as indicated by underscores.
   311 
   312   Altogether this determines a production for a context-free priority grammar,
   313   where for each argument \<open>i\<close> the syntactic category is determined by \<open>\<tau>\<^sub>i\<close>
   314   (with priority \<open>p\<^sub>i\<close>), and the result category is determined from \<open>\<tau>\<close> (with
   315   priority \<open>p\<close>). Priority specifications are optional, with default 0 for
   316   arguments and 1000 for the result.\<^footnote>\<open>Omitting priorities is prone to
   317   syntactic ambiguities unless the delimiter tokens determine fully bracketed
   318   notation, as in \<open>if _ then _ else _ fi\<close>.\<close>
   319 
   320   Since \<open>\<tau>\<close> may be again a function type, the constant type scheme may have
   321   more argument positions than the mixfix pattern. Printing a nested
   322   application \<open>c t\<^sub>1 \<dots> t\<^sub>m\<close> for \<open>m > n\<close> works by attaching concrete notation
   323   only to the innermost part, essentially by printing \<open>(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m\<close>
   324   instead. If a term has fewer arguments than specified in the mixfix
   325   template, the concrete syntax is ignored.
   326 
   327   \<^medskip>
   328   A mixfix template may also contain additional directives for pretty
   329   printing, notably spaces, blocks, and breaks. The general template format is
   330   a sequence over any of the following entities.
   331 
   332   \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence delimiter items of the
   333   following form:
   334     \<^enum> a control symbol followed by a cartouche
   335     \<^enum> a single symbol, excluding the following special characters:
   336       \<^medskip>
   337       \begin{tabular}{ll}
   338         \<^verbatim>\<open>'\<close> & single quote \\
   339         \<^verbatim>\<open>_\<close> & underscore \\
   340         \<open>\<index>\<close> & index symbol \\
   341         \<^verbatim>\<open>(\<close> & open parenthesis \\
   342         \<^verbatim>\<open>)\<close> & close parenthesis \\
   343         \<^verbatim>\<open>/\<close> & slash \\
   344         \<open>\<open> \<close>\<close> & cartouche delimiters \\
   345       \end{tabular}
   346       \<^medskip>
   347 
   348   \<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these meta-characters, producing a
   349   literal version of the following character, unless that is a blank.
   350 
   351   A single quote followed by a blank separates delimiters, without affecting
   352   printing, but input tokens may have additional white space here.
   353 
   354   \<^descr> \<^verbatim>\<open>_\<close> is an argument position, which stands for a certain syntactic
   355   category in the underlying grammar.
   356 
   357   \<^descr> \<open>\<index>\<close> is an indexed argument position; this is the place where implicit
   358   structure arguments can be attached.
   359 
   360   \<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing. This and the following
   361   specifications do not affect parsing at all.
   362 
   363   \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block. The optional natural number
   364   specifies the block indentation, i.e. how much spaces to add when a line
   365   break occurs within the block. The default indentation is 0.
   366 
   367   \<^descr> \<^verbatim>\<open>(\<close>\<open>\<open>properties\<close>\<close> opens a pretty printing block, with properties
   368   specified within the given text cartouche. The syntax and semantics of
   369   the category @{syntax_ref mixfix_properties} is described below.
   370 
   371   \<^descr> \<^verbatim>\<open>)\<close> closes a pretty printing block.
   372 
   373   \<^descr> \<^verbatim>\<open>//\<close> forces a line break.
   374 
   375   \<^descr> \<^verbatim>\<open>/\<close>\<open>s\<close> allows a line break. Here \<open>s\<close> stands for the string of spaces
   376   (zero or more) right after the slash. These spaces are printed if the break
   377   is \<^emph>\<open>not\<close> taken.
   378 
   379 
   380   \<^medskip>
   381   Block properties allow more control over the details of pretty-printed
   382   output. The concrete syntax is defined as follows.
   383 
   384   @{rail \<open>
   385     @{syntax_def "mixfix_properties"}: (entry *)
   386     ;
   387     entry: atom ('=' atom)?
   388     ;
   389     atom: @{syntax short_ident} | @{syntax int} | @{syntax float} | @{syntax cartouche}
   390   \<close>}
   391 
   392   Each @{syntax entry} is a name-value pair: if the value is omitted, if
   393   defaults to \<^verbatim>\<open>true\<close> (intended for Boolean properties). The following
   394   standard block properties are supported:
   395 
   396     \<^item> \<open>indent\<close> (natural number): the block indentation --- the same as for the
   397     simple syntax without block properties.
   398 
   399     \<^item> \<open>consistent\<close> (Boolean): this block has consistent breaks (if one break
   400     is taken, all breaks are taken).
   401 
   402     \<^item> \<open>unbreakable\<close> (Boolean): all possible breaks of the block are disabled
   403     (turned into spaces).
   404 
   405     \<^item> \<open>markup\<close> (string): the optional name of the markup node. If this is
   406     provided, all remaining properties are turned into its XML attributes.
   407     This allows to specify free-form PIDE markup, e.g.\ for specialized
   408     output.
   409 
   410   \<^medskip>
   411   Note that the general idea of pretty printing with blocks and breaks is
   412   described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
   413 \<close>
   414 
   415 
   416 subsection \<open>Infixes\<close>
   417 
   418 text \<open>
   419   Infix operators are specified by convenient short forms that abbreviate
   420   general mixfix annotations as follows:
   421 
   422   \begin{center}
   423   \begin{tabular}{lll}
   424 
   425   \<^verbatim>\<open>(\<close>@{keyword_def "infix"}~\<^verbatim>\<open>"\<close>\<open>sy\<close>\<^verbatim>\<open>"\<close> \<open>p\<close>\<^verbatim>\<open>)\<close>
   426   & \<open>\<mapsto>\<close> &
   427   \<^verbatim>\<open>("(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)" [\<close>\<open>p + 1\<close>\<^verbatim>\<open>,\<close>~\<open>p + 1\<close>\<^verbatim>\<open>]\<close>~\<open>p\<close>\<^verbatim>\<open>)\<close> \\
   428   \<^verbatim>\<open>(\<close>@{keyword_def "infixl"}~\<^verbatim>\<open>"\<close>\<open>sy\<close>\<^verbatim>\<open>"\<close> \<open>p\<close>\<^verbatim>\<open>)\<close>
   429   & \<open>\<mapsto>\<close> &
   430   \<^verbatim>\<open>("(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)" [\<close>\<open>p\<close>\<^verbatim>\<open>,\<close>~\<open>p + 1\<close>\<^verbatim>\<open>]\<close>~\<open>p\<close>\<^verbatim>\<open>)\<close> \\
   431   \<^verbatim>\<open>(\<close>@{keyword_def "infixr"}~\<^verbatim>\<open>"\<close>\<open>sy\<close>\<^verbatim>\<open>"\<close>~\<open>p\<close>\<^verbatim>\<open>)\<close>
   432   & \<open>\<mapsto>\<close> &
   433   \<^verbatim>\<open>("(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)" [\<close>\<open>p + 1\<close>\<^verbatim>\<open>,\<close>~\<open>p\<close>\<^verbatim>\<open>]\<close>~\<open>p\<close>\<^verbatim>\<open>)\<close> \\
   434 
   435   \end{tabular}
   436   \end{center}
   437 
   438   The mixfix template \<^verbatim>\<open>"(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)"\<close> specifies two argument positions;
   439   the delimiter is preceded by a space and followed by a space or line break;
   440   the entire phrase is a pretty printing block.
   441 
   442   The alternative notation \<^verbatim>\<open>(\<close>\<open>sy\<close>\<^verbatim>\<open>)\<close> is introduced in addition. Thus any
   443   infix operator may be written in prefix form (as in Haskell), independently of
   444   the number of arguments in the term. To avoid conflict with the comment brackets
   445   \<^verbatim>\<open>(*\<close> and \<^verbatim>\<open>*)\<close>, infix operators that begin or end with a \<^verbatim>\<open>*\<close> require
   446   extra spaces, e.g. \<^verbatim>\<open>( * )\<close>.
   447 \<close>
   448 
   449 
   450 subsection \<open>Binders\<close>
   451 
   452 text \<open>
   453   A \<^emph>\<open>binder\<close> is a variable-binding construct such as a quantifier. The idea
   454   to formalize \<open>\<forall>x. b\<close> as \<open>All (\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close>
   455   already goes back to @{cite church40}. Isabelle declarations of certain
   456   higher-order operators may be annotated with @{keyword_def "binder"}
   457   annotations as follows:
   458 
   459   \begin{center}
   460   \<open>c ::\<close>~\<^verbatim>\<open>"\<close>\<open>(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3\<close>\<^verbatim>\<open>"  (\<close>@{keyword "binder"}~\<^verbatim>\<open>"\<close>\<open>sy\<close>\<^verbatim>\<open>" [\<close>\<open>p\<close>\<^verbatim>\<open>]\<close>~\<open>q\<close>\<^verbatim>\<open>)\<close>
   461   \end{center}
   462 
   463   This introduces concrete binder syntax \<open>sy x. b\<close>, where \<open>x\<close> is a bound
   464   variable of type \<open>\<tau>\<^sub>1\<close>, the body \<open>b\<close> has type \<open>\<tau>\<^sub>2\<close> and the whole term has
   465   type \<open>\<tau>\<^sub>3\<close>. The optional integer \<open>p\<close> specifies the syntactic priority of the
   466   body; the default is \<open>q\<close>, which is also the priority of the whole construct.
   467 
   468   Internally, the binder syntax is expanded to something like this:
   469   \begin{center}
   470   \<open>c_binder ::\<close>~\<^verbatim>\<open>"\<close>\<open>idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3\<close>\<^verbatim>\<open>"  ("(3\<close>\<open>sy\<close>\<^verbatim>\<open>_./ _)" [0,\<close>~\<open>p\<close>\<^verbatim>\<open>]\<close>~\<open>q\<close>\<^verbatim>\<open>)\<close>
   471   \end{center}
   472 
   473   Here @{syntax (inner) idts} is the nonterminal symbol for a list of
   474   identifiers with optional type constraints (see also
   475   \secref{sec:pure-grammar}). The mixfix template \<^verbatim>\<open>"(3\<close>\<open>sy\<close>\<^verbatim>\<open>_./ _)"\<close> defines
   476   argument positions for the bound identifiers and the body, separated by a
   477   dot with optional line break; the entire phrase is a pretty printing block
   478   of indentation level 3. Note that there is no extra space after \<open>sy\<close>, so it
   479   needs to be included user specification if the binder syntax ends with a
   480   token that may be continued by an identifier token at the start of @{syntax
   481   (inner) idts}.
   482 
   483   Furthermore, a syntax translation to transforms \<open>c_binder x\<^sub>1 \<dots> x\<^sub>n b\<close> into
   484   iterated application \<open>c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)\<close>. This works in both
   485   directions, for parsing and printing.
   486 \<close>
   487 
   488 
   489 section \<open>Explicit notation \label{sec:notation}\<close>
   490 
   491 text \<open>
   492   \begin{matharray}{rcll}
   493     @{command_def "type_notation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   494     @{command_def "no_type_notation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   495     @{command_def "notation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   496     @{command_def "no_notation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   497     @{command_def "write"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
   498   \end{matharray}
   499 
   500   Commands that introduce new logical entities (terms or types) usually allow
   501   to provide mixfix annotations on the spot, which is convenient for default
   502   notation. Nonetheless, the syntax may be modified later on by declarations
   503   for explicit notation. This allows to add or delete mixfix annotations for
   504   of existing logical entities within the current context.
   505 
   506   @{rail \<open>
   507     (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
   508       (@{syntax name} @{syntax mixfix} + @'and')
   509     ;
   510     (@@{command notation} | @@{command no_notation}) @{syntax mode}? \<newline>
   511       (@{syntax name} @{syntax mixfix} + @'and')
   512     ;
   513     @@{command write} @{syntax mode}? (@{syntax name} @{syntax mixfix} + @'and')
   514   \<close>}
   515 
   516   \<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix syntax with an
   517   existing type constructor. The arity of the constructor is retrieved from
   518   the context.
   519 
   520   \<^descr> @{command "no_type_notation"} is similar to @{command "type_notation"},
   521   but removes the specified syntax annotation from the present context.
   522 
   523   \<^descr> @{command "notation"}~\<open>c (mx)\<close> associates mixfix syntax with an existing
   524   constant or fixed variable. The type declaration of the given entity is
   525   retrieved from the context.
   526 
   527   \<^descr> @{command "no_notation"} is similar to @{command "notation"}, but removes
   528   the specified syntax annotation from the present context.
   529 
   530   \<^descr> @{command "write"} is similar to @{command "notation"}, but works within
   531   an Isar proof body.
   532 \<close>
   533 
   534 
   535 section \<open>The Pure syntax \label{sec:pure-syntax}\<close>
   536 
   537 subsection \<open>Lexical matters \label{sec:inner-lex}\<close>
   538 
   539 text \<open>
   540   The inner lexical syntax vaguely resembles the outer one
   541   (\secref{sec:outer-lex}), but some details are different. There are two main
   542   categories of inner syntax tokens:
   543 
   544   \<^enum> \<^emph>\<open>delimiters\<close> --- the literal tokens occurring in productions of the given
   545   priority grammar (cf.\ \secref{sec:priority-grammar});
   546 
   547   \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc.
   548 
   549 
   550   Delimiters override named tokens and may thus render certain identifiers
   551   inaccessible. Sometimes the logical context admits alternative ways to refer
   552   to the same entity, potentially via qualified names.
   553 
   554   \<^medskip>
   555   The categories for named tokens are defined once and for all as follows,
   556   reusing some categories of the outer token syntax (\secref{sec:outer-lex}).
   557 
   558   \begin{center}
   559   \begin{supertabular}{rcl}
   560     @{syntax_def (inner) id} & = & @{syntax_ref short_ident} \\
   561     @{syntax_def (inner) longid} & = & @{syntax_ref long_ident} \\
   562     @{syntax_def (inner) var} & = & @{syntax_ref var} \\
   563     @{syntax_def (inner) tid} & = & @{syntax_ref type_ident} \\
   564     @{syntax_def (inner) tvar} & = & @{syntax_ref type_var} \\
   565     @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
   566     @{syntax_def (inner) float_token} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
   567     @{syntax_def (inner) str_token} & = & \<^verbatim>\<open>''\<close> \<open>\<dots>\<close> \<^verbatim>\<open>''\<close> \\
   568     @{syntax_def (inner) string_token} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
   569     @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
   570   \end{supertabular}
   571   \end{center}
   572 
   573   The token categories @{syntax (inner) num_token}, @{syntax (inner)
   574   float_token}, @{syntax (inner) str_token}, @{syntax (inner) string_token},
   575   and @{syntax (inner) cartouche} are not used in Pure. Object-logics may
   576   implement numerals and string literals by adding appropriate syntax
   577   declarations, together with some translation functions (e.g.\ see
   578   \<^file>\<open>~~/src/HOL/Tools/string_syntax.ML\<close>).
   579 
   580   The derived categories @{syntax_def (inner) num_const}, and @{syntax_def
   581   (inner) float_const}, provide robust access to the respective tokens: the
   582   syntax tree holds a syntactic constant instead of a free variable.
   583 
   584   Formal document comments (\secref{sec:comments}) may be also used within the
   585   inner syntax.
   586 \<close>
   587 
   588 
   589 subsection \<open>Priority grammars \label{sec:priority-grammar}\<close>
   590 
   591 text \<open>
   592   A context-free grammar consists of a set of \<^emph>\<open>terminal symbols\<close>, a set of
   593   \<^emph>\<open>nonterminal symbols\<close> and a set of \<^emph>\<open>productions\<close>. Productions have the
   594   form \<open>A = \<gamma>\<close>, where \<open>A\<close> is a nonterminal and \<open>\<gamma>\<close> is a string of terminals
   595   and nonterminals. One designated nonterminal is called the \<^emph>\<open>root symbol\<close>.
   596   The language defined by the grammar consists of all strings of terminals
   597   that can be derived from the root symbol by applying productions as rewrite
   598   rules.
   599 
   600   The standard Isabelle parser for inner syntax uses a \<^emph>\<open>priority grammar\<close>.
   601   Each nonterminal is decorated by an integer priority: \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>. In a
   602   derivation, \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> may be rewritten using a production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> only
   603   if \<open>p \<le> q\<close>. Any priority grammar can be translated into a normal
   604   context-free grammar by introducing new nonterminals and productions.
   605 
   606   \<^medskip>
   607   Formally, a set of context free productions \<open>G\<close> induces a derivation
   608   relation \<open>\<longrightarrow>\<^sub>G\<close> as follows. Let \<open>\<alpha>\<close> and \<open>\<beta>\<close> denote strings of terminal or
   609   nonterminal symbols. Then \<open>\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>\<close> holds if and only if \<open>G\<close>
   610   contains some production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> for \<open>p \<le> q\<close>.
   611 
   612   \<^medskip>
   613   The following grammar for arithmetic expressions demonstrates how binding
   614   power and associativity of operators can be enforced by priorities.
   615 
   616   \begin{center}
   617   \begin{tabular}{rclr}
   618   \<open>A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>=\<close> & \<^verbatim>\<open>(\<close> \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> \<^verbatim>\<open>)\<close> \\
   619   \<open>A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>=\<close> & \<^verbatim>\<open>0\<close> \\
   620   \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> & \<open>=\<close> & \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> \<^verbatim>\<open>+\<close> \<open>A\<^sup>(\<^sup>1\<^sup>)\<close> \\
   621   \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>=\<close> & \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \<^verbatim>\<open>*\<close> \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> \\
   622   \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>=\<close> & \<^verbatim>\<open>-\<close> \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \\
   623   \end{tabular}
   624   \end{center}
   625   The choice of priorities determines that \<^verbatim>\<open>-\<close> binds tighter than \<^verbatim>\<open>*\<close>, which
   626   binds tighter than \<^verbatim>\<open>+\<close>. Furthermore \<^verbatim>\<open>+\<close> associates to the left and \<^verbatim>\<open>*\<close> to
   627   the right.
   628 
   629   \<^medskip>
   630   For clarity, grammars obey these conventions:
   631 
   632     \<^item> All priorities must lie between 0 and 1000.
   633 
   634     \<^item> Priority 0 on the right-hand side and priority 1000 on the left-hand
   635     side may be omitted.
   636 
   637     \<^item> The production \<open>A\<^sup>(\<^sup>p\<^sup>) = \<alpha>\<close> is written as \<open>A = \<alpha> (p)\<close>, i.e.\ the
   638     priority of the left-hand side actually appears in a column on the far
   639     right.
   640 
   641     \<^item> Alternatives are separated by \<open>|\<close>.
   642 
   643     \<^item> Repetition is indicated by dots \<open>(\<dots>)\<close> in an informal but obvious way.
   644 
   645   Using these conventions, the example grammar specification above
   646   takes the form:
   647   \begin{center}
   648   \begin{tabular}{rclc}
   649     \<open>A\<close> & \<open>=\<close> & \<^verbatim>\<open>(\<close> \<open>A\<close> \<^verbatim>\<open>)\<close> \\
   650               & \<open>|\<close> & \<^verbatim>\<open>0\<close> & \qquad\qquad \\
   651               & \<open>|\<close> & \<open>A\<close> \<^verbatim>\<open>+\<close> \<open>A\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(0)\<close> \\
   652               & \<open>|\<close> & \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \<^verbatim>\<open>*\<close> \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>(2)\<close> \\
   653               & \<open>|\<close> & \<^verbatim>\<open>-\<close> \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
   654   \end{tabular}
   655   \end{center}
   656 \<close>
   657 
   658 
   659 subsection \<open>The Pure grammar \label{sec:pure-grammar}\<close>
   660 
   661 text \<open>
   662   The priority grammar of the \<open>Pure\<close> theory is defined approximately like
   663   this:
   664 
   665   \begin{center}
   666   \begin{supertabular}{rclr}
   667 
   668   @{syntax_def (inner) any} & = & \<open>prop  |  logic\<close> \\\\
   669 
   670   @{syntax_def (inner) prop} & = & \<^verbatim>\<open>(\<close> \<open>prop\<close> \<^verbatim>\<open>)\<close> \\
   671     & \<open>|\<close> & \<open>prop\<^sup>(\<^sup>4\<^sup>)\<close> \<^verbatim>\<open>::\<close> \<open>type\<close> & \<open>(3)\<close> \\
   672     & \<open>|\<close> & \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> \<^verbatim>\<open>==\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(2)\<close> \\
   673     & \<open>|\<close> & \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> \<open>\<equiv>\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(2)\<close> \\
   674     & \<open>|\<close> & \<open>prop\<^sup>(\<^sup>3\<^sup>)\<close> \<^verbatim>\<open>&&&\<close> \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>(2)\<close> \\
   675     & \<open>|\<close> & \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> \<^verbatim>\<open>==>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
   676     & \<open>|\<close> & \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> \<open>\<Longrightarrow>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
   677     & \<open>|\<close> & \<^verbatim>\<open>[|\<close> \<open>prop\<close> \<^verbatim>\<open>;\<close> \<open>\<dots>\<close> \<^verbatim>\<open>;\<close> \<open>prop\<close> \<^verbatim>\<open>|]\<close> \<^verbatim>\<open>==>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
   678     & \<open>|\<close> & \<open>\<lbrakk>\<close> \<open>prop\<close> \<^verbatim>\<open>;\<close> \<open>\<dots>\<close> \<^verbatim>\<open>;\<close> \<open>prop\<close> \<open>\<rbrakk>\<close> \<open>\<Longrightarrow>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\
   679     & \<open>|\<close> & \<^verbatim>\<open>!!\<close> \<open>idts\<close> \<^verbatim>\<open>.\<close> \<open>prop\<close> & \<open>(0)\<close> \\
   680     & \<open>|\<close> & \<open>\<And>\<close> \<open>idts\<close> \<^verbatim>\<open>.\<close> \<open>prop\<close> & \<open>(0)\<close> \\
   681     & \<open>|\<close> & \<^verbatim>\<open>OFCLASS\<close> \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>,\<close> \<open>logic\<close> \<^verbatim>\<open>)\<close> \\
   682     & \<open>|\<close> & \<^verbatim>\<open>SORT_CONSTRAINT\<close> \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>)\<close> \\
   683     & \<open>|\<close> & \<^verbatim>\<open>TERM\<close> \<open>logic\<close> \\
   684     & \<open>|\<close> & \<^verbatim>\<open>PROP\<close> \<open>aprop\<close> \\\\
   685 
   686   @{syntax_def (inner) aprop} & = & \<^verbatim>\<open>(\<close> \<open>aprop\<close> \<^verbatim>\<open>)\<close> \\
   687     & \<open>|\<close> & \<open>id  |  longid  |  var  |\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>...\<close> \\
   688     & \<open>|\<close> & \<^verbatim>\<open>CONST\<close> \<open>id  |\<close>~~\<^verbatim>\<open>CONST\<close> \<open>longid\<close> \\
   689     & \<open>|\<close> & \<^verbatim>\<open>XCONST\<close> \<open>id  |\<close>~~\<^verbatim>\<open>XCONST\<close> \<open>longid\<close> \\
   690     & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>(999)\<close> \\\\
   691 
   692   @{syntax_def (inner) logic} & = & \<^verbatim>\<open>(\<close> \<open>logic\<close> \<^verbatim>\<open>)\<close> \\
   693     & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>4\<^sup>)\<close> \<^verbatim>\<open>::\<close> \<open>type\<close> & \<open>(3)\<close> \\
   694     & \<open>|\<close> & \<open>id  |  longid  |  var  |\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>...\<close> \\
   695     & \<open>|\<close> & \<^verbatim>\<open>CONST\<close> \<open>id  |\<close>~~\<^verbatim>\<open>CONST\<close> \<open>longid\<close> \\
   696     & \<open>|\<close> & \<^verbatim>\<open>XCONST\<close> \<open>id  |\<close>~~\<^verbatim>\<open>XCONST\<close> \<open>longid\<close> \\
   697     & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>(999)\<close> \\
   698     & \<open>|\<close> & \<^verbatim>\<open>%\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
   699     & \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
   700     & \<open>|\<close> & \<^verbatim>\<open>(==)\<close>~~\<open>|\<close>~~\<^verbatim>\<open>(\<close>\<open>\<equiv>\<close>\<^verbatim>\<open>)\<close>~~\<open>|\<close>~~\<^verbatim>\<open>(&&&)\<close> \\
   701     & \<open>|\<close> & \<^verbatim>\<open>(==>)\<close>~~\<open>|\<close>~~\<^verbatim>\<open>(\<close>\<open>\<Longrightarrow>\<close>\<^verbatim>\<open>)\<close> \\
   702     & \<open>|\<close> & \<^verbatim>\<open>TYPE\<close> \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>)\<close> \\\\
   703 
   704   @{syntax_def (inner) idt} & = & \<^verbatim>\<open>(\<close> \<open>idt\<close> \<^verbatim>\<open>)\<close>~~\<open>|  id  |\<close>~~\<^verbatim>\<open>_\<close> \\
   705     & \<open>|\<close> & \<open>id\<close> \<^verbatim>\<open>::\<close> \<open>type\<close> & \<open>(0)\<close> \\
   706     & \<open>|\<close> & \<^verbatim>\<open>_\<close> \<^verbatim>\<open>::\<close> \<open>type\<close> & \<open>(0)\<close> \\\\
   707 
   708   @{syntax_def (inner) index} & = & \<^verbatim>\<open>\<^bsub>\<close> \<open>logic\<^sup>(\<^sup>0\<^sup>)\<close> \<^verbatim>\<open>\<^esub>\<close>~~\<open>|  |  \<index>\<close> \\\\
   709 
   710   @{syntax_def (inner) idts} & = & \<open>idt  |  idt\<^sup>(\<^sup>1\<^sup>) idts\<close> & \<open>(0)\<close> \\\\
   711 
   712   @{syntax_def (inner) pttrn} & = & \<open>idt\<close> \\\\
   713 
   714   @{syntax_def (inner) pttrns} & = & \<open>pttrn  |  pttrn\<^sup>(\<^sup>1\<^sup>) pttrns\<close> & \<open>(0)\<close> \\\\
   715 
   716   @{syntax_def (inner) type} & = & \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>)\<close> \\
   717     & \<open>|\<close> & \<open>tid  |  tvar  |\<close>~~\<^verbatim>\<open>_\<close> \\
   718     & \<open>|\<close> & \<open>tid\<close> \<^verbatim>\<open>::\<close> \<open>sort  |  tvar\<close>~~\<^verbatim>\<open>::\<close> \<open>sort  |\<close>~~\<^verbatim>\<open>_\<close> \<^verbatim>\<open>::\<close> \<open>sort\<close> \\
   719     & \<open>|\<close> & \<open>type_name  |  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) type_name\<close> \\
   720     & \<open>|\<close> & \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> \<open>type\<close> \<^verbatim>\<open>)\<close> \<open>type_name\<close> \\
   721     & \<open>|\<close> & \<open>type\<^sup>(\<^sup>1\<^sup>)\<close> \<^verbatim>\<open>=>\<close> \<open>type\<close> & \<open>(0)\<close> \\
   722     & \<open>|\<close> & \<open>type\<^sup>(\<^sup>1\<^sup>)\<close> \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\
   723     & \<open>|\<close> & \<^verbatim>\<open>[\<close> \<open>type\<close> \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> \<open>type\<close> \<^verbatim>\<open>]\<close> \<^verbatim>\<open>=>\<close> \<open>type\<close> & \<open>(0)\<close> \\
   724     & \<open>|\<close> & \<^verbatim>\<open>[\<close> \<open>type\<close> \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> \<open>type\<close> \<^verbatim>\<open>]\<close> \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\
   725   @{syntax_def (inner) type_name} & = & \<open>id  |  longid\<close> \\\\
   726 
   727   @{syntax_def (inner) sort} & = & @{syntax class_name}~~\<open>|\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>{}\<close> \\
   728     & \<open>|\<close> & \<^verbatim>\<open>{\<close> @{syntax class_name} \<^verbatim>\<open>,\<close> \<open>\<dots>\<close> \<^verbatim>\<open>,\<close> @{syntax class_name} \<^verbatim>\<open>}\<close> \\
   729   @{syntax_def (inner) class_name} & = & \<open>id  |  longid\<close> \\
   730   \end{supertabular}
   731   \end{center}
   732 
   733   \<^medskip>
   734   Here literal terminals are printed \<^verbatim>\<open>verbatim\<close>; see also
   735   \secref{sec:inner-lex} for further token categories of the inner syntax. The
   736   meaning of the nonterminals defined by the above grammar is as follows:
   737 
   738   \<^descr> @{syntax_ref (inner) any} denotes any term.
   739 
   740   \<^descr> @{syntax_ref (inner) prop} denotes meta-level propositions, which are
   741   terms of type @{typ prop}. The syntax of such formulae of the meta-logic is
   742   carefully distinguished from usual conventions for object-logics. In
   743   particular, plain \<open>\<lambda>\<close>-term notation is \<^emph>\<open>not\<close> recognized as @{syntax (inner)
   744   prop}.
   745 
   746   \<^descr> @{syntax_ref (inner) aprop} denotes atomic propositions, which are
   747   embedded into regular @{syntax (inner) prop} by means of an explicit \<^verbatim>\<open>PROP\<close>
   748   token.
   749 
   750   Terms of type @{typ prop} with non-constant head, e.g.\ a plain variable,
   751   are printed in this form. Constants that yield type @{typ prop} are expected
   752   to provide their own concrete syntax; otherwise the printed version will
   753   appear like @{syntax (inner) logic} and cannot be parsed again as @{syntax
   754   (inner) prop}.
   755 
   756   \<^descr> @{syntax_ref (inner) logic} denotes arbitrary terms of a logical type,
   757   excluding type @{typ prop}. This is the main syntactic category of
   758   object-logic entities, covering plain \<open>\<lambda>\<close>-term notation (variables,
   759   abstraction, application), plus anything defined by the user.
   760 
   761   When specifying notation for logical entities, all logical types (excluding
   762   @{typ prop}) are \<^emph>\<open>collapsed\<close> to this single category of @{syntax (inner)
   763   logic}.
   764 
   765   \<^descr> @{syntax_ref (inner) index} denotes an optional index term for indexed
   766   syntax. If omitted, it refers to the first @{keyword_ref "structure"}
   767   variable in the context. The special dummy ``\<open>\<index>\<close>'' serves as pattern
   768   variable in mixfix annotations that introduce indexed notation.
   769 
   770   \<^descr> @{syntax_ref (inner) idt} denotes identifiers, possibly constrained by
   771   types.
   772 
   773   \<^descr> @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref (inner)
   774   idt}. This is the most basic category for variables in iterated binders,
   775   such as \<open>\<lambda>\<close> or \<open>\<And>\<close>.
   776 
   777   \<^descr> @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns} denote
   778   patterns for abstraction, cases bindings etc. In Pure, these categories
   779   start as a merely copy of @{syntax (inner) idt} and @{syntax (inner) idts},
   780   respectively. Object-logics may add additional productions for binding
   781   forms.
   782 
   783   \<^descr> @{syntax_ref (inner) type} denotes types of the meta-logic.
   784 
   785   \<^descr> @{syntax_ref (inner) sort} denotes meta-level sorts.
   786 
   787 
   788   Here are some further explanations of certain syntax features.
   789 
   790   \<^item> In @{syntax (inner) idts}, note that \<open>x :: nat y\<close> is parsed as \<open>x :: (nat
   791   y)\<close>, treating \<open>y\<close> like a type constructor applied to \<open>nat\<close>. To avoid this
   792   interpretation, write \<open>(x :: nat) y\<close> with explicit parentheses.
   793 
   794   \<^item> Similarly, \<open>x :: nat y :: nat\<close> is parsed as \<open>x :: (nat y :: nat)\<close>. The
   795   correct form is \<open>(x :: nat) (y :: nat)\<close>, or \<open>(x :: nat) y :: nat\<close> if \<open>y\<close> is
   796   last in the sequence of identifiers.
   797 
   798   \<^item> Type constraints for terms bind very weakly. For example, \<open>x < y :: nat\<close>
   799   is normally parsed as \<open>(x < y) :: nat\<close>, unless \<open><\<close> has a very low priority,
   800   in which case the input is likely to be ambiguous. The correct form is \<open>x <
   801   (y :: nat)\<close>.
   802 
   803   \<^item> Dummy variables (written as underscore) may occur in different
   804   roles.
   805 
   806     \<^descr> A sort ``\<open>_\<close>'' refers to a vacuous constraint for type variables, which
   807     is effectively ignored in type-inference.
   808 
   809     \<^descr> A type ``\<open>_\<close>'' or ``\<open>_ :: sort\<close>'' acts like an anonymous inference
   810     parameter, which is filled-in according to the most general type produced
   811     by the type-checking phase.
   812 
   813     \<^descr> A bound ``\<open>_\<close>'' refers to a vacuous abstraction, where the body does not
   814     refer to the binding introduced here. As in the term @{term "\<lambda>x _. x"},
   815     which is \<open>\<alpha>\<close>-equivalent to \<open>\<lambda>x y. x\<close>.
   816 
   817     \<^descr> A free ``\<open>_\<close>'' refers to an implicit outer binding. Higher definitional
   818     packages usually allow forms like \<open>f x _ = x\<close>.
   819 
   820     \<^descr> A schematic ``\<open>_\<close>'' (within a term pattern, see \secref{sec:term-decls})
   821     refers to an anonymous variable that is implicitly abstracted over its
   822     context of locally bound variables. For example, this allows pattern
   823     matching of \<open>{x. f x = g x}\<close> against \<open>{x. _ = _}\<close>, or even \<open>{_. _ = _}\<close> by
   824     using both bound and schematic dummies.
   825 
   826   \<^descr> The three literal dots ``\<^verbatim>\<open>...\<close>'' may be also written as ellipsis symbol
   827   \<^verbatim>\<open>\<dots>\<close>. In both cases this refers to a special schematic variable, which is
   828   bound in the context. This special term abbreviation works nicely with
   829   calculational reasoning (\secref{sec:calculation}).
   830 
   831   \<^descr> \<^verbatim>\<open>CONST\<close> ensures that the given identifier is treated as constant term,
   832   and passed through the parse tree in fully internalized form. This is
   833   particularly relevant for translation rules (\secref{sec:syn-trans}),
   834   notably on the RHS.
   835 
   836   \<^descr> \<^verbatim>\<open>XCONST\<close> is similar to \<^verbatim>\<open>CONST\<close>, but retains the constant name as given.
   837   This is only relevant to translation rules (\secref{sec:syn-trans}), notably
   838   on the LHS.
   839 \<close>
   840 
   841 
   842 subsection \<open>Inspecting the syntax\<close>
   843 
   844 text \<open>
   845   \begin{matharray}{rcl}
   846     @{command_def "print_syntax"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   847   \end{matharray}
   848 
   849   \<^descr> @{command "print_syntax"} prints the inner syntax of the current context.
   850   The output can be quite large; the most important sections are explained
   851   below.
   852 
   853     \<^descr> \<open>lexicon\<close> lists the delimiters of the inner token language; see
   854     \secref{sec:inner-lex}.
   855 
   856     \<^descr> \<open>productions\<close> lists the productions of the underlying priority grammar;
   857     see \secref{sec:priority-grammar}.
   858 
   859     Many productions have an extra \<open>\<dots> \<^bold>\<Rightarrow> name\<close>. These names later become the
   860     heads of parse trees; they also guide the pretty printer.
   861 
   862     Productions without such parse tree names are called \<^emph>\<open>copy productions\<close>.
   863     Their right-hand side must have exactly one nonterminal symbol (or named
   864     token). The parser does not create a new parse tree node for copy
   865     productions, but simply returns the parse tree of the right-hand symbol.
   866 
   867     If the right-hand side of a copy production consists of a single
   868     nonterminal without any delimiters, then it is called a \<^emph>\<open>chain
   869     production\<close>. Chain productions act as abbreviations: conceptually, they
   870     are removed from the grammar by adding new productions. Priority
   871     information attached to chain productions is ignored.
   872 
   873     \<^descr> \<open>print modes\<close> lists the alternative print modes provided by this
   874     grammar; see \secref{sec:print-modes}.
   875 
   876     \<^descr> \<open>parse_rules\<close> and \<open>print_rules\<close> relate to syntax translations (macros);
   877     see \secref{sec:syn-trans}.
   878 
   879     \<^descr> \<open>parse_ast_translation\<close> and \<open>print_ast_translation\<close> list sets of
   880     constants that invoke translation functions for abstract syntax trees,
   881     which are only required in very special situations; see
   882     \secref{sec:tr-funs}.
   883 
   884     \<^descr> \<open>parse_translation\<close> and \<open>print_translation\<close> list the sets of constants
   885     that invoke regular translation functions; see \secref{sec:tr-funs}.
   886 \<close>
   887 
   888 
   889 subsection \<open>Ambiguity of parsed expressions\<close>
   890 
   891 text \<open>
   892   \begin{tabular}{rcll}
   893     @{attribute_def syntax_ambiguity_warning} & : & \<open>attribute\<close> & default \<open>true\<close> \\
   894     @{attribute_def syntax_ambiguity_limit} & : & \<open>attribute\<close> & default \<open>10\<close> \\
   895   \end{tabular}
   896 
   897   Depending on the grammar and the given input, parsing may be ambiguous.
   898   Isabelle lets the Earley parser enumerate all possible parse trees, and then
   899   tries to make the best out of the situation. Terms that cannot be
   900   type-checked are filtered out, which often leads to a unique result in the
   901   end. Unlike regular type reconstruction, which is applied to the whole
   902   collection of input terms simultaneously, the filtering stage only treats
   903   each given term in isolation. Filtering is also not attempted for individual
   904   types or raw ASTs (as required for @{command translations}).
   905 
   906   Certain warning or error messages are printed, depending on the situation
   907   and the given configuration options. Parsing ultimately fails, if multiple
   908   results remain after the filtering phase.
   909 
   910   \<^descr> @{attribute syntax_ambiguity_warning} controls output of explicit warning
   911   messages about syntax ambiguity.
   912 
   913   \<^descr> @{attribute syntax_ambiguity_limit} determines the number of resulting
   914   parse trees that are shown as part of the printed message in case of an
   915   ambiguity.
   916 \<close>
   917 
   918 
   919 section \<open>Syntax transformations \label{sec:syntax-transformations}\<close>
   920 
   921 text \<open>
   922   The inner syntax engine of Isabelle provides separate mechanisms to
   923   transform parse trees either via rewrite systems on first-order ASTs
   924   (\secref{sec:syn-trans}), or ML functions on ASTs or syntactic \<open>\<lambda>\<close>-terms
   925   (\secref{sec:tr-funs}). This works both for parsing and printing, as
   926   outlined in \figref{fig:parse-print}.
   927 
   928   \begin{figure}[htbp]
   929   \begin{center}
   930   \begin{tabular}{cl}
   931   string          & \\
   932   \<open>\<down>\<close>     & lexer + parser \\
   933   parse tree      & \\
   934   \<open>\<down>\<close>     & parse AST translation \\
   935   AST             & \\
   936   \<open>\<down>\<close>     & AST rewriting (macros) \\
   937   AST             & \\
   938   \<open>\<down>\<close>     & parse translation \\
   939   --- pre-term ---    & \\
   940   \<open>\<down>\<close>     & print translation \\
   941   AST             & \\
   942   \<open>\<down>\<close>     & AST rewriting (macros) \\
   943   AST             & \\
   944   \<open>\<down>\<close>     & print AST translation \\
   945   string          &
   946   \end{tabular}
   947   \end{center}
   948   \caption{Parsing and printing with translations}\label{fig:parse-print}
   949   \end{figure}
   950 
   951   These intermediate syntax tree formats eventually lead to a pre-term with
   952   all names and binding scopes resolved, but most type information still
   953   missing. Explicit type constraints might be given by the user, or implicit
   954   position information by the system --- both need to be passed-through
   955   carefully by syntax transformations.
   956 
   957   Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and \<^emph>\<open>uncheck\<close>
   958   phases that are intertwined with type-inference (see also @{cite
   959   "isabelle-implementation"}). The latter allows to operate on higher-order
   960   abstract syntax with proper binding and type information already available.
   961 
   962   As a rule of thumb, anything that manipulates bindings of variables or
   963   constants needs to be implemented as syntax transformation (see below).
   964   Anything else is better done via check/uncheck: a prominent example
   965   application is the @{command abbreviation} concept of Isabelle/Pure.
   966 \<close>
   967 
   968 
   969 subsection \<open>Abstract syntax trees \label{sec:ast}\<close>
   970 
   971 text \<open>
   972   The ML datatype @{ML_type Ast.ast} explicitly represents the intermediate
   973   AST format that is used for syntax rewriting (\secref{sec:syn-trans}). It is
   974   defined in ML as follows:
   975   @{verbatim [display]
   976 \<open>datatype ast =
   977   Constant of string |
   978   Variable of string |
   979   Appl of ast list\<close>}
   980 
   981   An AST is either an atom (constant or variable) or a list of (at least two)
   982   subtrees. Occasional diagnostic output of ASTs uses notation that resembles
   983   S-expression of LISP. Constant atoms are shown as quoted strings, variable
   984   atoms as non-quoted strings and applications as a parenthesized list of
   985   subtrees. For example, the AST
   986   @{ML [display] \<open>Ast.Appl [Ast.Constant "_abs", Ast.Variable "x", Ast.Variable "t"]\<close>}
   987   is pretty-printed as \<^verbatim>\<open>("_abs" x t)\<close>. Note that \<^verbatim>\<open>()\<close> and \<^verbatim>\<open>(x)\<close> are
   988   excluded as ASTs, because they have too few subtrees.
   989 
   990   \<^medskip>
   991   AST application is merely a pro-forma mechanism to indicate certain
   992   syntactic structures. Thus \<^verbatim>\<open>(c a b)\<close> could mean either term application or
   993   type application, depending on the syntactic context.
   994 
   995   Nested application like \<^verbatim>\<open>(("_abs" x t) u)\<close> is also possible, but ASTs are
   996   definitely first-order: the syntax constant \<^verbatim>\<open>"_abs"\<close> does not bind the \<^verbatim>\<open>x\<close>
   997   in any way. Proper bindings are introduced in later stages of the term
   998   syntax, where \<^verbatim>\<open>("_abs" x t)\<close> becomes an @{ML Abs} node and occurrences of
   999   \<^verbatim>\<open>x\<close> in \<^verbatim>\<open>t\<close> are replaced by bound variables (represented as de-Bruijn
  1000   indices).
  1001 \<close>
  1002 
  1003 
  1004 subsubsection \<open>AST constants versus variables\<close>
  1005 
  1006 text \<open>
  1007   Depending on the situation --- input syntax, output syntax, translation
  1008   patterns --- the distinction of atomic ASTs as @{ML Ast.Constant} versus
  1009   @{ML Ast.Variable} serves slightly different purposes.
  1010 
  1011   Input syntax of a term such as \<open>f a b = c\<close> does not yet indicate the scopes
  1012   of atomic entities \<open>f, a, b, c\<close>: they could be global constants or local
  1013   variables, even bound ones depending on the context of the term. @{ML
  1014   Ast.Variable} leaves this choice still open: later syntax layers (or
  1015   translation functions) may capture such a variable to determine its role
  1016   specifically, to make it a constant, bound variable, free variable etc. In
  1017   contrast, syntax translations that introduce already known constants would
  1018   rather do it via @{ML Ast.Constant} to prevent accidental re-interpretation
  1019   later on.
  1020 
  1021   Output syntax turns term constants into @{ML Ast.Constant} and variables
  1022   (free or schematic) into @{ML Ast.Variable}. This information is precise
  1023   when printing fully formal \<open>\<lambda>\<close>-terms.
  1024 
  1025   \<^medskip>
  1026   AST translation patterns (\secref{sec:syn-trans}) that represent terms
  1027   cannot distinguish constants and variables syntactically. Explicit
  1028   indication of \<open>CONST c\<close> inside the term language is required, unless \<open>c\<close> is
  1029   known as special \<^emph>\<open>syntax constant\<close> (see also @{command syntax}). It is also
  1030   possible to use @{command syntax} declarations (without mixfix annotation)
  1031   to enforce that certain unqualified names are always treated as constant
  1032   within the syntax machinery.
  1033 
  1034   The situation is simpler for ASTs that represent types or sorts, since the
  1035   concrete syntax already distinguishes type variables from type constants
  1036   (constructors). So \<open>('a, 'b) foo\<close> corresponds to an AST application of some
  1037   constant for \<open>foo\<close> and variable arguments for \<open>'a\<close> and \<open>'b\<close>. Note that the
  1038   postfix application is merely a feature of the concrete syntax, while in the
  1039   AST the constructor occurs in head position.
  1040 \<close>
  1041 
  1042 
  1043 subsubsection \<open>Authentic syntax names\<close>
  1044 
  1045 text \<open>
  1046   Naming constant entities within ASTs is another delicate issue. Unqualified
  1047   names are resolved in the name space tables in the last stage of parsing,
  1048   after all translations have been applied. Since syntax transformations do
  1049   not know about this later name resolution, there can be surprises in
  1050   boundary cases.
  1051 
  1052   \<^emph>\<open>Authentic syntax names\<close> for @{ML Ast.Constant} avoid this problem: the
  1053   fully-qualified constant name with a special prefix for its formal category
  1054   (\<open>class\<close>, \<open>type\<close>, \<open>const\<close>, \<open>fixed\<close>) represents the information faithfully
  1055   within the untyped AST format. Accidental overlap with free or bound
  1056   variables is excluded as well. Authentic syntax names work implicitly in the
  1057   following situations:
  1058 
  1059     \<^item> Input of term constants (or fixed variables) that are introduced by
  1060     concrete syntax via @{command notation}: the correspondence of a
  1061     particular grammar production to some known term entity is preserved.
  1062 
  1063     \<^item> Input of type constants (constructors) and type classes --- thanks to
  1064     explicit syntactic distinction independently on the context.
  1065 
  1066     \<^item> Output of term constants, type constants, type classes --- this
  1067     information is already available from the internal term to be printed.
  1068 
  1069   In other words, syntax transformations that operate on input terms written
  1070   as prefix applications are difficult to make robust. Luckily, this case
  1071   rarely occurs in practice, because syntax forms to be translated usually
  1072   correspond to some concrete notation.
  1073 \<close>
  1074 
  1075 
  1076 subsection \<open>Raw syntax and translations \label{sec:syn-trans}\<close>
  1077 
  1078 text \<open>
  1079   \begin{tabular}{rcll}
  1080     @{command_def "nonterminal"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1081     @{command_def "syntax"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1082     @{command_def "no_syntax"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1083     @{command_def "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1084     @{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1085     @{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
  1086     @{attribute_def syntax_ast_stats} & : & \<open>attribute\<close> & default \<open>false\<close> \\
  1087   \end{tabular}
  1088   \<^medskip>
  1089 
  1090   Unlike mixfix notation for existing formal entities (\secref{sec:notation}),
  1091   raw syntax declarations provide full access to the priority grammar of the
  1092   inner syntax, without any sanity checks. This includes additional syntactic
  1093   categories (via @{command nonterminal}) and free-form grammar productions
  1094   (via @{command syntax}). Additional syntax translations (or macros, via
  1095   @{command translations}) are required to turn resulting parse trees into
  1096   proper representations of formal entities again.
  1097 
  1098   @{rail \<open>
  1099     @@{command nonterminal} (@{syntax name} + @'and')
  1100     ;
  1101     (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +)
  1102     ;
  1103     (@@{command translations} | @@{command no_translations})
  1104       (transpat ('==' | '=>' | '<=' | '\<rightleftharpoons>' | '\<rightharpoonup>' | '\<leftharpoondown>') transpat +)
  1105     ;
  1106 
  1107     constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
  1108     ;
  1109     mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
  1110     ;
  1111     transpat: ('(' @{syntax name} ')')? @{syntax string}
  1112   \<close>}
  1113 
  1114   \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without
  1115   arguments) to act as purely syntactic type: a nonterminal symbol of the
  1116   inner syntax.
  1117 
  1118   \<^descr> @{command "syntax"}~\<open>(mode) c :: \<sigma> (mx)\<close> augments the priority grammar and
  1119   the pretty printer table for the given print mode (default \<^verbatim>\<open>""\<close>). An
  1120   optional keyword @{keyword_ref "output"} means that only the pretty printer
  1121   table is affected.
  1122 
  1123   Following \secref{sec:mixfix}, the mixfix annotation \<open>mx = template ps q\<close>
  1124   together with type \<open>\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> and specify a grammar production.
  1125   The \<open>template\<close> contains delimiter tokens that surround \<open>n\<close> argument
  1126   positions (\<^verbatim>\<open>_\<close>). The latter correspond to nonterminal symbols \<open>A\<^sub>i\<close> derived
  1127   from the argument types \<open>\<tau>\<^sub>i\<close> as follows:
  1128 
  1129     \<^item> \<open>prop\<close> if \<open>\<tau>\<^sub>i = prop\<close>
  1130 
  1131     \<^item> \<open>logic\<close> if \<open>\<tau>\<^sub>i = (\<dots>)\<kappa>\<close> for logical type constructor \<open>\<kappa> \<noteq> prop\<close>
  1132 
  1133     \<^item> \<open>any\<close> if \<open>\<tau>\<^sub>i = \<alpha>\<close> for type variables
  1134 
  1135     \<^item> \<open>\<kappa>\<close> if \<open>\<tau>\<^sub>i = \<kappa>\<close> for nonterminal \<open>\<kappa>\<close> (syntactic type constructor)
  1136 
  1137   Each \<open>A\<^sub>i\<close> is decorated by priority \<open>p\<^sub>i\<close> from the given list \<open>ps\<close>; missing
  1138   priorities default to 0.
  1139 
  1140   The resulting nonterminal of the production is determined similarly from
  1141   type \<open>\<tau>\<close>, with priority \<open>q\<close> and default 1000.
  1142 
  1143   \<^medskip>
  1144   Parsing via this production produces parse trees \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> for the
  1145   argument slots. The resulting parse tree is composed as \<open>c t\<^sub>1 \<dots> t\<^sub>n\<close>, by
  1146   using the syntax constant \<open>c\<close> of the syntax declaration.
  1147 
  1148   Such syntactic constants are invented on the spot, without formal check
  1149   wrt.\ existing declarations. It is conventional to use plain identifiers
  1150   prefixed by a single underscore (e.g.\ \<open>_foobar\<close>). Names should be chosen
  1151   with care, to avoid clashes with other syntax declarations.
  1152 
  1153   \<^medskip>
  1154   The special case of copy production is specified by \<open>c =\<close>~\<^verbatim>\<open>""\<close> (empty
  1155   string). It means that the resulting parse tree \<open>t\<close> is copied directly,
  1156   without any further decoration.
  1157 
  1158   \<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar declarations (and
  1159   translations) resulting from \<open>decls\<close>, which are interpreted in the same
  1160   manner as for @{command "syntax"} above.
  1161 
  1162   \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic translation rules
  1163   (i.e.\ macros) as first-order rewrite rules on ASTs (\secref{sec:ast}). The
  1164   theory context maintains two independent lists translation rules: parse
  1165   rules (\<^verbatim>\<open>=>\<close> or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>). For convenience, both
  1166   can be specified simultaneously as parse~/ print rules (\<^verbatim>\<open>==\<close> or \<open>\<rightleftharpoons>\<close>).
  1167 
  1168   Translation patterns may be prefixed by the syntactic category to be used
  1169   for parsing; the default is \<open>logic\<close> which means that regular term syntax is
  1170   used. Both sides of the syntax translation rule undergo parsing and parse
  1171   AST translations \secref{sec:tr-funs}, in order to perform some fundamental
  1172   normalization like \<open>\<lambda>x y. b \<leadsto> \<lambda>x. \<lambda>y. b\<close>, but other AST translation rules
  1173   are \<^emph>\<open>not\<close> applied recursively here.
  1174 
  1175   When processing AST patterns, the inner syntax lexer runs in a different
  1176   mode that allows identifiers to start with underscore. This accommodates the
  1177   usual naming convention for auxiliary syntax constants --- those that do not
  1178   have a logical counter part --- by allowing to specify arbitrary AST
  1179   applications within the term syntax, independently of the corresponding
  1180   concrete syntax.
  1181 
  1182   Atomic ASTs are distinguished as @{ML Ast.Constant} versus @{ML
  1183   Ast.Variable} as follows: a qualified name or syntax constant declared via
  1184   @{command syntax}, or parse tree head of concrete notation becomes @{ML
  1185   Ast.Constant}, anything else @{ML Ast.Variable}. Note that \<open>CONST\<close> and
  1186   \<open>XCONST\<close> within the term language (\secref{sec:pure-grammar}) allow to
  1187   enforce treatment as constants.
  1188 
  1189   AST rewrite rules \<open>(lhs, rhs)\<close> need to obey the following side-conditions:
  1190 
  1191     \<^item> Rules must be left linear: \<open>lhs\<close> must not contain repeated
  1192     variables.\<^footnote>\<open>The deeper reason for this is that AST equality is not
  1193     well-defined: different occurrences of the ``same'' AST could be decorated
  1194     differently by accidental type-constraints or source position information,
  1195     for example.\<close>
  1196 
  1197     \<^item> Every variable in \<open>rhs\<close> must also occur in \<open>lhs\<close>.
  1198 
  1199   \<^descr> @{command "no_translations"}~\<open>rules\<close> removes syntactic translation rules,
  1200   which are interpreted in the same manner as for @{command "translations"}
  1201   above.
  1202 
  1203   \<^descr> @{attribute syntax_ast_trace} and @{attribute syntax_ast_stats} control
  1204   diagnostic output in the AST normalization process, when translation rules
  1205   are applied to concrete input or output.
  1206 
  1207 
  1208   Raw syntax and translations provides a slightly more low-level access to the
  1209   grammar and the form of resulting parse trees. It is often possible to avoid
  1210   this untyped macro mechanism, and use type-safe @{command abbreviation} or
  1211   @{command notation} instead. Some important situations where @{command
  1212   syntax} and @{command translations} are really need are as follows:
  1213 
  1214   \<^item> Iterated replacement via recursive @{command translations}. For example,
  1215   consider list enumeration @{term "[a, b, c, d]"} as defined in theory
  1216   @{theory List} in Isabelle/HOL.
  1217 
  1218   \<^item> Change of binding status of variables: anything beyond the built-in
  1219   @{keyword "binder"} mixfix annotation requires explicit syntax translations.
  1220   For example, consider list filter comprehension @{term "[x \<leftarrow> xs . P]"} as
  1221   defined in theory @{theory List} in Isabelle/HOL.
  1222 \<close>
  1223 
  1224 
  1225 subsubsection \<open>Applying translation rules\<close>
  1226 
  1227 text \<open>
  1228   As a term is being parsed or printed, an AST is generated as an intermediate
  1229   form according to \figref{fig:parse-print}. The AST is normalized by
  1230   applying translation rules in the manner of a first-order term rewriting
  1231   system. We first examine how a single rule is applied.
  1232 
  1233   Let \<open>t\<close> be the abstract syntax tree to be normalized and \<open>(lhs, rhs)\<close> some
  1234   translation rule. A subtree \<open>u\<close> of \<open>t\<close> is called \<^emph>\<open>redex\<close> if it is an
  1235   instance of \<open>lhs\<close>; in this case the pattern \<open>lhs\<close> is said to match the
  1236   object \<open>u\<close>. A redex matched by \<open>lhs\<close> may be replaced by the corresponding
  1237   instance of \<open>rhs\<close>, thus \<^emph>\<open>rewriting\<close> the AST \<open>t\<close>. Matching requires some
  1238   notion of \<^emph>\<open>place-holders\<close> in rule patterns: @{ML Ast.Variable} serves this
  1239   purpose.
  1240 
  1241   More precisely, the matching of the object \<open>u\<close> against the pattern \<open>lhs\<close> is
  1242   performed as follows:
  1243 
  1244     \<^item> Objects of the form @{ML Ast.Variable}~\<open>x\<close> or @{ML Ast.Constant}~\<open>x\<close> are
  1245     matched by pattern @{ML Ast.Constant}~\<open>x\<close>. Thus all atomic ASTs in the
  1246     object are treated as (potential) constants, and a successful match makes
  1247     them actual constants even before name space resolution (see also
  1248     \secref{sec:ast}).
  1249 
  1250     \<^item> Object \<open>u\<close> is matched by pattern @{ML Ast.Variable}~\<open>x\<close>, binding \<open>x\<close> to
  1251     \<open>u\<close>.
  1252 
  1253     \<^item> Object @{ML Ast.Appl}~\<open>us\<close> is matched by @{ML Ast.Appl}~\<open>ts\<close> if \<open>us\<close> and
  1254     \<open>ts\<close> have the same length and each corresponding subtree matches.
  1255 
  1256     \<^item> In every other case, matching fails.
  1257 
  1258   A successful match yields a substitution that is applied to \<open>rhs\<close>,
  1259   generating the instance that replaces \<open>u\<close>.
  1260 
  1261   Normalizing an AST involves repeatedly applying translation rules until none
  1262   are applicable. This works yoyo-like: top-down, bottom-up, top-down, etc. At
  1263   each subtree position, rules are chosen in order of appearance in the theory
  1264   definitions.
  1265 
  1266   The configuration options @{attribute syntax_ast_trace} and @{attribute
  1267   syntax_ast_stats} might help to understand this process and diagnose
  1268   problems.
  1269 
  1270   \begin{warn}
  1271   If syntax translation rules work incorrectly, the output of @{command_ref
  1272   print_syntax} with its \<^emph>\<open>rules\<close> sections reveals the actual internal forms
  1273   of AST pattern, without potentially confusing concrete syntax. Recall that
  1274   AST constants appear as quoted strings and variables without quotes.
  1275   \end{warn}
  1276 
  1277   \begin{warn}
  1278   If @{attribute_ref eta_contract} is set to \<open>true\<close>, terms will be
  1279   \<open>\<eta>\<close>-contracted \<^emph>\<open>before\<close> the AST rewriter sees them. Thus some abstraction
  1280   nodes needed for print rules to match may vanish. For example, \<open>Ball A (\<lambda>x.
  1281   P x)\<close> would contract to \<open>Ball A P\<close> and the standard print rule would fail to
  1282   apply. This problem can be avoided by hand-written ML translation functions
  1283   (see also \secref{sec:tr-funs}), which is in fact the same mechanism used in
  1284   built-in @{keyword "binder"} declarations.
  1285   \end{warn}
  1286 \<close>
  1287 
  1288 
  1289 subsection \<open>Syntax translation functions \label{sec:tr-funs}\<close>
  1290 
  1291 text \<open>
  1292   \begin{matharray}{rcl}
  1293     @{command_def "parse_ast_translation"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1294     @{command_def "parse_translation"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1295     @{command_def "print_translation"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1296     @{command_def "typed_print_translation"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1297     @{command_def "print_ast_translation"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1298     @{ML_antiquotation_def "class_syntax"} & : & \<open>ML antiquotation\<close> \\
  1299     @{ML_antiquotation_def "type_syntax"} & : & \<open>ML antiquotation\<close> \\
  1300     @{ML_antiquotation_def "const_syntax"} & : & \<open>ML antiquotation\<close> \\
  1301     @{ML_antiquotation_def "syntax_const"} & : & \<open>ML antiquotation\<close> \\
  1302   \end{matharray}
  1303 
  1304   Syntax translation functions written in ML admit almost arbitrary
  1305   manipulations of inner syntax, at the expense of some complexity and
  1306   obscurity in the implementation.
  1307 
  1308   @{rail \<open>
  1309   ( @@{command parse_ast_translation} | @@{command parse_translation} |
  1310     @@{command print_translation} | @@{command typed_print_translation} |
  1311     @@{command print_ast_translation}) @{syntax text}
  1312   ;
  1313   (@@{ML_antiquotation class_syntax} |
  1314    @@{ML_antiquotation type_syntax} |
  1315    @@{ML_antiquotation const_syntax} |
  1316    @@{ML_antiquotation syntax_const}) embedded
  1317   \<close>}
  1318 
  1319   \<^descr> @{command parse_translation} etc. declare syntax translation functions to
  1320   the theory. Any of these commands have a single @{syntax text} argument that
  1321   refers to an ML expression of appropriate type as follows:
  1322 
  1323   \<^medskip>
  1324   {\footnotesize
  1325   \begin{tabular}{l}
  1326   @{command parse_ast_translation} : \\
  1327   \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\
  1328   @{command parse_translation} : \\
  1329   \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\
  1330   @{command print_translation} : \\
  1331   \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\
  1332   @{command typed_print_translation} : \\
  1333   \quad @{ML_type "(string * (Proof.context -> typ -> term list -> term)) list"} \\
  1334   @{command print_ast_translation} : \\
  1335   \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\
  1336   \end{tabular}}
  1337   \<^medskip>
  1338 
  1339   The argument list consists of \<open>(c, tr)\<close> pairs, where \<open>c\<close> is the syntax name
  1340   of the formal entity involved, and \<open>tr\<close> a function that translates a syntax
  1341   form \<open>c args\<close> into \<open>tr ctxt args\<close> (depending on the context). The
  1342   Isabelle/ML naming convention for parse translations is \<open>c_tr\<close> and for print
  1343   translations \<open>c_tr'\<close>.
  1344 
  1345   The @{command_ref print_syntax} command displays the sets of names
  1346   associated with the translation functions of a theory under
  1347   \<open>parse_ast_translation\<close> etc.
  1348 
  1349   \<^descr> \<open>@{class_syntax c}\<close>, \<open>@{type_syntax c}\<close>, \<open>@{const_syntax c}\<close> inline the
  1350   authentic syntax name of the given formal entities into the ML source. This
  1351   is the fully-qualified logical name prefixed by a special marker to indicate
  1352   its kind: thus different logical name spaces are properly distinguished
  1353   within parse trees.
  1354 
  1355   \<^descr> \<open>@{const_syntax c}\<close> inlines the name \<open>c\<close> of the given syntax constant,
  1356   having checked that it has been declared via some @{command syntax} commands
  1357   within the theory context. Note that the usual naming convention makes
  1358   syntax constants start with underscore, to reduce the chance of accidental
  1359   clashes with other names occurring in parse trees (unqualified constants
  1360   etc.).
  1361 \<close>
  1362 
  1363 
  1364 subsubsection \<open>The translation strategy\<close>
  1365 
  1366 text \<open>
  1367   The different kinds of translation functions are invoked during the
  1368   transformations between parse trees, ASTs and syntactic terms (cf.\
  1369   \figref{fig:parse-print}). Whenever a combination of the form \<open>c x\<^sub>1 \<dots> x\<^sub>n\<close>
  1370   is encountered, and a translation function \<open>f\<close> of appropriate kind is
  1371   declared for \<open>c\<close>, the result is produced by evaluation of \<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close>
  1372   in ML.
  1373 
  1374   For AST translations, the arguments \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> are ASTs. A combination
  1375   has the form @{ML "Ast.Constant"}~\<open>c\<close> or @{ML "Ast.Appl"}~\<open>[\<close>@{ML
  1376   Ast.Constant}~\<open>c, x\<^sub>1, \<dots>, x\<^sub>n]\<close>. For term translations, the arguments are
  1377   terms and a combination has the form @{ML Const}~\<open>(c, \<tau>)\<close> or @{ML
  1378   Const}~\<open>(c, \<tau>) $ x\<^sub>1 $ \<dots> $ x\<^sub>n\<close>. Terms allow more sophisticated
  1379   transformations than ASTs do, typically involving abstractions and bound
  1380   variables. \<^emph>\<open>Typed\<close> print translations may even peek at the type \<open>\<tau>\<close> of the
  1381   constant they are invoked on, although some information might have been
  1382   suppressed for term output already.
  1383 
  1384   Regardless of whether they act on ASTs or terms, translation functions
  1385   called during the parsing process differ from those for printing in their
  1386   overall behaviour:
  1387 
  1388     \<^descr>[Parse translations] are applied bottom-up. The arguments are already in
  1389     translated form. The translations must not fail; exceptions trigger an
  1390     error message. There may be at most one function associated with any
  1391     syntactic name.
  1392 
  1393     \<^descr>[Print translations] are applied top-down. They are supplied with
  1394     arguments that are partly still in internal form. The result again
  1395     undergoes translation; therefore a print translation should not introduce
  1396     as head the very constant that invoked it. The function may raise
  1397     exception @{ML Match} to indicate failure; in this event it has no effect.
  1398     Multiple functions associated with some syntactic name are tried in the
  1399     order of declaration in the theory.
  1400 
  1401   Only constant atoms --- constructor @{ML Ast.Constant} for ASTs and @{ML
  1402   Const} for terms --- can invoke translation functions. This means that parse
  1403   translations can only be associated with parse tree heads of concrete
  1404   syntax, or syntactic constants introduced via other translations. For plain
  1405   identifiers within the term language, the status of constant versus variable
  1406   is not yet know during parsing. This is in contrast to print translations,
  1407   where constants are explicitly known from the given term in its fully
  1408   internal form.
  1409 \<close>
  1410 
  1411 
  1412 subsection \<open>Built-in syntax transformations\<close>
  1413 
  1414 text \<open>
  1415   Here are some further details of the main syntax transformation phases of
  1416   \figref{fig:parse-print}.
  1417 \<close>
  1418 
  1419 
  1420 subsubsection \<open>Transforming parse trees to ASTs\<close>
  1421 
  1422 text \<open>
  1423   The parse tree is the raw output of the parser. It is transformed into an
  1424   AST according to some basic scheme that may be augmented by AST translation
  1425   functions as explained in \secref{sec:tr-funs}.
  1426 
  1427   The parse tree is constructed by nesting the right-hand sides of the
  1428   productions used to recognize the input. Such parse trees are simply lists
  1429   of tokens and constituent parse trees, the latter representing the
  1430   nonterminals of the productions. Ignoring AST translation functions, parse
  1431   trees are transformed to ASTs by stripping out delimiters and copy
  1432   productions, while retaining some source position information from input
  1433   tokens.
  1434 
  1435   The Pure syntax provides predefined AST translations to make the basic
  1436   \<open>\<lambda>\<close>-term structure more apparent within the (first-order) AST
  1437   representation, and thus facilitate the use of @{command translations} (see
  1438   also \secref{sec:syn-trans}). This covers ordinary term application, type
  1439   application, nested abstraction, iterated meta implications and function
  1440   types. The effect is illustrated on some representative input strings is as
  1441   follows:
  1442 
  1443   \begin{center}
  1444   \begin{tabular}{ll}
  1445   input source & AST \\
  1446   \hline
  1447   \<open>f x y z\<close> & \<^verbatim>\<open>(f x y z)\<close> \\
  1448   \<open>'a ty\<close> & \<^verbatim>\<open>(ty 'a)\<close> \\
  1449   \<open>('a, 'b)ty\<close> & \<^verbatim>\<open>(ty 'a 'b)\<close> \\
  1450   \<open>\<lambda>x y z. t\<close> & \<^verbatim>\<open>("_abs" x ("_abs" y ("_abs" z t)))\<close> \\
  1451   \<open>\<lambda>x :: 'a. t\<close> & \<^verbatim>\<open>("_abs" ("_constrain" x 'a) t)\<close> \\
  1452   \<open>\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S\<close> & \<^verbatim>\<open>("Pure.imp" P ("Pure.imp" Q ("Pure.imp" R S)))\<close> \\
  1453    \<open>['a, 'b, 'c] \<Rightarrow> 'd\<close> & \<^verbatim>\<open>("fun" 'a ("fun" 'b ("fun" 'c 'd)))\<close> \\
  1454   \end{tabular}
  1455   \end{center}
  1456 
  1457   Note that type and sort constraints may occur in further places ---
  1458   translations need to be ready to cope with them. The built-in syntax
  1459   transformation from parse trees to ASTs insert additional constraints that
  1460   represent source positions.
  1461 \<close>
  1462 
  1463 
  1464 subsubsection \<open>Transforming ASTs to terms\<close>
  1465 
  1466 text \<open>
  1467   After application of macros (\secref{sec:syn-trans}), the AST is transformed
  1468   into a term. This term still lacks proper type information, but it might
  1469   contain some constraints consisting of applications with head \<^verbatim>\<open>_constrain\<close>,
  1470   where the second argument is a type encoded as a pre-term within the syntax.
  1471   Type inference later introduces correct types, or indicates type errors in
  1472   the input.
  1473 
  1474   Ignoring parse translations, ASTs are transformed to terms by mapping AST
  1475   constants to term constants, AST variables to term variables or constants
  1476   (according to the name space), and AST applications to iterated term
  1477   applications.
  1478 
  1479   The outcome is still a first-order term. Proper abstractions and bound
  1480   variables are introduced by parse translations associated with certain
  1481   syntax constants. Thus \<^verbatim>\<open>("_abs" x x)\<close> eventually becomes a de-Bruijn term
  1482   \<^verbatim>\<open>Abs ("x", _, Bound 0)\<close>.
  1483 \<close>
  1484 
  1485 
  1486 subsubsection \<open>Printing of terms\<close>
  1487 
  1488 text \<open>
  1489   The output phase is essentially the inverse of the input phase. Terms are
  1490   translated via abstract syntax trees into pretty-printed text.
  1491 
  1492   Ignoring print translations, the transformation maps term constants,
  1493   variables and applications to the corresponding constructs on ASTs.
  1494   Abstractions are mapped to applications of the special constant \<^verbatim>\<open>_abs\<close> as
  1495   seen before. Type constraints are represented via special \<^verbatim>\<open>_constrain\<close>
  1496   forms, according to various policies of type annotation determined
  1497   elsewhere. Sort constraints of type variables are handled in a similar
  1498   fashion.
  1499 
  1500   After application of macros (\secref{sec:syn-trans}), the AST is finally
  1501   pretty-printed. The built-in print AST translations reverse the
  1502   corresponding parse AST translations.
  1503 
  1504   \<^medskip>
  1505   For the actual printing process, the priority grammar
  1506   (\secref{sec:priority-grammar}) plays a vital role: productions are used as
  1507   templates for pretty printing, with argument slots stemming from
  1508   nonterminals, and syntactic sugar stemming from literal tokens.
  1509 
  1510   Each AST application with constant head \<open>c\<close> and arguments \<open>t\<^sub>1\<close>, \dots,
  1511   \<open>t\<^sub>n\<close> (for \<open>n = 0\<close> the AST is just the constant \<open>c\<close> itself) is printed
  1512   according to the first grammar production of result name \<open>c\<close>. The required
  1513   syntax priority of the argument slot is given by its nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>.
  1514   The argument \<open>t\<^sub>i\<close> that corresponds to the position of \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is printed
  1515   recursively, and then put in parentheses \<^emph>\<open>if\<close> its priority \<open>p\<close> requires
  1516   this. The resulting output is concatenated with the syntactic sugar
  1517   according to the grammar production.
  1518 
  1519   If an AST application \<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> has more arguments than the
  1520   corresponding production, it is first split into \<open>((c x\<^sub>1 \<dots> x\<^sub>n) x\<^sub>n\<^sub>+\<^sub>1 \<dots>
  1521   x\<^sub>m)\<close> and then printed recursively as above.
  1522 
  1523   Applications with too few arguments or with non-constant head or without a
  1524   corresponding production are printed in prefix-form like \<open>f t\<^sub>1 \<dots> t\<^sub>n\<close> for
  1525   terms.
  1526 
  1527   Multiple productions associated with some name \<open>c\<close> are tried in order of
  1528   appearance within the grammar. An occurrence of some AST variable \<open>x\<close> is
  1529   printed as \<open>x\<close> outright.
  1530 
  1531   \<^medskip>
  1532   White space is \<^emph>\<open>not\<close> inserted automatically. If blanks (or breaks) are
  1533   required to separate tokens, they need to be specified in the mixfix
  1534   declaration (\secref{sec:mixfix}).
  1535 \<close>
  1536 
  1537 end