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