doc-src/IsarRef/Thy/Inner_Syntax.thy
author wenzelm
Sun, 05 Feb 2012 21:00:38 +0100
changeset 46292 4eb48958b50f
parent 46291 a1827b8b45ae
child 46293 f248b5f2783a
permissions -rw-r--r--
updated section on raw syntax; misc tuning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     1
theory Inner_Syntax
42651
e3fdb7c96be5 formal Base theory;
wenzelm
parents: 42596
diff changeset
     2
imports Base Main
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     3
begin
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     4
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
     5
chapter {* Inner syntax --- the term language \label{ch:inner-syntax} *}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     6
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
     7
text {* The inner syntax of Isabelle provides concrete notation for
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
     8
  the main entities of the logical framework, notably @{text
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
     9
  "\<lambda>"}-terms with types and type classes.  Applications may either
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    10
  extend existing syntactic categories by additional notation, or
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    11
  define new sub-languages that are linked to the standard term
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    12
  language via some explicit markers.  For example @{verbatim
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    13
  FOO}~@{text "foo"} could embed the syntax corresponding for some
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    14
  user-defined nonterminal @{text "foo"} --- within the bounds of the
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    15
  given lexical syntax of Isabelle/Pure.
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    16
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    17
  The most basic way to specify concrete syntax for logical entities
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    18
  works via mixfix annotations (\secref{sec:mixfix}), which may be
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    19
  usually given as part of the original declaration or via explicit
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    20
  notation commands later on (\secref{sec:notation}).  This already
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    21
  covers many needs of concrete syntax without having to understand
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    22
  the full complexity of inner syntax layers.
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    23
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    24
  Further details of the syntax engine involves the classical
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    25
  distinction of lexical language versus context-free grammar (see
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    26
  \secref{sec:pure-syntax}), and various mechanisms for \emph{syntax
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    27
  translations} --- either as rewrite systems on first-order ASTs
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    28
  (\secref{sec:syn-trans}) or ML functions on ASTs or @{text
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    29
  "\<lambda>"}-terms that represent parse trees (\secref{sec:tr-funs}).
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    30
*}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    31
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
    32
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    33
section {* Printing logical entities *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    34
46284
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
    35
subsection {* Diagnostic commands \label{sec:print-diag} *}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    36
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    37
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    38
  \begin{matharray}{rcl}
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    39
    @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    40
    @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    41
    @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    42
    @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    43
    @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    44
    @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    45
    @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    46
  \end{matharray}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    47
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    48
  These diagnostic commands assist interactive development by printing
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    49
  internal logical entities in a human-readable fashion.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    50
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
    51
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
    52
    @@{command typ} @{syntax modes}? @{syntax type}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    53
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
    54
    @@{command term} @{syntax modes}? @{syntax term}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    55
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
    56
    @@{command prop} @{syntax modes}? @{syntax prop}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    57
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
    58
    @@{command thm} @{syntax modes}? @{syntax thmrefs}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    59
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
    60
    ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thmrefs}?
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    61
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
    62
    @@{command pr} @{syntax modes}? @{syntax nat}?
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    63
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    64
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
    65
    @{syntax_def modes}: '(' (@{syntax name} + ) ')'
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
    66
  "}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    67
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    68
  \begin{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    69
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    70
  \item @{command "typ"}~@{text \<tau>} reads and prints types of the
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    71
  meta-logic according to the current theory or proof context.
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    72
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    73
  \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    74
  read, type-check and print terms or propositions according to the
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    75
  current theory or proof context; the inferred type of @{text t} is
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    76
  output as well.  Note that these commands are also useful in
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    77
  inspecting the current environment of term abbreviations.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    78
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    79
  \item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    80
  theorems from the current theory or proof context.  Note that any
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    81
  attributes included in the theorem specifications are applied to a
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    82
  temporary context derived from the current theory or proof; the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    83
  result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    84
  \<dots>, a\<^sub>n"} do not have any permanent effect.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    85
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    86
  \item @{command "prf"} displays the (compact) proof term of the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    87
  current proof state (if present), or of the given theorems. Note
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    88
  that this requires proof terms to be switched on for the current
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    89
  object logic (see the ``Proof terms'' section of the Isabelle
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    90
  reference manual for information on how to do this).
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    91
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    92
  \item @{command "full_prf"} is like @{command "prf"}, but displays
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    93
  the full proof term, i.e.\ also displays information omitted in the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    94
  compact proof term, which is denoted by ``@{text _}'' placeholders
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    95
  there.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    96
39165
e790a5560834 discontinued obsolete ProofContext.prems_limit;
wenzelm
parents: 39137
diff changeset
    97
  \item @{command "pr"}~@{text "goals"} prints the current proof state
e790a5560834 discontinued obsolete ProofContext.prems_limit;
wenzelm
parents: 39137
diff changeset
    98
  (if present), including current facts and goals.  The optional limit
e790a5560834 discontinued obsolete ProofContext.prems_limit;
wenzelm
parents: 39137
diff changeset
    99
  arguments affect the number of goals to be displayed, which is
e790a5560834 discontinued obsolete ProofContext.prems_limit;
wenzelm
parents: 39137
diff changeset
   100
  initially 10.  Omitting limit value leaves the current setting
e790a5560834 discontinued obsolete ProofContext.prems_limit;
wenzelm
parents: 39137
diff changeset
   101
  unchanged.
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
   102
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   103
  \end{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   104
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   105
  All of the diagnostic commands above admit a list of @{text modes}
42926
a8b655d089ac tuned secref (still dangling);
wenzelm
parents: 42705
diff changeset
   106
  to be specified, which is appended to the current print mode; see
46284
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   107
  also \secref{sec:print-modes}.  Thus the output behavior may be
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   108
  modified according particular print mode features.  For example,
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   109
  @{command "pr"}~@{text "(latex xsymbols)"} would print the current
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   110
  proof state with mathematical symbols and special characters
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   111
  represented in {\LaTeX} source, according to the Isabelle style
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   112
  \cite{isabelle-sys}.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   113
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   114
  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   115
  systematic way to include formal items into the printed text
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   116
  document.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   117
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   118
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   119
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   120
subsection {* Details of printed content *}
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   121
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   122
text {*
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   123
  \begin{tabular}{rcll}
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   124
    @{attribute_def show_types} & : & @{text attribute} & default @{text false} \\
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   125
    @{attribute_def show_sorts} & : & @{text attribute} & default @{text false} \\
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   126
    @{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   127
    @{attribute_def show_abbrevs} & : & @{text attribute} & default @{text true} \\
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   128
    @{attribute_def show_brackets} & : & @{text attribute} & default @{text false} \\
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42655
diff changeset
   129
    @{attribute_def names_long} & : & @{text attribute} & default @{text false} \\
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42655
diff changeset
   130
    @{attribute_def names_short} & : & @{text attribute} & default @{text false} \\
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42655
diff changeset
   131
    @{attribute_def names_unique} & : & @{text attribute} & default @{text true} \\
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   132
    @{attribute_def eta_contract} & : & @{text attribute} & default @{text true} \\
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   133
    @{attribute_def goals_limit} & : & @{text attribute} & default @{text 10} \\
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   134
    @{attribute_def show_main_goal} & : & @{text attribute} & default @{text false} \\
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   135
    @{attribute_def show_hyps} & : & @{text attribute} & default @{text false} \\
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   136
    @{attribute_def show_tags} & : & @{text attribute} & default @{text false} \\
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   137
    @{attribute_def show_question_marks} & : & @{text attribute} & default @{text true} \\
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   138
  \end{tabular}
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   139
  \medskip
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   140
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   141
  These configuration options control the detail of information that
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   142
  is displayed for types, terms, theorems, goals etc.  See also
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   143
  \secref{sec:config}.
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   144
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   145
  \begin{description}
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   146
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   147
  \item @{attribute show_types} and @{attribute show_sorts} control
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   148
  printing of type constraints for term variables, and sort
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   149
  constraints for type variables.  By default, neither of these are
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   150
  shown in output.  If @{attribute show_sorts} is enabled, types are
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   151
  always shown as well.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   152
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   153
  Note that displaying types and sorts may explain why a polymorphic
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   154
  inference rule fails to resolve with some goal, or why a rewrite
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   155
  rule does not apply as expected.
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   156
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   157
  \item @{attribute show_consts} controls printing of types of
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   158
  constants when displaying a goal state.
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   159
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   160
  Note that the output can be enormous, because polymorphic constants
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   161
  often occur at several different type instances.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   162
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   163
  \item @{attribute show_abbrevs} controls folding of constant
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   164
  abbreviations.
40879
ca132ef44944 configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents: 40255
diff changeset
   165
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   166
  \item @{attribute show_brackets} controls bracketing in pretty
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   167
  printed output.  If enabled, all sub-expressions of the pretty
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   168
  printing tree will be parenthesized, even if this produces malformed
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   169
  term syntax!  This crude way of showing the internal structure of
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   170
  pretty printed entities may occasionally help to diagnose problems
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   171
  with operator priorities, for example.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   172
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42655
diff changeset
   173
  \item @{attribute names_long}, @{attribute names_short}, and
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42655
diff changeset
   174
  @{attribute names_unique} control the way of printing fully
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42279
diff changeset
   175
  qualified internal names in external form.  See also
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42279
diff changeset
   176
  \secref{sec:antiq} for the document antiquotation options of the
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42279
diff changeset
   177
  same names.
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42279
diff changeset
   178
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   179
  \item @{attribute eta_contract} controls @{text "\<eta>"}-contracted
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   180
  printing of terms.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   181
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   182
  The @{text \<eta>}-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"},
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   183
  provided @{text x} is not free in @{text f}.  It asserts
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   184
  \emph{extensionality} of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv>
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   185
  g x"} for all @{text x}.  Higher-order unification frequently puts
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   186
  terms into a fully @{text \<eta>}-expanded form.  For example, if @{text
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   187
  F} has type @{text "(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>"} then its expanded form is @{term
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   188
  "\<lambda>h. F (\<lambda>x. h x)"}.
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   189
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   190
  Enabling @{attribute eta_contract} makes Isabelle perform @{text
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   191
  \<eta>}-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"}
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   192
  appears simply as @{text F}.
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   193
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   194
  Note that the distinction between a term and its @{text \<eta>}-expanded
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   195
  form occasionally matters.  While higher-order resolution and
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   196
  rewriting operate modulo @{text "\<alpha>\<beta>\<eta>"}-conversion, some other tools
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   197
  might look at terms more discretely.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   198
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   199
  \item @{attribute goals_limit} controls the maximum number of
39130
12dac4b58df8 updated configuration options;
wenzelm
parents: 39050
diff changeset
   200
  subgoals to be shown in goal output.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   201
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   202
  \item @{attribute show_main_goal} controls whether the main result
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   203
  to be proven should be displayed.  This information might be
39130
12dac4b58df8 updated configuration options;
wenzelm
parents: 39050
diff changeset
   204
  relevant for schematic goals, to inspect the current claim that has
12dac4b58df8 updated configuration options;
wenzelm
parents: 39050
diff changeset
   205
  been synthesized so far.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   206
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   207
  \item @{attribute show_hyps} controls printing of implicit
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   208
  hypotheses of local facts.  Normally, only those hypotheses are
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   209
  displayed that are \emph{not} covered by the assumptions of the
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   210
  current context: this situation indicates a fault in some tool being
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   211
  used.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   212
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   213
  By enabling @{attribute show_hyps}, output of \emph{all} hypotheses
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   214
  can be enforced, which is occasionally useful for diagnostic
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   215
  purposes.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   216
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   217
  \item @{attribute show_tags} controls printing of extra annotations
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   218
  within theorems, such as internal position information, or the case
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   219
  names being attached by the attribute @{attribute case_names}.
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   220
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   221
  Note that the @{attribute tagged} and @{attribute untagged}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   222
  attributes provide low-level access to the collection of tags
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   223
  associated with a theorem.
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   224
42655
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   225
  \item @{attribute show_question_marks} controls printing of question
eb95e2f3b218 updated configuration options -- no ML here;
wenzelm
parents: 42651
diff changeset
   226
  marks for schematic variables, such as @{text ?x}.  Only the leading
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   227
  question mark is affected, the remaining text is unchanged
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   228
  (including proper markup for schematic variables that might be
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   229
  relevant for user interfaces).
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   230
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   231
  \end{description}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   232
*}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   233
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   234
46284
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   235
subsection {* Alternative print modes \label{sec:print-modes} *}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   236
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   237
text {*
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   238
  \begin{mldecls}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   239
    @{index_ML print_mode_value: "unit -> string list"} \\
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   240
    @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   241
  \end{mldecls}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   242
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   243
  The \emph{print mode} facility allows to modify various operations
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   244
  for printing.  Commands like @{command typ}, @{command term},
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   245
  @{command thm} (see \secref{sec:print-diag}) take additional print
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   246
  modes as optional argument.  The underlying ML operations are as
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   247
  follows.
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   248
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   249
  \begin{description}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   250
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   251
  \item @{ML "print_mode_value ()"} yields the list of currently
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   252
  active print mode names.  This should be understood as symbolic
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   253
  representation of certain individual features for printing (with
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   254
  precedence from left to right).
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   255
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   256
  \item @{ML Print_Mode.with_modes}~@{text "modes f x"} evaluates
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   257
  @{text "f x"} in an execution context where the print mode is
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   258
  prepended by the given @{text "modes"}.  This provides a thread-safe
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   259
  way to augment print modes.  It is also monotonic in the set of mode
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   260
  names: it retains the default print mode that certain
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   261
  user-interfaces might have installed for their proper functioning!
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   262
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   263
  \end{description}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   264
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   265
  \begin{warn}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   266
  The old global reference @{ML print_mode} should never be used
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   267
  directly in applications.  Its main reason for being publicly
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   268
  accessible is to support historic versions of Proof~General.
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   269
  \end{warn}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   270
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   271
  \medskip The pretty printer for inner syntax maintains alternative
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   272
  mixfix productions for any print mode name invented by the user, say
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   273
  in commands like @{command notation} or @{command abbreviation}.
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   274
  Mode names can be arbitrary, but the following ones have a specific
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   275
  meaning by convention:
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   276
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   277
  \begin{itemize}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   278
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   279
  \item @{verbatim "\"\""} (the empty string): default mode;
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   280
  implicitly active as last element in the list of modes.
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   281
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   282
  \item @{verbatim input}: dummy print mode that is never active; may
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   283
  be used to specify notation that is only available for input.
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   284
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   285
  \item @{verbatim internal} dummy print mode that is never active;
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   286
  used internally in Isabelle/Pure.
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   287
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   288
  \item @{verbatim xsymbols}: enable proper mathematical symbols
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   289
  instead of ASCII art.\footnote{This traditional mode name stems from
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   290
  the ``X-Symbol'' package for old versions Proof~General with XEmacs,
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   291
  although that package has been superseded by Unicode in recent
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   292
  years.}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   293
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   294
  \item @{verbatim HTML}: additional mode that is active in HTML
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   295
  presentation of Isabelle theory sources; allows to provide
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   296
  alternative output notation.
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   297
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   298
  \item @{verbatim latex}: additional mode that is active in {\LaTeX}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   299
  document preparation of Isabelle theory sources; allows to provide
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   300
  alternative output notation.
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   301
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   302
  \end{itemize}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   303
*}
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   304
6233d0b74d71 updated section on print modes;
wenzelm
parents: 46282
diff changeset
   305
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   306
subsection {* Printing limits *}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   307
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   308
text {*
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   309
  \begin{mldecls}
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36508
diff changeset
   310
    @{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   311
    @{index_ML print_depth: "int -> unit"} \\
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   312
  \end{mldecls}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   313
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   314
  These ML functions set limits for pretty printed text.
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   315
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   316
  \begin{description}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   317
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36508
diff changeset
   318
  \item @{ML Pretty.margin_default} indicates the global default for
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36508
diff changeset
   319
  the right margin of the built-in pretty printer, with initial value
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36508
diff changeset
   320
  76.  Note that user-interfaces typically control margins
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36508
diff changeset
   321
  automatically when resizing windows, or even bypass the formatting
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36508
diff changeset
   322
  engine of Isabelle/ML altogether and do it within the front end via
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36508
diff changeset
   323
  Isabelle/Scala.
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   324
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   325
  \item @{ML print_depth}~@{text n} limits the printing depth of the
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   326
  ML toplevel pretty printer; the precise effect depends on the ML
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   327
  compiler and run-time system.  Typically @{text n} should be less
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   328
  than 10.  Bigger values such as 100--1000 are useful for debugging.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   329
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   330
  \end{description}
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   331
*}
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   332
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   333
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   334
section {* Mixfix annotations \label{sec:mixfix} *}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   335
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   336
text {* Mixfix annotations specify concrete \emph{inner syntax} of
35351
7425aece4ee3 allow general mixfix syntax for type constructors;
wenzelm
parents: 32833
diff changeset
   337
  Isabelle types and terms.  Locally fixed parameters in toplevel
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   338
  theorem statements, locale and class specifications also admit
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   339
  mixfix annotations in a fairly uniform manner.  A mixfix annotation
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   340
  describes describes the concrete syntax, the translation to abstract
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   341
  syntax, and the pretty printing.  Special case annotations provide a
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   342
  simple means of specifying infix operators and binders.
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   343
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   344
  Isabelle mixfix syntax is inspired by {\OBJ} \cite{OBJ}.  It allows
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   345
  to specify any context-free priority grammar, which is more general
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   346
  than the fixity declarations of ML and Prolog.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   347
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
   348
  @{rail "
46289
wenzelm
parents: 46288
diff changeset
   349
    @{syntax_def mixfix}: '(' mfix ')'
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   350
    ;
46289
wenzelm
parents: 46288
diff changeset
   351
    @{syntax_def struct_mixfix}: '(' ( mfix | @'structure' ) ')'
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   352
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   353
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   354
    mfix: @{syntax template} prios? @{syntax nat}? |
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   355
      (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   356
      @'binder' @{syntax template} prios? @{syntax nat}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   357
    ;
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   358
    template: string
46289
wenzelm
parents: 46288
diff changeset
   359
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
   360
    prios: '[' (@{syntax nat} + ',') ']'
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
   361
  "}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   362
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   363
  The string given as @{text template} may include literal text,
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   364
  spacing, blocks, and arguments (denoted by ``@{text _}''); the
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   365
  special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   366
  represents an index argument that specifies an implicit structure
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   367
  reference (see also \secref{sec:locale}).  Infix and binder
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   368
  declarations provide common abbreviations for particular mixfix
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   369
  declarations.  So in practice, mixfix templates mostly degenerate to
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   370
  literal text for concrete syntax, such as ``@{verbatim "++"}'' for
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   371
  an infix symbol.
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   372
*}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   373
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   374
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   375
subsection {* The general mixfix form *}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   376
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   377
text {* In full generality, mixfix declarations work as follows.
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   378
  Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is annotated by
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   379
  @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text "mixfix"} is a string
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   380
  @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of delimiters that surround
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   381
  argument positions as indicated by underscores.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   382
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   383
  Altogether this determines a production for a context-free priority
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   384
  grammar, where for each argument @{text "i"} the syntactic category
46292
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   385
  is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and the
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   386
  result category is determined from @{text "\<tau>"} (with priority @{text
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   387
  "p"}).  Priority specifications are optional, with default 0 for
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   388
  arguments and 1000 for the result.\footnote{Omitting priorities is
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   389
  prone to syntactic ambiguities unless the delimiter tokens determine
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   390
  fully bracketed notation, as in @{text "if _ then _ else _ fi"}.}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   391
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   392
  Since @{text "\<tau>"} may be again a function type, the constant
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   393
  type scheme may have more argument positions than the mixfix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   394
  pattern.  Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   395
  @{text "m > n"} works by attaching concrete notation only to the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   396
  innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   397
  instead.  If a term has fewer arguments than specified in the mixfix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   398
  template, the concrete syntax is ignored.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   399
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   400
  \medskip A mixfix template may also contain additional directives
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   401
  for pretty printing, notably spaces, blocks, and breaks.  The
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   402
  general template format is a sequence over any of the following
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   403
  entities.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   404
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   405
  \begin{description}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   406
28771
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   407
  \item @{text "d"} is a delimiter, namely a non-empty sequence of
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   408
  characters other than the following special characters:
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   409
28771
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   410
  \smallskip
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   411
  \begin{tabular}{ll}
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   412
    @{verbatim "'"} & single quote \\
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   413
    @{verbatim "_"} & underscore \\
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   414
    @{text "\<index>"} & index symbol \\
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   415
    @{verbatim "("} & open parenthesis \\
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   416
    @{verbatim ")"} & close parenthesis \\
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   417
    @{verbatim "/"} & slash \\
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   418
  \end{tabular}
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   419
  \medskip
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   420
28771
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   421
  \item @{verbatim "'"} escapes the special meaning of these
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   422
  meta-characters, producing a literal version of the following
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   423
  character, unless that is a blank.
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   424
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   425
  A single quote followed by a blank separates delimiters, without
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   426
  affecting printing, but input tokens may have additional white space
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   427
  here.
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   428
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   429
  \item @{verbatim "_"} is an argument position, which stands for a
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   430
  certain syntactic category in the underlying grammar.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   431
28771
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   432
  \item @{text "\<index>"} is an indexed argument position; this is the place
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   433
  where implicit structure arguments can be attached.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   434
28771
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   435
  \item @{text "s"} is a non-empty sequence of spaces for printing.
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   436
  This and the following specifications do not affect parsing at all.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   437
28771
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   438
  \item @{verbatim "("}@{text n} opens a pretty printing block.  The
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   439
  optional number specifies how much indentation to add when a line
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   440
  break occurs within the block.  If the parenthesis is not followed
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   441
  by digits, the indentation defaults to 0.  A block specified via
28771
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   442
  @{verbatim "(00"} is unbreakable.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   443
28771
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   444
  \item @{verbatim ")"} closes a pretty printing block.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   445
28771
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   446
  \item @{verbatim "//"} forces a line break.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   447
28771
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   448
  \item @{verbatim "/"}@{text s} allows a line break.  Here @{text s}
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   449
  stands for the string of spaces (zero or more) right after the
4510201c6aaf mixfix annotations: verbatim for special symbols;
wenzelm
parents: 28770
diff changeset
   450
  slash.  These spaces are printed if the break is \emph{not} taken.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   451
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   452
  \end{description}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   453
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   454
  The general idea of pretty printing with blocks and breaks is also
46286
7233d0521c43 more refs;
wenzelm
parents: 46285
diff changeset
   455
  described in \cite{paulson-ml2}; it goes back to \cite{Oppen:1980}.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   456
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   457
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   458
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   459
subsection {* Infixes *}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   460
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   461
text {* Infix operators are specified by convenient short forms that
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   462
  abbreviate general mixfix annotations as follows:
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   463
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   464
  \begin{center}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   465
  \begin{tabular}{lll}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   466
46292
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   467
  @{verbatim "("}@{keyword_def "infix"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   468
  & @{text "\<mapsto>"} &
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   469
  @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
46292
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   470
  @{verbatim "("}@{keyword_def "infixl"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   471
  & @{text "\<mapsto>"} &
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   472
  @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
46292
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   473
  @{verbatim "("}@{keyword_def "infixr"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   474
  & @{text "\<mapsto>"} &
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   475
  @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   476
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   477
  \end{tabular}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   478
  \end{center}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   479
46292
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   480
  The mixfix template @{verbatim "\"(_ "}@{text sy}@{verbatim "/ _)\""}
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   481
  specifies two argument positions; the delimiter is preceded by a
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   482
  space and followed by a space or line break; the entire phrase is a
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   483
  pretty printing block.
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   484
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   485
  The alternative notation @{verbatim "op"}~@{text sy} is introduced
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   486
  in addition.  Thus any infix operator may be written in prefix form
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   487
  (as in ML), independently of the number of arguments in the term.
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   488
*}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   489
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   490
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   491
subsection {* Binders *}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   492
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   493
text {* A \emph{binder} is a variable-binding construct such as a
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   494
  quantifier.  The idea to formalize @{text "\<forall>x. b"} as @{text "All
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   495
  (\<lambda>x. b)"} for @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} already goes back
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   496
  to \cite{church40}.  Isabelle declarations of certain higher-order
46292
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   497
  operators may be annotated with @{keyword_def "binder"} annotations
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
   498
  as follows:
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   499
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   500
  \begin{center}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   501
  @{text "c :: "}@{verbatim "\""}@{text "(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\"  ("}@{keyword "binder"}@{verbatim " \""}@{text "sy"}@{verbatim "\" ["}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   502
  \end{center}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   503
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   504
  This introduces concrete binder syntax @{text "sy x. b"}, where
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   505
  @{text x} is a bound variable of type @{text "\<tau>\<^sub>1"}, the body @{text
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   506
  b} has type @{text "\<tau>\<^sub>2"} and the whole term has type @{text "\<tau>\<^sub>3"}.
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   507
  The optional integer @{text p} specifies the syntactic priority of
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   508
  the body; the default is @{text "q"}, which is also the priority of
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   509
  the whole construct.
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   510
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   511
  Internally, the binder syntax is expanded to something like this:
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   512
  \begin{center}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   513
  @{text "c_binder :: "}@{verbatim "\""}@{text "idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\"  (\"(3"}@{text sy}@{verbatim "_./ _)\" [0, "}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   514
  \end{center}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   515
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   516
  Here @{syntax (inner) idts} is the nonterminal symbol for a list of
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   517
  identifiers with optional type constraints (see also
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   518
  \secref{sec:pure-grammar}).  The mixfix template @{verbatim
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   519
  "\"(3"}@{text sy}@{verbatim "_./ _)\""} defines argument positions
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   520
  for the bound identifiers and the body, separated by a dot with
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   521
  optional line break; the entire phrase is a pretty printing block of
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   522
  indentation level 3.  Note that there is no extra space after @{text
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   523
  "sy"}, so it needs to be included user specification if the binder
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   524
  syntax ends with a token that may be continued by an identifier
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   525
  token at the start of @{syntax (inner) idts}.
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   526
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   527
  Furthermore, a syntax translation to transforms @{text "c_binder x\<^sub>1
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   528
  \<dots> x\<^sub>n b"} into iterated application @{text "c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)"}.
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   529
  This works in both directions, for parsing and printing.  *}
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   530
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   531
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   532
section {* Explicit notation \label{sec:notation} *}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   533
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   534
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   535
  \begin{matharray}{rcll}
35413
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   536
    @{command_def "type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   537
    @{command_def "no_type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   538
    @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   539
    @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
36508
03d2a2d0ee4a allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents: 35413
diff changeset
   540
    @{command_def "write"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   541
  \end{matharray}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   542
46288
8a2c5dc0b00e more on explicit notation;
wenzelm
parents: 46287
diff changeset
   543
  Commands that introduce new logical entities (terms or types)
8a2c5dc0b00e more on explicit notation;
wenzelm
parents: 46287
diff changeset
   544
  usually allow to provide mixfix annotations on the spot, which is
8a2c5dc0b00e more on explicit notation;
wenzelm
parents: 46287
diff changeset
   545
  convenient for default notation.  Nonetheless, the syntax may be
8a2c5dc0b00e more on explicit notation;
wenzelm
parents: 46287
diff changeset
   546
  modified later on by declarations for explicit notation.  This
8a2c5dc0b00e more on explicit notation;
wenzelm
parents: 46287
diff changeset
   547
  allows to add or delete mixfix annotations for of existing logical
8a2c5dc0b00e more on explicit notation;
wenzelm
parents: 46287
diff changeset
   548
  entities within the current context.
8a2c5dc0b00e more on explicit notation;
wenzelm
parents: 46287
diff changeset
   549
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
   550
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
   551
    (@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
   552
      @{syntax mode}? \\ (@{syntax nameref} @{syntax mixfix} + @'and')
35413
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   553
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
   554
    (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \\
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42669
diff changeset
   555
      (@{syntax nameref} @{syntax struct_mixfix} + @'and')
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   556
    ;
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42669
diff changeset
   557
    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax struct_mixfix} + @'and')
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
   558
  "}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   559
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   560
  \begin{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   561
35413
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   562
  \item @{command "type_notation"}~@{text "c (mx)"} associates mixfix
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   563
  syntax with an existing type constructor.  The arity of the
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   564
  constructor is retrieved from the context.
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   565
35413
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   566
  \item @{command "no_type_notation"} is similar to @{command
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   567
  "type_notation"}, but removes the specified syntax annotation from
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   568
  the present context.
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   569
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   570
  \item @{command "notation"}~@{text "c (mx)"} associates mixfix
35413
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   571
  syntax with an existing constant or fixed variable.  The type
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   572
  declaration of the given entity is retrieved from the context.
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   573
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   574
  \item @{command "no_notation"} is similar to @{command "notation"},
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   575
  but removes the specified syntax annotation from the present
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   576
  context.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   577
36508
03d2a2d0ee4a allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents: 35413
diff changeset
   578
  \item @{command "write"} is similar to @{command "notation"}, but
03d2a2d0ee4a allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents: 35413
diff changeset
   579
  works within an Isar proof body.
03d2a2d0ee4a allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents: 35413
diff changeset
   580
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   581
  \end{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   582
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   583
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   584
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   585
section {* The Pure syntax \label{sec:pure-syntax} *}
28769
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   586
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   587
subsection {* Lexical matters \label{sec:inner-lex} *}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   588
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   589
text {* The inner lexical syntax vaguely resembles the outer one
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   590
  (\secref{sec:outer-lex}), but some details are different.  There are
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   591
  two main categories of inner syntax tokens:
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   592
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   593
  \begin{enumerate}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   594
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   595
  \item \emph{delimiters} --- the literal tokens occurring in
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   596
  productions of the given priority grammar (cf.\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   597
  \secref{sec:priority-grammar});
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   598
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   599
  \item \emph{named tokens} --- various categories of identifiers etc.
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   600
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   601
  \end{enumerate}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   602
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   603
  Delimiters override named tokens and may thus render certain
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   604
  identifiers inaccessible.  Sometimes the logical context admits
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   605
  alternative ways to refer to the same entity, potentially via
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   606
  qualified names.
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   607
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   608
  \medskip The categories for named tokens are defined once and for
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   609
  all as follows, reusing some categories of the outer token syntax
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   610
  (\secref{sec:outer-lex}).
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   611
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   612
  \begin{center}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   613
  \begin{supertabular}{rcl}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   614
    @{syntax_def (inner) id} & = & @{syntax_ref ident} \\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   615
    @{syntax_def (inner) longid} & = & @{syntax_ref longident} \\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   616
    @{syntax_def (inner) var} & = & @{syntax_ref var} \\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   617
    @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   618
    @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   619
    @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   620
    @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   621
    @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   622
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   623
    @{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   624
  \end{supertabular}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   625
  \end{center}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   626
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   627
  The token categories @{syntax (inner) num_token}, @{syntax (inner)
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   628
  float_token}, @{syntax (inner) xnum_token}, and @{syntax (inner)
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   629
  xstr} are not used in Pure.  Object-logics may implement numerals
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   630
  and string constants by adding appropriate syntax declarations,
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   631
  together with some translation functions (e.g.\ see Isabelle/HOL).
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   632
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   633
  The derived categories @{syntax_def (inner) num_const}, @{syntax_def
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   634
  (inner) float_const}, and @{syntax_def (inner) num_const} provide
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   635
  robust access to the respective tokens: the syntax tree holds a
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   636
  syntactic constant instead of a free variable.
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   637
*}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   638
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   639
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   640
subsection {* Priority grammars \label{sec:priority-grammar} *}
28769
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   641
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   642
text {* A context-free grammar consists of a set of \emph{terminal
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   643
  symbols}, a set of \emph{nonterminal symbols} and a set of
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   644
  \emph{productions}.  Productions have the form @{text "A = \<gamma>"},
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   645
  where @{text A} is a nonterminal and @{text \<gamma>} is a string of
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   646
  terminals and nonterminals.  One designated nonterminal is called
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   647
  the \emph{root symbol}.  The language defined by the grammar
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   648
  consists of all strings of terminals that can be derived from the
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   649
  root symbol by applying productions as rewrite rules.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   650
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   651
  The standard Isabelle parser for inner syntax uses a \emph{priority
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   652
  grammar}.  Each nonterminal is decorated by an integer priority:
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   653
  @{text "A\<^sup>(\<^sup>p\<^sup>)"}.  In a derivation, @{text "A\<^sup>(\<^sup>p\<^sup>)"} may be rewritten
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   654
  using a production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} only if @{text "p \<le> q"}.  Any
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   655
  priority grammar can be translated into a normal context-free
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   656
  grammar by introducing new nonterminals and productions.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   657
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   658
  \medskip Formally, a set of context free productions @{text G}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   659
  induces a derivation relation @{text "\<longrightarrow>\<^sub>G"} as follows.  Let @{text
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   660
  \<alpha>} and @{text \<beta>} denote strings of terminal or nonterminal symbols.
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   661
  Then @{text "\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>"} holds if and only if @{text G}
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   662
  contains some production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} for @{text "p \<le> q"}.
28769
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   663
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   664
  \medskip The following grammar for arithmetic expressions
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   665
  demonstrates how binding power and associativity of operators can be
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   666
  enforced by priorities.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   667
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   668
  \begin{center}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   669
  \begin{tabular}{rclr}
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   670
  @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim "("} @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim ")"} \\
28769
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   671
  @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim 0} \\
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   672
  @{text "A\<^sup>(\<^sup>0\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} \\
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   673
  @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} \\
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   674
  @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "="} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} \\
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   675
  \end{tabular}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   676
  \end{center}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   677
  The choice of priorities determines that @{verbatim "-"} binds
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   678
  tighter than @{verbatim "*"}, which binds tighter than @{verbatim
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   679
  "+"}.  Furthermore @{verbatim "+"} associates to the left and
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   680
  @{verbatim "*"} to the right.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   681
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   682
  \medskip For clarity, grammars obey these conventions:
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   683
  \begin{itemize}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   684
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   685
  \item All priorities must lie between 0 and 1000.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   686
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   687
  \item Priority 0 on the right-hand side and priority 1000 on the
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   688
  left-hand side may be omitted.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   689
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   690
  \item The production @{text "A\<^sup>(\<^sup>p\<^sup>) = \<alpha>"} is written as @{text "A = \<alpha>
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   691
  (p)"}, i.e.\ the priority of the left-hand side actually appears in
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   692
  a column on the far right.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   693
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   694
  \item Alternatives are separated by @{text "|"}.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   695
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   696
  \item Repetition is indicated by dots @{text "(\<dots>)"} in an informal
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   697
  but obvious way.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   698
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   699
  \end{itemize}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   700
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   701
  Using these conventions, the example grammar specification above
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   702
  takes the form:
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   703
  \begin{center}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   704
  \begin{tabular}{rclc}
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   705
    @{text A} & @{text "="} & @{verbatim "("} @{text A} @{verbatim ")"} \\
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   706
              & @{text "|"} & @{verbatim 0} & \qquad\qquad \\
28769
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   707
              & @{text "|"} & @{text A} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} & @{text "(0)"} \\
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   708
              & @{text "|"} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   709
              & @{text "|"} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   710
  \end{tabular}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   711
  \end{center}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   712
*}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   713
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   714
46290
465851ba524e updated/unified section on mixfix annotations;
wenzelm
parents: 46289
diff changeset
   715
subsection {* The Pure grammar \label{sec:pure-grammar} *}
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   716
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   717
text {* The priority grammar of the @{text "Pure"} theory is defined
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   718
  approximately like this:
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   719
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   720
  \begin{center}
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   721
  \begin{supertabular}{rclr}
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   722
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   723
  @{syntax_def (inner) any} & = & @{text "prop  |  logic"} \\\\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   724
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   725
  @{syntax_def (inner) prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   726
    & @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   727
    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   728
    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28779
diff changeset
   729
    & @{text "|"} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   730
    & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   731
    & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   732
    & @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   733
    & @{text "|"} & @{text "\<lbrakk>"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{text "\<rbrakk>"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   734
    & @{text "|"} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   735
    & @{text "|"} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   736
    & @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   737
    & @{text "|"} & @{verbatim SORT_CONSTRAINT} @{verbatim "("} @{text type} @{verbatim ")"} \\
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28779
diff changeset
   738
    & @{text "|"} & @{verbatim TERM} @{text logic} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   739
    & @{text "|"} & @{verbatim PROP} @{text aprop} \\\\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   740
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28779
diff changeset
   741
  @{syntax_def (inner) aprop} & = & @{verbatim "("} @{text aprop} @{verbatim ")"} \\
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28779
diff changeset
   742
    & @{text "|"} & @{text "id  |  longid  |  var  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "..."} \\
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28779
diff changeset
   743
    & @{text "|"} & @{verbatim CONST} @{text "id  |  "}@{verbatim CONST} @{text "longid"} \\
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   744
    & @{text "|"} & @{verbatim XCONST} @{text "id  |  "}@{verbatim XCONST} @{text "longid"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   745
    & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\\\
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   746
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   747
  @{syntax_def (inner) logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   748
    & @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   749
    & @{text "|"} & @{text "id  |  longid  |  var  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "..."} \\
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 28779
diff changeset
   750
    & @{text "|"} & @{verbatim CONST} @{text "id  |  "}@{verbatim CONST} @{text "longid"} \\
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   751
    & @{text "|"} & @{verbatim XCONST} @{text "id  |  "}@{verbatim XCONST} @{text "longid"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   752
    & @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   753
    & @{text "|"} & @{text "\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} \\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   754
    & @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   755
    & @{text "|"} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   756
    & @{text "|"} & @{verbatim op} @{verbatim "=="}@{text "  |  "}@{verbatim op} @{text "\<equiv>"}@{text "  |  "}@{verbatim op} @{verbatim "&&&"} \\
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   757
    & @{text "|"} & @{verbatim op} @{verbatim "==>"}@{text "  |  "}@{verbatim op} @{text "\<Longrightarrow>"} \\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   758
    & @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   759
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   760
  @{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text "  |  id  |  "}@{verbatim "_"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   761
    & @{text "|"} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   762
    & @{text "|"} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   763
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   764
  @{syntax_def (inner) index} & = & @{verbatim "\<^bsub>"} @{text "logic\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "\<^esub>"}@{text "  |  |  \<index>"} \\\\
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   765
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   766
  @{syntax_def (inner) idts} & = & @{text "idt  |  idt\<^sup>(\<^sup>1\<^sup>) idts"} & @{text "(0)"} \\\\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   767
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   768
  @{syntax_def (inner) pttrn} & = & @{text idt} \\\\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   769
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   770
  @{syntax_def (inner) pttrns} & = & @{text "pttrn  |  pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} & @{text "(0)"} \\\\
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   771
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   772
  @{syntax_def (inner) type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   773
    & @{text "|"} & @{text "tid  |  tvar  |  "}@{verbatim "_"} \\
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   774
    & @{text "|"} & @{text "tid"} @{verbatim "::"} @{text "sort  |  tvar  "}@{verbatim "::"} @{text "sort  |  "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   775
    & @{text "|"} & @{text "type_name  |  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) type_name"} \\
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   776
    & @{text "|"} & @{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text type_name} \\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   777
    & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   778
    & @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   779
    & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   780
    & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   781
  @{syntax_def (inner) type_name} & = & @{text "id  |  longid"} \\\\
28772
3f6bc48ebb9b added Pure grammer (from old ref manual);
wenzelm
parents: 28771
diff changeset
   782
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   783
  @{syntax_def (inner) sort} & = & @{syntax class_name}~@{text "  |  "}@{verbatim "{}"} \\
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   784
    & @{text "|"} & @{verbatim "{"} @{syntax class_name} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{syntax class_name} @{verbatim "}"} \\
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   785
  @{syntax_def (inner) class_name} & = & @{text "id  |  longid"} \\
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   786
  \end{supertabular}
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   787
  \end{center}
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   788
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   789
  \medskip Here literal terminals are printed @{verbatim "verbatim"};
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   790
  see also \secref{sec:inner-lex} for further token categories of the
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   791
  inner syntax.  The meaning of the nonterminals defined by the above
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   792
  grammar is as follows:
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   793
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   794
  \begin{description}
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   795
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   796
  \item @{syntax_ref (inner) any} denotes any term.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   797
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   798
  \item @{syntax_ref (inner) prop} denotes meta-level propositions,
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   799
  which are terms of type @{typ prop}.  The syntax of such formulae of
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   800
  the meta-logic is carefully distinguished from usual conventions for
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   801
  object-logics.  In particular, plain @{text "\<lambda>"}-term notation is
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   802
  \emph{not} recognized as @{syntax (inner) prop}.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   803
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   804
  \item @{syntax_ref (inner) aprop} denotes atomic propositions, which
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   805
  are embedded into regular @{syntax (inner) prop} by means of an
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   806
  explicit @{verbatim PROP} token.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   807
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   808
  Terms of type @{typ prop} with non-constant head, e.g.\ a plain
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   809
  variable, are printed in this form.  Constants that yield type @{typ
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   810
  prop} are expected to provide their own concrete syntax; otherwise
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   811
  the printed version will appear like @{syntax (inner) logic} and
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   812
  cannot be parsed again as @{syntax (inner) prop}.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   813
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   814
  \item @{syntax_ref (inner) logic} denotes arbitrary terms of a
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   815
  logical type, excluding type @{typ prop}.  This is the main
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   816
  syntactic category of object-logic entities, covering plain @{text
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   817
  \<lambda>}-term notation (variables, abstraction, application), plus
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   818
  anything defined by the user.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   819
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   820
  When specifying notation for logical entities, all logical types
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   821
  (excluding @{typ prop}) are \emph{collapsed} to this single category
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   822
  of @{syntax (inner) logic}.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   823
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   824
  \item @{syntax_ref (inner) index} denotes an optional index term for
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   825
  indexed syntax.  If omitted, it refers to the first @{keyword
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   826
  "structure"} variable in the context.  The special dummy ``@{text
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   827
  "\<index>"}'' serves as pattern variable in mixfix annotations that
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   828
  introduce indexed notation.
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   829
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   830
  \item @{syntax_ref (inner) idt} denotes identifiers, possibly
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   831
  constrained by types.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   832
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   833
  \item @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   834
  (inner) idt}.  This is the most basic category for variables in
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   835
  iterated binders, such as @{text "\<lambda>"} or @{text "\<And>"}.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   836
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   837
  \item @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns}
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   838
  denote patterns for abstraction, cases bindings etc.  In Pure, these
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   839
  categories start as a merely copy of @{syntax (inner) idt} and
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   840
  @{syntax (inner) idts}, respectively.  Object-logics may add
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   841
  additional productions for binding forms.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   842
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   843
  \item @{syntax_ref (inner) type} denotes types of the meta-logic.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   844
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   845
  \item @{syntax_ref (inner) sort} denotes meta-level sorts.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   846
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   847
  \end{description}
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   848
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   849
  Here are some further explanations of certain syntax features.
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   850
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   851
  \begin{itemize}
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   852
28778
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   853
  \item In @{syntax (inner) idts}, note that @{text "x :: nat y"} is
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   854
  parsed as @{text "x :: (nat y)"}, treating @{text y} like a type
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   855
  constructor applied to @{text nat}.  To avoid this interpretation,
a25630deacaf misc tuning of inner syntax;
wenzelm
parents: 28777
diff changeset
   856
  write @{text "(x :: nat) y"} with explicit parentheses.
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   857
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   858
  \item Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x ::
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   859
  (nat y :: nat)"}.  The correct form is @{text "(x :: nat) (y ::
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   860
  nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   861
  sequence of identifiers.
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   862
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   863
  \item Type constraints for terms bind very weakly.  For example,
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   864
  @{text "x < y :: nat"} is normally parsed as @{text "(x < y) ::
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   865
  nat"}, unless @{text "<"} has a very low priority, in which case the
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   866
  input is likely to be ambiguous.  The correct form is @{text "x < (y
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   867
  :: nat)"}.
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   868
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   869
  \item Constraints may be either written with two literal colons
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   870
  ``@{verbatim "::"}'' or the double-colon symbol @{verbatim "\<Colon>"},
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   871
  which actually looks exactly the same in some {\LaTeX} styles.
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   872
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   873
  \item Dummy variables (written as underscore) may occur in different
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   874
  roles.
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   875
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   876
  \begin{description}
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   877
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   878
  \item A type ``@{text "_"}'' or ``@{text "_ :: sort"}'' acts like an
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   879
  anonymous inference parameter, which is filled-in according to the
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   880
  most general type produced by the type-checking phase.
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   881
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   882
  \item A bound ``@{text "_"}'' refers to a vacuous abstraction, where
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   883
  the body does not refer to the binding introduced here.  As in the
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   884
  term @{term "\<lambda>x _. x"}, which is @{text "\<alpha>"}-equivalent to @{text
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   885
  "\<lambda>x y. x"}.
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   886
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   887
  \item A free ``@{text "_"}'' refers to an implicit outer binding.
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   888
  Higher definitional packages usually allow forms like @{text "f x _
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   889
  = x"}.
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   890
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   891
  \item A schematic ``@{text "_"}'' (within a term pattern, see
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   892
  \secref{sec:term-decls}) refers to an anonymous variable that is
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   893
  implicitly abstracted over its context of locally bound variables.
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   894
  For example, this allows pattern matching of @{text "{x. f x = g
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   895
  x}"} against @{text "{x. _ = _}"}, or even @{text "{_. _ = _}"} by
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   896
  using both bound and schematic dummies.
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   897
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   898
  \end{description}
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   899
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   900
  \item The three literal dots ``@{verbatim "..."}'' may be also
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   901
  written as ellipsis symbol @{verbatim "\<dots>"}.  In both cases this
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   902
  refers to a special schematic variable, which is bound in the
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   903
  context.  This special term abbreviation works nicely with
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   904
  calculational reasoning (\secref{sec:calculation}).
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   905
46287
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   906
  \item @{verbatim CONST} ensures that the given identifier is treated
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   907
  as constant term, and passed through the parse tree in fully
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   908
  internalized form.  This is particularly relevant for translation
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   909
  rules (\secref{sec:syn-trans}), notably on the RHS.
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   910
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   911
  \item @{verbatim XCONST} is similar to @{verbatim CONST}, but
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   912
  retains the constant name as given.  This is only relevant to
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   913
  translation rules (\secref{sec:syn-trans}), notably on the LHS.
0bb3d8ee5d25 more accurate Pure grammar;
wenzelm
parents: 46286
diff changeset
   914
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28772
diff changeset
   915
  \end{itemize}
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   916
*}
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   917
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   918
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   919
subsection {* Inspecting the syntax *}
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   920
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   921
text {*
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   922
  \begin{matharray}{rcl}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   923
    @{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   924
  \end{matharray}
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   925
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   926
  \begin{description}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   927
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   928
  \item @{command "print_syntax"} prints the inner syntax of the
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   929
  current context.  The output can be quite large; the most important
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   930
  sections are explained below.
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   931
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   932
  \begin{description}
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   933
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   934
  \item @{text "lexicon"} lists the delimiters of the inner token
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   935
  language; see \secref{sec:inner-lex}.
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   936
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   937
  \item @{text "prods"} lists the productions of the underlying
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   938
  priority grammar; see \secref{sec:priority-grammar}.
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   939
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   940
  The nonterminal @{text "A\<^sup>(\<^sup>p\<^sup>)"} is rendered in plain text as @{text
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   941
  "A[p]"}; delimiters are quoted.  Many productions have an extra
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   942
  @{text "\<dots> => name"}.  These names later become the heads of parse
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   943
  trees; they also guide the pretty printer.
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   944
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   945
  Productions without such parse tree names are called \emph{copy
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   946
  productions}.  Their right-hand side must have exactly one
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   947
  nonterminal symbol (or named token).  The parser does not create a
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   948
  new parse tree node for copy productions, but simply returns the
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   949
  parse tree of the right-hand symbol.
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   950
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   951
  If the right-hand side of a copy production consists of a single
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   952
  nonterminal without any delimiters, then it is called a \emph{chain
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   953
  production}.  Chain productions act as abbreviations: conceptually,
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   954
  they are removed from the grammar by adding new productions.
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   955
  Priority information attached to chain productions is ignored; only
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   956
  the dummy value @{text "-1"} is displayed.
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   957
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   958
  \item @{text "print modes"} lists the alternative print modes
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   959
  provided by this grammar; see \secref{sec:print-modes}.
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   960
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   961
  \item @{text "parse_rules"} and @{text "print_rules"} relate to
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   962
  syntax translations (macros); see \secref{sec:syn-trans}.
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   963
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   964
  \item @{text "parse_ast_translation"} and @{text
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   965
  "print_ast_translation"} list sets of constants that invoke
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   966
  translation functions for abstract syntax trees, which are only
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   967
  required in very special situations; see \secref{sec:tr-funs}.
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   968
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   969
  \item @{text "parse_translation"} and @{text "print_translation"}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   970
  list the sets of constants that invoke regular translation
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   971
  functions; see \secref{sec:tr-funs}.
29157
461f34ed79ec added float_token, and num_const, float_const;
wenzelm
parents: 28856
diff changeset
   972
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   973
  \end{description}
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   974
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
   975
  \end{description}
28777
2eeeced17228 added inner lexical syntax, reusing outer one;
wenzelm
parents: 28774
diff changeset
   976
*}
28774
0e25ef17b06b more tuning of Pure grammer;
wenzelm
parents: 28773
diff changeset
   977
28770
93a372e2dc7a added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents: 28769
diff changeset
   978
46291
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   979
subsection {* Ambiguity of parsed expressions *}
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   980
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   981
text {*
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   982
  \begin{tabular}{rcll}
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   983
    @{attribute_def syntax_ambiguity_level} & : & @{text attribute} & default @{text 1} \\
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   984
  \end{tabular}
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   985
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   986
  \begin{mldecls}
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   987
    @{index_ML Syntax.ambiguity_limit: "int Config.T"} \\  %FIXME attribute
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   988
  \end{mldecls}
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   989
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   990
  Depending on the grammar and the given input, parsing may be
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   991
  ambiguous.  Isabelle lets the Earley parser enumerate all possible
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   992
  parse trees, and then tries to make the best out of the situation.
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   993
  Terms that cannot be type-checked are filtered out, which often
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   994
  leads to a unique result in the end.  Unlike regular type
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   995
  reconstruction, which is applied to the whole collection of input
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   996
  terms simultaneously, the filtering stage only treats each given
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   997
  term in isolation.  Filtering is also not attempted for individual
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   998
  types or raw ASTs (as required for @{command translations}).
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
   999
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1000
  Certain warning or error messages are printed, depending on the
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1001
  situation and the given configuration options.  Parsing ultimately
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1002
  fails, if multiple results remain after the filtering phase.
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1003
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1004
  \begin{description}
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1005
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1006
  \item @{attribute syntax_ambiguity_level} determines the number of
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1007
  parser results that are tolerated without printing a detailed
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1008
  message.
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1009
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1010
  \item @{ML Syntax.ambiguity_limit} determines the number of
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1011
  resulting parse trees that are shown as part of the printed message
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1012
  in case of an ambiguity.
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1013
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1014
  \end{description}
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1015
*}
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1016
a1827b8b45ae updated section about syntax ambiguity;
wenzelm
parents: 46290
diff changeset
  1017
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
  1018
section {* Raw syntax and translations \label{sec:syn-trans} *}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1019
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1020
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1021
  \begin{matharray}{rcl}
41229
d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents: 40879
diff changeset
  1022
    @{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1023
    @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1024
    @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1025
    @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1026
    @{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1027
  \end{matharray}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1028
46292
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1029
  Unlike mixfix notation for existing formal entities
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1030
  (\secref{sec:notation}), raw syntax declarations provide full access
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1031
  to the priority grammar of the inner syntax.  This includes
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1032
  additional syntactic categories (via @{command nonterminal}) and
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1033
  free-form grammar productions (via @{command syntax}).  Additional
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1034
  syntax translations (or macros, via @{command translations}) are
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1035
  required to turn resulting parse trees into proper representations
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1036
  of formal entities again.
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1037
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1038
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1039
    @@{command nonterminal} (@{syntax name} + @'and')
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1040
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1041
    (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (@{syntax constdecl} +)
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1042
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1043
    (@@{command translations} | @@{command no_translations})
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1044
      (transpat ('==' | '=>' | '<=' | '\<rightleftharpoons>' | '\<rightharpoonup>' | '\<leftharpoondown>') transpat +)
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1045
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1046
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1047
    mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1048
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1049
    transpat: ('(' @{syntax nameref} ')')? @{syntax string}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1050
  "}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1051
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1052
  \begin{description}
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
  1053
41229
d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents: 40879
diff changeset
  1054
  \item @{command "nonterminal"}~@{text c} declares a type
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1055
  constructor @{text c} (without arguments) to act as purely syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1056
  type: a nonterminal symbol of the inner syntax.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1057
46292
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1058
  \item @{command "syntax"}~@{text "(mode) c :: \<sigma> (mx)"} augments the
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1059
  priority grammar and the pretty printer table for the given print
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1060
  mode (default @{verbatim "\"\""}). An optional keyword @{keyword_ref
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1061
  "output"} means that only the pretty printer table is affected.
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1062
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1063
  Following \secref{sec:mixfix}, the mixfix annotation @{text "mx =
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1064
  template ps q"} together with type @{text "\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} and
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1065
  specify a grammar production.  The @{text template} contains
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1066
  delimiter tokens that surround @{text "n"} argument positions
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1067
  (@{verbatim "_"}).  The latter correspond to nonterminal symbols
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1068
  @{text "A\<^sub>i"} derived from the argument types @{text "\<tau>\<^sub>i"} as
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1069
  follows:
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1070
  \begin{itemize}
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1071
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1072
  \item @{text "prop"} if @{text "\<tau>\<^sub>i = prop"}
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1073
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1074
  \item @{text "logic"} if @{text "\<tau>\<^sub>i = (\<dots>)\<kappa>"} for logical type
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1075
  constructor @{text "\<kappa> \<noteq> prop"}
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1076
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1077
  \item @{text any} if @{text "\<tau>\<^sub>i = \<alpha>"} for type variables
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1078
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1079
  \item @{text "\<kappa>"} if @{text "\<tau>\<^sub>i = \<kappa>"} for nonterminal @{text "\<kappa>"}
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1080
  (syntactic type constructor)
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1081
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1082
  \end{itemize}
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1083
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1084
  Each @{text "A\<^sub>i"} is decorated by priority @{text "p\<^sub>i"} from the
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1085
  given list @{text "ps"}; misssing priorities default to 0.
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1086
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1087
  The resulting nonterminal of the production is determined similarly
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1088
  from type @{text "\<tau>"}, with priority @{text "q"} and default 1000.
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1089
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1090
  \medskip Parsing via this production produces parse trees @{text
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1091
  "t\<^sub>1, \<dots>, t\<^sub>n"} for the argument slots.  The resulting parse tree is
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1092
  composed as @{text "c t\<^sub>1 \<dots> t\<^sub>n"}, by using the syntax constant @{text
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1093
  "c"} of the syntax declaration.
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1094
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1095
  Such syntactic constants are invented on the spot, without formal
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1096
  check wrt.\ existing declarations.  It is conventional to use plain
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1097
  identifiers prefixed by a single underscore (e.g.\ @{text
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1098
  "_foobar"}).  Names should be chosen with care, to avoid clashes
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1099
  with unrelated syntax declarations.
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1100
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1101
  \medskip The special case of copy production is specified by @{text
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1102
  "c = "}@{verbatim "\"\""} (empty string).  It means that the
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1103
  resulting parse tree @{text "t"} is copied directly, without any
4eb48958b50f updated section on raw syntax;
wenzelm
parents: 46291
diff changeset
  1104
  further decoration.
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
  1105
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1106
  \item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1107
  declarations (and translations) resulting from @{text decls}, which
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1108
  are interpreted in the same manner as for @{command "syntax"} above.
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
  1109
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1110
  \item @{command "translations"}~@{text rules} specifies syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1111
  translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1112
  parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1113
  Translation patterns may be prefixed by the syntactic category to be
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1114
  used for parsing; the default is @{text logic}.
46282
83864b045a72 clarified syntax section structure;
wenzelm
parents: 45703
diff changeset
  1115
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1116
  \item @{command "no_translations"}~@{text rules} removes syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1117
  translation rules, which are interpreted in the same manner as for
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1118
  @{command "translations"} above.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1119
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1120
  \end{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1121
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1122
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1123
28779
698960f08652 separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents: 28778
diff changeset
  1124
section {* Syntax translation functions \label{sec:tr-funs} *}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1125
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1126
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1127
  \begin{matharray}{rcl}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1128
    @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1129
    @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1130
    @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1131
    @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1132
    @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1133
  \end{matharray}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1134
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1135
  @{rail "
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1136
  ( @@{command parse_ast_translation} | @@{command parse_translation} |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1137
    @@{command print_translation} | @@{command typed_print_translation} |
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1138
    @@{command print_ast_translation}) ('(' @'advanced' ')')? @{syntax text}
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1139
  "}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1140
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1141
  Syntax translation functions written in ML admit almost arbitrary
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1142
  manipulations of Isabelle's inner syntax.  Any of the above commands
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 42358
diff changeset
  1143
  have a single @{syntax text} argument that refers to an ML
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1144
  expression of appropriate type, which are as follows by default:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1145
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1146
%FIXME proper antiquotations
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1147
\begin{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1148
val parse_ast_translation   : (string * (ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1149
val parse_translation       : (string * (term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1150
val print_translation       : (string * (term list -> term)) list
42247
12fe41a92cd5 typed_print_translation: discontinued show_sorts argument;
wenzelm
parents: 41229
diff changeset
  1151
val typed_print_translation : (string * (typ -> term list -> term)) list
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1152
val print_ast_translation   : (string * (ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1153
\end{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1154
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1155
  If the @{text "(advanced)"} option is given, the corresponding
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1156
  translation functions may depend on the current theory or proof
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1157
  context.  This allows to implement advanced syntax mechanisms, as
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1158
  translations functions may refer to specific theory declarations or
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1159
  auxiliary proof data.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1160
30397
b6212ae21656 markup antiquotation options;
wenzelm
parents: 29741
diff changeset
  1161
  See also \cite{isabelle-ref} for more information on the general
b6212ae21656 markup antiquotation options;
wenzelm
parents: 29741
diff changeset
  1162
  concept of syntax transformations in Isabelle.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1163
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1164
%FIXME proper antiquotations
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1165
\begin{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1166
val parse_ast_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1167
  (string * (Proof.context -> ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1168
val parse_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1169
  (string * (Proof.context -> term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1170
val print_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1171
  (string * (Proof.context -> term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1172
val typed_print_translation:
42247
12fe41a92cd5 typed_print_translation: discontinued show_sorts argument;
wenzelm
parents: 41229
diff changeset
  1173
  (string * (Proof.context -> typ -> term list -> term)) list
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1174
val print_ast_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1175
  (string * (Proof.context -> ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1176
\end{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1177
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1178
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
  1179
end