doc-src/IsarRef/Thy/Inner_Syntax.thy
author wenzelm
Thu, 13 Nov 2008 21:48:19 +0100
changeset 28762 f5d79aeffd81
child 28763 b5e6122ff575
permissions -rw-r--r--
separate chapter "Inner syntax --- the term language";
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}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    15
    @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    16
    @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    17
    @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    18
    @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    19
    @{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    20
    @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    21
    @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
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}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    28
    'pr' modes? nat? (',' nat)?
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
    'thm' modes? thmrefs
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
    'term' modes? term
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    33
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    34
    'prop' modes? prop
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    35
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    36
    'typ' modes? type
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    37
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    38
    'prf' modes? thmrefs?
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
    'full\_prf' modes? thmrefs?
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    41
    ;
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
    modes: '(' (name + ) ')'
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
  \end{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    46
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    47
  \begin{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    48
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    49
  \item @{command "pr"}~@{text "goals, prems"} prints the current
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    50
  proof state (if present), including the proof context, current facts
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    51
  and goals.  The optional limit arguments affect the number of goals
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    52
  and premises to be displayed, which is initially 10 for both.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    53
  Omitting limit values leaves the current setting unchanged.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    54
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    55
  \item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    56
  theorems from the current theory or proof context.  Note that any
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    57
  attributes included in the theorem specifications are applied to a
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    58
  temporary context derived from the current theory or proof; the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    59
  result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    60
  \<dots>, a\<^sub>n"} do not have any permanent effect.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    61
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    62
  \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    63
  read, type-check and print terms or propositions according to the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    64
  current theory or proof context; the inferred type of @{text t} is
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    65
  output as well.  Note that these commands are also useful in
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    66
  inspecting the current environment of term abbreviations.
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
  \item @{command "typ"}~@{text \<tau>} reads and prints types of the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    69
  meta-logic according to the current theory or proof context.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    70
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    71
  \item @{command "prf"} displays the (compact) proof term of the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    72
  current proof state (if present), or of the given theorems. Note
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    73
  that this requires proof terms to be switched on for the current
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    74
  object logic (see the ``Proof terms'' section of the Isabelle
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    75
  reference manual for information on how to do this).
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    76
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    77
  \item @{command "full_prf"} is like @{command "prf"}, but displays
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    78
  the full proof term, i.e.\ also displays information omitted in the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    79
  compact proof term, which is denoted by ``@{text _}'' placeholders
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    80
  there.
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
  \end{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    83
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    84
  All of the diagnostic commands above admit a list of @{text modes}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    85
  to be specified, which is appended to the current print mode (see
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    86
  also \cite{isabelle-ref}).  Thus the output behavior may be modified
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    87
  according particular print mode features.  For example, @{command
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    88
  "pr"}~@{text "(latex xsymbols)"} would print the current proof state
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    89
  with mathematical symbols and special characters represented in
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    90
  {\LaTeX} source, according to the Isabelle style
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    91
  \cite{isabelle-sys}.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    92
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    93
  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    94
  systematic way to include formal items into the printed text
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    95
  document.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    96
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    97
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    98
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
    99
section {* Mixfix annotations *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   100
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   101
text {* Mixfix annotations specify concrete \emph{inner syntax} of
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   102
  Isabelle types and terms.  Some commands such as @{command "types"}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   103
  (see \secref{sec:types-pure}) admit infixes only, while @{command
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   104
  "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   105
  \secref{sec:syn-trans}) support the full range of general mixfixes
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   106
  and binders.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   107
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   108
  \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   109
  \begin{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   110
    infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   111
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   112
    mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
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
    structmixfix: mixfix | '(' 'structure' ')'
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   115
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   116
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   117
    prios: '[' (nat + ',') ']'
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
  \end{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   120
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   121
  Here the \railtok{string} specifications refer to the actual mixfix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   122
  template, which may include literal text, spacing, blocks, and
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   123
  arguments (denoted by ``@{text _}''); the special symbol
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   124
  ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   125
  argument that specifies an implicit structure reference (see also
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   126
  \secref{sec:locale}).  Infix and binder declarations provide common
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   127
  abbreviations for particular mixfix declarations.  So in practice,
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   128
  mixfix templates mostly degenerate to literal text for concrete
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   129
  syntax, such as ``@{verbatim "++"}'' for an infix symbol.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   130
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   131
  \medskip In full generality, mixfix declarations work as follows.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   132
  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
   133
  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
   134
  "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
   135
  delimiters that surround argument positions as indicated by
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   136
  underscores.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   137
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   138
  Altogether this determines a production for a context-free priority
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   139
  grammar, where for each argument @{text "i"} the syntactic category
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   140
  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
   141
  the result category is determined from @{text "\<tau>"} (with
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   142
  priority @{text "p"}).  Priority specifications are optional, with
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   143
  default 0 for arguments and 1000 for the result.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   144
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   145
  Since @{text "\<tau>"} may be again a function type, the constant
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   146
  type scheme may have more argument positions than the mixfix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   147
  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
   148
  @{text "m > n"} works by attaching concrete notation only to the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   149
  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
   150
  instead.  If a term has fewer arguments than specified in the mixfix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   151
  template, the concrete syntax is ignored.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   152
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   153
  \medskip A mixfix template may also contain additional directives
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   154
  for pretty printing, notably spaces, blocks, and breaks.  The
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   155
  general template format is a sequence over any of the following
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   156
  entities.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   157
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   158
  \begin{itemize}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   159
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   160
  \item @{text "\<^bold>d"} is a delimiter, namely a non-empty
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   161
  sequence of characters other than the special characters @{text "'"}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   162
  (single quote), @{text "_"} (underscore), @{text "\<index>"} (index
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   163
  symbol), @{text "/"} (slash), @{text "("} and @{text ")"}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   164
  (parentheses).
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   165
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   166
  A single quote escapes the special meaning of these meta-characters,
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   167
  producing a literal version of the following character, unless that
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   168
  is a blank.  A single quote followed by a blank separates
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   169
  delimiters, without affecting printing, but input tokens may have
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   170
  additional white space here.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   171
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   172
  \item @{text "_"} is an argument position, which stands for a
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   173
  certain syntactic category in the underlying grammar.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   174
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   175
  \item @{text "\<index>"} is an indexed argument position; this is
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   176
  the place where implicit structure arguments can be attached.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   177
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   178
  \item @{text "\<^bold>s"} is a non-empty sequence of spaces for
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   179
  printing.  This and the following specifications do not affect
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   180
  parsing at all.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   181
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   182
  \item @{text "(\<^bold>n"} opens a pretty printing block.  The
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   183
  optional number specifies how much indentation to add when a line
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   184
  break occurs within the block.  If the parenthesis is not followed
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   185
  by digits, the indentation defaults to 0.  A block specified via
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   186
  @{text "(00"} is unbreakable.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   187
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   188
  \item @{text ")"} closes a pretty printing block.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   189
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   190
  \item @{text "//"} forces a line break.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   191
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   192
  \item @{text "/\<^bold>s"} allows a line break.  Here @{text
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   193
  "\<^bold>s"} stands for the string of spaces (zero or more) right
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   194
  after the slash.  These spaces are printed if the break is
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   195
  \emph{not} taken.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   196
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   197
  \end{itemize}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   198
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   199
  For example, the template @{text "(_ +/ _)"} specifies an infix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   200
  operator.  There are two argument positions; the delimiter @{text
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   201
  "+"} 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
   202
  the entire phrase is a pretty printing block.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   203
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   204
  The general idea of pretty printing with blocks and breaks is also
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   205
  described in \cite{paulson-ml2}.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   206
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   207
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   208
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   209
section {* Additional term notation *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   210
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   211
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   212
  \begin{matharray}{rcll}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   213
    @{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   214
    @{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   215
  \end{matharray}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   216
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   217
  \begin{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   218
    ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   219
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   220
  \end{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   221
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   222
  \begin{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   223
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   224
  \item @{command "notation"}~@{text "c (mx)"} associates mixfix
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   225
  syntax with an existing constant or fixed variable.  This is a
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   226
  robust interface to the underlying @{command "syntax"} primitive
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   227
  (\secref{sec:syn-trans}).  Type declaration and internal syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   228
  representation of the given entity is retrieved from the context.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   229
  
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   230
  \item @{command "no_notation"} is similar to @{command "notation"},
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   231
  but removes the specified syntax annotation from the present
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   232
  context.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   233
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   234
  \end{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   235
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   236
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   237
section {* Syntax and translations \label{sec:syn-trans} *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   238
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   239
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   240
  \begin{matharray}{rcl}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   241
    @{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   242
    @{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   243
    @{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   244
    @{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   245
    @{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   246
  \end{matharray}
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
  \begin{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   249
    'nonterminals' (name +)
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   250
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   251
    ('syntax' | 'no\_syntax') mode? (constdecl +)
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   252
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   253
    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
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
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   256
    mode: ('(' ( name | 'output' | name 'output' ) ')')
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   257
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   258
    transpat: ('(' nameref ')')? string
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   259
    ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   260
  \end{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   261
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   262
  \begin{description}
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
  \item @{command "nonterminals"}~@{text c} declares a type
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   265
  constructor @{text c} (without arguments) to act as purely syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   266
  type: a nonterminal symbol of the inner syntax.
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
  \item @{command "syntax"}~@{text "(mode) decls"} is similar to
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   269
  @{command "consts"}~@{text decls}, except that the actual logical
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   270
  signature extension is omitted.  Thus the context free grammar of
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   271
  Isabelle's inner syntax may be augmented in arbitrary ways,
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   272
  independently of the logic.  The @{text mode} argument refers to the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   273
  print mode that the grammar rules belong; unless the @{keyword_ref
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   274
  "output"} indicator is given, all productions are added both to the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   275
  input and output grammar.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   276
  
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   277
  \item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   278
  declarations (and translations) resulting from @{text decls}, which
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   279
  are interpreted in the same manner as for @{command "syntax"} above.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   280
  
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   281
  \item @{command "translations"}~@{text rules} specifies syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   282
  translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   283
  parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   284
  Translation patterns may be prefixed by the syntactic category to be
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   285
  used for parsing; the default is @{text logic}.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   286
  
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   287
  \item @{command "no_translations"}~@{text rules} removes syntactic
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   288
  translation rules, which are interpreted in the same manner as for
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   289
  @{command "translations"} above.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   290
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   291
  \end{description}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   292
*}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   293
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   294
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   295
section {* Syntax translation functions *}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   296
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   297
text {*
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   298
  \begin{matharray}{rcl}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   299
    @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   300
    @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   301
    @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   302
    @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   303
    @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   304
  \end{matharray}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   305
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   306
  \begin{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   307
  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   308
    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   309
  ;
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   310
  \end{rail}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   311
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   312
  Syntax translation functions written in ML admit almost arbitrary
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   313
  manipulations of Isabelle's inner syntax.  Any of the above commands
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   314
  have a single \railqtok{text} argument that refers to an ML
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   315
  expression of appropriate type, which are as follows by default:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   316
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   317
%FIXME proper antiquotations
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   318
\begin{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   319
val parse_ast_translation   : (string * (ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   320
val parse_translation       : (string * (term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   321
val print_translation       : (string * (term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   322
val typed_print_translation :
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   323
  (string * (bool -> typ -> term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   324
val print_ast_translation   : (string * (ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   325
\end{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   326
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   327
  If the @{text "(advanced)"} option is given, the corresponding
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   328
  translation functions may depend on the current theory or proof
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   329
  context.  This allows to implement advanced syntax mechanisms, as
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   330
  translations functions may refer to specific theory declarations or
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   331
  auxiliary proof data.
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   332
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   333
  See also \cite[\S8]{isabelle-ref} for more information on the
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   334
  general concept of syntax transformations in Isabelle.
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
%FIXME proper antiquotations
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   337
\begin{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   338
val parse_ast_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   339
  (string * (Proof.context -> ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   340
val parse_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   341
  (string * (Proof.context -> term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   342
val print_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   343
  (string * (Proof.context -> term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   344
val typed_print_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   345
  (string * (Proof.context -> bool -> typ -> term list -> term)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   346
val print_ast_translation:
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   347
  (string * (Proof.context -> ast list -> ast)) list
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   348
\end{ttbox}
f5d79aeffd81 separate chapter "Inner syntax --- the term language";
wenzelm
parents:
diff changeset
   349
*}
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
end