doc-src/IsarRef/Thy/Inner_Syntax.thy
author wenzelm
Thu, 13 Nov 2008 21:54:51 +0100
changeset 28769 8fc228f21861
parent 28767 f09ceb800d00
child 28770 93a372e2dc7a
permissions -rw-r--r--
added section "Priority grammars" (variant from old ref manual);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     1
(* $Id$ *)
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     2
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     3
theory Inner_Syntax
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     4
imports Main
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     5
begin
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     6
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     7
chapter {* Inner syntax --- the term language *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     8
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
     9
section {* Printing logical entities *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    10
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    11
subsection {* Diagnostic commands *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    12
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    13
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    14
  \begin{matharray}{rcl}
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    15
    @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    16
    @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    17
    @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    18
    @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    19
    @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    20
    @{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
    21
    @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    22
  \end{matharray}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    23
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    24
  These diagnostic commands assist interactive development by printing
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    25
  internal logical entities in a human-readable fashion.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    26
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    27
  \begin{rail}
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    28
    'typ' modes? type
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    29
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    30
    'term' modes? term
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    31
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    32
    'prop' modes? prop
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    33
    ;
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    34
    'thm' modes? thmrefs
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    35
    ;
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    36
    ( 'prf' | 'full\_prf' ) modes? thmrefs?
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    37
    ;
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    38
    'pr' modes? nat? (',' nat)?
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    39
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    40
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    41
    modes: '(' (name + ) ')'
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    42
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    43
  \end{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    44
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    45
  \begin{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    46
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    47
  \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
    48
  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
    49
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    50
  \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
    51
  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
    52
  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
    53
  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
    54
  inspecting the current environment of term abbreviations.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    55
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    56
  \item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    57
  theorems from the current theory or proof context.  Note that any
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    58
  attributes included in the theorem specifications are applied to a
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    59
  temporary context derived from the current theory or proof; the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    60
  result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    61
  \<dots>, a\<^sub>n"} do not have any permanent effect.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    62
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    63
  \item @{command "prf"} displays the (compact) proof term of the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    64
  current proof state (if present), or of the given theorems. Note
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    65
  that this requires proof terms to be switched on for the current
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    66
  object logic (see the ``Proof terms'' section of the Isabelle
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    67
  reference manual for information on how to do this).
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    68
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    69
  \item @{command "full_prf"} is like @{command "prf"}, but displays
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    70
  the full proof term, i.e.\ also displays information omitted in the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    71
  compact proof term, which is denoted by ``@{text _}'' placeholders
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    72
  there.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    73
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    74
  \item @{command "pr"}~@{text "goals, prems"} prints the current
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    75
  proof state (if present), including the proof context, current facts
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    76
  and goals.  The optional limit arguments affect the number of goals
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    77
  and premises to be displayed, which is initially 10 for both.
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    78
  Omitting limit values leaves the current setting unchanged.
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
    79
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    80
  \end{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    81
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    82
  All of the diagnostic commands above admit a list of @{text modes}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    83
  to be specified, which is appended to the current print mode (see
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    84
  also \cite{isabelle-ref}).  Thus the output behavior may be modified
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    85
  according particular print mode features.  For example, @{command
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    86
  "pr"}~@{text "(latex xsymbols)"} would print the current proof state
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    87
  with mathematical symbols and special characters represented in
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    88
  {\LaTeX} source, according to the Isabelle style
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    89
  \cite{isabelle-sys}.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    90
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    91
  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    92
  systematic way to include formal items into the printed text
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    93
  document.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    94
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    95
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    96
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
    97
subsection {* Details of printed content *}
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
    98
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
    99
text {*
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   100
  \begin{mldecls} 
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   101
    @{index_ML show_types: "bool ref"} & default @{ML false} \\
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   102
    @{index_ML show_sorts: "bool ref"} & default @{ML false} \\
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   103
    @{index_ML show_consts: "bool ref"} & default @{ML false} \\
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   104
    @{index_ML long_names: "bool ref"} & default @{ML false} \\
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   105
    @{index_ML short_names: "bool ref"} & default @{ML false} \\
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   106
    @{index_ML unique_names: "bool ref"} & default @{ML true} \\
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   107
    @{index_ML show_brackets: "bool ref"} & default @{ML false} \\
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   108
    @{index_ML eta_contract: "bool ref"} & default @{ML true} \\
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   109
    @{index_ML goals_limit: "int ref"} & default @{ML 10} \\
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   110
    @{index_ML Proof.show_main_goal: "bool ref"} & default @{ML false} \\
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   111
    @{index_ML show_hyps: "bool ref"} & default @{ML false} \\
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   112
    @{index_ML show_tags: "bool ref"} & default @{ML false} \\
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   113
    @{index_ML show_question_marks: "bool ref"} & default @{ML true} \\
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   114
  \end{mldecls}
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   115
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   116
  These global ML variables control the detail of information that is
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   117
  displayed for types, terms, theorems, goals etc.
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   118
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   119
  In interactive sessions, the user interface usually manages these
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   120
  global parameters of the Isabelle process, even with some concept of
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   121
  persistence.  Nonetheless it is occasionally useful to manipulate ML
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   122
  variables directly, e.g.\ using @{command "ML_val"} or @{command
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   123
  "ML_command"}.
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   124
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   125
  Batch-mode logic sessions may be configured by putting appropriate
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   126
  ML text directly into the @{verbatim ROOT.ML} file.
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   127
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   128
  \begin{description}
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   129
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   130
  \item @{ML show_types} and @{ML show_sorts} control printing of type
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   131
  constraints for term variables, and sort constraints for type
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   132
  variables.  By default, neither of these are shown in output.  If
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   133
  @{ML show_sorts} is set to @{ML true}, types are always shown as
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   134
  well.
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   135
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   136
  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
   137
  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
   138
  rule does not apply as expected.
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   139
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   140
  \item @{ML show_consts} controls printing of types of constants when
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   141
  displaying a goal state.
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   142
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   143
  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
   144
  often occur at several different type instances.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   145
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   146
  \item @{ML long_names}, @{ML short_names}, and @{ML unique_names}
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   147
  control the way of printing fully qualified internal names in
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   148
  external form.  See also \secref{sec:antiq} for the document
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   149
  antiquotation options of the same names.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   150
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   151
  \item @{ML show_brackets} controls bracketing in pretty printed
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   152
  output.  If set to @{ML true}, all sub-expressions of the pretty
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   153
  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
   154
  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
   155
  pretty printed entities may occasionally help to diagnose problems
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   156
  with operator priorities, for example.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   157
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   158
  \item @{ML eta_contract} controls @{text "\<eta>"}-contracted printing of
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   159
  terms.
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   160
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   161
  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
   162
  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
   163
  \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
   164
  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
   165
  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
   166
  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
   167
  "\<lambda>h. F (\<lambda>x. h x)"}.
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   168
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   169
  Setting @{ML eta_contract} makes Isabelle perform @{text
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   170
  \<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
   171
  appears simply as @{text F}.
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   172
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   173
  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
   174
  form occasionally matters.  While higher-order resolution and
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   175
  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
   176
  might look at terms more discretely.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   177
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   178
  \item @{ML goals_limit} controls the maximum number of subgoals to
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   179
  be shown in goal output.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   180
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   181
  \item @{ML Proof.show_main_goal} controls whether the main result to
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   182
  be proven should be displayed.  This information might be relevant
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   183
  for schematic goals, to inspect the current claim that has been
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   184
  synthesized so far.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   185
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   186
  \item @{ML show_hyps} controls printing of implicit hypotheses of
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   187
  local facts.  Normally, only those hypotheses are displayed that are
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   188
  \emph{not} covered by the assumptions of the current context: this
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   189
  situation indicates a fault in some tool being used.
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   190
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   191
  By setting @{ML show_hyps} to @{ML true}, output of \emph{all}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   192
  hypotheses can be enforced, which is occasionally useful for
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   193
  diagnostic purposes.
28763
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   194
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   195
  \item @{ML show_tags} controls printing of extra annotations within
28765
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   196
  theorems, such as internal position information, or the case names
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   197
  being attached by the attribute @{attribute case_names}.
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   198
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   199
  Note that the @{attribute tagged} and @{attribute untagged}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   200
  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
   201
  associated with a theorem.
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   202
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   203
  \item @{ML show_question_marks} controls printing of question marks
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   204
  for schematic variables, such as @{text ?x}.  Only the leading
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   205
  question mark is affected, the remaining text is unchanged
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   206
  (including proper markup for schematic variables that might be
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   207
  relevant for user interfaces).
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   208
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   209
  \end{description}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   210
*}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   211
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   212
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   213
subsection {* Printing limits *}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   214
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   215
text {*
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   216
  \begin{mldecls}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   217
    @{index_ML Pretty.setdepth: "int -> unit"} \\
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   218
    @{index_ML Pretty.setmargin: "int -> unit"} \\
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   219
    @{index_ML print_depth: "int -> unit"} \\
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   220
  \end{mldecls}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   221
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   222
  These ML functions set limits for pretty printed text.
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   223
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   224
  \begin{description}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   225
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   226
  \item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   227
  limit the printing depth to @{text d}.  This affects the display of
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   228
  types, terms, theorems etc.  The default value is 0, which permits
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   229
  printing to an arbitrary depth.  Other useful values for @{text d}
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   230
  are 10 and 20.
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   231
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   232
  \item @{ML Pretty.setmargin}~@{text m} tells the pretty printer to
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   233
  assume a right margin (page width) of @{text m}.  The initial margin
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   234
  is 76, but user interfaces might adapt the margin automatically when
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   235
  resizing windows.
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   236
da8f6f4a74be misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28763
diff changeset
   237
  \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
   238
  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
   239
  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
   240
  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
   241
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   242
  \end{description}
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   243
*}
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   244
b5e6122ff575 added pretty printing options (from old ref manual);
wenzelm
parents: 28762
diff changeset
   245
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   246
section {* Mixfix annotations *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   247
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   248
text {* Mixfix annotations specify concrete \emph{inner syntax} of
28767
f09ceb800d00 minor tuning (according to old ref manual);
wenzelm
parents: 28766
diff changeset
   249
  Isabelle types and terms.  Some commands such as @{command
f09ceb800d00 minor tuning (according to old ref manual);
wenzelm
parents: 28766
diff changeset
   250
  "typedecl"} admit infixes only, while @{command "definition"} etc.\
f09ceb800d00 minor tuning (according to old ref manual);
wenzelm
parents: 28766
diff changeset
   251
  support the full range of general mixfixes and binders.  Fixed
f09ceb800d00 minor tuning (according to old ref manual);
wenzelm
parents: 28766
diff changeset
   252
  parameters in toplevel theorem statements, locale specifications
f09ceb800d00 minor tuning (according to old ref manual);
wenzelm
parents: 28766
diff changeset
   253
  also admit mixfix annotations.
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   254
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   255
  \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   256
  \begin{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   257
    infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   258
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   259
    mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   260
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   261
    structmixfix: mixfix | '(' 'structure' ')'
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   262
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   263
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   264
    prios: '[' (nat + ',') ']'
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   265
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   266
  \end{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   267
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   268
  Here the \railtok{string} specifications refer to the actual mixfix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   269
  template, which may include literal text, spacing, blocks, and
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   270
  arguments (denoted by ``@{text _}''); the special symbol
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   271
  ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   272
  argument that specifies an implicit structure reference (see also
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   273
  \secref{sec:locale}).  Infix and binder declarations provide common
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   274
  abbreviations for particular mixfix declarations.  So in practice,
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   275
  mixfix templates mostly degenerate to literal text for concrete
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   276
  syntax, such as ``@{verbatim "++"}'' for an infix symbol.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   277
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   278
  \medskip In full generality, mixfix declarations work as follows.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   279
  Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   280
  annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   281
  "mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   282
  delimiters that surround argument positions as indicated by
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   283
  underscores.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   284
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   285
  Altogether this determines a production for a context-free priority
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   286
  grammar, where for each argument @{text "i"} the syntactic category
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   287
  is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   288
  the result category is determined from @{text "\<tau>"} (with
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   289
  priority @{text "p"}).  Priority specifications are optional, with
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   290
  default 0 for arguments and 1000 for the result.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   291
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   292
  Since @{text "\<tau>"} may be again a function type, the constant
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   293
  type scheme may have more argument positions than the mixfix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   294
  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
   295
  @{text "m > n"} works by attaching concrete notation only to the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   296
  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
   297
  instead.  If a term has fewer arguments than specified in the mixfix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   298
  template, the concrete syntax is ignored.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   299
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   300
  \medskip A mixfix template may also contain additional directives
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   301
  for pretty printing, notably spaces, blocks, and breaks.  The
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   302
  general template format is a sequence over any of the following
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   303
  entities.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   304
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   305
  \begin{itemize}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   306
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   307
  \item @{text "\<^bold>d"} is a delimiter, namely a non-empty
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   308
  sequence of characters other than the special characters @{text "'"}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   309
  (single quote), @{text "_"} (underscore), @{text "\<index>"} (index
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   310
  symbol), @{text "/"} (slash), @{text "("} and @{text ")"}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   311
  (parentheses).
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   312
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   313
  A single quote escapes the special meaning of these meta-characters,
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   314
  producing a literal version of the following character, unless that
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   315
  is a blank.  A single quote followed by a blank separates
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   316
  delimiters, without affecting printing, but input tokens may have
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   317
  additional white space here.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   318
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   319
  \item @{text "_"} is an argument position, which stands for a
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   320
  certain syntactic category in the underlying grammar.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   321
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   322
  \item @{text "\<index>"} is an indexed argument position; this is
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   323
  the place where implicit structure arguments can be attached.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   324
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   325
  \item @{text "\<^bold>s"} is a non-empty sequence of spaces for
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   326
  printing.  This and the following specifications do not affect
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   327
  parsing at all.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   328
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   329
  \item @{text "(\<^bold>n"} opens a pretty printing block.  The
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   330
  optional number specifies how much indentation to add when a line
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   331
  break occurs within the block.  If the parenthesis is not followed
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   332
  by digits, the indentation defaults to 0.  A block specified via
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   333
  @{text "(00"} is unbreakable.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   334
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   335
  \item @{text ")"} closes a pretty printing block.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   336
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   337
  \item @{text "//"} forces a line break.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   338
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   339
  \item @{text "/\<^bold>s"} allows a line break.  Here @{text
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   340
  "\<^bold>s"} stands for the string of spaces (zero or more) right
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   341
  after the slash.  These spaces are printed if the break is
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   342
  \emph{not} taken.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   343
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   344
  \end{itemize}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   345
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   346
  For example, the template @{text "(_ +/ _)"} specifies an infix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   347
  operator.  There are two argument positions; the delimiter @{text
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   348
  "+"} is preceded by a space and followed by a space or line break;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   349
  the entire phrase is a pretty printing block.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   350
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   351
  The general idea of pretty printing with blocks and breaks is also
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   352
  described in \cite{paulson-ml2}.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   353
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   354
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   355
28766
accab7594b8e misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents: 28765
diff changeset
   356
section {* Explicit term notation *}
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   357
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   358
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   359
  \begin{matharray}{rcll}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   360
    @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   361
    @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   362
  \end{matharray}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   363
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   364
  \begin{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   365
    ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   366
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   367
  \end{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   368
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   369
  \begin{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   370
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   371
  \item @{command "notation"}~@{text "c (mx)"} associates mixfix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   372
  syntax with an existing constant or fixed variable.  This is a
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   373
  robust interface to the underlying @{command "syntax"} primitive
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   374
  (\secref{sec:syn-trans}).  Type declaration and internal syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   375
  representation of the given entity is retrieved from the context.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   376
  
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   377
  \item @{command "no_notation"} is similar to @{command "notation"},
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   378
  but removes the specified syntax annotation from the present
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   379
  context.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   380
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   381
  \end{description}
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
28769
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   384
section {* The Pure syntax *}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   385
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   386
subsection {* Priority grammars *}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   387
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   388
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
   389
  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
   390
  \emph{productions}.  Productions have the form @{text "A = \<gamma>"},
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   391
  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
   392
  terminals and nonterminals.  One designated nonterminal is called
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   393
  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
   394
  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
   395
  root symbol by applying productions as rewrite rules.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   396
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   397
  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
   398
  grammar}.  Each nonterminal is decorated by an integer priority:
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   399
  @{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
   400
  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
   401
  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
   402
  grammar by introducing new nonterminals and productions.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   403
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   404
  \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
   405
  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
   406
  \<alpha>} and @{text \<beta>} denote strings of terminal or nonterminal symbols.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   407
  Then
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   408
  \[
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   409
    @{text "\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>"}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   410
  \]
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   411
  if and only if @{text G} contains some production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   412
  for @{text "p \<le> q"}.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   413
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   414
  \medskip The following grammar for arithmetic expressions
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   415
  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
   416
  enforced by priorities.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   417
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   418
  \begin{center}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   419
  \begin{tabular}{rclr}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   420
  @{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
   421
  @{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim "("} @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim ")"} \\
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   422
  @{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
   423
  @{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
   424
  @{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
   425
  \end{tabular}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   426
  \end{center}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   427
  The choice of priorities determines that @{verbatim "-"} binds
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   428
  tighter than @{verbatim "*"}, which binds tighter than @{verbatim
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   429
  "+"}.  Furthermore @{verbatim "+"} associates to the left and
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   430
  @{verbatim "*"} to the right.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   431
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   432
  \medskip For clarity, grammars obey these conventions:
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   433
  \begin{itemize}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   434
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   435
  \item All priorities must lie between 0 and 1000.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   436
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   437
  \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
   438
  left-hand side may be omitted.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   439
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   440
  \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
   441
  (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
   442
  a column on the far right.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   443
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   444
  \item Alternatives are separated by @{text "|"}.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   445
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   446
  \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
   447
  but obvious way.
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   448
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   449
  \end{itemize}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   450
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   451
  Using these conventions, the example grammar specification above
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   452
  takes the form:
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   453
  \begin{center}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   454
  \begin{tabular}{rclc}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   455
    @{text A} & @{text "="} & @{verbatim 0} & \qquad\qquad \\
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   456
              & @{text "|"} & @{verbatim "("} @{text A} @{verbatim ")"} \\
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   457
              & @{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
   458
              & @{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
   459
              & @{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
   460
  \end{tabular}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   461
  \end{center}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   462
*}
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   463
8fc228f21861 added section "Priority grammars" (variant from old ref manual);
wenzelm
parents: 28767
diff changeset
   464
28762
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   465
section {* Syntax and translations \label{sec:syn-trans} *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   466
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   467
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   468
  \begin{matharray}{rcl}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   469
    @{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   470
    @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   471
    @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   472
    @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   473
    @{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   474
  \end{matharray}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   475
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   476
  \begin{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   477
    'nonterminals' (name +)
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   478
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   479
    ('syntax' | 'no\_syntax') mode? (constdecl +)
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   480
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   481
    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   482
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   483
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   484
    mode: ('(' ( name | 'output' | name 'output' ) ')')
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   485
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   486
    transpat: ('(' nameref ')')? string
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   487
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   488
  \end{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   489
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   490
  \begin{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   491
  
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   492
  \item @{command "nonterminals"}~@{text c} declares a type
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   493
  constructor @{text c} (without arguments) to act as purely syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   494
  type: a nonterminal symbol of the inner syntax.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   495
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   496
  \item @{command "syntax"}~@{text "(mode) decls"} is similar to
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   497
  @{command "consts"}~@{text decls}, except that the actual logical
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   498
  signature extension is omitted.  Thus the context free grammar of
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   499
  Isabelle's inner syntax may be augmented in arbitrary ways,
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   500
  independently of the logic.  The @{text mode} argument refers to the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   501
  print mode that the grammar rules belong; unless the @{keyword_ref
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   502
  "output"} indicator is given, all productions are added both to the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   503
  input and output grammar.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   504
  
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   505
  \item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   506
  declarations (and translations) resulting from @{text decls}, which
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   507
  are interpreted in the same manner as for @{command "syntax"} above.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   508
  
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   509
  \item @{command "translations"}~@{text rules} specifies syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   510
  translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   511
  parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   512
  Translation patterns may be prefixed by the syntactic category to be
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   513
  used for parsing; the default is @{text logic}.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   514
  
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   515
  \item @{command "no_translations"}~@{text rules} removes syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   516
  translation rules, which are interpreted in the same manner as for
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   517
  @{command "translations"} above.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   518
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   519
  \end{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   520
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   521
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   522
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   523
section {* Syntax translation functions *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   524
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   525
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   526
  \begin{matharray}{rcl}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   527
    @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   528
    @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   529
    @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   530
    @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   531
    @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   532
  \end{matharray}
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
  \begin{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   535
  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   536
    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   537
  ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   538
  \end{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   539
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   540
  Syntax translation functions written in ML admit almost arbitrary
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   541
  manipulations of Isabelle's inner syntax.  Any of the above commands
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   542
  have a single \railqtok{text} argument that refers to an ML
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   543
  expression of appropriate type, which are as follows by default:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   544
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   545
%FIXME proper antiquotations
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   546
\begin{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   547
val parse_ast_translation   : (string * (ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   548
val parse_translation       : (string * (term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   549
val print_translation       : (string * (term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   550
val typed_print_translation :
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   551
  (string * (bool -> typ -> term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   552
val print_ast_translation   : (string * (ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   553
\end{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   554
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   555
  If the @{text "(advanced)"} option is given, the corresponding
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   556
  translation functions may depend on the current theory or proof
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   557
  context.  This allows to implement advanced syntax mechanisms, as
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   558
  translations functions may refer to specific theory declarations or
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   559
  auxiliary proof data.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   560
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   561
  See also \cite[\S8]{isabelle-ref} for more information on the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   562
  general concept of syntax transformations in Isabelle.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   563
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   564
%FIXME proper antiquotations
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   565
\begin{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   566
val parse_ast_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   567
  (string * (Proof.context -> ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   568
val parse_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   569
  (string * (Proof.context -> term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   570
val print_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   571
  (string * (Proof.context -> term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   572
val typed_print_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   573
  (string * (Proof.context -> bool -> typ -> term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   574
val print_ast_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   575
  (string * (Proof.context -> ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   576
\end{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   577
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   578
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   579
end