src/Doc/Isar_Ref/Inner_Syntax.thy
 changeset 62106 d6af554512d7 parent 61997 4d9518c3d031 child 62107 f74a33b14200
     1.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jan 08 19:46:30 2016 +0100
1.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jan 08 20:06:48 2016 +0100
1.3 @@ -6,26 +6,25 @@
1.4
1.5  chapter \<open>Inner syntax --- the term language \label{ch:inner-syntax}\<close>
1.6
1.7 -text \<open>The inner syntax of Isabelle provides concrete notation for
1.8 -  the main entities of the logical framework, notably \<open>\<lambda>\<close>-terms with types and type classes.  Applications may either
1.9 -  extend existing syntactic categories by additional notation, or
1.10 -  define new sub-languages that are linked to the standard term
1.11 -  language via some explicit markers.  For example \<^verbatim>\<open>FOO\<close>~\<open>foo\<close> could
1.12 -  embed the syntax corresponding for some
1.13 -  user-defined nonterminal \<open>foo\<close> --- within the bounds of the
1.14 -  given lexical syntax of Isabelle/Pure.
1.15 +text \<open>
1.16 +  The inner syntax of Isabelle provides concrete notation for the main
1.17 +  entities of the logical framework, notably \<open>\<lambda>\<close>-terms with types and type
1.18 +  classes. Applications may either extend existing syntactic categories by
1.19 +  additional notation, or define new sub-languages that are linked to the
1.20 +  standard term language via some explicit markers. For example \<^verbatim>\<open>FOO\<close>~\<open>foo\<close>
1.21 +  could embed the syntax corresponding for some user-defined nonterminal \<open>foo\<close>
1.22 +  --- within the bounds of the given lexical syntax of Isabelle/Pure.
1.23
1.24 -  The most basic way to specify concrete syntax for logical entities
1.25 -  works via mixfix annotations (\secref{sec:mixfix}), which may be
1.26 -  usually given as part of the original declaration or via explicit
1.27 -  notation commands later on (\secref{sec:notation}).  This already
1.28 -  covers many needs of concrete syntax without having to understand
1.29 -  the full complexity of inner syntax layers.
1.30 +  The most basic way to specify concrete syntax for logical entities works via
1.31 +  mixfix annotations (\secref{sec:mixfix}), which may be usually given as part
1.32 +  of the original declaration or via explicit notation commands later on
1.33 +  (\secref{sec:notation}). This already covers many needs of concrete syntax
1.34 +  without having to understand the full complexity of inner syntax layers.
1.35
1.36 -  Further details of the syntax engine involves the classical
1.37 -  distinction of lexical language versus context-free grammar (see
1.38 -  \secref{sec:pure-syntax}), and various mechanisms for \<^emph>\<open>syntax
1.39 -  transformations\<close> (see \secref{sec:syntax-transformations}).
1.40 +  Further details of the syntax engine involves the classical distinction of
1.41 +  lexical language versus context-free grammar (see \secref{sec:pure-syntax}),
1.42 +  and various mechanisms for \<^emph>\<open>syntax transformations\<close> (see
1.43 +  \secref{sec:syntax-transformations}).
1.44  \<close>
1.45
1.46
1.47 @@ -63,43 +62,39 @@
1.48      @{syntax_def modes}: '(' (@{syntax name} + ) ')'
1.49    \<close>}
1.50
1.51 -  \<^descr> @{command "typ"}~\<open>\<tau>\<close> reads and prints a type expression
1.52 -  according to the current context.
1.53 +  \<^descr> @{command "typ"}~\<open>\<tau>\<close> reads and prints a type expression according to the
1.54 +  current context.
1.55
1.56 -  \<^descr> @{command "typ"}~\<open>\<tau> :: s\<close> uses type-inference to
1.57 -  determine the most general way to make \<open>\<tau>\<close> conform to sort
1.58 -  \<open>s\<close>.  For concrete \<open>\<tau>\<close> this checks if the type
1.59 -  belongs to that sort.  Dummy type parameters \<open>_\<close>''
1.60 -  (underscore) are assigned to fresh type variables with most general
1.61 -  sorts, according the the principles of type-inference.
1.62 +  \<^descr> @{command "typ"}~\<open>\<tau> :: s\<close> uses type-inference to determine the most
1.63 +  general way to make \<open>\<tau>\<close> conform to sort \<open>s\<close>. For concrete \<open>\<tau>\<close> this checks if
1.64 +  the type belongs to that sort. Dummy type parameters \<open>_\<close>'' (underscore)
1.65 +  are assigned to fresh type variables with most general sorts, according the
1.66 +  the principles of type-inference.
1.67
1.68 -  \<^descr> @{command "term"}~\<open>t\<close> and @{command "prop"}~\<open>\<phi>\<close>
1.69 -  read, type-check and print terms or propositions according to the
1.70 -  current theory or proof context; the inferred type of \<open>t\<close> is
1.71 -  output as well.  Note that these commands are also useful in
1.72 -  inspecting the current environment of term abbreviations.
1.73 +    \<^descr> @{command "term"}~\<open>t\<close> and @{command "prop"}~\<open>\<phi>\<close> read, type-check and
1.74 +    print terms or propositions according to the current theory or proof
1.75 +    context; the inferred type of \<open>t\<close> is output as well. Note that these
1.76 +    commands are also useful in inspecting the current environment of term
1.77 +    abbreviations.
1.78
1.79 -  \<^descr> @{command "thm"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> retrieves
1.80 -  theorems from the current theory or proof context.  Note that any
1.81 -  attributes included in the theorem specifications are applied to a
1.82 -  temporary context derived from the current theory or proof; the
1.83 -  result is discarded, i.e.\ attributes involved in \<open>a\<^sub>1,
1.84 -  \<dots>, a\<^sub>n\<close> do not have any permanent effect.
1.85 +    \<^descr> @{command "thm"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> retrieves theorems from the current theory
1.86 +    or proof context. Note that any attributes included in the theorem
1.87 +    specifications are applied to a temporary context derived from the current
1.88 +    theory or proof; the result is discarded, i.e.\ attributes involved in
1.89 +    \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> do not have any permanent effect.
1.90
1.91 -  \<^descr> @{command "prf"} displays the (compact) proof term of the
1.92 -  current proof state (if present), or of the given theorems. Note
1.93 -  that this requires proof terms to be switched on for the current
1.94 -  object logic (see the Proof terms'' section of the Isabelle
1.95 -  reference manual for information on how to do this).
1.96 +    \<^descr> @{command "prf"} displays the (compact) proof term of the current proof
1.97 +    state (if present), or of the given theorems. Note that this requires
1.98 +    proof terms to be switched on for the current object logic (see the
1.99 +    Proof terms'' section of the Isabelle reference manual for information
1.100 +    on how to do this).
1.101
1.102 -  \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays
1.103 -  the full proof term, i.e.\ also displays information omitted in the
1.104 -  compact proof term, which is denoted by \<open>_\<close>'' placeholders
1.105 -  there.
1.106 +    \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays the full
1.107 +    proof term, i.e.\ also displays information omitted in the compact proof
1.108 +    term, which is denoted by \<open>_\<close>'' placeholders there.
1.109
1.110 -  \<^descr> @{command "print_state"} prints the current proof state (if
1.111 -  present), including current facts and goals.
1.112 -
1.113 +    \<^descr> @{command "print_state"} prints the current proof state (if present),
1.114 +    including current facts and goals.
1.115
1.116    All of the diagnostic commands above admit a list of \<open>modes\<close> to be
1.117    specified, which is appended to the current print mode; see also
1.118 @@ -109,9 +104,8 @@
1.119    symbols and special characters represented in {\LaTeX} source, according to
1.120    the Isabelle style @{cite "isabelle-system"}.
1.121
1.122 -  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
1.123 -  systematic way to include formal items into the printed text
1.124 -  document.
1.125 +  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic
1.126 +  way to include formal items into the printed text document.
1.127  \<close>
1.128
1.129
1.130 @@ -137,100 +131,90 @@
1.131    \end{tabular}
1.132    \<^medskip>
1.133
1.134 -  These configuration options control the detail of information that
1.135 -  is displayed for types, terms, theorems, goals etc.  See also
1.136 +  These configuration options control the detail of information that is
1.138    \secref{sec:config}.
1.139
1.140 -  \<^descr> @{attribute show_markup} controls direct inlining of markup
1.141 -  into the printed representation of formal entities --- notably type
1.142 -  and sort constraints.  This enables Prover IDE users to retrieve
1.143 -  that information via tooltips or popups while hovering with the
1.144 -  mouse over the output window, for example.  Consequently, this
1.145 -  option is enabled by default for Isabelle/jEdit.
1.146 +  \<^descr> @{attribute show_markup} controls direct inlining of markup into the
1.147 +  printed representation of formal entities --- notably type and sort
1.148 +  constraints. This enables Prover IDE users to retrieve that information via
1.149 +  tooltips or popups while hovering with the mouse over the output window, for
1.150 +  example. Consequently, this option is enabled by default for Isabelle/jEdit.
1.151
1.152 -  \<^descr> @{attribute show_types} and @{attribute show_sorts} control
1.153 -  printing of type constraints for term variables, and sort
1.154 -  constraints for type variables.  By default, neither of these are
1.155 -  shown in output.  If @{attribute show_sorts} is enabled, types are
1.156 -  always shown as well.  In Isabelle/jEdit, manual setting of these
1.157 -  options is normally not required thanks to @{attribute show_markup}
1.158 -  above.
1.159 +  \<^descr> @{attribute show_types} and @{attribute show_sorts} control printing of
1.160 +  type constraints for term variables, and sort constraints for type
1.161 +  variables. By default, neither of these are shown in output. If @{attribute
1.162 +  show_sorts} is enabled, types are always shown as well. In Isabelle/jEdit,
1.163 +  manual setting of these options is normally not required thanks to
1.164 +  @{attribute show_markup} above.
1.165
1.166 -  Note that displaying types and sorts may explain why a polymorphic
1.167 -  inference rule fails to resolve with some goal, or why a rewrite
1.168 -  rule does not apply as expected.
1.169 -
1.170 -  \<^descr> @{attribute show_consts} controls printing of types of
1.171 -  constants when displaying a goal state.
1.172 +  Note that displaying types and sorts may explain why a polymorphic inference
1.173 +  rule fails to resolve with some goal, or why a rewrite rule does not apply
1.174 +  as expected.
1.175
1.176 -  Note that the output can be enormous, because polymorphic constants
1.177 -  often occur at several different type instances.
1.178 +  \<^descr> @{attribute show_consts} controls printing of types of constants when
1.179 +  displaying a goal state.
1.180
1.181 -  \<^descr> @{attribute show_abbrevs} controls folding of constant
1.182 -  abbreviations.
1.183 +  Note that the output can be enormous, because polymorphic constants often
1.184 +  occur at several different type instances.
1.185 +
1.186 +  \<^descr> @{attribute show_abbrevs} controls folding of constant abbreviations.
1.187
1.188 -  \<^descr> @{attribute show_brackets} controls bracketing in pretty
1.189 -  printed output.  If enabled, all sub-expressions of the pretty
1.190 -  printing tree will be parenthesized, even if this produces malformed
1.191 -  term syntax!  This crude way of showing the internal structure of
1.192 -  pretty printed entities may occasionally help to diagnose problems
1.193 -  with operator priorities, for example.
1.194 +  \<^descr> @{attribute show_brackets} controls bracketing in pretty printed output.
1.195 +  If enabled, all sub-expressions of the pretty printing tree will be
1.196 +  parenthesized, even if this produces malformed term syntax! This crude way
1.197 +  of showing the internal structure of pretty printed entities may
1.198 +  occasionally help to diagnose problems with operator priorities, for
1.199 +  example.
1.200
1.201 -  \<^descr> @{attribute names_long}, @{attribute names_short}, and
1.202 -  @{attribute names_unique} control the way of printing fully
1.204 -  \secref{sec:antiq} for the document antiquotation options of the
1.205 -  same names.
1.206 +  \<^descr> @{attribute names_long}, @{attribute names_short}, and @{attribute
1.207 +  names_unique} control the way of printing fully qualified internal names in
1.209 +  options of the same names.
1.210
1.211 -  \<^descr> @{attribute eta_contract} controls \<open>\<eta>\<close>-contracted
1.212 -  printing of terms.
1.213 +  \<^descr> @{attribute eta_contract} controls \<open>\<eta>\<close>-contracted printing of terms.
1.214
1.215 -  The \<open>\<eta>\<close>-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"},
1.216 -  provided \<open>x\<close> is not free in \<open>f\<close>.  It asserts
1.217 -  \<^emph>\<open>extensionality\<close> of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv>
1.218 -  g x"} for all \<open>x\<close>.  Higher-order unification frequently puts
1.219 -  terms into a fully \<open>\<eta>\<close>-expanded form.  For example, if \<open>F\<close> has type \<open>(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>\<close> then its expanded form is @{term
1.220 -  "\<lambda>h. F (\<lambda>x. h x)"}.
1.221 +  The \<open>\<eta>\<close>-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"}, provided \<open>x\<close> is not
1.222 +  free in \<open>f\<close>. It asserts \<^emph>\<open>extensionality\<close> of functions: @{prop "f \<equiv> g"} if
1.223 +  @{prop "f x \<equiv> g x"} for all \<open>x\<close>. Higher-order unification frequently puts
1.224 +  terms into a fully \<open>\<eta>\<close>-expanded form. For example, if \<open>F\<close> has type \<open>(\<tau> \<Rightarrow> \<tau>)
1.225 +  \<Rightarrow> \<tau>\<close> then its expanded form is @{term "\<lambda>h. F (\<lambda>x. h x)"}.
1.226
1.227 -  Enabling @{attribute eta_contract} makes Isabelle perform \<open>\<eta>\<close>-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"}
1.228 -  appears simply as \<open>F\<close>.
1.229 +  Enabling @{attribute eta_contract} makes Isabelle perform \<open>\<eta>\<close>-contractions
1.230 +  before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"} appears simply as \<open>F\<close>.
1.231
1.232 -  Note that the distinction between a term and its \<open>\<eta>\<close>-expanded
1.233 -  form occasionally matters.  While higher-order resolution and
1.234 -  rewriting operate modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion, some other tools
1.235 -  might look at terms more discretely.
1.236 +  Note that the distinction between a term and its \<open>\<eta>\<close>-expanded form
1.237 +  occasionally matters. While higher-order resolution and rewriting operate
1.238 +  modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion, some other tools might look at terms more
1.239 +  discretely.
1.240
1.241 -  \<^descr> @{attribute goals_limit} controls the maximum number of
1.242 -  subgoals to be printed.
1.243 +  \<^descr> @{attribute goals_limit} controls the maximum number of subgoals to be
1.244 +  printed.
1.245
1.246 -  \<^descr> @{attribute show_main_goal} controls whether the main result
1.247 -  to be proven should be displayed.  This information might be
1.248 -  relevant for schematic goals, to inspect the current claim that has
1.249 -  been synthesized so far.
1.250 +  \<^descr> @{attribute show_main_goal} controls whether the main result to be proven
1.251 +  should be displayed. This information might be relevant for schematic goals,
1.252 +  to inspect the current claim that has been synthesized so far.
1.253
1.254 -  \<^descr> @{attribute show_hyps} controls printing of implicit
1.255 -  hypotheses of local facts.  Normally, only those hypotheses are
1.256 -  displayed that are \<^emph>\<open>not\<close> covered by the assumptions of the
1.257 -  current context: this situation indicates a fault in some tool being
1.258 -  used.
1.259 +  \<^descr> @{attribute show_hyps} controls printing of implicit hypotheses of local
1.260 +  facts. Normally, only those hypotheses are displayed that are \<^emph>\<open>not\<close> covered
1.261 +  by the assumptions of the current context: this situation indicates a fault
1.262 +  in some tool being used.
1.263
1.264 -  By enabling @{attribute show_hyps}, output of \<^emph>\<open>all\<close> hypotheses
1.265 -  can be enforced, which is occasionally useful for diagnostic
1.266 -  purposes.
1.267 +  By enabling @{attribute show_hyps}, output of \<^emph>\<open>all\<close> hypotheses can be
1.268 +  enforced, which is occasionally useful for diagnostic purposes.
1.269
1.270 -  \<^descr> @{attribute show_tags} controls printing of extra annotations
1.271 -  within theorems, such as internal position information, or the case
1.272 -  names being attached by the attribute @{attribute case_names}.
1.273 +  \<^descr> @{attribute show_tags} controls printing of extra annotations within
1.274 +  theorems, such as internal position information, or the case names being
1.275 +  attached by the attribute @{attribute case_names}.
1.276
1.277 -  Note that the @{attribute tagged} and @{attribute untagged}
1.279 -  associated with a theorem.
1.280 +  Note that the @{attribute tagged} and @{attribute untagged} attributes
1.281 +  provide low-level access to the collection of tags associated with a
1.282 +  theorem.
1.283
1.284 -  \<^descr> @{attribute show_question_marks} controls printing of question
1.285 -  marks for schematic variables, such as \<open>?x\<close>.  Only the leading
1.286 -  question mark is affected, the remaining text is unchanged
1.287 -  (including proper markup for schematic variables that might be
1.288 -  relevant for user interfaces).
1.289 +  \<^descr> @{attribute show_question_marks} controls printing of question marks for
1.290 +  schematic variables, such as \<open>?x\<close>. Only the leading question mark is
1.291 +  affected, the remaining text is unchanged (including proper markup for
1.292 +  schematic variables that might be relevant for user interfaces).
1.293  \<close>
1.294
1.295
1.296 @@ -242,62 +226,58 @@
1.297      @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\
1.298    \end{mldecls}
1.299
1.300 -  The \<^emph>\<open>print mode\<close> facility allows to modify various operations
1.301 -  for printing.  Commands like @{command typ}, @{command term},
1.302 -  @{command thm} (see \secref{sec:print-diag}) take additional print
1.303 -  modes as optional argument.  The underlying ML operations are as
1.304 -  follows.
1.305 +  The \<^emph>\<open>print mode\<close> facility allows to modify various operations for printing.
1.306 +  Commands like @{command typ}, @{command term}, @{command thm} (see
1.307 +  \secref{sec:print-diag}) take additional print modes as optional argument.
1.308 +  The underlying ML operations are as follows.
1.309
1.310 -  \<^descr> @{ML "print_mode_value ()"} yields the list of currently
1.311 -  active print mode names.  This should be understood as symbolic
1.312 -  representation of certain individual features for printing (with
1.313 -  precedence from left to right).
1.314 +    \<^descr> @{ML "print_mode_value ()"} yields the list of currently active print
1.315 +    mode names. This should be understood as symbolic representation of
1.316 +    certain individual features for printing (with precedence from left to
1.317 +    right).
1.318
1.319 -  \<^descr> @{ML Print_Mode.with_modes}~\<open>modes f x\<close> evaluates
1.320 -  \<open>f x\<close> in an execution context where the print mode is
1.321 -  prepended by the given \<open>modes\<close>.  This provides a thread-safe
1.322 -  way to augment print modes.  It is also monotonic in the set of mode
1.323 -  names: it retains the default print mode that certain
1.324 -  user-interfaces might have installed for their proper functioning!
1.325 -
1.326 +    \<^descr> @{ML Print_Mode.with_modes}~\<open>modes f x\<close> evaluates \<open>f x\<close> in an execution
1.327 +    context where the print mode is prepended by the given \<open>modes\<close>. This
1.328 +    provides a thread-safe way to augment print modes. It is also monotonic in
1.329 +    the set of mode names: it retains the default print mode that certain
1.330 +    user-interfaces might have installed for their proper functioning!
1.331
1.332    \<^medskip>
1.333 -  The pretty printer for inner syntax maintains alternative
1.334 -  mixfix productions for any print mode name invented by the user, say
1.335 -  in commands like @{command notation} or @{command abbreviation}.
1.336 -  Mode names can be arbitrary, but the following ones have a specific
1.337 -  meaning by convention:
1.338 +  The pretty printer for inner syntax maintains alternative mixfix productions
1.339 +  for any print mode name invented by the user, say in commands like @{command
1.340 +  notation} or @{command abbreviation}. Mode names can be arbitrary, but the
1.341 +  following ones have a specific meaning by convention:
1.342
1.343 -  \<^item> \<^verbatim>\<open>""\<close> (the empty string): default mode;
1.344 -  implicitly active as last element in the list of modes.
1.345 +    \<^item> \<^verbatim>\<open>""\<close> (the empty string): default mode; implicitly active as last
1.346 +    element in the list of modes.
1.347
1.348 -  \<^item> \<^verbatim>\<open>input\<close>: dummy print mode that is never active; may
1.349 -  be used to specify notation that is only available for input.
1.350 +    \<^item> \<^verbatim>\<open>input\<close>: dummy print mode that is never active; may be used to specify
1.351 +    notation that is only available for input.
1.352
1.353 -  \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active;
1.354 -  used internally in Isabelle/Pure.
1.355 +    \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active; used internally in
1.356 +    Isabelle/Pure.
1.357
1.358 -  \<^item> \<^verbatim>\<open>ASCII\<close>: prefer ASCII art over mathematical symbols.
1.359 +    \<^item> \<^verbatim>\<open>ASCII\<close>: prefer ASCII art over mathematical symbols.
1.360
1.361 -  \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX}
1.362 -  document preparation of Isabelle theory sources; allows to provide
1.363 -  alternative output notation.
1.364 +    \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX} document
1.365 +    preparation of Isabelle theory sources; allows to provide alternative
1.366 +    output notation.
1.367  \<close>
1.368
1.369
1.370  section \<open>Mixfix annotations \label{sec:mixfix}\<close>
1.371
1.372 -text \<open>Mixfix annotations specify concrete \<^emph>\<open>inner syntax\<close> of
1.373 -  Isabelle types and terms.  Locally fixed parameters in toplevel
1.374 -  theorem statements, locale and class specifications also admit
1.375 -  mixfix annotations in a fairly uniform manner.  A mixfix annotation
1.376 -  describes the concrete syntax, the translation to abstract
1.377 -  syntax, and the pretty printing.  Special case annotations provide a
1.378 -  simple means of specifying infix operators and binders.
1.379 +text \<open>
1.380 +  Mixfix annotations specify concrete \<^emph>\<open>inner syntax\<close> of Isabelle types and
1.381 +  terms. Locally fixed parameters in toplevel theorem statements, locale and
1.382 +  class specifications also admit mixfix annotations in a fairly uniform
1.383 +  manner. A mixfix annotation describes the concrete syntax, the translation
1.384 +  to abstract syntax, and the pretty printing. Special case annotations
1.385 +  provide a simple means of specifying infix operators and binders.
1.386
1.387 -  Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}.  It allows
1.388 -  to specify any context-free priority grammar, which is more general
1.389 -  than the fixity declarations of ML and Prolog.
1.390 +  Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}. It allows to
1.391 +  specify any context-free priority grammar, which is more general than the
1.392 +  fixity declarations of ML and Prolog.
1.393
1.394    @{rail \<open>
1.395      @{syntax_def mixfix}: '('
1.396 @@ -311,52 +291,48 @@
1.397      prios: '[' (@{syntax nat} + ',') ']'
1.398    \<close>}
1.399
1.400 -  The string given as \<open>template\<close> may include literal text,
1.401 -  spacing, blocks, and arguments (denoted by \<open>_\<close>''); the
1.402 -  special symbol \<^verbatim>\<open>\<index>\<close>'' (printed as \<open>\<index>\<close>'')
1.403 -  represents an index argument that specifies an implicit @{keyword
1.405 -  fixed variables may be declared as @{keyword "structure"}.
1.406 +  The string given as \<open>template\<close> may include literal text, spacing, blocks,
1.407 +  and arguments (denoted by \<open>_\<close>''); the special symbol \<^verbatim>\<open>\<index>\<close>'' (printed as
1.408 +  \<open>\<index>\<close>'') represents an index argument that specifies an implicit @{keyword
1.410 +  variables may be declared as @{keyword "structure"}.
1.411
1.412 -  Infix and binder declarations provide common abbreviations for
1.413 -  particular mixfix declarations.  So in practice, mixfix templates
1.414 -  mostly degenerate to literal text for concrete syntax, such as
1.415 -  \<^verbatim>\<open>++\<close>'' for an infix symbol.
1.416 +  Infix and binder declarations provide common abbreviations for particular
1.417 +  mixfix declarations. So in practice, mixfix templates mostly degenerate to
1.418 +  literal text for concrete syntax, such as \<^verbatim>\<open>++\<close>'' for an infix symbol.
1.419  \<close>
1.420
1.421
1.422  subsection \<open>The general mixfix form\<close>
1.423
1.424 -text \<open>In full generality, mixfix declarations work as follows.
1.425 -  Suppose a constant \<open>c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> is annotated by
1.426 -  \<open>(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)\<close>, where \<open>mixfix\<close> is a string
1.427 -  \<open>d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n\<close> consisting of delimiters that surround
1.428 -  argument positions as indicated by underscores.
1.429 +text \<open>
1.430 +  In full generality, mixfix declarations work as follows. Suppose a constant
1.431 +  \<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
1.432 +  \<open>mixfix\<close> is a string \<open>d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n\<close> consisting of delimiters that
1.433 +  surround argument positions as indicated by underscores.
1.434
1.435 -  Altogether this determines a production for a context-free priority
1.436 -  grammar, where for each argument \<open>i\<close> the syntactic category
1.437 -  is determined by \<open>\<tau>\<^sub>i\<close> (with priority \<open>p\<^sub>i\<close>), and the
1.438 -  result category is determined from \<open>\<tau>\<close> (with priority \<open>p\<close>).  Priority specifications are optional, with default 0 for
1.439 -  arguments and 1000 for the result.\<^footnote>\<open>Omitting priorities is
1.440 -  prone to syntactic ambiguities unless the delimiter tokens determine
1.441 -  fully bracketed notation, as in \<open>if _ then _ else _ fi\<close>.\<close>
1.442 +  Altogether this determines a production for a context-free priority grammar,
1.443 +  where for each argument \<open>i\<close> the syntactic category is determined by \<open>\<tau>\<^sub>i\<close>
1.444 +  (with priority \<open>p\<^sub>i\<close>), and the result category is determined from \<open>\<tau>\<close> (with
1.445 +  priority \<open>p\<close>). Priority specifications are optional, with default 0 for
1.446 +  arguments and 1000 for the result.\<^footnote>\<open>Omitting priorities is prone to
1.447 +  syntactic ambiguities unless the delimiter tokens determine fully bracketed
1.448 +  notation, as in \<open>if _ then _ else _ fi\<close>.\<close>
1.449
1.450 -  Since \<open>\<tau>\<close> may be again a function type, the constant
1.451 -  type scheme may have more argument positions than the mixfix
1.452 -  pattern.  Printing a nested application \<open>c t\<^sub>1 \<dots> t\<^sub>m\<close> for
1.453 -  \<open>m > n\<close> works by attaching concrete notation only to the
1.454 -  innermost part, essentially by printing \<open>(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m\<close>
1.455 -  instead.  If a term has fewer arguments than specified in the mixfix
1.456 +  Since \<open>\<tau>\<close> may be again a function type, the constant type scheme may have
1.457 +  more argument positions than the mixfix pattern. Printing a nested
1.458 +  application \<open>c t\<^sub>1 \<dots> t\<^sub>m\<close> for \<open>m > n\<close> works by attaching concrete notation
1.459 +  only to the innermost part, essentially by printing \<open>(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m\<close>
1.460 +  instead. If a term has fewer arguments than specified in the mixfix
1.461    template, the concrete syntax is ignored.
1.462
1.463    \<^medskip>
1.464 -  A mixfix template may also contain additional directives
1.465 -  for pretty printing, notably spaces, blocks, and breaks.  The
1.466 -  general template format is a sequence over any of the following
1.467 -  entities.
1.468 +  A mixfix template may also contain additional directives for pretty
1.469 +  printing, notably spaces, blocks, and breaks. The general template format is
1.470 +  a sequence over any of the following entities.
1.471
1.472 -  \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of
1.473 -  characters other than the following special characters:
1.474 +  \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of characters other than
1.475 +  the following special characters:
1.476
1.477    \<^medskip>
1.478    \begin{tabular}{ll}
1.479 @@ -369,47 +345,45 @@
1.480    \end{tabular}
1.481    \<^medskip>
1.482
1.483 -  \<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these
1.484 -  meta-characters, producing a literal version of the following
1.485 -  character, unless that is a blank.
1.486 +  \<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these meta-characters, producing a
1.487 +  literal version of the following character, unless that is a blank.
1.488
1.489 -  A single quote followed by a blank separates delimiters, without
1.490 -  affecting printing, but input tokens may have additional white space
1.491 -  here.
1.492 +  A single quote followed by a blank separates delimiters, without affecting
1.493 +  printing, but input tokens may have additional white space here.
1.494
1.495 -  \<^descr> \<^verbatim>\<open>_\<close> is an argument position, which stands for a
1.496 -  certain syntactic category in the underlying grammar.
1.497 +  \<^descr> \<^verbatim>\<open>_\<close> is an argument position, which stands for a certain syntactic
1.498 +  category in the underlying grammar.
1.499
1.500 -  \<^descr> \<open>\<index>\<close> is an indexed argument position; this is the place
1.501 -  where implicit structure arguments can be attached.
1.502 -
1.503 -  \<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing.
1.504 -  This and the following specifications do not affect parsing at all.
1.505 +  \<^descr> \<open>\<index>\<close> is an indexed argument position; this is the place where implicit
1.506 +  structure arguments can be attached.
1.507
1.508 -  \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block.  The
1.509 -  optional number specifies how much indentation to add when a line
1.510 -  break occurs within the block.  If the parenthesis is not followed
1.511 -  by digits, the indentation defaults to 0.  A block specified via
1.512 -  \<^verbatim>\<open>(00\<close> is unbreakable.
1.513 +  \<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing. This and the following
1.514 +  specifications do not affect parsing at all.
1.515 +
1.516 +  \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block. The optional number specifies how
1.517 +  much indentation to add when a line break occurs within the block. If the
1.518 +  parenthesis is not followed by digits, the indentation defaults to 0. A
1.519 +  block specified via \<^verbatim>\<open>(00\<close> is unbreakable.
1.520
1.521    \<^descr> \<^verbatim>\<open>)\<close> closes a pretty printing block.
1.522
1.523    \<^descr> \<^verbatim>\<open>//\<close> forces a line break.
1.524
1.525 -  \<^descr> \<^verbatim>\<open>/\<close>\<open>s\<close> allows a line break.  Here \<open>s\<close>
1.526 -  stands for the string of spaces (zero or more) right after the
1.527 -  slash.  These spaces are printed if the break is \<^emph>\<open>not\<close> taken.
1.528 +  \<^descr> \<^verbatim>\<open>/\<close>\<open>s\<close> allows a line break. Here \<open>s\<close> stands for the string of spaces
1.529 +  (zero or more) right after the slash. These spaces are printed if the break
1.530 +  is \<^emph>\<open>not\<close> taken.
1.531
1.532
1.533 -  The general idea of pretty printing with blocks and breaks is also
1.534 -  described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
1.535 +  The general idea of pretty printing with blocks and breaks is also described
1.536 +  in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
1.537  \<close>
1.538
1.539
1.540  subsection \<open>Infixes\<close>
1.541
1.542 -text \<open>Infix operators are specified by convenient short forms that
1.543 -  abbreviate general mixfix annotations as follows:
1.544 +text \<open>
1.545 +  Infix operators are specified by convenient short forms that abbreviate
1.546 +  general mixfix annotations as follows:
1.547
1.548    \begin{center}
1.549    \begin{tabular}{lll}
1.550 @@ -427,35 +401,33 @@
1.551    \end{tabular}
1.552    \end{center}
1.553
1.554 -  The mixfix template \<^verbatim>\<open>"(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)"\<close>
1.555 -  specifies two argument positions; the delimiter is preceded by a
1.556 -  space and followed by a space or line break; the entire phrase is a
1.557 -  pretty printing block.
1.558 +  The mixfix template \<^verbatim>\<open>"(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)"\<close> specifies two argument positions;
1.559 +  the delimiter is preceded by a space and followed by a space or line break;
1.560 +  the entire phrase is a pretty printing block.
1.561
1.562 -  The alternative notation \<^verbatim>\<open>op\<close>~\<open>sy\<close> is introduced
1.563 -  in addition.  Thus any infix operator may be written in prefix form
1.564 -  (as in ML), independently of the number of arguments in the term.
1.565 +  The alternative notation \<^verbatim>\<open>op\<close>~\<open>sy\<close> is introduced in addition. Thus any
1.566 +  infix operator may be written in prefix form (as in ML), independently of
1.567 +  the number of arguments in the term.
1.568  \<close>
1.569
1.570
1.571  subsection \<open>Binders\<close>
1.572
1.573 -text \<open>A \<^emph>\<open>binder\<close> is a variable-binding construct such as a
1.574 -  quantifier.  The idea to formalize \<open>\<forall>x. b\<close> as \<open>All
1.575 -  (\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close> already goes back
1.576 -  to @{cite church40}.  Isabelle declarations of certain higher-order
1.577 -  operators may be annotated with @{keyword_def "binder"} annotations
1.578 -  as follows:
1.579 +text \<open>
1.580 +  A \<^emph>\<open>binder\<close> is a variable-binding construct such as a quantifier. The idea
1.581 +  to formalize \<open>\<forall>x. b\<close> as \<open>All (\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close>
1.582 +  already goes back to @{cite church40}. Isabelle declarations of certain
1.583 +  higher-order operators may be annotated with @{keyword_def "binder"}
1.584 +  annotations as follows:
1.585
1.586    \begin{center}
1.587    \<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>
1.588    \end{center}
1.589
1.590 -  This introduces concrete binder syntax \<open>sy x. b\<close>, where
1.591 -  \<open>x\<close> is a bound 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 type \<open>\<tau>\<^sub>3\<close>.
1.592 -  The optional integer \<open>p\<close> specifies the syntactic priority of
1.593 -  the body; the default is \<open>q\<close>, which is also the priority of
1.594 -  the whole construct.
1.595 +  This introduces concrete binder syntax \<open>sy x. b\<close>, where \<open>x\<close> is a bound
1.596 +  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
1.597 +  type \<open>\<tau>\<^sub>3\<close>. The optional integer \<open>p\<close> specifies the syntactic priority of the
1.598 +  body; the default is \<open>q\<close>, which is also the priority of the whole construct.
1.599
1.600    Internally, the binder syntax is expanded to something like this:
1.601    \begin{center}
1.602 @@ -464,17 +436,18 @@
1.603
1.604    Here @{syntax (inner) idts} is the nonterminal symbol for a list of
1.606 -  \secref{sec:pure-grammar}).  The mixfix template \<^verbatim>\<open>"(3\<close>\<open>sy\<close>\<^verbatim>\<open>_./ _)"\<close>
1.607 -  defines argument positions
1.608 -  for the bound identifiers and the body, separated by a dot with
1.609 -  optional line break; the entire phrase is a pretty printing block of
1.610 -  indentation level 3.  Note that there is no extra space after \<open>sy\<close>, so it needs to be included user specification if the binder
1.611 -  syntax ends with a token that may be continued by an identifier
1.612 -  token at the start of @{syntax (inner) idts}.
1.613 +  \secref{sec:pure-grammar}). The mixfix template \<^verbatim>\<open>"(3\<close>\<open>sy\<close>\<^verbatim>\<open>_./ _)"\<close> defines
1.614 +  argument positions for the bound identifiers and the body, separated by a
1.615 +  dot with optional line break; the entire phrase is a pretty printing block
1.616 +  of indentation level 3. Note that there is no extra space after \<open>sy\<close>, so it
1.617 +  needs to be included user specification if the binder syntax ends with a
1.618 +  token that may be continued by an identifier token at the start of @{syntax
1.619 +  (inner) idts}.
1.620
1.621 -  Furthermore, a syntax translation to transforms \<open>c_binder x\<^sub>1
1.622 -  \<dots> x\<^sub>n b\<close> into iterated application \<open>c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)\<close>.
1.623 -  This works in both directions, for parsing and printing.\<close>
1.624 +  Furthermore, a syntax translation to transforms \<open>c_binder x\<^sub>1 \<dots> x\<^sub>n b\<close> into
1.625 +  iterated application \<open>c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)\<close>. This works in both
1.626 +  directions, for parsing and printing.
1.627 +\<close>
1.628
1.629
1.630  section \<open>Explicit notation \label{sec:notation}\<close>
1.631 @@ -488,12 +461,11 @@
1.632      @{command_def "write"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
1.633    \end{matharray}
1.634
1.635 -  Commands that introduce new logical entities (terms or types)
1.636 -  usually allow to provide mixfix annotations on the spot, which is
1.637 -  convenient for default notation.  Nonetheless, the syntax may be
1.638 -  modified later on by declarations for explicit notation.  This
1.639 -  allows to add or delete mixfix annotations for of existing logical
1.640 -  entities within the current context.
1.641 +  Commands that introduce new logical entities (terms or types) usually allow
1.642 +  to provide mixfix annotations on the spot, which is convenient for default
1.643 +  notation. Nonetheless, the syntax may be modified later on by declarations
1.644 +  for explicit notation. This allows to add or delete mixfix annotations for
1.645 +  of existing logical entities within the current context.
1.646
1.647    @{rail \<open>
1.648      (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
1.649 @@ -505,24 +477,22 @@
1.650      @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
1.651    \<close>}
1.652
1.653 -  \<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix
1.654 -  syntax with an existing type constructor.  The arity of the
1.656 +  \<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix syntax with an
1.657 +  existing type constructor. The arity of the constructor is retrieved from
1.658 +  the context.
1.659
1.660 -  \<^descr> @{command "no_type_notation"} is similar to @{command
1.661 -  "type_notation"}, but removes the specified syntax annotation from
1.662 -  the present context.
1.663 +  \<^descr> @{command "no_type_notation"} is similar to @{command "type_notation"},
1.664 +  but removes the specified syntax annotation from the present context.
1.665
1.666 -  \<^descr> @{command "notation"}~\<open>c (mx)\<close> associates mixfix
1.667 -  syntax with an existing constant or fixed variable.  The type
1.668 -  declaration of the given entity is retrieved from the context.
1.669 +  \<^descr> @{command "notation"}~\<open>c (mx)\<close> associates mixfix syntax with an existing
1.670 +  constant or fixed variable. The type declaration of the given entity is
1.672
1.673 -  \<^descr> @{command "no_notation"} is similar to @{command "notation"},
1.674 -  but removes the specified syntax annotation from the present
1.675 -  context.
1.676 +  \<^descr> @{command "no_notation"} is similar to @{command "notation"}, but removes
1.677 +  the specified syntax annotation from the present context.
1.678
1.679 -  \<^descr> @{command "write"} is similar to @{command "notation"}, but
1.680 -  works within an Isar proof body.
1.681 +  \<^descr> @{command "write"} is similar to @{command "notation"}, but works within
1.682 +  an Isar proof body.
1.683  \<close>
1.684
1.685
1.686 @@ -530,26 +500,24 @@
1.687
1.688  subsection \<open>Lexical matters \label{sec:inner-lex}\<close>
1.689
1.690 -text \<open>The inner lexical syntax vaguely resembles the outer one
1.691 -  (\secref{sec:outer-lex}), but some details are different.  There are
1.692 -  two main categories of inner syntax tokens:
1.693 +text \<open>
1.694 +  The inner lexical syntax vaguely resembles the outer one
1.695 +  (\secref{sec:outer-lex}), but some details are different. There are two main
1.696 +  categories of inner syntax tokens:
1.697
1.698 -  \<^enum> \<^emph>\<open>delimiters\<close> --- the literal tokens occurring in
1.699 -  productions of the given priority grammar (cf.\
1.700 -  \secref{sec:priority-grammar});
1.701 +  \<^enum> \<^emph>\<open>delimiters\<close> --- the literal tokens occurring in productions of the given
1.702 +  priority grammar (cf.\ \secref{sec:priority-grammar});
1.703
1.704    \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc.
1.705
1.706
1.707 -  Delimiters override named tokens and may thus render certain
1.708 -  identifiers inaccessible.  Sometimes the logical context admits
1.709 -  alternative ways to refer to the same entity, potentially via
1.710 -  qualified names.
1.711 +  Delimiters override named tokens and may thus render certain identifiers
1.712 +  inaccessible. Sometimes the logical context admits alternative ways to refer
1.713 +  to the same entity, potentially via qualified names.
1.714
1.715    \<^medskip>
1.716 -  The categories for named tokens are defined once and for
1.717 -  all as follows, reusing some categories of the outer token syntax
1.718 -  (\secref{sec:outer-lex}).
1.719 +  The categories for named tokens are defined once and for all as follows,
1.720 +  reusing some categories of the outer token syntax (\secref{sec:outer-lex}).
1.721
1.722    \begin{center}
1.723    \begin{supertabular}{rcl}
1.724 @@ -581,32 +549,30 @@
1.725
1.726  subsection \<open>Priority grammars \label{sec:priority-grammar}\<close>
1.727
1.728 -text \<open>A context-free grammar consists of a set of \<^emph>\<open>terminal
1.729 -  symbols\<close>, a set of \<^emph>\<open>nonterminal symbols\<close> and a set of
1.730 -  \<^emph>\<open>productions\<close>.  Productions have the form \<open>A = \<gamma>\<close>,
1.731 -  where \<open>A\<close> is a nonterminal and \<open>\<gamma>\<close> is a string of
1.732 -  terminals and nonterminals.  One designated nonterminal is called
1.733 -  the \<^emph>\<open>root symbol\<close>.  The language defined by the grammar
1.734 -  consists of all strings of terminals that can be derived from the
1.735 -  root symbol by applying productions as rewrite rules.
1.736 +text \<open>
1.737 +  A context-free grammar consists of a set of \<^emph>\<open>terminal symbols\<close>, a set of
1.738 +  \<^emph>\<open>nonterminal symbols\<close> and a set of \<^emph>\<open>productions\<close>. Productions have the
1.739 +  form \<open>A = \<gamma>\<close>, where \<open>A\<close> is a nonterminal and \<open>\<gamma>\<close> is a string of terminals
1.740 +  and nonterminals. One designated nonterminal is called the \<^emph>\<open>root symbol\<close>.
1.741 +  The language defined by the grammar consists of all strings of terminals
1.742 +  that can be derived from the root symbol by applying productions as rewrite
1.743 +  rules.
1.744
1.745 -  The standard Isabelle parser for inner syntax uses a \<^emph>\<open>priority
1.746 -  grammar\<close>.  Each nonterminal is decorated by an integer priority:
1.747 -  \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>.  In a derivation, \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> may be rewritten
1.748 -  using a production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> only if \<open>p \<le> q\<close>.  Any
1.749 -  priority grammar can be translated into a normal context-free
1.750 -  grammar by introducing new nonterminals and productions.
1.751 +  The standard Isabelle parser for inner syntax uses a \<^emph>\<open>priority grammar\<close>.
1.752 +  Each nonterminal is decorated by an integer priority: \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>. In a
1.753 +  derivation, \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> may be rewritten using a production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> only
1.754 +  if \<open>p \<le> q\<close>. Any priority grammar can be translated into a normal
1.755 +  context-free grammar by introducing new nonterminals and productions.
1.756
1.757    \<^medskip>
1.758 -  Formally, a set of context free productions \<open>G\<close>
1.759 -  induces a derivation relation \<open>\<longrightarrow>\<^sub>G\<close> as follows.  Let \<open>\<alpha>\<close> and \<open>\<beta>\<close> denote strings of terminal or nonterminal symbols.
1.760 -  Then \<open>\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>\<close> holds if and only if \<open>G\<close>
1.761 +  Formally, a set of context free productions \<open>G\<close> induces a derivation
1.762 +  relation \<open>\<longrightarrow>\<^sub>G\<close> as follows. Let \<open>\<alpha>\<close> and \<open>\<beta>\<close> denote strings of terminal or
1.763 +  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>
1.764    contains some production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> for \<open>p \<le> q\<close>.
1.765
1.766    \<^medskip>
1.767 -  The following grammar for arithmetic expressions
1.768 -  demonstrates how binding power and associativity of operators can be
1.769 -  enforced by priorities.
1.770 +  The following grammar for arithmetic expressions demonstrates how binding
1.771 +  power and associativity of operators can be enforced by priorities.
1.772
1.773    \begin{center}
1.774    \begin{tabular}{rclr}
1.775 @@ -617,28 +583,25 @@
1.776    \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>=\<close> & \<^verbatim>\<open>-\<close> \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \\
1.777    \end{tabular}
1.778    \end{center}
1.779 -  The choice of priorities determines that \<^verbatim>\<open>-\<close> binds
1.780 -  tighter than \<^verbatim>\<open>*\<close>, which binds tighter than \<^verbatim>\<open>+\<close>.
1.781 -  Furthermore \<^verbatim>\<open>+\<close> associates to the left and
1.782 -  \<^verbatim>\<open>*\<close> to the right.
1.783 +  The choice of priorities determines that \<^verbatim>\<open>-\<close> binds tighter than \<^verbatim>\<open>*\<close>, which
1.784 +  binds tighter than \<^verbatim>\<open>+\<close>. Furthermore \<^verbatim>\<open>+\<close> associates to the left and \<^verbatim>\<open>*\<close> to
1.785 +  the right.
1.786
1.787    \<^medskip>
1.788    For clarity, grammars obey these conventions:
1.789
1.790 -  \<^item> All priorities must lie between 0 and 1000.
1.791 +    \<^item> All priorities must lie between 0 and 1000.
1.792
1.793 -  \<^item> Priority 0 on the right-hand side and priority 1000 on the
1.794 -  left-hand side may be omitted.
1.795 +    \<^item> Priority 0 on the right-hand side and priority 1000 on the left-hand
1.796 +    side may be omitted.
1.797
1.798 -  \<^item> The production \<open>A\<^sup>(\<^sup>p\<^sup>) = \<alpha>\<close> is written as \<open>A = \<alpha>
1.799 -  (p)\<close>, i.e.\ the priority of the left-hand side actually appears in
1.800 -  a column on the far right.
1.801 +    \<^item> The production \<open>A\<^sup>(\<^sup>p\<^sup>) = \<alpha>\<close> is written as \<open>A = \<alpha> (p)\<close>, i.e.\ the
1.802 +    priority of the left-hand side actually appears in a column on the far
1.803 +    right.
1.804
1.805 -  \<^item> Alternatives are separated by \<open>|\<close>.
1.806 +    \<^item> Alternatives are separated by \<open>|\<close>.
1.807
1.808 -  \<^item> Repetition is indicated by dots \<open>(\<dots>)\<close> in an informal
1.809 -  but obvious way.
1.810 -
1.811 +    \<^item> Repetition is indicated by dots \<open>(\<dots>)\<close> in an informal but obvious way.
1.812
1.813    Using these conventions, the example grammar specification above
1.814    takes the form:
1.815 @@ -656,8 +619,9 @@
1.816
1.817  subsection \<open>The Pure grammar \label{sec:pure-grammar}\<close>
1.818
1.819 -text \<open>The priority grammar of the \<open>Pure\<close> theory is defined
1.820 -  approximately like this:
1.821 +text \<open>
1.822 +  The priority grammar of the \<open>Pure\<close> theory is defined approximately like
1.823 +  this:
1.824
1.825    \begin{center}
1.826    \begin{supertabular}{rclr}
1.827 @@ -729,55 +693,54 @@
1.828    \end{center}
1.829
1.830    \<^medskip>
1.831 -  Here literal terminals are printed \<^verbatim>\<open>verbatim\<close>;
1.833 -  inner syntax.  The meaning of the nonterminals defined by the above
1.834 -  grammar is as follows:
1.836 +  \secref{sec:inner-lex} for further token categories of the inner syntax. The
1.837 +  meaning of the nonterminals defined by the above grammar is as follows:
1.838
1.839    \<^descr> @{syntax_ref (inner) any} denotes any term.
1.840
1.841 -  \<^descr> @{syntax_ref (inner) prop} denotes meta-level propositions,
1.842 -  which are terms of type @{typ prop}.  The syntax of such formulae of
1.843 -  the meta-logic is carefully distinguished from usual conventions for
1.844 -  object-logics.  In particular, plain \<open>\<lambda>\<close>-term notation is
1.845 -  \<^emph>\<open>not\<close> recognized as @{syntax (inner) prop}.
1.846 +  \<^descr> @{syntax_ref (inner) prop} denotes meta-level propositions, which are
1.847 +  terms of type @{typ prop}. The syntax of such formulae of the meta-logic is
1.848 +  carefully distinguished from usual conventions for object-logics. In
1.849 +  particular, plain \<open>\<lambda>\<close>-term notation is \<^emph>\<open>not\<close> recognized as @{syntax (inner)
1.850 +  prop}.
1.851
1.852 -  \<^descr> @{syntax_ref (inner) aprop} denotes atomic propositions, which
1.853 -  are embedded into regular @{syntax (inner) prop} by means of an
1.854 -  explicit \<^verbatim>\<open>PROP\<close> token.
1.855 +  \<^descr> @{syntax_ref (inner) aprop} denotes atomic propositions, which are
1.856 +  embedded into regular @{syntax (inner) prop} by means of an explicit \<^verbatim>\<open>PROP\<close>
1.857 +  token.
1.858
1.859 -  Terms of type @{typ prop} with non-constant head, e.g.\ a plain
1.860 -  variable, are printed in this form.  Constants that yield type @{typ
1.861 -  prop} are expected to provide their own concrete syntax; otherwise
1.862 -  the printed version will appear like @{syntax (inner) logic} and
1.863 -  cannot be parsed again as @{syntax (inner) prop}.
1.864 +  Terms of type @{typ prop} with non-constant head, e.g.\ a plain variable,
1.865 +  are printed in this form. Constants that yield type @{typ prop} are expected
1.866 +  to provide their own concrete syntax; otherwise the printed version will
1.867 +  appear like @{syntax (inner) logic} and cannot be parsed again as @{syntax
1.868 +  (inner) prop}.
1.869
1.870 -  \<^descr> @{syntax_ref (inner) logic} denotes arbitrary terms of a
1.871 -  logical type, excluding type @{typ prop}.  This is the main
1.872 -  syntactic category of object-logic entities, covering plain \<open>\<lambda>\<close>-term notation (variables, abstraction, application), plus
1.873 -  anything defined by the user.
1.874 +  \<^descr> @{syntax_ref (inner) logic} denotes arbitrary terms of a logical type,
1.875 +  excluding type @{typ prop}. This is the main syntactic category of
1.876 +  object-logic entities, covering plain \<open>\<lambda>\<close>-term notation (variables,
1.877 +  abstraction, application), plus anything defined by the user.
1.878
1.879 -  When specifying notation for logical entities, all logical types
1.880 -  (excluding @{typ prop}) are \<^emph>\<open>collapsed\<close> to this single category
1.881 -  of @{syntax (inner) logic}.
1.882 +  When specifying notation for logical entities, all logical types (excluding
1.883 +  @{typ prop}) are \<^emph>\<open>collapsed\<close> to this single category of @{syntax (inner)
1.884 +  logic}.
1.885
1.886 -  \<^descr> @{syntax_ref (inner) index} denotes an optional index term for
1.887 -  indexed syntax.  If omitted, it refers to the first @{keyword_ref
1.888 -  "structure"} variable in the context.  The special dummy \<open>\<index>\<close>'' serves as pattern variable in mixfix annotations that
1.889 -  introduce indexed notation.
1.890 +  \<^descr> @{syntax_ref (inner) index} denotes an optional index term for indexed
1.891 +  syntax. If omitted, it refers to the first @{keyword_ref "structure"}
1.892 +  variable in the context. The special dummy \<open>\<index>\<close>'' serves as pattern
1.893 +  variable in mixfix annotations that introduce indexed notation.
1.894
1.895 -  \<^descr> @{syntax_ref (inner) idt} denotes identifiers, possibly
1.896 -  constrained by types.
1.897 +  \<^descr> @{syntax_ref (inner) idt} denotes identifiers, possibly constrained by
1.898 +  types.
1.899
1.900 -  \<^descr> @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref
1.901 -  (inner) idt}.  This is the most basic category for variables in
1.902 -  iterated binders, such as \<open>\<lambda>\<close> or \<open>\<And>\<close>.
1.903 +  \<^descr> @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref (inner)
1.904 +  idt}. This is the most basic category for variables in iterated binders,
1.905 +  such as \<open>\<lambda>\<close> or \<open>\<And>\<close>.
1.906
1.907 -  \<^descr> @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns}
1.908 -  denote patterns for abstraction, cases bindings etc.  In Pure, these
1.909 -  categories start as a merely copy of @{syntax (inner) idt} and
1.910 -  @{syntax (inner) idts}, respectively.  Object-logics may add
1.911 -  additional productions for binding forms.
1.912 +  \<^descr> @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns} denote
1.913 +  patterns for abstraction, cases bindings etc. In Pure, these categories
1.914 +  start as a merely copy of @{syntax (inner) idt} and @{syntax (inner) idts},
1.916 +  forms.
1.917
1.918    \<^descr> @{syntax_ref (inner) type} denotes types of the meta-logic.
1.919
1.920 @@ -786,58 +749,52 @@
1.921
1.922    Here are some further explanations of certain syntax features.
1.923
1.924 -  \<^item> In @{syntax (inner) idts}, note that \<open>x :: nat y\<close> is
1.925 -  parsed as \<open>x :: (nat y)\<close>, treating \<open>y\<close> like a type
1.926 -  constructor applied to \<open>nat\<close>.  To avoid this interpretation,
1.927 -  write \<open>(x :: nat) y\<close> with explicit parentheses.
1.928 +  \<^item> In @{syntax (inner) idts}, note that \<open>x :: nat y\<close> is parsed as \<open>x :: (nat
1.929 +  y)\<close>, treating \<open>y\<close> like a type constructor applied to \<open>nat\<close>. To avoid this
1.930 +  interpretation, write \<open>(x :: nat) y\<close> with explicit parentheses.
1.931
1.932 -  \<^item> Similarly, \<open>x :: nat y :: nat\<close> is parsed as \<open>x ::
1.933 -  (nat y :: nat)\<close>.  The correct form is \<open>(x :: nat) (y ::
1.934 -  nat)\<close>, or \<open>(x :: nat) y :: nat\<close> if \<open>y\<close> is last in the
1.935 -  sequence of identifiers.
1.936 +  \<^item> Similarly, \<open>x :: nat y :: nat\<close> is parsed as \<open>x :: (nat y :: nat)\<close>. The
1.937 +  correct form is \<open>(x :: nat) (y :: nat)\<close>, or \<open>(x :: nat) y :: nat\<close> if \<open>y\<close> is
1.938 +  last in the sequence of identifiers.
1.939
1.940 -  \<^item> Type constraints for terms bind very weakly.  For example,
1.941 -  \<open>x < y :: nat\<close> is normally parsed as \<open>(x < y) ::
1.942 -  nat\<close>, unless \<open><\<close> has a very low priority, in which case the
1.943 -  input is likely to be ambiguous.  The correct form is \<open>x < (y
1.944 -  :: nat)\<close>.
1.945 +  \<^item> Type constraints for terms bind very weakly. For example, \<open>x < y :: nat\<close>
1.946 +  is normally parsed as \<open>(x < y) :: nat\<close>, unless \<open><\<close> has a very low priority,
1.947 +  in which case the input is likely to be ambiguous. The correct form is \<open>x <
1.948 +  (y :: nat)\<close>.
1.949
1.950    \<^item> Dummy variables (written as underscore) may occur in different
1.951    roles.
1.952
1.953 -    \<^descr> A type \<open>_\<close>'' or \<open>_ :: sort\<close>'' acts like an
1.954 -    anonymous inference parameter, which is filled-in according to the
1.955 -    most general type produced by the type-checking phase.
1.956 +    \<^descr> A type \<open>_\<close>'' or \<open>_ :: sort\<close>'' acts like an anonymous inference
1.957 +    parameter, which is filled-in according to the most general type produced
1.958 +    by the type-checking phase.
1.959
1.960 -    \<^descr> A bound \<open>_\<close>'' refers to a vacuous abstraction, where
1.961 -    the body does not refer to the binding introduced here.  As in the
1.962 -    term @{term "\<lambda>x _. x"}, which is \<open>\<alpha>\<close>-equivalent to \<open>\<lambda>x y. x\<close>.
1.963 +    \<^descr> A bound \<open>_\<close>'' refers to a vacuous abstraction, where the body does not
1.964 +    refer to the binding introduced here. As in the term @{term "\<lambda>x _. x"},
1.965 +    which is \<open>\<alpha>\<close>-equivalent to \<open>\<lambda>x y. x\<close>.
1.966
1.967 -    \<^descr> A free \<open>_\<close>'' refers to an implicit outer binding.
1.968 -    Higher definitional packages usually allow forms like \<open>f x _
1.969 -    = x\<close>.
1.970 +    \<^descr> A free \<open>_\<close>'' refers to an implicit outer binding. Higher definitional
1.971 +    packages usually allow forms like \<open>f x _ = x\<close>.
1.972
1.973 -    \<^descr> A schematic \<open>_\<close>'' (within a term pattern, see
1.974 -    \secref{sec:term-decls}) refers to an anonymous variable that is
1.975 -    implicitly abstracted over its context of locally bound variables.
1.976 -    For example, this allows pattern matching of \<open>{x. f x = g
1.977 -    x}\<close> against \<open>{x. _ = _}\<close>, or even \<open>{_. _ = _}\<close> by
1.978 +    \<^descr> A schematic \<open>_\<close>'' (within a term pattern, see \secref{sec:term-decls})
1.979 +    refers to an anonymous variable that is implicitly abstracted over its
1.980 +    context of locally bound variables. For example, this allows pattern
1.981 +    matching of \<open>{x. f x = g x}\<close> against \<open>{x. _ = _}\<close>, or even \<open>{_. _ = _}\<close> by
1.982      using both bound and schematic dummies.
1.983
1.984 -  \<^descr> The three literal dots \<^verbatim>\<open>...\<close>'' may be also
1.985 -  written as ellipsis symbol \<^verbatim>\<open>\<dots>\<close>.  In both cases this
1.986 -  refers to a special schematic variable, which is bound in the
1.987 -  context.  This special term abbreviation works nicely with
1.988 +  \<^descr> The three literal dots \<^verbatim>\<open>...\<close>'' may be also written as ellipsis symbol
1.989 +  \<^verbatim>\<open>\<dots>\<close>. In both cases this refers to a special schematic variable, which is
1.990 +  bound in the context. This special term abbreviation works nicely with
1.991    calculational reasoning (\secref{sec:calculation}).
1.992
1.993 -  \<^descr> \<^verbatim>\<open>CONST\<close> ensures that the given identifier is treated
1.994 -  as constant term, and passed through the parse tree in fully
1.995 -  internalized form.  This is particularly relevant for translation
1.996 -  rules (\secref{sec:syn-trans}), notably on the RHS.
1.997 +  \<^descr> \<^verbatim>\<open>CONST\<close> ensures that the given identifier is treated as constant term,
1.998 +  and passed through the parse tree in fully internalized form. This is
1.999 +  particularly relevant for translation rules (\secref{sec:syn-trans}),
1.1000 +  notably on the RHS.
1.1001
1.1002 -  \<^descr> \<^verbatim>\<open>XCONST\<close> is similar to \<^verbatim>\<open>CONST\<close>, but
1.1003 -  retains the constant name as given.  This is only relevant to
1.1004 -  translation rules (\secref{sec:syn-trans}), notably on the LHS.
1.1005 +  \<^descr> \<^verbatim>\<open>XCONST\<close> is similar to \<^verbatim>\<open>CONST\<close>, but retains the constant name as given.
1.1006 +  This is only relevant to translation rules (\secref{sec:syn-trans}), notably
1.1007 +  on the LHS.
1.1008  \<close>
1.1009
1.1010
1.1011 @@ -848,46 +805,45 @@
1.1012      @{command_def "print_syntax"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
1.1013    \end{matharray}
1.1014
1.1015 -  \<^descr> @{command "print_syntax"} prints the inner syntax of the
1.1016 -  current context.  The output can be quite large; the most important
1.1017 -  sections are explained below.
1.1018 +  \<^descr> @{command "print_syntax"} prints the inner syntax of the current context.
1.1019 +  The output can be quite large; the most important sections are explained
1.1020 +  below.
1.1021
1.1022 -    \<^descr> \<open>lexicon\<close> lists the delimiters of the inner token
1.1023 -    language; see \secref{sec:inner-lex}.
1.1024 -
1.1025 -    \<^descr> \<open>prods\<close> lists the productions of the underlying
1.1026 -    priority grammar; see \secref{sec:priority-grammar}.
1.1027 +    \<^descr> \<open>lexicon\<close> lists the delimiters of the inner token language; see
1.1028 +    \secref{sec:inner-lex}.
1.1029
1.1030 -    The nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is rendered in plain text as \<open>A[p]\<close>; delimiters are quoted.  Many productions have an extra
1.1031 -    \<open>\<dots> => name\<close>.  These names later become the heads of parse
1.1032 -    trees; they also guide the pretty printer.
1.1033 +    \<^descr> \<open>prods\<close> lists the productions of the underlying priority grammar; see
1.1034 +    \secref{sec:priority-grammar}.
1.1035
1.1036 -    Productions without such parse tree names are called \<^emph>\<open>copy
1.1037 -    productions\<close>.  Their right-hand side must have exactly one
1.1038 -    nonterminal symbol (or named token).  The parser does not create a
1.1039 -    new parse tree node for copy productions, but simply returns the
1.1040 -    parse tree of the right-hand symbol.
1.1041 +    The nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is rendered in plain text as \<open>A[p]\<close>; delimiters
1.1042 +    are quoted. Many productions have an extra \<open>\<dots> => name\<close>. These names later
1.1043 +    become the heads of parse trees; they also guide the pretty printer.
1.1044 +
1.1045 +    Productions without such parse tree names are called \<^emph>\<open>copy productions\<close>.
1.1046 +    Their right-hand side must have exactly one nonterminal symbol (or named
1.1047 +    token). The parser does not create a new parse tree node for copy
1.1048 +    productions, but simply returns the parse tree of the right-hand symbol.
1.1049
1.1050      If the right-hand side of a copy production consists of a single
1.1051      nonterminal without any delimiters, then it is called a \<^emph>\<open>chain
1.1052 -    production\<close>.  Chain productions act as abbreviations: conceptually,
1.1053 -    they are removed from the grammar by adding new productions.
1.1054 -    Priority information attached to chain productions is ignored; only
1.1055 -    the dummy value \<open>-1\<close> is displayed.
1.1056 +    production\<close>. Chain productions act as abbreviations: conceptually, they
1.1057 +    are removed from the grammar by adding new productions. Priority
1.1058 +    information attached to chain productions is ignored; only the dummy value
1.1059 +    \<open>-1\<close> is displayed.
1.1060
1.1061 -    \<^descr> \<open>print modes\<close> lists the alternative print modes
1.1062 -    provided by this grammar; see \secref{sec:print-modes}.
1.1063 +    \<^descr> \<open>print modes\<close> lists the alternative print modes provided by this
1.1064 +    grammar; see \secref{sec:print-modes}.
1.1065
1.1066 -    \<^descr> \<open>parse_rules\<close> and \<open>print_rules\<close> relate to
1.1067 -    syntax translations (macros); see \secref{sec:syn-trans}.
1.1068 +    \<^descr> \<open>parse_rules\<close> and \<open>print_rules\<close> relate to syntax translations (macros);
1.1069 +    see \secref{sec:syn-trans}.
1.1070
1.1071 -    \<^descr> \<open>parse_ast_translation\<close> and \<open>print_ast_translation\<close> list sets of constants that invoke
1.1072 -    translation functions for abstract syntax trees, which are only
1.1073 -    required in very special situations; see \secref{sec:tr-funs}.
1.1074 +    \<^descr> \<open>parse_ast_translation\<close> and \<open>print_ast_translation\<close> list sets of
1.1075 +    constants that invoke translation functions for abstract syntax trees,
1.1076 +    which are only required in very special situations; see
1.1077 +    \secref{sec:tr-funs}.
1.1078
1.1079 -    \<^descr> \<open>parse_translation\<close> and \<open>print_translation\<close>
1.1080 -    list the sets of constants that invoke regular translation
1.1081 -    functions; see \secref{sec:tr-funs}.
1.1082 +    \<^descr> \<open>parse_translation\<close> and \<open>print_translation\<close> list the sets of constants
1.1083 +    that invoke regular translation functions; see \secref{sec:tr-funs}.
1.1084  \<close>
1.1085
1.1086
1.1087 @@ -899,37 +855,36 @@
1.1088      @{attribute_def syntax_ambiguity_limit} & : & \<open>attribute\<close> & default \<open>10\<close> \\
1.1089    \end{tabular}
1.1090
1.1091 -  Depending on the grammar and the given input, parsing may be
1.1092 -  ambiguous.  Isabelle lets the Earley parser enumerate all possible
1.1093 -  parse trees, and then tries to make the best out of the situation.
1.1094 -  Terms that cannot be type-checked are filtered out, which often
1.1095 -  leads to a unique result in the end.  Unlike regular type
1.1096 -  reconstruction, which is applied to the whole collection of input
1.1097 -  terms simultaneously, the filtering stage only treats each given
1.1098 -  term in isolation.  Filtering is also not attempted for individual
1.1099 +  Depending on the grammar and the given input, parsing may be ambiguous.
1.1100 +  Isabelle lets the Earley parser enumerate all possible parse trees, and then
1.1101 +  tries to make the best out of the situation. Terms that cannot be
1.1102 +  type-checked are filtered out, which often leads to a unique result in the
1.1103 +  end. Unlike regular type reconstruction, which is applied to the whole
1.1104 +  collection of input terms simultaneously, the filtering stage only treats
1.1105 +  each given term in isolation. Filtering is also not attempted for individual
1.1106    types or raw ASTs (as required for @{command translations}).
1.1107
1.1108 -  Certain warning or error messages are printed, depending on the
1.1109 -  situation and the given configuration options.  Parsing ultimately
1.1110 -  fails, if multiple results remain after the filtering phase.
1.1111 +  Certain warning or error messages are printed, depending on the situation
1.1112 +  and the given configuration options. Parsing ultimately fails, if multiple
1.1113 +  results remain after the filtering phase.
1.1114
1.1115 -  \<^descr> @{attribute syntax_ambiguity_warning} controls output of
1.1116 -  explicit warning messages about syntax ambiguity.
1.1117 +  \<^descr> @{attribute syntax_ambiguity_warning} controls output of explicit warning
1.1118 +  messages about syntax ambiguity.
1.1119
1.1120 -  \<^descr> @{attribute syntax_ambiguity_limit} determines the number of
1.1121 -  resulting parse trees that are shown as part of the printed message
1.1122 -  in case of an ambiguity.
1.1123 +  \<^descr> @{attribute syntax_ambiguity_limit} determines the number of resulting
1.1124 +  parse trees that are shown as part of the printed message in case of an
1.1125 +  ambiguity.
1.1126  \<close>
1.1127
1.1128
1.1129  section \<open>Syntax transformations \label{sec:syntax-transformations}\<close>
1.1130
1.1131 -text \<open>The inner syntax engine of Isabelle provides separate
1.1132 -  mechanisms to transform parse trees either via rewrite systems on
1.1133 -  first-order ASTs (\secref{sec:syn-trans}), or ML functions on ASTs
1.1134 -  or syntactic \<open>\<lambda>\<close>-terms (\secref{sec:tr-funs}).  This works
1.1135 -  both for parsing and printing, as outlined in
1.1136 -  \figref{fig:parse-print}.
1.1137 +text \<open>
1.1138 +  The inner syntax engine of Isabelle provides separate mechanisms to
1.1139 +  transform parse trees either via rewrite systems on first-order ASTs
1.1140 +  (\secref{sec:syn-trans}), or ML functions on ASTs or syntactic \<open>\<lambda>\<close>-terms
1.1141 +  (\secref{sec:tr-funs}). This works both for parsing and printing, as
1.1142 +  outlined in \figref{fig:parse-print}.
1.1143
1.1144    \begin{figure}[htbp]
1.1145    \begin{center}
1.1146 @@ -954,137 +909,129 @@
1.1147    \caption{Parsing and printing with translations}\label{fig:parse-print}
1.1148    \end{figure}
1.1149
1.1150 -  These intermediate syntax tree formats eventually lead to a pre-term
1.1151 -  with all names and binding scopes resolved, but most type
1.1152 -  information still missing.  Explicit type constraints might be given by
1.1153 -  the user, or implicit position information by the system --- both
1.1154 -  need to be passed-through carefully by syntax transformations.
1.1155 +  These intermediate syntax tree formats eventually lead to a pre-term with
1.1156 +  all names and binding scopes resolved, but most type information still
1.1157 +  missing. Explicit type constraints might be given by the user, or implicit
1.1158 +  position information by the system --- both need to be passed-through
1.1159 +  carefully by syntax transformations.
1.1160
1.1161 -  Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and
1.1162 -  \<^emph>\<open>uncheck\<close> phases that are intertwined with type-inference (see
1.1163 -  also @{cite "isabelle-implementation"}).  The latter allows to operate
1.1164 -  on higher-order abstract syntax with proper binding and type
1.1166 +  Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and \<^emph>\<open>uncheck\<close>
1.1168 +  "isabelle-implementation"}). The latter allows to operate on higher-order
1.1169 +  abstract syntax with proper binding and type information already available.
1.1170
1.1171 -  As a rule of thumb, anything that manipulates bindings of variables
1.1172 -  or constants needs to be implemented as syntax transformation (see
1.1173 -  below).  Anything else is better done via check/uncheck: a prominent
1.1174 -  example application is the @{command abbreviation} concept of
1.1175 -  Isabelle/Pure.\<close>
1.1176 +  As a rule of thumb, anything that manipulates bindings of variables or
1.1177 +  constants needs to be implemented as syntax transformation (see below).
1.1178 +  Anything else is better done via check/uncheck: a prominent example
1.1179 +  application is the @{command abbreviation} concept of Isabelle/Pure.
1.1180 +\<close>
1.1181
1.1182
1.1183  subsection \<open>Abstract syntax trees \label{sec:ast}\<close>
1.1184
1.1185 -text \<open>The ML datatype @{ML_type Ast.ast} explicitly represents the
1.1186 -  intermediate AST format that is used for syntax rewriting
1.1187 -  (\secref{sec:syn-trans}).  It is defined in ML as follows:
1.1188 +text \<open>
1.1189 +  The ML datatype @{ML_type Ast.ast} explicitly represents the intermediate
1.1190 +  AST format that is used for syntax rewriting (\secref{sec:syn-trans}). It is
1.1191 +  defined in ML as follows:
1.1192    @{verbatim [display]
1.1193  \<open>datatype ast =
1.1194    Constant of string |
1.1195    Variable of string |
1.1196    Appl of ast list\<close>}
1.1197
1.1198 -  An AST is either an atom (constant or variable) or a list of (at
1.1199 -  least two) subtrees.  Occasional diagnostic output of ASTs uses
1.1200 -  notation that resembles S-expression of LISP.  Constant atoms are
1.1201 -  shown as quoted strings, variable atoms as non-quoted strings and
1.1202 -  applications as a parenthesized list of subtrees.  For example, the
1.1203 -  AST
1.1204 +  An AST is either an atom (constant or variable) or a list of (at least two)
1.1205 +  subtrees. Occasional diagnostic output of ASTs uses notation that resembles
1.1206 +  S-expression of LISP. Constant atoms are shown as quoted strings, variable
1.1207 +  atoms as non-quoted strings and applications as a parenthesized list of
1.1208 +  subtrees. For example, the AST
1.1209    @{ML [display] \<open>Ast.Appl [Ast.Constant "_abs", Ast.Variable "x", Ast.Variable "t"]\<close>}
1.1210 -  is pretty-printed as \<^verbatim>\<open>("_abs" x t)\<close>.  Note that
1.1211 -  \<^verbatim>\<open>()\<close> and \<^verbatim>\<open>(x)\<close> are excluded as ASTs, because
1.1212 -  they have too few subtrees.
1.1213 +  is pretty-printed as \<^verbatim>\<open>("_abs" x t)\<close>. Note that \<^verbatim>\<open>()\<close> and \<^verbatim>\<open>(x)\<close> are
1.1214 +  excluded as ASTs, because they have too few subtrees.
1.1215
1.1216    \<^medskip>
1.1217 -  AST application is merely a pro-forma mechanism to indicate
1.1218 -  certain syntactic structures.  Thus \<^verbatim>\<open>(c a b)\<close> could mean
1.1219 -  either term application or type application, depending on the
1.1220 -  syntactic context.
1.1221 +  AST application is merely a pro-forma mechanism to indicate certain
1.1222 +  syntactic structures. Thus \<^verbatim>\<open>(c a b)\<close> could mean either term application or
1.1223 +  type application, depending on the syntactic context.
1.1224
1.1225 -  Nested application like \<^verbatim>\<open>(("_abs" x t) u)\<close> is also
1.1226 -  possible, but ASTs are definitely first-order: the syntax constant
1.1227 -  \<^verbatim>\<open>"_abs"\<close> does not bind the \<^verbatim>\<open>x\<close> in any way.
1.1228 -  Proper bindings are introduced in later stages of the term syntax,
1.1229 -  where \<^verbatim>\<open>("_abs" x t)\<close> becomes an @{ML Abs} node and
1.1230 -  occurrences of \<^verbatim>\<open>x\<close> in \<^verbatim>\<open>t\<close> are replaced by bound
1.1231 -  variables (represented as de-Bruijn indices).
1.1232 +  Nested application like \<^verbatim>\<open>(("_abs" x t) u)\<close> is also possible, but ASTs are
1.1233 +  definitely first-order: the syntax constant \<^verbatim>\<open>"_abs"\<close> does not bind the \<^verbatim>\<open>x\<close>
1.1234 +  in any way. Proper bindings are introduced in later stages of the term
1.1235 +  syntax, where \<^verbatim>\<open>("_abs" x t)\<close> becomes an @{ML Abs} node and occurrences of
1.1236 +  \<^verbatim>\<open>x\<close> in \<^verbatim>\<open>t\<close> are replaced by bound variables (represented as de-Bruijn
1.1237 +  indices).
1.1238  \<close>
1.1239
1.1240
1.1241  subsubsection \<open>AST constants versus variables\<close>
1.1242
1.1243 -text \<open>Depending on the situation --- input syntax, output syntax,
1.1244 -  translation patterns --- the distinction of atomic ASTs as @{ML
1.1245 -  Ast.Constant} versus @{ML Ast.Variable} serves slightly different
1.1246 -  purposes.
1.1247 +text \<open>
1.1248 +  Depending on the situation --- input syntax, output syntax, translation
1.1249 +  patterns --- the distinction of atomic ASTs as @{ML Ast.Constant} versus
1.1250 +  @{ML Ast.Variable} serves slightly different purposes.
1.1251
1.1252 -  Input syntax of a term such as \<open>f a b = c\<close> does not yet
1.1253 -  indicate the scopes of atomic entities \<open>f, a, b, c\<close>: they
1.1254 -  could be global constants or local variables, even bound ones
1.1255 -  depending on the context of the term.  @{ML Ast.Variable} leaves
1.1256 -  this choice still open: later syntax layers (or translation
1.1257 -  functions) may capture such a variable to determine its role
1.1258 -  specifically, to make it a constant, bound variable, free variable
1.1259 -  etc.  In contrast, syntax translations that introduce already known
1.1260 -  constants would rather do it via @{ML Ast.Constant} to prevent
1.1261 -  accidental re-interpretation later on.
1.1262 +  Input syntax of a term such as \<open>f a b = c\<close> does not yet indicate the scopes
1.1263 +  of atomic entities \<open>f, a, b, c\<close>: they could be global constants or local
1.1264 +  variables, even bound ones depending on the context of the term. @{ML
1.1265 +  Ast.Variable} leaves this choice still open: later syntax layers (or
1.1266 +  translation functions) may capture such a variable to determine its role
1.1267 +  specifically, to make it a constant, bound variable, free variable etc. In
1.1268 +  contrast, syntax translations that introduce already known constants would
1.1269 +  rather do it via @{ML Ast.Constant} to prevent accidental re-interpretation
1.1270 +  later on.
1.1271
1.1272 -  Output syntax turns term constants into @{ML Ast.Constant} and
1.1273 -  variables (free or schematic) into @{ML Ast.Variable}.  This
1.1274 -  information is precise when printing fully formal \<open>\<lambda>\<close>-terms.
1.1275 +  Output syntax turns term constants into @{ML Ast.Constant} and variables
1.1276 +  (free or schematic) into @{ML Ast.Variable}. This information is precise
1.1277 +  when printing fully formal \<open>\<lambda>\<close>-terms.
1.1278
1.1279    \<^medskip>
1.1280 -  AST translation patterns (\secref{sec:syn-trans}) that
1.1281 -  represent terms cannot distinguish constants and variables
1.1282 -  syntactically.  Explicit indication of \<open>CONST c\<close> inside the
1.1283 -  term language is required, unless \<open>c\<close> is known as special
1.1285 -  possible to use @{command syntax} declarations (without mixfix
1.1286 -  annotation) to enforce that certain unqualified names are always
1.1287 -  treated as constant within the syntax machinery.
1.1288 +  AST translation patterns (\secref{sec:syn-trans}) that represent terms
1.1289 +  cannot distinguish constants and variables syntactically. Explicit
1.1290 +  indication of \<open>CONST c\<close> inside the term language is required, unless \<open>c\<close> is
1.1291 +  known as special \<^emph>\<open>syntax constant\<close> (see also @{command syntax}). It is also
1.1292 +  possible to use @{command syntax} declarations (without mixfix annotation)
1.1293 +  to enforce that certain unqualified names are always treated as constant
1.1294 +  within the syntax machinery.
1.1295
1.1296 -  The situation is simpler for ASTs that represent types or sorts,
1.1297 -  since the concrete syntax already distinguishes type variables from
1.1298 -  type constants (constructors).  So \<open>('a, 'b) foo\<close>
1.1299 -  corresponds to an AST application of some constant for \<open>foo\<close>
1.1300 -  and variable arguments for \<open>'a\<close> and \<open>'b\<close>.  Note that
1.1301 -  the postfix application is merely a feature of the concrete syntax,
1.1302 -  while in the AST the constructor occurs in head position.\<close>
1.1303 +  The situation is simpler for ASTs that represent types or sorts, since the
1.1304 +  concrete syntax already distinguishes type variables from type constants
1.1305 +  (constructors). So \<open>('a, 'b) foo\<close> corresponds to an AST application of some
1.1306 +  constant for \<open>foo\<close> and variable arguments for \<open>'a\<close> and \<open>'b\<close>. Note that the
1.1307 +  postfix application is merely a feature of the concrete syntax, while in the
1.1308 +  AST the constructor occurs in head position.
1.1309 +\<close>
1.1310
1.1311
1.1312  subsubsection \<open>Authentic syntax names\<close>
1.1313
1.1314 -text \<open>Naming constant entities within ASTs is another delicate
1.1315 -  issue.  Unqualified names are resolved in the name space tables in
1.1316 -  the last stage of parsing, after all translations have been applied.
1.1318 -  resolution, there can be surprises in boundary cases.
1.1319 +text \<open>
1.1320 +  Naming constant entities within ASTs is another delicate issue. Unqualified
1.1321 +  names are resolved in the name space tables in the last stage of parsing,
1.1322 +  after all translations have been applied. Since syntax transformations do
1.1324 +  boundary cases.
1.1325
1.1326 -  \<^emph>\<open>Authentic syntax names\<close> for @{ML Ast.Constant} avoid this
1.1327 -  problem: the fully-qualified constant name with a special prefix for
1.1328 -  its formal category (\<open>class\<close>, \<open>type\<close>, \<open>const\<close>, \<open>fixed\<close>) represents the information faithfully
1.1329 -  within the untyped AST format.  Accidental overlap with free or
1.1330 -  bound variables is excluded as well.  Authentic syntax names work
1.1331 -  implicitly in the following situations:
1.1332 +  \<^emph>\<open>Authentic syntax names\<close> for @{ML Ast.Constant} avoid this problem: the
1.1333 +  fully-qualified constant name with a special prefix for its formal category
1.1334 +  (\<open>class\<close>, \<open>type\<close>, \<open>const\<close>, \<open>fixed\<close>) represents the information faithfully
1.1335 +  within the untyped AST format. Accidental overlap with free or bound
1.1336 +  variables is excluded as well. Authentic syntax names work implicitly in the
1.1337 +  following situations:
1.1338
1.1339 -  \<^item> Input of term constants (or fixed variables) that are
1.1340 -  introduced by concrete syntax via @{command notation}: the
1.1341 -  correspondence of a particular grammar production to some known term
1.1342 -  entity is preserved.
1.1343 +    \<^item> Input of term constants (or fixed variables) that are introduced by
1.1344 +    concrete syntax via @{command notation}: the correspondence of a
1.1345 +    particular grammar production to some known term entity is preserved.
1.1346
1.1347 -  \<^item> Input of type constants (constructors) and type classes ---
1.1348 -  thanks to explicit syntactic distinction independently on the
1.1349 -  context.
1.1350 +    \<^item> Input of type constants (constructors) and type classes --- thanks to
1.1351 +    explicit syntactic distinction independently on the context.
1.1352
1.1353 -  \<^item> Output of term constants, type constants, type classes ---
1.1354 -  this information is already available from the internal term to be
1.1355 -  printed.
1.1356 -
1.1357 +    \<^item> Output of term constants, type constants, type classes --- this
1.1358 +    information is already available from the internal term to be printed.
1.1359
1.1360 -  In other words, syntax transformations that operate on input terms
1.1361 -  written as prefix applications are difficult to make robust.
1.1362 -  Luckily, this case rarely occurs in practice, because syntax forms
1.1363 -  to be translated usually correspond to some concrete notation.\<close>
1.1364 +  In other words, syntax transformations that operate on input terms written
1.1365 +  as prefix applications are difficult to make robust. Luckily, this case
1.1366 +  rarely occurs in practice, because syntax forms to be translated usually
1.1367 +  correspond to some concrete notation.
1.1368 +\<close>
1.1369
1.1370
1.1371  subsection \<open>Raw syntax and translations \label{sec:syn-trans}\<close>
1.1372 @@ -1101,14 +1048,13 @@
1.1373    \end{tabular}
1.1374    \<^medskip>
1.1375
1.1376 -  Unlike mixfix notation for existing formal entities
1.1377 -  (\secref{sec:notation}), raw syntax declarations provide full access
1.1378 -  to the priority grammar of the inner syntax, without any sanity
1.1379 -  checks.  This includes additional syntactic categories (via
1.1380 -  @{command nonterminal}) and free-form grammar productions (via
1.1381 -  @{command syntax}).  Additional syntax translations (or macros, via
1.1382 -  @{command translations}) are required to turn resulting parse trees
1.1383 -  into proper representations of formal entities again.
1.1384 +  Unlike mixfix notation for existing formal entities (\secref{sec:notation}),
1.1385 +  raw syntax declarations provide full access to the priority grammar of the
1.1386 +  inner syntax, without any sanity checks. This includes additional syntactic
1.1387 +  categories (via @{command nonterminal}) and free-form grammar productions
1.1388 +  (via @{command syntax}). Additional syntax translations (or macros, via
1.1389 +  @{command translations}) are required to turn resulting parse trees into
1.1390 +  proper representations of formal entities again.
1.1391
1.1392    @{rail \<open>
1.1393      @@{command nonterminal} (@{syntax name} + @'and')
1.1394 @@ -1126,193 +1072,177 @@
1.1395      transpat: ('(' @{syntax nameref} ')')? @{syntax string}
1.1396    \<close>}
1.1397
1.1398 -  \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type
1.1399 -  constructor \<open>c\<close> (without arguments) to act as purely syntactic
1.1400 -  type: a nonterminal symbol of the inner syntax.
1.1401 +  \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without
1.1402 +  arguments) to act as purely syntactic type: a nonterminal symbol of the
1.1403 +  inner syntax.
1.1404
1.1405 -  \<^descr> @{command "syntax"}~\<open>(mode) c :: \<sigma> (mx)\<close> augments the
1.1406 -  priority grammar and the pretty printer table for the given print
1.1407 -  mode (default \<^verbatim>\<open>""\<close>). An optional keyword @{keyword_ref
1.1408 -  "output"} means that only the pretty printer table is affected.
1.1409 +  \<^descr> @{command "syntax"}~\<open>(mode) c :: \<sigma> (mx)\<close> augments the priority grammar and
1.1410 +  the pretty printer table for the given print mode (default \<^verbatim>\<open>""\<close>). An
1.1411 +  optional keyword @{keyword_ref "output"} means that only the pretty printer
1.1412 +  table is affected.
1.1413
1.1414 -  Following \secref{sec:mixfix}, the mixfix annotation \<open>mx =
1.1415 -  template ps q\<close> together with type \<open>\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> and
1.1416 -  specify a grammar production.  The \<open>template\<close> contains
1.1417 -  delimiter tokens that surround \<open>n\<close> argument positions
1.1418 -  (\<^verbatim>\<open>_\<close>).  The latter correspond to nonterminal symbols
1.1419 -  \<open>A\<^sub>i\<close> derived from the argument types \<open>\<tau>\<^sub>i\<close> as
1.1420 -  follows:
1.1421 +  Following \secref{sec:mixfix}, the mixfix annotation \<open>mx = template ps q\<close>
1.1422 +  together with type \<open>\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> and specify a grammar production.
1.1423 +  The \<open>template\<close> contains delimiter tokens that surround \<open>n\<close> argument
1.1424 +  positions (\<^verbatim>\<open>_\<close>). The latter correspond to nonterminal symbols \<open>A\<^sub>i\<close> derived
1.1425 +  from the argument types \<open>\<tau>\<^sub>i\<close> as follows:
1.1426
1.1427      \<^item> \<open>prop\<close> if \<open>\<tau>\<^sub>i = prop\<close>
1.1428
1.1429 -    \<^item> \<open>logic\<close> if \<open>\<tau>\<^sub>i = (\<dots>)\<kappa>\<close> for logical type
1.1430 -    constructor \<open>\<kappa> \<noteq> prop\<close>
1.1431 +    \<^item> \<open>logic\<close> if \<open>\<tau>\<^sub>i = (\<dots>)\<kappa>\<close> for logical type constructor \<open>\<kappa> \<noteq> prop\<close>
1.1432
1.1433      \<^item> \<open>any\<close> if \<open>\<tau>\<^sub>i = \<alpha>\<close> for type variables
1.1434
1.1435 -    \<^item> \<open>\<kappa>\<close> if \<open>\<tau>\<^sub>i = \<kappa>\<close> for nonterminal \<open>\<kappa>\<close>
1.1436 -    (syntactic type constructor)
1.1437 +    \<^item> \<open>\<kappa>\<close> if \<open>\<tau>\<^sub>i = \<kappa>\<close> for nonterminal \<open>\<kappa>\<close> (syntactic type constructor)
1.1438
1.1439 -  Each \<open>A\<^sub>i\<close> is decorated by priority \<open>p\<^sub>i\<close> from the
1.1440 -  given list \<open>ps\<close>; missing priorities default to 0.
1.1441 +  Each \<open>A\<^sub>i\<close> is decorated by priority \<open>p\<^sub>i\<close> from the given list \<open>ps\<close>; missing
1.1442 +  priorities default to 0.
1.1443
1.1444 -  The resulting nonterminal of the production is determined similarly
1.1445 -  from type \<open>\<tau>\<close>, with priority \<open>q\<close> and default 1000.
1.1446 +  The resulting nonterminal of the production is determined similarly from
1.1447 +  type \<open>\<tau>\<close>, with priority \<open>q\<close> and default 1000.
1.1448
1.1449    \<^medskip>
1.1450 -  Parsing via this production produces parse trees \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> for the argument slots.  The resulting parse tree is
1.1451 -  composed as \<open>c t\<^sub>1 \<dots> t\<^sub>n\<close>, by using the syntax constant \<open>c\<close> of the syntax declaration.
1.1452 +  Parsing via this production produces parse trees \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> for the
1.1453 +  argument slots. The resulting parse tree is composed as \<open>c t\<^sub>1 \<dots> t\<^sub>n\<close>, by
1.1454 +  using the syntax constant \<open>c\<close> of the syntax declaration.
1.1455
1.1456 -  Such syntactic constants are invented on the spot, without formal
1.1457 -  check wrt.\ existing declarations.  It is conventional to use plain
1.1458 -  identifiers prefixed by a single underscore (e.g.\ \<open>_foobar\<close>).  Names should be chosen with care, to avoid clashes
1.1459 -  with other syntax declarations.
1.1460 +  Such syntactic constants are invented on the spot, without formal check
1.1461 +  wrt.\ existing declarations. It is conventional to use plain identifiers
1.1462 +  prefixed by a single underscore (e.g.\ \<open>_foobar\<close>). Names should be chosen
1.1463 +  with care, to avoid clashes with other syntax declarations.
1.1464
1.1465    \<^medskip>
1.1466 -  The special case of copy production is specified by \<open>c =\<close>~\<^verbatim>\<open>""\<close> (empty string).
1.1467 -  It means that the resulting parse tree \<open>t\<close> is copied directly, without any
1.1468 -  further decoration.
1.1469 +  The special case of copy production is specified by \<open>c =\<close>~\<^verbatim>\<open>""\<close> (empty
1.1470 +  string). It means that the resulting parse tree \<open>t\<close> is copied directly,
1.1471 +  without any further decoration.
1.1472
1.1473 -  \<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar
1.1474 -  declarations (and translations) resulting from \<open>decls\<close>, which
1.1475 -  are interpreted in the same manner as for @{command "syntax"} above.
1.1476 +  \<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar declarations (and
1.1477 +  translations) resulting from \<open>decls\<close>, which are interpreted in the same
1.1478 +  manner as for @{command "syntax"} above.
1.1479 +
1.1480 +  \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic translation rules
1.1481 +  (i.e.\ macros) as first-order rewrite rules on ASTs (\secref{sec:ast}). The
1.1482 +  theory context maintains two independent lists translation rules: parse
1.1483 +  rules (\<^verbatim>\<open>=>\<close> or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>). For convenience, both
1.1484 +  can be specified simultaneously as parse~/ print rules (\<^verbatim>\<open>==\<close> or \<open>\<rightleftharpoons>\<close>).
1.1485
1.1486 -  \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic
1.1487 -  translation rules (i.e.\ macros) as first-order rewrite rules on
1.1488 -  ASTs (\secref{sec:ast}).  The theory context maintains two
1.1489 -  independent lists translation rules: parse rules (\<^verbatim>\<open>=>\<close>
1.1490 -  or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>).
1.1491 -  For convenience, both can be specified simultaneously as parse~/
1.1492 -  print rules (\<^verbatim>\<open>==\<close> or \<open>\<rightleftharpoons>\<close>).
1.1493 +  Translation patterns may be prefixed by the syntactic category to be used
1.1494 +  for parsing; the default is \<open>logic\<close> which means that regular term syntax is
1.1495 +  used. Both sides of the syntax translation rule undergo parsing and parse
1.1496 +  AST translations \secref{sec:tr-funs}, in order to perform some fundamental
1.1497 +  normalization like \<open>\<lambda>x y. b \<leadsto> \<lambda>x. \<lambda>y. b\<close>, but other AST translation rules
1.1498 +  are \<^emph>\<open>not\<close> applied recursively here.
1.1499
1.1500 -  Translation patterns may be prefixed by the syntactic category to be
1.1501 -  used for parsing; the default is \<open>logic\<close> which means that
1.1502 -  regular term syntax is used.  Both sides of the syntax translation
1.1503 -  rule undergo parsing and parse AST translations
1.1504 -  \secref{sec:tr-funs}, in order to perform some fundamental
1.1505 -  normalization like \<open>\<lambda>x y. b \<leadsto> \<lambda>x. \<lambda>y. b\<close>, but other AST
1.1506 -  translation rules are \<^emph>\<open>not\<close> applied recursively here.
1.1507 -
1.1508 -  When processing AST patterns, the inner syntax lexer runs in a
1.1510 -  This accommodates the usual naming convention for auxiliary syntax
1.1511 -  constants --- those that do not have a logical counter part --- by
1.1512 -  allowing to specify arbitrary AST applications within the term
1.1513 -  syntax, independently of the corresponding concrete syntax.
1.1514 +  When processing AST patterns, the inner syntax lexer runs in a different
1.1515 +  mode that allows identifiers to start with underscore. This accommodates the
1.1516 +  usual naming convention for auxiliary syntax constants --- those that do not
1.1517 +  have a logical counter part --- by allowing to specify arbitrary AST
1.1518 +  applications within the term syntax, independently of the corresponding
1.1519 +  concrete syntax.
1.1520
1.1521    Atomic ASTs are distinguished as @{ML Ast.Constant} versus @{ML
1.1522 -  Ast.Variable} as follows: a qualified name or syntax constant
1.1523 -  declared via @{command syntax}, or parse tree head of concrete
1.1524 -  notation becomes @{ML Ast.Constant}, anything else @{ML
1.1525 -  Ast.Variable}.  Note that \<open>CONST\<close> and \<open>XCONST\<close> within
1.1526 -  the term language (\secref{sec:pure-grammar}) allow to enforce
1.1527 -  treatment as constants.
1.1528 +  Ast.Variable} as follows: a qualified name or syntax constant declared via
1.1529 +  @{command syntax}, or parse tree head of concrete notation becomes @{ML
1.1530 +  Ast.Constant}, anything else @{ML Ast.Variable}. Note that \<open>CONST\<close> and
1.1531 +  \<open>XCONST\<close> within the term language (\secref{sec:pure-grammar}) allow to
1.1532 +  enforce treatment as constants.
1.1533
1.1534 -  AST rewrite rules \<open>(lhs, rhs)\<close> need to obey the following
1.1535 -  side-conditions:
1.1536 +  AST rewrite rules \<open>(lhs, rhs)\<close> need to obey the following side-conditions:
1.1537
1.1538 -    \<^item> Rules must be left linear: \<open>lhs\<close> must not contain
1.1539 -    repeated variables.\<^footnote>\<open>The deeper reason for this is that AST
1.1540 -    equality is not well-defined: different occurrences of the same''
1.1541 -    AST could be decorated differently by accidental type-constraints or
1.1542 -    source position information, for example.\<close>
1.1543 +    \<^item> Rules must be left linear: \<open>lhs\<close> must not contain repeated
1.1544 +    variables.\<^footnote>\<open>The deeper reason for this is that AST equality is not
1.1545 +    well-defined: different occurrences of the same'' AST could be decorated
1.1546 +    differently by accidental type-constraints or source position information,
1.1547 +    for example.\<close>
1.1548
1.1549      \<^item> Every variable in \<open>rhs\<close> must also occur in \<open>lhs\<close>.
1.1550
1.1551 -  \<^descr> @{command "no_translations"}~\<open>rules\<close> removes syntactic
1.1552 -  translation rules, which are interpreted in the same manner as for
1.1553 -  @{command "translations"} above.
1.1554 +  \<^descr> @{command "no_translations"}~\<open>rules\<close> removes syntactic translation rules,
1.1555 +  which are interpreted in the same manner as for @{command "translations"}
1.1556 +  above.
1.1557
1.1558 -  \<^descr> @{attribute syntax_ast_trace} and @{attribute
1.1559 -  syntax_ast_stats} control diagnostic output in the AST normalization
1.1560 -  process, when translation rules are applied to concrete input or
1.1561 -  output.
1.1562 +  \<^descr> @{attribute syntax_ast_trace} and @{attribute syntax_ast_stats} control
1.1563 +  diagnostic output in the AST normalization process, when translation rules
1.1564 +  are applied to concrete input or output.
1.1565
1.1566
1.1567 -  Raw syntax and translations provides a slightly more low-level
1.1568 -  access to the grammar and the form of resulting parse trees.  It is
1.1569 -  often possible to avoid this untyped macro mechanism, and use
1.1570 -  type-safe @{command abbreviation} or @{command notation} instead.
1.1571 -  Some important situations where @{command syntax} and @{command
1.1572 -  translations} are really need are as follows:
1.1573 +  Raw syntax and translations provides a slightly more low-level access to the
1.1574 +  grammar and the form of resulting parse trees. It is often possible to avoid
1.1575 +  this untyped macro mechanism, and use type-safe @{command abbreviation} or
1.1576 +  @{command notation} instead. Some important situations where @{command
1.1577 +  syntax} and @{command translations} are really need are as follows:
1.1578
1.1579 -  \<^item> Iterated replacement via recursive @{command translations}.
1.1580 -  For example, consider list enumeration @{term "[a, b, c, d]"} as
1.1581 -  defined in theory @{theory List} in Isabelle/HOL.
1.1582 +  \<^item> Iterated replacement via recursive @{command translations}. For example,
1.1583 +  consider list enumeration @{term "[a, b, c, d]"} as defined in theory
1.1584 +  @{theory List} in Isabelle/HOL.
1.1585
1.1586 -  \<^item> Change of binding status of variables: anything beyond the
1.1587 -  built-in @{keyword "binder"} mixfix annotation requires explicit
1.1588 -  syntax translations.  For example, consider list filter
1.1589 -  comprehension @{term "[x \<leftarrow> xs . P]"} as defined in theory @{theory
1.1590 -  List} in Isabelle/HOL.
1.1591 +  \<^item> Change of binding status of variables: anything beyond the built-in
1.1592 +  @{keyword "binder"} mixfix annotation requires explicit syntax translations.
1.1593 +  For example, consider list filter comprehension @{term "[x \<leftarrow> xs . P]"} as
1.1594 +  defined in theory @{theory List} in Isabelle/HOL.
1.1595  \<close>
1.1596
1.1597
1.1598  subsubsection \<open>Applying translation rules\<close>
1.1599
1.1600 -text \<open>As a term is being parsed or printed, an AST is generated as
1.1601 -  an intermediate form according to \figref{fig:parse-print}.  The AST
1.1602 -  is normalized by applying translation rules in the manner of a
1.1603 -  first-order term rewriting system.  We first examine how a single
1.1604 -  rule is applied.
1.1605 +text \<open>
1.1606 +  As a term is being parsed or printed, an AST is generated as an intermediate
1.1607 +  form according to \figref{fig:parse-print}. The AST is normalized by
1.1608 +  applying translation rules in the manner of a first-order term rewriting
1.1609 +  system. We first examine how a single rule is applied.
1.1610
1.1611 -  Let \<open>t\<close> be the abstract syntax tree to be normalized and
1.1612 -  \<open>(lhs, rhs)\<close> some translation rule.  A subtree \<open>u\<close>
1.1613 -  of \<open>t\<close> is called \<^emph>\<open>redex\<close> if it is an instance of \<open>lhs\<close>; in this case the pattern \<open>lhs\<close> is said to match the
1.1614 -  object \<open>u\<close>.  A redex matched by \<open>lhs\<close> may be
1.1615 -  replaced by the corresponding instance of \<open>rhs\<close>, thus
1.1616 -  \<^emph>\<open>rewriting\<close> the AST \<open>t\<close>.  Matching requires some notion
1.1617 -  of \<^emph>\<open>place-holders\<close> in rule patterns: @{ML Ast.Variable} serves
1.1618 -  this purpose.
1.1619 +  Let \<open>t\<close> be the abstract syntax tree to be normalized and \<open>(lhs, rhs)\<close> some
1.1620 +  translation rule. A subtree \<open>u\<close> of \<open>t\<close> is called \<^emph>\<open>redex\<close> if it is an
1.1621 +  instance of \<open>lhs\<close>; in this case the pattern \<open>lhs\<close> is said to match the
1.1622 +  object \<open>u\<close>. A redex matched by \<open>lhs\<close> may be replaced by the corresponding
1.1623 +  instance of \<open>rhs\<close>, thus \<^emph>\<open>rewriting\<close> the AST \<open>t\<close>. Matching requires some
1.1624 +  notion of \<^emph>\<open>place-holders\<close> in rule patterns: @{ML Ast.Variable} serves this
1.1625 +  purpose.
1.1626
1.1627 -  More precisely, the matching of the object \<open>u\<close> against the
1.1628 -  pattern \<open>lhs\<close> is performed as follows:
1.1629 +  More precisely, the matching of the object \<open>u\<close> against the pattern \<open>lhs\<close> is
1.1630 +  performed as follows:
1.1631
1.1632 -  \<^item> Objects of the form @{ML Ast.Variable}~\<open>x\<close> or @{ML
1.1633 -  Ast.Constant}~\<open>x\<close> are matched by pattern @{ML
1.1634 -  Ast.Constant}~\<open>x\<close>.  Thus all atomic ASTs in the object are
1.1635 -  treated as (potential) constants, and a successful match makes them
1.1637 -  \secref{sec:ast}).
1.1638 +    \<^item> Objects of the form @{ML Ast.Variable}~\<open>x\<close> or @{ML Ast.Constant}~\<open>x\<close> are
1.1639 +    matched by pattern @{ML Ast.Constant}~\<open>x\<close>. Thus all atomic ASTs in the
1.1640 +    object are treated as (potential) constants, and a successful match makes
1.1641 +    them actual constants even before name space resolution (see also
1.1642 +    \secref{sec:ast}).
1.1643
1.1644 -  \<^item> Object \<open>u\<close> is matched by pattern @{ML
1.1645 -  Ast.Variable}~\<open>x\<close>, binding \<open>x\<close> to \<open>u\<close>.
1.1646 +    \<^item> Object \<open>u\<close> is matched by pattern @{ML Ast.Variable}~\<open>x\<close>, binding \<open>x\<close> to
1.1647 +    \<open>u\<close>.
1.1648
1.1649 -  \<^item> Object @{ML Ast.Appl}~\<open>us\<close> is matched by @{ML
1.1650 -  Ast.Appl}~\<open>ts\<close> if \<open>us\<close> and \<open>ts\<close> have the
1.1651 -  same length and each corresponding subtree matches.
1.1652 +    \<^item> Object @{ML Ast.Appl}~\<open>us\<close> is matched by @{ML Ast.Appl}~\<open>ts\<close> if \<open>us\<close> and
1.1653 +    \<open>ts\<close> have the same length and each corresponding subtree matches.
1.1654
1.1655 -  \<^item> In every other case, matching fails.
1.1656 +    \<^item> In every other case, matching fails.
1.1657
1.1658 -
1.1659 -  A successful match yields a substitution that is applied to \<open>rhs\<close>, generating the instance that replaces \<open>u\<close>.
1.1660 +  A successful match yields a substitution that is applied to \<open>rhs\<close>,
1.1661 +  generating the instance that replaces \<open>u\<close>.
1.1662
1.1663 -  Normalizing an AST involves repeatedly applying translation rules
1.1664 -  until none are applicable.  This works yoyo-like: top-down,
1.1665 -  bottom-up, top-down, etc.  At each subtree position, rules are
1.1666 -  chosen in order of appearance in the theory definitions.
1.1667 +  Normalizing an AST involves repeatedly applying translation rules until none
1.1668 +  are applicable. This works yoyo-like: top-down, bottom-up, top-down, etc. At
1.1669 +  each subtree position, rules are chosen in order of appearance in the theory
1.1670 +  definitions.
1.1671
1.1672 -  The configuration options @{attribute syntax_ast_trace} and
1.1673 -  @{attribute syntax_ast_stats} might help to understand this process
1.1674 -  and diagnose problems.
1.1675 +  The configuration options @{attribute syntax_ast_trace} and @{attribute
1.1676 +  syntax_ast_stats} might help to understand this process and diagnose
1.1677 +  problems.
1.1678
1.1679    \begin{warn}
1.1680 -  If syntax translation rules work incorrectly, the output of
1.1681 -  @{command_ref print_syntax} with its \<^emph>\<open>rules\<close> sections reveals the
1.1682 -  actual internal forms of AST pattern, without potentially confusing
1.1683 -  concrete syntax.  Recall that AST constants appear as quoted strings
1.1684 -  and variables without quotes.
1.1685 +  If syntax translation rules work incorrectly, the output of @{command_ref
1.1686 +  print_syntax} with its \<^emph>\<open>rules\<close> sections reveals the actual internal forms
1.1687 +  of AST pattern, without potentially confusing concrete syntax. Recall that
1.1688 +  AST constants appear as quoted strings and variables without quotes.
1.1689    \end{warn}
1.1690
1.1691    \begin{warn}
1.1692 -  If @{attribute_ref eta_contract} is set to \<open>true\<close>, terms
1.1693 -  will be \<open>\<eta>\<close>-contracted \<^emph>\<open>before\<close> the AST rewriter sees
1.1694 -  them.  Thus some abstraction nodes needed for print rules to match
1.1695 -  may vanish.  For example, \<open>Ball A (\<lambda>x. P x)\<close> would contract
1.1696 -  to \<open>Ball A P\<close> and the standard print rule would fail to
1.1697 -  apply.  This problem can be avoided by hand-written ML translation
1.1698 -  functions (see also \secref{sec:tr-funs}), which is in fact the same
1.1699 -  mechanism used in built-in @{keyword "binder"} declarations.
1.1700 +  If @{attribute_ref eta_contract} is set to \<open>true\<close>, terms will be
1.1701 +  \<open>\<eta>\<close>-contracted \<^emph>\<open>before\<close> the AST rewriter sees them. Thus some abstraction
1.1702 +  nodes needed for print rules to match may vanish. For example, \<open>Ball A (\<lambda>x.
1.1703 +  P x)\<close> would contract to \<open>Ball A P\<close> and the standard print rule would fail to
1.1704 +  apply. This problem can be avoided by hand-written ML translation functions
1.1705 +  (see also \secref{sec:tr-funs}), which is in fact the same mechanism used in
1.1706 +  built-in @{keyword "binder"} declarations.
1.1707    \end{warn}
1.1708  \<close>
1.1709
1.1710 @@ -1347,10 +1277,9 @@
1.1711     @@{ML_antiquotation syntax_const}) name
1.1712    \<close>}
1.1713
1.1714 -  \<^descr> @{command parse_translation} etc. declare syntax translation
1.1715 -  functions to the theory.  Any of these commands have a single
1.1716 -  @{syntax text} argument that refers to an ML expression of
1.1717 -  appropriate type as follows:
1.1718 +  \<^descr> @{command parse_translation} etc. declare syntax translation functions to
1.1719 +  the theory. Any of these commands have a single @{syntax text} argument that
1.1720 +  refers to an ML expression of appropriate type as follows:
1.1721
1.1722    \<^medskip>
1.1723    {\footnotesize
1.1724 @@ -1368,110 +1297,108 @@
1.1725    \end{tabular}}
1.1726    \<^medskip>
1.1727
1.1728 -  The argument list consists of \<open>(c, tr)\<close> pairs, where \<open>c\<close> is the syntax name of the formal entity involved, and \<open>tr\<close> a function that translates a syntax form \<open>c args\<close> into
1.1729 -  \<open>tr ctxt args\<close> (depending on the context).  The Isabelle/ML
1.1730 -  naming convention for parse translations is \<open>c_tr\<close> and for
1.1731 -  print translations \<open>c_tr'\<close>.
1.1732 +  The argument list consists of \<open>(c, tr)\<close> pairs, where \<open>c\<close> is the syntax name
1.1733 +  of the formal entity involved, and \<open>tr\<close> a function that translates a syntax
1.1734 +  form \<open>c args\<close> into \<open>tr ctxt args\<close> (depending on the context). The
1.1735 +  Isabelle/ML naming convention for parse translations is \<open>c_tr\<close> and for print
1.1736 +  translations \<open>c_tr'\<close>.
1.1737
1.1738    The @{command_ref print_syntax} command displays the sets of names
1.1739 -  associated with the translation functions of a theory under \<open>parse_ast_translation\<close> etc.
1.1740 +  associated with the translation functions of a theory under
1.1741 +  \<open>parse_ast_translation\<close> etc.
1.1742
1.1743 -  \<^descr> \<open>@{class_syntax c}\<close>, \<open>@{type_syntax c}\<close>,
1.1744 -  \<open>@{const_syntax c}\<close> inline the authentic syntax name of the
1.1745 -  given formal entities into the ML source.  This is the
1.1746 -  fully-qualified logical name prefixed by a special marker to
1.1747 -  indicate its kind: thus different logical name spaces are properly
1.1748 -  distinguished within parse trees.
1.1749 +  \<^descr> \<open>@{class_syntax c}\<close>, \<open>@{type_syntax c}\<close>, \<open>@{const_syntax c}\<close> inline the
1.1750 +  authentic syntax name of the given formal entities into the ML source. This
1.1751 +  is the fully-qualified logical name prefixed by a special marker to indicate
1.1752 +  its kind: thus different logical name spaces are properly distinguished
1.1753 +  within parse trees.
1.1754
1.1755 -  \<^descr> \<open>@{const_syntax c}\<close> inlines the name \<open>c\<close> of
1.1756 -  the given syntax constant, having checked that it has been declared
1.1757 -  via some @{command syntax} commands within the theory context.  Note
1.1758 -  that the usual naming convention makes syntax constants start with
1.1759 -  underscore, to reduce the chance of accidental clashes with other
1.1760 -  names occurring in parse trees (unqualified constants etc.).
1.1761 +  \<^descr> \<open>@{const_syntax c}\<close> inlines the name \<open>c\<close> of the given syntax constant,
1.1762 +  having checked that it has been declared via some @{command syntax} commands
1.1763 +  within the theory context. Note that the usual naming convention makes
1.1764 +  syntax constants start with underscore, to reduce the chance of accidental
1.1765 +  clashes with other names occurring in parse trees (unqualified constants
1.1766 +  etc.).
1.1767  \<close>
1.1768
1.1769
1.1770  subsubsection \<open>The translation strategy\<close>
1.1771
1.1772 -text \<open>The different kinds of translation functions are invoked during
1.1773 -  the transformations between parse trees, ASTs and syntactic terms
1.1774 -  (cf.\ \figref{fig:parse-print}).  Whenever a combination of the form
1.1775 -  \<open>c x\<^sub>1 \<dots> x\<^sub>n\<close> is encountered, and a translation function
1.1776 -  \<open>f\<close> of appropriate kind is declared for \<open>c\<close>, the
1.1777 -  result is produced by evaluation of \<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> in ML.
1.1778 +text \<open>
1.1779 +  The different kinds of translation functions are invoked during the
1.1780 +  transformations between parse trees, ASTs and syntactic terms (cf.\
1.1781 +  \figref{fig:parse-print}). Whenever a combination of the form \<open>c x\<^sub>1 \<dots> x\<^sub>n\<close>
1.1782 +  is encountered, and a translation function \<open>f\<close> of appropriate kind is
1.1783 +  declared for \<open>c\<close>, the result is produced by evaluation of \<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close>
1.1784 +  in ML.
1.1785
1.1786 -  For AST translations, the arguments \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> are ASTs.  A
1.1787 -  combination has the form @{ML "Ast.Constant"}~\<open>c\<close> or @{ML
1.1788 -  "Ast.Appl"}~\<open>[\<close>@{ML Ast.Constant}~\<open>c, x\<^sub>1, \<dots>, x\<^sub>n]\<close>.
1.1789 -  For term translations, the arguments are terms and a combination has
1.1790 -  the form @{ML Const}~\<open>(c, \<tau>)\<close> or @{ML Const}~\<open>(c, \<tau>)
1.1791 -  $x\<^sub>1$ \<dots> $x\<^sub>n\<close>. Terms allow more sophisticated transformations 1.1792 - than ASTs do, typically involving abstractions and bound 1.1793 - variables. \<^emph>\<open>Typed\<close> print translations may even peek at the type 1.1794 - \<open>\<tau>\<close> of the constant they are invoked on, although some 1.1795 - information might have been suppressed for term output already. 1.1796 + For AST translations, the arguments \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> are ASTs. A combination 1.1797 + has the form @{ML "Ast.Constant"}~\<open>c\<close> or @{ML "Ast.Appl"}~\<open>[\<close>@{ML 1.1798 + Ast.Constant}~\<open>c, x\<^sub>1, \<dots>, x\<^sub>n]\<close>. For term translations, the arguments are 1.1799 + terms and a combination has the form @{ML Const}~\<open>(c, \<tau>)\<close> or @{ML 1.1800 + Const}~\<open>(c, \<tau>)$ x\<^sub>1 $\<dots>$ x\<^sub>n\<close>. Terms allow more sophisticated
1.1801 +  transformations than ASTs do, typically involving abstractions and bound
1.1802 +  variables. \<^emph>\<open>Typed\<close> print translations may even peek at the type \<open>\<tau>\<close> of the
1.1803 +  constant they are invoked on, although some information might have been
1.1804 +  suppressed for term output already.
1.1805
1.1806 -  Regardless of whether they act on ASTs or terms, translation
1.1807 -  functions called during the parsing process differ from those for
1.1808 -  printing in their overall behaviour:
1.1809 +  Regardless of whether they act on ASTs or terms, translation functions
1.1810 +  called during the parsing process differ from those for printing in their
1.1811 +  overall behaviour:
1.1812
1.1813 -  \<^descr>[Parse translations] are applied bottom-up.  The arguments are
1.1814 -  already in translated form.  The translations must not fail;
1.1815 -  exceptions trigger an error message.  There may be at most one
1.1816 -  function associated with any syntactic name.
1.1817 +    \<^descr>[Parse translations] are applied bottom-up. The arguments are already in
1.1818 +    translated form. The translations must not fail; exceptions trigger an
1.1819 +    error message. There may be at most one function associated with any
1.1820 +    syntactic name.
1.1821
1.1822 -  \<^descr>[Print translations] are applied top-down.  They are supplied
1.1823 -  with arguments that are partly still in internal form.  The result
1.1824 -  again undergoes translation; therefore a print translation should
1.1825 -  not introduce as head the very constant that invoked it.  The
1.1826 -  function may raise exception @{ML Match} to indicate failure; in
1.1827 -  this event it has no effect.  Multiple functions associated with
1.1828 -  some syntactic name are tried in the order of declaration in the
1.1829 -  theory.
1.1830 +    \<^descr>[Print translations] are applied top-down. They are supplied with
1.1831 +    arguments that are partly still in internal form. The result again
1.1832 +    undergoes translation; therefore a print translation should not introduce
1.1833 +    as head the very constant that invoked it. The function may raise
1.1834 +    exception @{ML Match} to indicate failure; in this event it has no effect.
1.1835 +    Multiple functions associated with some syntactic name are tried in the
1.1836 +    order of declaration in the theory.
1.1837
1.1838 -
1.1839 -  Only constant atoms --- constructor @{ML Ast.Constant} for ASTs and
1.1840 -  @{ML Const} for terms --- can invoke translation functions.  This
1.1841 -  means that parse translations can only be associated with parse tree
1.1842 -  heads of concrete syntax, or syntactic constants introduced via
1.1843 -  other translations.  For plain identifiers within the term language,
1.1844 -  the status of constant versus variable is not yet know during
1.1845 -  parsing.  This is in contrast to print translations, where constants
1.1846 -  are explicitly known from the given term in its fully internal form.
1.1847 +  Only constant atoms --- constructor @{ML Ast.Constant} for ASTs and @{ML
1.1848 +  Const} for terms --- can invoke translation functions. This means that parse
1.1849 +  translations can only be associated with parse tree heads of concrete
1.1850 +  syntax, or syntactic constants introduced via other translations. For plain
1.1851 +  identifiers within the term language, the status of constant versus variable
1.1852 +  is not yet know during parsing. This is in contrast to print translations,
1.1853 +  where constants are explicitly known from the given term in its fully
1.1854 +  internal form.
1.1855  \<close>
1.1856
1.1857
1.1858  subsection \<open>Built-in syntax transformations\<close>
1.1859
1.1860  text \<open>
1.1861 -  Here are some further details of the main syntax transformation
1.1862 -  phases of \figref{fig:parse-print}.
1.1863 +  Here are some further details of the main syntax transformation phases of
1.1864 +  \figref{fig:parse-print}.
1.1865  \<close>
1.1866
1.1867
1.1868  subsubsection \<open>Transforming parse trees to ASTs\<close>
1.1869
1.1870 -text \<open>The parse tree is the raw output of the parser.  It is
1.1871 -  transformed into an AST according to some basic scheme that may be
1.1872 -  augmented by AST translation functions as explained in
1.1873 -  \secref{sec:tr-funs}.
1.1874 +text \<open>
1.1875 +  The parse tree is the raw output of the parser. It is transformed into an
1.1876 +  AST according to some basic scheme that may be augmented by AST translation
1.1877 +  functions as explained in \secref{sec:tr-funs}.
1.1878
1.1879    The parse tree is constructed by nesting the right-hand sides of the
1.1880 -  productions used to recognize the input.  Such parse trees are
1.1881 -  simply lists of tokens and constituent parse trees, the latter
1.1882 -  representing the nonterminals of the productions.  Ignoring AST
1.1883 -  translation functions, parse trees are transformed to ASTs by
1.1884 -  stripping out delimiters and copy productions, while retaining some
1.1885 -  source position information from input tokens.
1.1886 +  productions used to recognize the input. Such parse trees are simply lists
1.1887 +  of tokens and constituent parse trees, the latter representing the
1.1888 +  nonterminals of the productions. Ignoring AST translation functions, parse
1.1889 +  trees are transformed to ASTs by stripping out delimiters and copy
1.1890 +  productions, while retaining some source position information from input
1.1891 +  tokens.
1.1892
1.1893 -  The Pure syntax provides predefined AST translations to make the
1.1894 -  basic \<open>\<lambda>\<close>-term structure more apparent within the
1.1895 -  (first-order) AST representation, and thus facilitate the use of
1.1897 -  covers ordinary term application, type application, nested
1.1898 -  abstraction, iterated meta implications and function types.  The
1.1899 -  effect is illustrated on some representative input strings is as
1.1900 +  The Pure syntax provides predefined AST translations to make the basic
1.1901 +  \<open>\<lambda>\<close>-term structure more apparent within the (first-order) AST
1.1902 +  representation, and thus facilitate the use of @{command translations} (see
1.1903 +  also \secref{sec:syn-trans}). This covers ordinary term application, type
1.1904 +  application, nested abstraction, iterated meta implications and function
1.1905 +  types. The effect is illustrated on some representative input strings is as
1.1906    follows:
1.1907
1.1908    \begin{center}
1.1909 @@ -1489,85 +1416,83 @@
1.1910    \end{center}
1.1911
1.1912    Note that type and sort constraints may occur in further places ---
1.1913 -  translations need to be ready to cope with them.  The built-in
1.1914 -  syntax transformation from parse trees to ASTs insert additional
1.1915 -  constraints that represent source positions.
1.1916 +  translations need to be ready to cope with them. The built-in syntax
1.1917 +  transformation from parse trees to ASTs insert additional constraints that
1.1918 +  represent source positions.
1.1919  \<close>
1.1920
1.1921
1.1922  subsubsection \<open>Transforming ASTs to terms\<close>
1.1923
1.1924 -text \<open>After application of macros (\secref{sec:syn-trans}), the AST
1.1925 -  is transformed into a term.  This term still lacks proper type
1.1926 -  information, but it might contain some constraints consisting of
1.1927 -  applications with head \<^verbatim>\<open>_constrain\<close>, where the second
1.1928 -  argument is a type encoded as a pre-term within the syntax.  Type
1.1929 -  inference later introduces correct types, or indicates type errors
1.1930 -  in the input.
1.1931 +text \<open>
1.1932 +  After application of macros (\secref{sec:syn-trans}), the AST is transformed
1.1933 +  into a term. This term still lacks proper type information, but it might
1.1934 +  contain some constraints consisting of applications with head \<^verbatim>\<open>_constrain\<close>,
1.1935 +  where the second argument is a type encoded as a pre-term within the syntax.
1.1936 +  Type inference later introduces correct types, or indicates type errors in
1.1937 +  the input.
1.1938
1.1939 -  Ignoring parse translations, ASTs are transformed to terms by
1.1940 -  mapping AST constants to term constants, AST variables to term
1.1941 -  variables or constants (according to the name space), and AST
1.1942 -  applications to iterated term applications.
1.1943 +  Ignoring parse translations, ASTs are transformed to terms by mapping AST
1.1944 +  constants to term constants, AST variables to term variables or constants
1.1945 +  (according to the name space), and AST applications to iterated term
1.1946 +  applications.
1.1947
1.1948 -  The outcome is still a first-order term.  Proper abstractions and
1.1949 -  bound variables are introduced by parse translations associated with
1.1950 -  certain syntax constants.  Thus \<^verbatim>\<open>("_abs" x x)\<close> eventually
1.1951 -  becomes a de-Bruijn term \<^verbatim>\<open>Abs ("x", _, Bound 0)\<close>.
1.1952 +  The outcome is still a first-order term. Proper abstractions and bound
1.1953 +  variables are introduced by parse translations associated with certain
1.1954 +  syntax constants. Thus \<^verbatim>\<open>("_abs" x x)\<close> eventually becomes a de-Bruijn term
1.1955 +  \<^verbatim>\<open>Abs ("x", _, Bound 0)\<close>.
1.1956  \<close>
1.1957
1.1958
1.1959  subsubsection \<open>Printing of terms\<close>
1.1960
1.1961 -text \<open>The output phase is essentially the inverse of the input
1.1962 -  phase.  Terms are translated via abstract syntax trees into
1.1963 -  pretty-printed text.
1.1964 +text \<open>
1.1965 +  The output phase is essentially the inverse of the input phase. Terms are
1.1966 +  translated via abstract syntax trees into pretty-printed text.
1.1967
1.1968    Ignoring print translations, the transformation maps term constants,
1.1969    variables and applications to the corresponding constructs on ASTs.
1.1970 -  Abstractions are mapped to applications of the special constant
1.1971 -  \<^verbatim>\<open>_abs\<close> as seen before.  Type constraints are represented
1.1972 -  via special \<^verbatim>\<open>_constrain\<close> forms, according to various
1.1973 -  policies of type annotation determined elsewhere.  Sort constraints
1.1974 -  of type variables are handled in a similar fashion.
1.1975 +  Abstractions are mapped to applications of the special constant \<^verbatim>\<open>_abs\<close> as
1.1976 +  seen before. Type constraints are represented via special \<^verbatim>\<open>_constrain\<close>
1.1977 +  forms, according to various policies of type annotation determined
1.1978 +  elsewhere. Sort constraints of type variables are handled in a similar
1.1979 +  fashion.
1.1980
1.1981 -  After application of macros (\secref{sec:syn-trans}), the AST is
1.1982 -  finally pretty-printed.  The built-in print AST translations reverse
1.1983 -  the corresponding parse AST translations.
1.1984 +  After application of macros (\secref{sec:syn-trans}), the AST is finally
1.1985 +  pretty-printed. The built-in print AST translations reverse the
1.1986 +  corresponding parse AST translations.
1.1987
1.1988    \<^medskip>
1.1989    For the actual printing process, the priority grammar
1.1990 -  (\secref{sec:priority-grammar}) plays a vital role: productions are
1.1991 -  used as templates for pretty printing, with argument slots stemming
1.1992 -  from nonterminals, and syntactic sugar stemming from literal tokens.
1.1993 +  (\secref{sec:priority-grammar}) plays a vital role: productions are used as
1.1994 +  templates for pretty printing, with argument slots stemming from
1.1995 +  nonterminals, and syntactic sugar stemming from literal tokens.
1.1996
1.1997 -  Each AST application with constant head \<open>c\<close> and arguments
1.1998 -  \<open>t\<^sub>1\<close>, \dots, \<open>t\<^sub>n\<close> (for \<open>n = 0\<close> the AST is
1.1999 -  just the constant \<open>c\<close> itself) is printed according to the
1.2000 -  first grammar production of result name \<open>c\<close>.  The required
1.2001 -  syntax priority of the argument slot is given by its nonterminal
1.2002 -  \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>.  The argument \<open>t\<^sub>i\<close> that corresponds to the
1.2003 -  position of \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is printed recursively, and then put in
1.2004 -  parentheses \<^emph>\<open>if\<close> its priority \<open>p\<close> requires this.  The
1.2005 -  resulting output is concatenated with the syntactic sugar according
1.2006 -  to the grammar production.
1.2007 +  Each AST application with constant head \<open>c\<close> and arguments \<open>t\<^sub>1\<close>, \dots,
1.2008 +  \<open>t\<^sub>n\<close> (for \<open>n = 0\<close> the AST is just the constant \<open>c\<close> itself) is printed
1.2009 +  according to the first grammar production of result name \<open>c\<close>. The required
1.2010 +  syntax priority of the argument slot is given by its nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>.
1.2011 +  The argument \<open>t\<^sub>i\<close> that corresponds to the position of \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is printed
1.2012 +  recursively, and then put in parentheses \<^emph>\<open>if\<close> its priority \<open>p\<close> requires
1.2013 +  this. The resulting output is concatenated with the syntactic sugar
1.2014 +  according to the grammar production.
1.2015
1.2016 -  If an AST application \<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> has more arguments than
1.2017 -  the corresponding production, it is first split into \<open>((c x\<^sub>1
1.2018 -  \<dots> x\<^sub>n) x\<^sub>n\<^sub>+\<^sub>1 \<dots> x\<^sub>m)\<close> and then printed recursively as above.
1.2019 +  If an AST application \<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> has more arguments than the
1.2020 +  corresponding production, it is first split into \<open>((c x\<^sub>1 \<dots> x\<^sub>n) x\<^sub>n\<^sub>+\<^sub>1 \<dots>
1.2021 +  x\<^sub>m)\<close> and then printed recursively as above.
1.2022
1.2023 -  Applications with too few arguments or with non-constant head or
1.2024 -  without a corresponding production are printed in prefix-form like
1.2025 -  \<open>f t\<^sub>1 \<dots> t\<^sub>n\<close> for terms.
1.2026 +  Applications with too few arguments or with non-constant head or without a
1.2027 +  corresponding production are printed in prefix-form like \<open>f t\<^sub>1 \<dots> t\<^sub>n\<close> for
1.2028 +  terms.
1.2029
1.2030 -  Multiple productions associated with some name \<open>c\<close> are tried
1.2031 -  in order of appearance within the grammar.  An occurrence of some
1.2032 -  AST variable \<open>x\<close> is printed as \<open>x\<close> outright.
1.2033 +  Multiple productions associated with some name \<open>c\<close> are tried in order of
1.2034 +  appearance within the grammar. An occurrence of some AST variable \<open>x\<close> is
1.2035 +  printed as \<open>x\<close> outright.
1.2036
1.2037    \<^medskip>
1.2038 -  White space is \<^emph>\<open>not\<close> inserted automatically.  If
1.2039 -  blanks (or breaks) are required to separate tokens, they need to be
1.2040 -  specified in the mixfix declaration (\secref{sec:mixfix}).
1.2041 +  White space is \<^emph>\<open>not\<close> inserted automatically. If blanks (or breaks) are
1.2042 +  required to separate tokens, they need to be specified in the mixfix
1.2043 +  declaration (\secref{sec:mixfix}).
1.2044  \<close>
1.2045
1.2046  end