author | wenzelm |
Wed, 15 Aug 2012 13:07:24 +0200 | |
changeset 48816 | 754b09cd616f |
parent 48792 | 4aa5b965f70e |
permissions | -rw-r--r-- |
28762 | 1 |
% |
2 |
\begin{isabellebody}% |
|
40406 | 3 |
\def\isabellecontext{Inner{\isaliteral{5F}{\isacharunderscore}}Syntax}% |
28762 | 4 |
% |
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
40406 | 11 |
\ Inner{\isaliteral{5F}{\isacharunderscore}}Syntax\isanewline |
42651 | 12 |
\isakeyword{imports}\ Base\ Main\isanewline |
28762 | 13 |
\isakeyword{begin}% |
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupchapter{Inner syntax --- the term language \label{ch:inner-syntax}% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
46282 | 25 |
\begin{isamarkuptext}% |
26 |
The inner syntax of Isabelle provides concrete notation for |
|
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 |
|
28 |
extend existing syntactic categories by additional notation, or |
|
29 |
define new sub-languages that are linked to the standard term |
|
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 |
|
31 |
user-defined nonterminal \isa{{\isaliteral{22}{\isachardoublequote}}foo{\isaliteral{22}{\isachardoublequote}}} --- within the bounds of the |
|
32 |
given lexical syntax of Isabelle/Pure. |
|
33 |
||
34 |
The most basic way to specify concrete syntax for logical entities |
|
35 |
works via mixfix annotations (\secref{sec:mixfix}), which may be |
|
36 |
usually given as part of the original declaration or via explicit |
|
37 |
notation commands later on (\secref{sec:notation}). This already |
|
38 |
covers many needs of concrete syntax without having to understand |
|
39 |
the full complexity of inner syntax layers. |
|
40 |
||
41 |
Further details of the syntax engine involves the classical |
|
42 |
distinction of lexical language versus context-free grammar (see |
|
43 |
\secref{sec:pure-syntax}), and various mechanisms for \emph{syntax |
|
48113 | 44 |
transformations} (see \secref{sec:syntax-transformations}).% |
46282 | 45 |
\end{isamarkuptext}% |
46 |
\isamarkuptrue% |
|
47 |
% |
|
28762 | 48 |
\isamarkupsection{Printing logical entities% |
49 |
} |
|
50 |
\isamarkuptrue% |
|
51 |
% |
|
46284 | 52 |
\isamarkupsubsection{Diagnostic commands \label{sec:print-diag}% |
28762 | 53 |
} |
54 |
\isamarkuptrue% |
|
55 |
% |
|
56 |
\begin{isamarkuptext}% |
|
57 |
\begin{matharray}{rcl} |
|
40406 | 58 |
\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}}} \\ |
59 |
\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}}} \\ |
|
60 |
\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}}} \\ |
|
61 |
\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}}} \\ |
|
62 |
\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}}} \\ |
|
63 |
\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}}} \\ |
|
64 |
\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 | 65 |
\end{matharray} |
66 |
||
67 |
These diagnostic commands assist interactive development by printing |
|
68 |
internal logical entities in a human-readable fashion. |
|
69 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
70 |
\begin{railoutput} |
42662 | 71 |
\rail@begin{2}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
72 |
\rail@term{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
73 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
74 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
75 |
\rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
76 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
77 |
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[] |
48792 | 78 |
\rail@bar |
79 |
\rail@nextbar{1} |
|
80 |
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[] |
|
81 |
\rail@nont{\hyperlink{syntax.sort}{\mbox{\isa{sort}}}}[] |
|
82 |
\rail@endbar |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
83 |
\rail@end |
42662 | 84 |
\rail@begin{2}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
85 |
\rail@term{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
86 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
87 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
88 |
\rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
89 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
90 |
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
91 |
\rail@end |
42662 | 92 |
\rail@begin{2}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
93 |
\rail@term{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
94 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
95 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
96 |
\rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
97 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
98 |
\rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
99 |
\rail@end |
42662 | 100 |
\rail@begin{2}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
101 |
\rail@term{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
102 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
103 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
104 |
\rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
105 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
106 |
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
107 |
\rail@end |
42662 | 108 |
\rail@begin{2}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
109 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
110 |
\rail@term{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}[] |
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@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
|
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.modes}{\mbox{\isa{modes}}}}[] |
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@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
119 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
120 |
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
121 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
122 |
\rail@end |
42662 | 123 |
\rail@begin{2}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
124 |
\rail@term{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}[] |
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.modes}{\mbox{\isa{modes}}}}[] |
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@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
130 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
131 |
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
132 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
133 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
134 |
\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
|
135 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
136 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
137 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
138 |
\rail@nextplus{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
139 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
140 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
141 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
142 |
\end{railoutput} |
28762 | 143 |
|
144 |
||
145 |
\begin{description} |
|
146 |
||
48792 | 147 |
\item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} reads and prints a type expression |
148 |
according to the current context. |
|
149 |
||
150 |
\item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ s{\isaliteral{22}{\isachardoublequote}}} uses type-inference to |
|
151 |
determine the most general way to make \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} conform to sort |
|
152 |
\isa{{\isaliteral{22}{\isachardoublequote}}s{\isaliteral{22}{\isachardoublequote}}}. For concrete \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} this checks if the type |
|
153 |
belongs to that sort. Dummy type parameters ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'' |
|
154 |
(underscore) are assigned to fresh type variables with most general |
|
155 |
sorts, according the the principles of type-inference. |
|
28762 | 156 |
|
40406 | 157 |
\item \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} |
28762 | 158 |
read, type-check and print terms or propositions according to the |
159 |
current theory or proof context; the inferred type of \isa{t} is |
|
160 |
output as well. Note that these commands are also useful in |
|
161 |
inspecting the current environment of term abbreviations. |
|
162 |
||
40406 | 163 |
\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 | 164 |
theorems from the current theory or proof context. Note that any |
165 |
attributes included in the theorem specifications are applied to a |
|
166 |
temporary context derived from the current theory or proof; the |
|
40406 | 167 |
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 | 168 |
|
169 |
\item \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}} displays the (compact) proof term of the |
|
170 |
current proof state (if present), or of the given theorems. Note |
|
171 |
that this requires proof terms to be switched on for the current |
|
172 |
object logic (see the ``Proof terms'' section of the Isabelle |
|
173 |
reference manual for information on how to do this). |
|
174 |
||
40406 | 175 |
\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 | 176 |
the full proof term, i.e.\ also displays information omitted in the |
40406 | 177 |
compact proof term, which is denoted by ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'' placeholders |
28762 | 178 |
there. |
179 |
||
40406 | 180 |
\item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}goals{\isaliteral{22}{\isachardoublequote}}} prints the current proof state |
39165 | 181 |
(if present), including current facts and goals. The optional limit |
182 |
arguments affect the number of goals to be displayed, which is |
|
183 |
initially 10. Omitting limit value leaves the current setting |
|
184 |
unchanged. |
|
28762 | 185 |
|
186 |
\end{description} |
|
187 |
||
188 |
All of the diagnostic commands above admit a list of \isa{modes} |
|
42926 | 189 |
to be specified, which is appended to the current print mode; see |
46284 | 190 |
also \secref{sec:print-modes}. Thus the output behavior may be |
191 |
modified according particular print mode features. For example, |
|
192 |
\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 |
|
193 |
proof state with mathematical symbols and special characters |
|
194 |
represented in {\LaTeX} source, according to the Isabelle style |
|
28762 | 195 |
\cite{isabelle-sys}. |
196 |
||
197 |
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
|
198 |
systematic way to include formal items into the printed text |
|
199 |
document.% |
|
200 |
\end{isamarkuptext}% |
|
201 |
\isamarkuptrue% |
|
202 |
% |
|
203 |
\isamarkupsubsection{Details of printed content% |
|
204 |
} |
|
205 |
\isamarkuptrue% |
|
206 |
% |
|
207 |
\begin{isamarkuptext}% |
|
42655 | 208 |
\begin{tabular}{rcll} |
209 |
\indexdef{}{attribute}{show\_types}\hypertarget{attribute.show-types}{\hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}}} & : & \isa{attribute} & default \isa{false} \\ |
|
210 |
\indexdef{}{attribute}{show\_sorts}\hypertarget{attribute.show-sorts}{\hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}}} & : & \isa{attribute} & default \isa{false} \\ |
|
211 |
\indexdef{}{attribute}{show\_consts}\hypertarget{attribute.show-consts}{\hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}}} & : & \isa{attribute} & default \isa{false} \\ |
|
212 |
\indexdef{}{attribute}{show\_abbrevs}\hypertarget{attribute.show-abbrevs}{\hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} & : & \isa{attribute} & default \isa{true} \\ |
|
213 |
\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
|
214 |
\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
|
215 |
\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
|
216 |
\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 | 217 |
\indexdef{}{attribute}{eta\_contract}\hypertarget{attribute.eta-contract}{\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}} & : & \isa{attribute} & default \isa{true} \\ |
218 |
\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}}} \\ |
|
219 |
\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} \\ |
|
220 |
\indexdef{}{attribute}{show\_hyps}\hypertarget{attribute.show-hyps}{\hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}}} & : & \isa{attribute} & default \isa{false} \\ |
|
221 |
\indexdef{}{attribute}{show\_tags}\hypertarget{attribute.show-tags}{\hyperlink{attribute.show-tags}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}tags}}}} & : & \isa{attribute} & default \isa{false} \\ |
|
222 |
\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} \\ |
|
223 |
\end{tabular} |
|
224 |
\medskip |
|
28762 | 225 |
|
42655 | 226 |
These configuration options control the detail of information that |
227 |
is displayed for types, terms, theorems, goals etc. See also |
|
228 |
\secref{sec:config}. |
|
28762 | 229 |
|
230 |
\begin{description} |
|
231 |
||
42655 | 232 |
\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 |
233 |
printing of type constraints for term variables, and sort |
|
234 |
constraints for type variables. By default, neither of these are |
|
235 |
shown in output. If \hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}} is enabled, types are |
|
236 |
always shown as well. |
|
28762 | 237 |
|
238 |
Note that displaying types and sorts may explain why a polymorphic |
|
239 |
inference rule fails to resolve with some goal, or why a rewrite |
|
240 |
rule does not apply as expected. |
|
241 |
||
42655 | 242 |
\item \hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}} controls printing of types of |
243 |
constants when displaying a goal state. |
|
28762 | 244 |
|
245 |
Note that the output can be enormous, because polymorphic constants |
|
246 |
often occur at several different type instances. |
|
247 |
||
42655 | 248 |
\item \hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}} controls folding of constant |
249 |
abbreviations. |
|
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40406
diff
changeset
|
250 |
|
42655 | 251 |
\item \hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}} controls bracketing in pretty |
252 |
printed output. If enabled, all sub-expressions of the pretty |
|
28762 | 253 |
printing tree will be parenthesized, even if this produces malformed |
254 |
term syntax! This crude way of showing the internal structure of |
|
255 |
pretty printed entities may occasionally help to diagnose problems |
|
256 |
with operator priorities, for example. |
|
257 |
||
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42662
diff
changeset
|
258 |
\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
|
259 |
\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
|
260 |
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
|
261 |
\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
|
262 |
same names. |
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42279
diff
changeset
|
263 |
|
42655 | 264 |
\item \hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}} controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted |
265 |
printing of terms. |
|
28762 | 266 |
|
40406 | 267 |
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 | 268 |
provided \isa{x} is not free in \isa{f}. It asserts |
40406 | 269 |
\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 |
270 |
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 | 271 |
|
42655 | 272 |
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 | 273 |
appears simply as \isa{F}. |
274 |
||
40406 | 275 |
Note that the distinction between a term and its \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-expanded |
28762 | 276 |
form occasionally matters. While higher-order resolution and |
40406 | 277 |
rewriting operate modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-conversion, some other tools |
28762 | 278 |
might look at terms more discretely. |
279 |
||
42655 | 280 |
\item \hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}} controls the maximum number of |
39130 | 281 |
subgoals to be shown in goal output. |
28762 | 282 |
|
42655 | 283 |
\item \hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}} controls whether the main result |
284 |
to be proven should be displayed. This information might be |
|
39130 | 285 |
relevant for schematic goals, to inspect the current claim that has |
286 |
been synthesized so far. |
|
28762 | 287 |
|
42655 | 288 |
\item \hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}} controls printing of implicit |
289 |
hypotheses of local facts. Normally, only those hypotheses are |
|
290 |
displayed that are \emph{not} covered by the assumptions of the |
|
291 |
current context: this situation indicates a fault in some tool being |
|
292 |
used. |
|
28762 | 293 |
|
42655 | 294 |
By enabling \hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}}, output of \emph{all} hypotheses |
295 |
can be enforced, which is occasionally useful for diagnostic |
|
296 |
purposes. |
|
28762 | 297 |
|
42655 | 298 |
\item \hyperlink{attribute.show-tags}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}tags}}} controls printing of extra annotations |
299 |
within theorems, such as internal position information, or the case |
|
300 |
names being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}. |
|
28762 | 301 |
|
302 |
Note that the \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} |
|
303 |
attributes provide low-level access to the collection of tags |
|
304 |
associated with a theorem. |
|
305 |
||
42655 | 306 |
\item \hyperlink{attribute.show-question-marks}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}question{\isaliteral{5F}{\isacharunderscore}}marks}}} controls printing of question |
307 |
marks for schematic variables, such as \isa{{\isaliteral{3F}{\isacharquery}}x}. Only the leading |
|
28762 | 308 |
question mark is affected, the remaining text is unchanged |
309 |
(including proper markup for schematic variables that might be |
|
310 |
relevant for user interfaces). |
|
311 |
||
312 |
\end{description}% |
|
313 |
\end{isamarkuptext}% |
|
314 |
\isamarkuptrue% |
|
315 |
% |
|
46284 | 316 |
\isamarkupsubsection{Alternative print modes \label{sec:print-modes}% |
317 |
} |
|
318 |
\isamarkuptrue% |
|
319 |
% |
|
320 |
\begin{isamarkuptext}% |
|
321 |
\begin{mldecls} |
|
322 |
\indexdef{}{ML}{print\_mode\_value}\verb|print_mode_value: unit -> string list| \\ |
|
323 |
\indexdef{}{ML}{Print\_Mode.with\_modes}\verb|Print_Mode.with_modes: string list -> ('a -> 'b) -> 'a -> 'b| \\ |
|
324 |
\end{mldecls} |
|
325 |
||
326 |
The \emph{print mode} facility allows to modify various operations |
|
327 |
for printing. Commands like \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}, \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}, |
|
328 |
\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}} (see \secref{sec:print-diag}) take additional print |
|
329 |
modes as optional argument. The underlying ML operations are as |
|
330 |
follows. |
|
331 |
||
332 |
\begin{description} |
|
333 |
||
334 |
\item \verb|print_mode_value ()| yields the list of currently |
|
335 |
active print mode names. This should be understood as symbolic |
|
336 |
representation of certain individual features for printing (with |
|
337 |
precedence from left to right). |
|
338 |
||
339 |
\item \verb|Print_Mode.with_modes|~\isa{{\isaliteral{22}{\isachardoublequote}}modes\ f\ x{\isaliteral{22}{\isachardoublequote}}} evaluates |
|
340 |
\isa{{\isaliteral{22}{\isachardoublequote}}f\ x{\isaliteral{22}{\isachardoublequote}}} in an execution context where the print mode is |
|
341 |
prepended by the given \isa{{\isaliteral{22}{\isachardoublequote}}modes{\isaliteral{22}{\isachardoublequote}}}. This provides a thread-safe |
|
342 |
way to augment print modes. It is also monotonic in the set of mode |
|
343 |
names: it retains the default print mode that certain |
|
344 |
user-interfaces might have installed for their proper functioning! |
|
345 |
||
346 |
\end{description} |
|
347 |
||
348 |
\begin{warn} |
|
349 |
The old global reference \verb|print_mode| should never be used |
|
350 |
directly in applications. Its main reason for being publicly |
|
351 |
accessible is to support historic versions of Proof~General. |
|
352 |
\end{warn} |
|
353 |
||
354 |
\medskip The pretty printer for inner syntax maintains alternative |
|
355 |
mixfix productions for any print mode name invented by the user, say |
|
356 |
in commands like \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}} or \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}. |
|
357 |
Mode names can be arbitrary, but the following ones have a specific |
|
358 |
meaning by convention: |
|
359 |
||
360 |
\begin{itemize} |
|
361 |
||
362 |
\item \verb|""| (the empty string): default mode; |
|
363 |
implicitly active as last element in the list of modes. |
|
364 |
||
365 |
\item \verb|input|: dummy print mode that is never active; may |
|
366 |
be used to specify notation that is only available for input. |
|
367 |
||
368 |
\item \verb|internal| dummy print mode that is never active; |
|
369 |
used internally in Isabelle/Pure. |
|
370 |
||
371 |
\item \verb|xsymbols|: enable proper mathematical symbols |
|
372 |
instead of ASCII art.\footnote{This traditional mode name stems from |
|
373 |
the ``X-Symbol'' package for old versions Proof~General with XEmacs, |
|
374 |
although that package has been superseded by Unicode in recent |
|
375 |
years.} |
|
376 |
||
377 |
\item \verb|HTML|: additional mode that is active in HTML |
|
378 |
presentation of Isabelle theory sources; allows to provide |
|
379 |
alternative output notation. |
|
380 |
||
381 |
\item \verb|latex|: additional mode that is active in {\LaTeX} |
|
382 |
document preparation of Isabelle theory sources; allows to provide |
|
383 |
alternative output notation. |
|
384 |
||
385 |
\end{itemize}% |
|
386 |
\end{isamarkuptext}% |
|
387 |
\isamarkuptrue% |
|
388 |
% |
|
28762 | 389 |
\isamarkupsubsection{Printing limits% |
390 |
} |
|
391 |
\isamarkuptrue% |
|
392 |
% |
|
393 |
\begin{isamarkuptext}% |
|
394 |
\begin{mldecls} |
|
36745 | 395 |
\indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\ |
30121 | 396 |
\indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\ |
28762 | 397 |
\end{mldecls} |
398 |
||
399 |
These ML functions set limits for pretty printed text. |
|
400 |
||
401 |
\begin{description} |
|
402 |
||
36745 | 403 |
\item \verb|Pretty.margin_default| indicates the global default for |
404 |
the right margin of the built-in pretty printer, with initial value |
|
405 |
76. Note that user-interfaces typically control margins |
|
406 |
automatically when resizing windows, or even bypass the formatting |
|
407 |
engine of Isabelle/ML altogether and do it within the front end via |
|
408 |
Isabelle/Scala. |
|
28762 | 409 |
|
410 |
\item \verb|print_depth|~\isa{n} limits the printing depth of the |
|
411 |
ML toplevel pretty printer; the precise effect depends on the ML |
|
412 |
compiler and run-time system. Typically \isa{n} should be less |
|
413 |
than 10. Bigger values such as 100--1000 are useful for debugging. |
|
414 |
||
415 |
\end{description}% |
|
416 |
\end{isamarkuptext}% |
|
417 |
\isamarkuptrue% |
|
418 |
% |
|
46282 | 419 |
\isamarkupsection{Mixfix annotations \label{sec:mixfix}% |
28762 | 420 |
} |
421 |
\isamarkuptrue% |
|
422 |
% |
|
423 |
\begin{isamarkuptext}% |
|
424 |
Mixfix annotations specify concrete \emph{inner syntax} of |
|
35351
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
32836
diff
changeset
|
425 |
Isabelle types and terms. Locally fixed parameters in toplevel |
46290 | 426 |
theorem statements, locale and class specifications also admit |
427 |
mixfix annotations in a fairly uniform manner. A mixfix annotation |
|
428 |
describes describes the concrete syntax, the translation to abstract |
|
429 |
syntax, and the pretty printing. Special case annotations provide a |
|
430 |
simple means of specifying infix operators and binders. |
|
431 |
||
432 |
Isabelle mixfix syntax is inspired by {\OBJ} \cite{OBJ}. It allows |
|
433 |
to specify any context-free priority grammar, which is more general |
|
434 |
than the fixity declarations of ML and Prolog. |
|
28762 | 435 |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
436 |
\begin{railoutput} |
46289 | 437 |
\rail@begin{1}{\indexdef{}{syntax}{mixfix}\hypertarget{syntax.mixfix}{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}} |
438 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
|
439 |
\rail@nont{\isa{mfix}}[] |
|
440 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
|
441 |
\rail@end |
|
442 |
\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
|
443 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
444 |
\rail@bar |
46289 | 445 |
\rail@nont{\isa{mfix}}[] |
446 |
\rail@nextbar{1} |
|
447 |
\rail@term{\isa{\isakeyword{structure}}}[] |
|
448 |
\rail@endbar |
|
449 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
|
450 |
\rail@end |
|
451 |
\rail@begin{7}{\isa{mfix}} |
|
452 |
\rail@bar |
|
46290 | 453 |
\rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[] |
46285
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
454 |
\rail@bar |
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
455 |
\rail@nextbar{1} |
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
456 |
\rail@nont{\isa{prios}}[] |
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
457 |
\rail@endbar |
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
458 |
\rail@bar |
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
459 |
\rail@nextbar{1} |
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
460 |
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] |
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
461 |
\rail@endbar |
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
462 |
\rail@nextbar{2} |
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
463 |
\rail@bar |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
464 |
\rail@term{\isa{\isakeyword{infix}}}[] |
46285
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
465 |
\rail@nextbar{3} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
466 |
\rail@term{\isa{\isakeyword{infixl}}}[] |
46285
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
467 |
\rail@nextbar{4} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
468 |
\rail@term{\isa{\isakeyword{infixr}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
469 |
\rail@endbar |
46290 | 470 |
\rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[] |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
471 |
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] |
46285
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
472 |
\rail@nextbar{5} |
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
473 |
\rail@term{\isa{\isakeyword{binder}}}[] |
46290 | 474 |
\rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[] |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
475 |
\rail@bar |
46285
30953ef09bcd
simplified mixfix (NB: infix is no longer required separately);
wenzelm
parents:
46284
diff
changeset
|
476 |
\rail@nextbar{6} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
477 |
\rail@nont{\isa{prios}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
478 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
479 |
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
480 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
481 |
\rail@end |
46290 | 482 |
\rail@begin{1}{\isa{template}} |
483 |
\rail@nont{\isa{string}}[] |
|
484 |
\rail@end |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
485 |
\rail@begin{2}{\isa{prios}} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
486 |
\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
487 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
488 |
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
489 |
\rail@nextplus{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
490 |
\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
491 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
492 |
\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
493 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
494 |
\end{railoutput} |
28762 | 495 |
|
496 |
||
46290 | 497 |
The string given as \isa{template} may include literal text, |
498 |
spacing, blocks, and arguments (denoted by ``\isa{{\isaliteral{5F}{\isacharunderscore}}}''); the |
|
499 |
special symbol ``\verb|\<index>|'' (printed as ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}}'') |
|
500 |
represents an index argument that specifies an implicit structure |
|
501 |
reference (see also \secref{sec:locale}). Infix and binder |
|
502 |
declarations provide common abbreviations for particular mixfix |
|
503 |
declarations. So in practice, mixfix templates mostly degenerate to |
|
504 |
literal text for concrete syntax, such as ``\verb|++|'' for |
|
505 |
an infix symbol.% |
|
506 |
\end{isamarkuptext}% |
|
507 |
\isamarkuptrue% |
|
508 |
% |
|
509 |
\isamarkupsubsection{The general mixfix form% |
|
510 |
} |
|
511 |
\isamarkuptrue% |
|
512 |
% |
|
513 |
\begin{isamarkuptext}% |
|
514 |
In full generality, mixfix declarations work as follows. |
|
515 |
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 |
|
516 |
\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 |
|
517 |
\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 |
|
518 |
argument positions as indicated by underscores. |
|
28762 | 519 |
|
520 |
Altogether this determines a production for a context-free priority |
|
40406 | 521 |
grammar, where for each argument \isa{{\isaliteral{22}{\isachardoublequote}}i{\isaliteral{22}{\isachardoublequote}}} the syntactic category |
46292 | 522 |
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 |
523 |
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 |
|
524 |
arguments and 1000 for the result.\footnote{Omitting priorities is |
|
525 |
prone to syntactic ambiguities unless the delimiter tokens determine |
|
526 |
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 | 527 |
|
40406 | 528 |
Since \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} may be again a function type, the constant |
28762 | 529 |
type scheme may have more argument positions than the mixfix |
40406 | 530 |
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 |
531 |
\isa{{\isaliteral{22}{\isachardoublequote}}m\ {\isaliteral{3E}{\isachargreater}}\ n{\isaliteral{22}{\isachardoublequote}}} works by attaching concrete notation only to the |
|
532 |
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 | 533 |
instead. If a term has fewer arguments than specified in the mixfix |
534 |
template, the concrete syntax is ignored. |
|
535 |
||
536 |
\medskip A mixfix template may also contain additional directives |
|
537 |
for pretty printing, notably spaces, blocks, and breaks. The |
|
538 |
general template format is a sequence over any of the following |
|
539 |
entities. |
|
540 |
||
541 |
\begin{description} |
|
542 |
||
40406 | 543 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}} is a delimiter, namely a non-empty sequence of |
28762 | 544 |
characters other than the following special characters: |
545 |
||
546 |
\smallskip |
|
547 |
\begin{tabular}{ll} |
|
548 |
\verb|'| & single quote \\ |
|
549 |
\verb|_| & underscore \\ |
|
40406 | 550 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}} & index symbol \\ |
28762 | 551 |
\verb|(| & open parenthesis \\ |
552 |
\verb|)| & close parenthesis \\ |
|
553 |
\verb|/| & slash \\ |
|
554 |
\end{tabular} |
|
555 |
\medskip |
|
556 |
||
557 |
\item \verb|'| escapes the special meaning of these |
|
558 |
meta-characters, producing a literal version of the following |
|
559 |
character, unless that is a blank. |
|
560 |
||
561 |
A single quote followed by a blank separates delimiters, without |
|
562 |
affecting printing, but input tokens may have additional white space |
|
563 |
here. |
|
564 |
||
565 |
\item \verb|_| is an argument position, which stands for a |
|
566 |
certain syntactic category in the underlying grammar. |
|
567 |
||
40406 | 568 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}} is an indexed argument position; this is the place |
28762 | 569 |
where implicit structure arguments can be attached. |
570 |
||
40406 | 571 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}s{\isaliteral{22}{\isachardoublequote}}} is a non-empty sequence of spaces for printing. |
28762 | 572 |
This and the following specifications do not affect parsing at all. |
573 |
||
574 |
\item \verb|(|\isa{n} opens a pretty printing block. The |
|
575 |
optional number specifies how much indentation to add when a line |
|
576 |
break occurs within the block. If the parenthesis is not followed |
|
577 |
by digits, the indentation defaults to 0. A block specified via |
|
578 |
\verb|(00| is unbreakable. |
|
579 |
||
580 |
\item \verb|)| closes a pretty printing block. |
|
581 |
||
582 |
\item \verb|//| forces a line break. |
|
583 |
||
584 |
\item \verb|/|\isa{s} allows a line break. Here \isa{s} |
|
585 |
stands for the string of spaces (zero or more) right after the |
|
586 |
slash. These spaces are printed if the break is \emph{not} taken. |
|
587 |
||
588 |
\end{description} |
|
589 |
||
590 |
The general idea of pretty printing with blocks and breaks is also |
|
46286 | 591 |
described in \cite{paulson-ml2}; it goes back to \cite{Oppen:1980}.% |
28762 | 592 |
\end{isamarkuptext}% |
593 |
\isamarkuptrue% |
|
594 |
% |
|
46290 | 595 |
\isamarkupsubsection{Infixes% |
596 |
} |
|
597 |
\isamarkuptrue% |
|
598 |
% |
|
599 |
\begin{isamarkuptext}% |
|
600 |
Infix operators are specified by convenient short forms that |
|
601 |
abbreviate general mixfix annotations as follows: |
|
602 |
||
603 |
\begin{center} |
|
604 |
\begin{tabular}{lll} |
|
605 |
||
46292 | 606 |
\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 | 607 |
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} & |
608 |
\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 | 609 |
\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 | 610 |
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} & |
611 |
\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 | 612 |
\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 | 613 |
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} & |
614 |
\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|)| \\ |
|
615 |
||
616 |
\end{tabular} |
|
617 |
\end{center} |
|
618 |
||
46292 | 619 |
The mixfix template \verb|"(_ |\isa{sy}\verb|/ _)"| |
620 |
specifies two argument positions; the delimiter is preceded by a |
|
621 |
space and followed by a space or line break; the entire phrase is a |
|
622 |
pretty printing block. |
|
46290 | 623 |
|
624 |
The alternative notation \verb|op|~\isa{sy} is introduced |
|
625 |
in addition. Thus any infix operator may be written in prefix form |
|
626 |
(as in ML), independently of the number of arguments in the term.% |
|
627 |
\end{isamarkuptext}% |
|
628 |
\isamarkuptrue% |
|
629 |
% |
|
630 |
\isamarkupsubsection{Binders% |
|
631 |
} |
|
632 |
\isamarkuptrue% |
|
633 |
% |
|
634 |
\begin{isamarkuptext}% |
|
635 |
A \emph{binder} is a variable-binding construct such as a |
|
636 |
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 |
|
637 |
to \cite{church40}. Isabelle declarations of certain higher-order |
|
46292 | 638 |
operators may be annotated with \indexdef{}{keyword}{binder}\hypertarget{keyword.binder}{\hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}}} annotations |
639 |
as follows: |
|
46290 | 640 |
|
641 |
\begin{center} |
|
642 |
\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|)| |
|
643 |
\end{center} |
|
644 |
||
645 |
This introduces concrete binder syntax \isa{{\isaliteral{22}{\isachardoublequote}}sy\ x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{22}{\isachardoublequote}}}, where |
|
646 |
\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}}}. |
|
647 |
The optional integer \isa{p} specifies the syntactic priority of |
|
648 |
the body; the default is \isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}}, which is also the priority of |
|
649 |
the whole construct. |
|
650 |
||
651 |
Internally, the binder syntax is expanded to something like this: |
|
652 |
\begin{center} |
|
653 |
\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|)| |
|
654 |
\end{center} |
|
655 |
||
656 |
Here \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}} is the nonterminal symbol for a list of |
|
657 |
identifiers with optional type constraints (see also |
|
658 |
\secref{sec:pure-grammar}). The mixfix template \verb|"(3|\isa{sy}\verb|_./ _)"| defines argument positions |
|
659 |
for the bound identifiers and the body, separated by a dot with |
|
660 |
optional line break; the entire phrase is a pretty printing block of |
|
661 |
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 |
|
662 |
syntax ends with a token that may be continued by an identifier |
|
663 |
token at the start of \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}. |
|
664 |
||
665 |
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}}}. |
|
666 |
This works in both directions, for parsing and printing.% |
|
667 |
\end{isamarkuptext}% |
|
668 |
\isamarkuptrue% |
|
669 |
% |
|
46282 | 670 |
\isamarkupsection{Explicit notation \label{sec:notation}% |
28762 | 671 |
} |
672 |
\isamarkuptrue% |
|
673 |
% |
|
674 |
\begin{isamarkuptext}% |
|
675 |
\begin{matharray}{rcll} |
|
40406 | 676 |
\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}}} \\ |
677 |
\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}}} \\ |
|
678 |
\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}}} \\ |
|
679 |
\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}}} \\ |
|
680 |
\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 | 681 |
\end{matharray} |
682 |
||
46288 | 683 |
Commands that introduce new logical entities (terms or types) |
684 |
usually allow to provide mixfix annotations on the spot, which is |
|
685 |
convenient for default notation. Nonetheless, the syntax may be |
|
686 |
modified later on by declarations for explicit notation. This |
|
687 |
allows to add or delete mixfix annotations for of existing logical |
|
688 |
entities within the current context. |
|
689 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
690 |
\begin{railoutput} |
42662 | 691 |
\rail@begin{5}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
692 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
693 |
\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
|
694 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
695 |
\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
|
696 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
697 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
698 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
699 |
\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
700 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
701 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
702 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
703 |
\rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
704 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
705 |
\rail@cr{3} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
706 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
707 |
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
708 |
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
709 |
\rail@nextplus{4} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
710 |
\rail@cterm{\isa{\isakeyword{and}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
711 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
712 |
\rail@end |
42662 | 713 |
\rail@begin{5}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
714 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
715 |
\rail@term{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
716 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
717 |
\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
|
718 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
719 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
720 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
721 |
\rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
722 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
723 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
724 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
725 |
\rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
726 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
727 |
\rail@cr{3} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
728 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
729 |
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] |
42705 | 730 |
\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
|
731 |
\rail@nextplus{4} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
732 |
\rail@cterm{\isa{\isakeyword{and}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
733 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
734 |
\rail@end |
42662 | 735 |
\rail@begin{2}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
736 |
\rail@term{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
737 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
738 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
739 |
\rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
740 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
741 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
742 |
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] |
42705 | 743 |
\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
|
744 |
\rail@nextplus{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
745 |
\rail@cterm{\isa{\isakeyword{and}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
746 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
747 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
748 |
\end{railoutput} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
749 |
|
28762 | 750 |
|
751 |
\begin{description} |
|
752 |
||
40406 | 753 |
\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 | 754 |
syntax with an existing type constructor. The arity of the |
755 |
constructor is retrieved from the context. |
|
46282 | 756 |
|
40406 | 757 |
\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 | 758 |
the present context. |
759 |
||
40406 | 760 |
\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 | 761 |
syntax with an existing constant or fixed variable. The type |
762 |
declaration of the given entity is retrieved from the context. |
|
46282 | 763 |
|
40406 | 764 |
\item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, |
28762 | 765 |
but removes the specified syntax annotation from the present |
766 |
context. |
|
767 |
||
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
|
768 |
\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
|
769 |
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
|
770 |
|
46289 | 771 |
\end{description}% |
28762 | 772 |
\end{isamarkuptext}% |
773 |
\isamarkuptrue% |
|
774 |
% |
|
775 |
\isamarkupsection{The Pure syntax \label{sec:pure-syntax}% |
|
776 |
} |
|
777 |
\isamarkuptrue% |
|
778 |
% |
|
46282 | 779 |
\isamarkupsubsection{Lexical matters \label{sec:inner-lex}% |
780 |
} |
|
781 |
\isamarkuptrue% |
|
782 |
% |
|
783 |
\begin{isamarkuptext}% |
|
784 |
The inner lexical syntax vaguely resembles the outer one |
|
785 |
(\secref{sec:outer-lex}), but some details are different. There are |
|
786 |
two main categories of inner syntax tokens: |
|
787 |
||
788 |
\begin{enumerate} |
|
789 |
||
790 |
\item \emph{delimiters} --- the literal tokens occurring in |
|
791 |
productions of the given priority grammar (cf.\ |
|
792 |
\secref{sec:priority-grammar}); |
|
793 |
||
794 |
\item \emph{named tokens} --- various categories of identifiers etc. |
|
795 |
||
796 |
\end{enumerate} |
|
797 |
||
798 |
Delimiters override named tokens and may thus render certain |
|
799 |
identifiers inaccessible. Sometimes the logical context admits |
|
800 |
alternative ways to refer to the same entity, potentially via |
|
801 |
qualified names. |
|
802 |
||
803 |
\medskip The categories for named tokens are defined once and for |
|
804 |
all as follows, reusing some categories of the outer token syntax |
|
805 |
(\secref{sec:outer-lex}). |
|
806 |
||
807 |
\begin{center} |
|
808 |
\begin{supertabular}{rcl} |
|
809 |
\indexdef{inner}{syntax}{id}\hypertarget{syntax.inner.id}{\hyperlink{syntax.inner.id}{\mbox{\isa{id}}}} & = & \indexref{}{syntax}{ident}\hyperlink{syntax.ident}{\mbox{\isa{ident}}} \\ |
|
810 |
\indexdef{inner}{syntax}{longid}\hypertarget{syntax.inner.longid}{\hyperlink{syntax.inner.longid}{\mbox{\isa{longid}}}} & = & \indexref{}{syntax}{longident}\hyperlink{syntax.longident}{\mbox{\isa{longident}}} \\ |
|
811 |
\indexdef{inner}{syntax}{var}\hypertarget{syntax.inner.var}{\hyperlink{syntax.inner.var}{\mbox{\isa{var}}}} & = & \indexref{}{syntax}{var}\hyperlink{syntax.var}{\mbox{\isa{var}}} \\ |
|
812 |
\indexdef{inner}{syntax}{tid}\hypertarget{syntax.inner.tid}{\hyperlink{syntax.inner.tid}{\mbox{\isa{tid}}}} & = & \indexref{}{syntax}{typefree}\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}} \\ |
|
813 |
\indexdef{inner}{syntax}{tvar}\hypertarget{syntax.inner.tvar}{\hyperlink{syntax.inner.tvar}{\mbox{\isa{tvar}}}} & = & \indexref{}{syntax}{typevar}\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}} \\ |
|
814 |
\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}}} \\ |
|
815 |
\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}}} \\ |
|
816 |
\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}}} \\ |
|
817 |
||
46483 | 818 |
\indexdef{inner}{syntax}{str\_token}\hypertarget{syntax.inner.str-token}{\hyperlink{syntax.inner.str-token}{\mbox{\isa{str{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \verb|''| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|''| \\ |
46282 | 819 |
\end{supertabular} |
820 |
\end{center} |
|
821 |
||
46483 | 822 |
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.str-token}{\mbox{\isa{str{\isaliteral{5F}{\isacharunderscore}}token}}} are not used in Pure. Object-logics may implement numerals |
46282 | 823 |
and string constants by adding appropriate syntax declarations, |
824 |
together with some translation functions (e.g.\ see Isabelle/HOL). |
|
825 |
||
826 |
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 |
|
827 |
robust access to the respective tokens: the syntax tree holds a |
|
828 |
syntactic constant instead of a free variable.% |
|
829 |
\end{isamarkuptext}% |
|
830 |
\isamarkuptrue% |
|
831 |
% |
|
28762 | 832 |
\isamarkupsubsection{Priority grammars \label{sec:priority-grammar}% |
833 |
} |
|
834 |
\isamarkuptrue% |
|
835 |
% |
|
836 |
\begin{isamarkuptext}% |
|
837 |
A context-free grammar consists of a set of \emph{terminal |
|
838 |
symbols}, a set of \emph{nonterminal symbols} and a set of |
|
40406 | 839 |
\emph{productions}. Productions have the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C67616D6D613E}{\isasymgamma}}{\isaliteral{22}{\isachardoublequote}}}, |
840 |
where \isa{A} is a nonterminal and \isa{{\isaliteral{5C3C67616D6D613E}{\isasymgamma}}} is a string of |
|
28762 | 841 |
terminals and nonterminals. One designated nonterminal is called |
842 |
the \emph{root symbol}. The language defined by the grammar |
|
843 |
consists of all strings of terminals that can be derived from the |
|
844 |
root symbol by applying productions as rewrite rules. |
|
845 |
||
846 |
The standard Isabelle parser for inner syntax uses a \emph{priority |
|
847 |
grammar}. Each nonterminal is decorated by an integer priority: |
|
40406 | 848 |
\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 |
849 |
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 | 850 |
priority grammar can be translated into a normal context-free |
851 |
grammar by introducing new nonterminals and productions. |
|
852 |
||
853 |
\medskip Formally, a set of context free productions \isa{G} |
|
40406 | 854 |
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. |
855 |
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} |
|
856 |
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 | 857 |
|
858 |
\medskip The following grammar for arithmetic expressions |
|
859 |
demonstrates how binding power and associativity of operators can be |
|
860 |
enforced by priorities. |
|
861 |
||
862 |
\begin{center} |
|
863 |
\begin{tabular}{rclr} |
|
40406 | 864 |
\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|)| \\ |
865 |
\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| \\ |
|
866 |
\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}}} \\ |
|
867 |
\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}}} \\ |
|
868 |
\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 | 869 |
\end{tabular} |
870 |
\end{center} |
|
871 |
The choice of priorities determines that \verb|-| binds |
|
872 |
tighter than \verb|*|, which binds tighter than \verb|+|. Furthermore \verb|+| associates to the left and |
|
873 |
\verb|*| to the right. |
|
874 |
||
875 |
\medskip For clarity, grammars obey these conventions: |
|
876 |
\begin{itemize} |
|
877 |
||
878 |
\item All priorities must lie between 0 and 1000. |
|
879 |
||
880 |
\item Priority 0 on the right-hand side and priority 1000 on the |
|
881 |
left-hand side may be omitted. |
|
882 |
||
40406 | 883 |
\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 | 884 |
a column on the far right. |
885 |
||
40406 | 886 |
\item Alternatives are separated by \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}. |
28762 | 887 |
|
40406 | 888 |
\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 | 889 |
but obvious way. |
890 |
||
891 |
\end{itemize} |
|
892 |
||
893 |
Using these conventions, the example grammar specification above |
|
894 |
takes the form: |
|
895 |
\begin{center} |
|
896 |
\begin{tabular}{rclc} |
|
40406 | 897 |
\isa{A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \verb|(| \isa{A} \verb|)| \\ |
898 |
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|0| & \qquad\qquad \\ |
|
899 |
& \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}}} \\ |
|
900 |
& \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}}} \\ |
|
901 |
& \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 | 902 |
\end{tabular} |
903 |
\end{center}% |
|
904 |
\end{isamarkuptext}% |
|
905 |
\isamarkuptrue% |
|
906 |
% |
|
46290 | 907 |
\isamarkupsubsection{The Pure grammar \label{sec:pure-grammar}% |
28762 | 908 |
} |
909 |
\isamarkuptrue% |
|
910 |
% |
|
911 |
\begin{isamarkuptext}% |
|
46287 | 912 |
The priority grammar of the \isa{{\isaliteral{22}{\isachardoublequote}}Pure{\isaliteral{22}{\isachardoublequote}}} theory is defined |
913 |
approximately like this: |
|
28762 | 914 |
|
915 |
\begin{center} |
|
916 |
\begin{supertabular}{rclr} |
|
917 |
||
40406 | 918 |
\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 | 919 |
|
920 |
\indexdef{inner}{syntax}{prop}\hypertarget{syntax.inner.prop}{\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}} & = & \verb|(| \isa{prop} \verb|)| \\ |
|
40406 | 921 |
& \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}}} \\ |
922 |
& \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}}} \\ |
|
923 |
& \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}}} \\ |
|
924 |
& \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}}} \\ |
|
925 |
& \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}}} \\ |
|
926 |
& \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}}} \\ |
|
927 |
& \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}}} \\ |
|
928 |
& \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}}} \\ |
|
929 |
& \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}}} \\ |
|
930 |
& \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}}} \\ |
|
931 |
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|OFCLASS| \verb|(| \isa{type} \verb|,| \isa{logic} \verb|)| \\ |
|
932 |
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|SORT_CONSTRAINT| \verb|(| \isa{type} \verb|)| \\ |
|
933 |
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|TERM| \isa{logic} \\ |
|
934 |
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|PROP| \isa{aprop} \\\\ |
|
28762 | 935 |
|
28857 | 936 |
\indexdef{inner}{syntax}{aprop}\hypertarget{syntax.inner.aprop}{\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}}} & = & \verb|(| \isa{aprop} \verb|)| \\ |
40406 | 937 |
& \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|...| \\ |
938 |
& \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 | 939 |
& \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 | 940 |
& \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 | 941 |
|
942 |
\indexdef{inner}{syntax}{logic}\hypertarget{syntax.inner.logic}{\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}} & = & \verb|(| \isa{logic} \verb|)| \\ |
|
40406 | 943 |
& \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}}} \\ |
944 |
& \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|...| \\ |
|
945 |
& \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 | 946 |
& \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 | 947 |
& \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 | 948 |
& \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 | 949 |
& \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}}} \\ |
950 |
& \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 | 951 |
& \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|&&&| \\ |
952 |
& \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 | 953 |
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|TYPE| \verb|(| \isa{type} \verb|)| \\\\ |
28762 | 954 |
|
40406 | 955 |
\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|_| \\ |
956 |
& \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}}} \\ |
|
957 |
& \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 | 958 |
|
46287 | 959 |
\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}}} \\\\ |
960 |
||
40406 | 961 |
\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 | 962 |
|
963 |
\indexdef{inner}{syntax}{pttrn}\hypertarget{syntax.inner.pttrn}{\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}}} & = & \isa{idt} \\\\ |
|
964 |
||
40406 | 965 |
\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 | 966 |
|
967 |
\indexdef{inner}{syntax}{type}\hypertarget{syntax.inner.type}{\hyperlink{syntax.inner.type}{\mbox{\isa{type}}}} & = & \verb|(| \isa{type} \verb|)| \\ |
|
40406 | 968 |
& \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|_| \\ |
969 |
& \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 | 970 |
& \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}}} \\ |
971 |
& \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 | 972 |
& \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}}} \\ |
973 |
& \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}}} \\ |
|
974 |
& \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 | 975 |
& \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}}} \\ |
976 |
\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 | 977 |
|
46287 | 978 |
\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|{}| \\ |
979 |
& \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|}| \\ |
|
980 |
\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 | 981 |
\end{supertabular} |
982 |
\end{center} |
|
983 |
||
984 |
\medskip Here literal terminals are printed \verb|verbatim|; |
|
985 |
see also \secref{sec:inner-lex} for further token categories of the |
|
986 |
inner syntax. The meaning of the nonterminals defined by the above |
|
987 |
grammar is as follows: |
|
988 |
||
989 |
\begin{description} |
|
990 |
||
991 |
\item \indexref{inner}{syntax}{any}\hyperlink{syntax.inner.any}{\mbox{\isa{any}}} denotes any term. |
|
992 |
||
993 |
\item \indexref{inner}{syntax}{prop}\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} denotes meta-level propositions, |
|
994 |
which are terms of type \isa{prop}. The syntax of such formulae of |
|
995 |
the meta-logic is carefully distinguished from usual conventions for |
|
40406 | 996 |
object-logics. In particular, plain \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-term notation is |
28762 | 997 |
\emph{not} recognized as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}. |
998 |
||
999 |
\item \indexref{inner}{syntax}{aprop}\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}} denotes atomic propositions, which |
|
1000 |
are embedded into regular \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} by means of an |
|
1001 |
explicit \verb|PROP| token. |
|
1002 |
||
1003 |
Terms of type \isa{prop} with non-constant head, e.g.\ a plain |
|
1004 |
variable, are printed in this form. Constants that yield type \isa{prop} are expected to provide their own concrete syntax; otherwise |
|
1005 |
the printed version will appear like \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} and |
|
1006 |
cannot be parsed again as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}. |
|
1007 |
||
1008 |
\item \indexref{inner}{syntax}{logic}\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} denotes arbitrary terms of a |
|
1009 |
logical type, excluding type \isa{prop}. This is the main |
|
40406 | 1010 |
syntactic category of object-logic entities, covering plain \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-term notation (variables, abstraction, application), plus |
28762 | 1011 |
anything defined by the user. |
1012 |
||
1013 |
When specifying notation for logical entities, all logical types |
|
1014 |
(excluding \isa{prop}) are \emph{collapsed} to this single category |
|
1015 |
of \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}. |
|
1016 |
||
46287 | 1017 |
\item \indexref{inner}{syntax}{index}\hyperlink{syntax.inner.index}{\mbox{\isa{index}}} denotes an optional index term for |
1018 |
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 |
|
1019 |
introduce indexed notation. |
|
1020 |
||
28762 | 1021 |
\item \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} denotes identifiers, possibly |
1022 |
constrained by types. |
|
1023 |
||
1024 |
\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 | 1025 |
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 | 1026 |
|
1027 |
\item \indexref{inner}{syntax}{pttrn}\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}} and \indexref{inner}{syntax}{pttrns}\hyperlink{syntax.inner.pttrns}{\mbox{\isa{pttrns}}} |
|
1028 |
denote patterns for abstraction, cases bindings etc. In Pure, these |
|
1029 |
categories start as a merely copy of \hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} and |
|
1030 |
\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, respectively. Object-logics may add |
|
1031 |
additional productions for binding forms. |
|
1032 |
||
1033 |
\item \indexref{inner}{syntax}{type}\hyperlink{syntax.inner.type}{\mbox{\isa{type}}} denotes types of the meta-logic. |
|
1034 |
||
1035 |
\item \indexref{inner}{syntax}{sort}\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}} denotes meta-level sorts. |
|
1036 |
||
1037 |
\end{description} |
|
1038 |
||
1039 |
Here are some further explanations of certain syntax features. |
|
1040 |
||
1041 |
\begin{itemize} |
|
1042 |
||
40406 | 1043 |
\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 |
1044 |
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 | 1045 |
constructor applied to \isa{nat}. To avoid this interpretation, |
40406 | 1046 |
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 | 1047 |
|
40406 | 1048 |
\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 | 1049 |
sequence of identifiers. |
1050 |
||
1051 |
\item Type constraints for terms bind very weakly. For example, |
|
40406 | 1052 |
\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 |
1053 |
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 | 1054 |
|
1055 |
\item Constraints may be either written with two literal colons |
|
1056 |
``\verb|::|'' or the double-colon symbol \verb|\<Colon>|, |
|
1057 |
which actually looks exactly the same in some {\LaTeX} styles. |
|
1058 |
||
1059 |
\item Dummy variables (written as underscore) may occur in different |
|
1060 |
roles. |
|
1061 |
||
1062 |
\begin{description} |
|
1063 |
||
40406 | 1064 |
\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 | 1065 |
anonymous inference parameter, which is filled-in according to the |
1066 |
most general type produced by the type-checking phase. |
|
1067 |
||
40406 | 1068 |
\item A bound ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'' refers to a vacuous abstraction, where |
28762 | 1069 |
the body does not refer to the binding introduced here. As in the |
40406 | 1070 |
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 | 1071 |
|
40406 | 1072 |
\item A free ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'' refers to an implicit outer binding. |
1073 |
Higher definitional packages usually allow forms like \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequote}}}. |
|
28762 | 1074 |
|
40406 | 1075 |
\item A schematic ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'' (within a term pattern, see |
28762 | 1076 |
\secref{sec:term-decls}) refers to an anonymous variable that is |
1077 |
implicitly abstracted over its context of locally bound variables. |
|
40406 | 1078 |
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 | 1079 |
using both bound and schematic dummies. |
1080 |
||
1081 |
\end{description} |
|
1082 |
||
1083 |
\item The three literal dots ``\verb|...|'' may be also |
|
1084 |
written as ellipsis symbol \verb|\<dots>|. In both cases this |
|
1085 |
refers to a special schematic variable, which is bound in the |
|
1086 |
context. This special term abbreviation works nicely with |
|
1087 |
calculational reasoning (\secref{sec:calculation}). |
|
1088 |
||
46287 | 1089 |
\item \verb|CONST| ensures that the given identifier is treated |
1090 |
as constant term, and passed through the parse tree in fully |
|
1091 |
internalized form. This is particularly relevant for translation |
|
1092 |
rules (\secref{sec:syn-trans}), notably on the RHS. |
|
1093 |
||
1094 |
\item \verb|XCONST| is similar to \verb|CONST|, but |
|
1095 |
retains the constant name as given. This is only relevant to |
|
1096 |
translation rules (\secref{sec:syn-trans}), notably on the LHS. |
|
1097 |
||
28762 | 1098 |
\end{itemize}% |
1099 |
\end{isamarkuptext}% |
|
1100 |
\isamarkuptrue% |
|
1101 |
% |
|
46282 | 1102 |
\isamarkupsubsection{Inspecting the syntax% |
28762 | 1103 |
} |
1104 |
\isamarkuptrue% |
|
1105 |
% |
|
1106 |
\begin{isamarkuptext}% |
|
46282 | 1107 |
\begin{matharray}{rcl} |
1108 |
\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}}} \\ |
|
1109 |
\end{matharray} |
|
28762 | 1110 |
|
46282 | 1111 |
\begin{description} |
28762 | 1112 |
|
46282 | 1113 |
\item \hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}syntax}}}} prints the inner syntax of the |
1114 |
current context. The output can be quite large; the most important |
|
1115 |
sections are explained below. |
|
28762 | 1116 |
|
46282 | 1117 |
\begin{description} |
28762 | 1118 |
|
46282 | 1119 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}lexicon{\isaliteral{22}{\isachardoublequote}}} lists the delimiters of the inner token |
1120 |
language; see \secref{sec:inner-lex}. |
|
28762 | 1121 |
|
46282 | 1122 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}prods{\isaliteral{22}{\isachardoublequote}}} lists the productions of the underlying |
1123 |
priority grammar; see \secref{sec:priority-grammar}. |
|
28762 | 1124 |
|
46282 | 1125 |
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 |
1126 |
\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 |
|
1127 |
trees; they also guide the pretty printer. |
|
28762 | 1128 |
|
46282 | 1129 |
Productions without such parse tree names are called \emph{copy |
1130 |
productions}. Their right-hand side must have exactly one |
|
1131 |
nonterminal symbol (or named token). The parser does not create a |
|
1132 |
new parse tree node for copy productions, but simply returns the |
|
1133 |
parse tree of the right-hand symbol. |
|
1134 |
||
1135 |
If the right-hand side of a copy production consists of a single |
|
1136 |
nonterminal without any delimiters, then it is called a \emph{chain |
|
1137 |
production}. Chain productions act as abbreviations: conceptually, |
|
1138 |
they are removed from the grammar by adding new productions. |
|
1139 |
Priority information attached to chain productions is ignored; only |
|
1140 |
the dummy value \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} is displayed. |
|
28762 | 1141 |
|
46282 | 1142 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}print\ modes{\isaliteral{22}{\isachardoublequote}}} lists the alternative print modes |
1143 |
provided by this grammar; see \secref{sec:print-modes}. |
|
1144 |
||
1145 |
\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 |
|
1146 |
syntax translations (macros); see \secref{sec:syn-trans}. |
|
28762 | 1147 |
|
46282 | 1148 |
\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 |
1149 |
translation functions for abstract syntax trees, which are only |
|
1150 |
required in very special situations; see \secref{sec:tr-funs}. |
|
29158 | 1151 |
|
46282 | 1152 |
\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}}} |
1153 |
list the sets of constants that invoke regular translation |
|
1154 |
functions; see \secref{sec:tr-funs}. |
|
1155 |
||
1156 |
\end{description} |
|
1157 |
||
1158 |
\end{description}% |
|
28762 | 1159 |
\end{isamarkuptext}% |
1160 |
\isamarkuptrue% |
|
1161 |
% |
|
46291 | 1162 |
\isamarkupsubsection{Ambiguity of parsed expressions% |
1163 |
} |
|
1164 |
\isamarkuptrue% |
|
1165 |
% |
|
1166 |
\begin{isamarkuptext}% |
|
1167 |
\begin{tabular}{rcll} |
|
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
1168 |
\indexdef{}{attribute}{syntax\_ambiguity\_warning}\hypertarget{attribute.syntax-ambiguity-warning}{\hyperlink{attribute.syntax-ambiguity-warning}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}warning}}}} & : & \isa{attribute} & default \isa{true} \\ |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46494
diff
changeset
|
1169 |
\indexdef{}{attribute}{syntax\_ambiguity\_limit}\hypertarget{attribute.syntax-ambiguity-limit}{\hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\ |
46291 | 1170 |
\end{tabular} |
1171 |
||
1172 |
Depending on the grammar and the given input, parsing may be |
|
1173 |
ambiguous. Isabelle lets the Earley parser enumerate all possible |
|
1174 |
parse trees, and then tries to make the best out of the situation. |
|
1175 |
Terms that cannot be type-checked are filtered out, which often |
|
1176 |
leads to a unique result in the end. Unlike regular type |
|
1177 |
reconstruction, which is applied to the whole collection of input |
|
1178 |
terms simultaneously, the filtering stage only treats each given |
|
1179 |
term in isolation. Filtering is also not attempted for individual |
|
1180 |
types or raw ASTs (as required for \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}). |
|
1181 |
||
1182 |
Certain warning or error messages are printed, depending on the |
|
1183 |
situation and the given configuration options. Parsing ultimately |
|
1184 |
fails, if multiple results remain after the filtering phase. |
|
1185 |
||
1186 |
\begin{description} |
|
1187 |
||
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
1188 |
\item \hyperlink{attribute.syntax-ambiguity-warning}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}warning}}} controls output of |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
1189 |
explicit warning messages about syntax ambiguity. |
46291 | 1190 |
|
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46494
diff
changeset
|
1191 |
\item \hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}} determines the number of |
46291 | 1192 |
resulting parse trees that are shown as part of the printed message |
1193 |
in case of an ambiguity. |
|
1194 |
||
1195 |
\end{description}% |
|
1196 |
\end{isamarkuptext}% |
|
1197 |
\isamarkuptrue% |
|
1198 |
% |
|
48113 | 1199 |
\isamarkupsection{Syntax transformations \label{sec:syntax-transformations}% |
1200 |
} |
|
1201 |
\isamarkuptrue% |
|
1202 |
% |
|
1203 |
\begin{isamarkuptext}% |
|
1204 |
The inner syntax engine of Isabelle provides separate |
|
1205 |
mechanisms to transform parse trees either as rewrite systems on |
|
1206 |
first-order ASTs (\secref{sec:syn-trans}), or ML functions on ASTs |
|
1207 |
or syntactic \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-terms (\secref{sec:tr-funs}). This works |
|
1208 |
both for parsing and printing, as outlined in |
|
1209 |
\figref{fig:parse-print}. |
|
1210 |
||
1211 |
\begin{figure}[htbp] |
|
1212 |
\begin{center} |
|
1213 |
\begin{tabular}{cl} |
|
1214 |
string & \\ |
|
1215 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & lexer + parser \\ |
|
1216 |
parse tree & \\ |
|
1217 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & parse AST translation \\ |
|
1218 |
AST & \\ |
|
1219 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & AST rewriting (macros) \\ |
|
1220 |
AST & \\ |
|
1221 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & parse translation \\ |
|
1222 |
--- pre-term --- & \\ |
|
1223 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & print translation \\ |
|
1224 |
AST & \\ |
|
1225 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & AST rewriting (macros) \\ |
|
1226 |
AST & \\ |
|
1227 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F776E3E}{\isasymdown}}{\isaliteral{22}{\isachardoublequote}}} & print AST translation \\ |
|
1228 |
string & |
|
1229 |
\end{tabular} |
|
1230 |
\end{center} |
|
1231 |
\caption{Parsing and printing with translations}\label{fig:parse-print} |
|
1232 |
\end{figure} |
|
1233 |
||
1234 |
These intermediate syntax tree formats eventually lead to a pre-term |
|
1235 |
with all names and binding scopes resolved, but most type |
|
1236 |
information still missing. Explicit type constraints might be given by |
|
1237 |
the user, or implicit position information by the system --- both |
|
48816 | 1238 |
need to be passed-through carefully by syntax transformations. |
48113 | 1239 |
|
1240 |
Pre-terms are further processed by the so-called \emph{check} and |
|
1241 |
\emph{unckeck} phases that are intertwined with type-inference (see |
|
1242 |
also \cite{isabelle-implementation}). The latter allows to operate |
|
1243 |
on higher-order abstract syntax with proper binding and type |
|
1244 |
information already available. |
|
1245 |
||
1246 |
As a rule of thumb, anything that manipulates bindings of variables |
|
1247 |
or constants needs to be implemented as syntax transformation (see |
|
1248 |
below). Anything else is better done via check/uncheck: a prominent |
|
1249 |
example application is the \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}} concept of |
|
1250 |
Isabelle/Pure.% |
|
1251 |
\end{isamarkuptext}% |
|
1252 |
\isamarkuptrue% |
|
1253 |
% |
|
48115 | 1254 |
\isamarkupsubsection{Abstract syntax trees \label{sec:ast}% |
48113 | 1255 |
} |
1256 |
\isamarkuptrue% |
|
1257 |
% |
|
1258 |
\begin{isamarkuptext}% |
|
48114 | 1259 |
The ML datatype \verb|Ast.ast| explicitly represents the |
1260 |
intermediate AST format that is used for syntax rewriting |
|
1261 |
(\secref{sec:syn-trans}). It is defined in ML as follows: |
|
1262 |
\begin{ttbox} |
|
1263 |
datatype ast = |
|
1264 |
Constant of string | |
|
1265 |
Variable of string | |
|
1266 |
Appl of ast list |
|
1267 |
\end{ttbox} |
|
1268 |
||
1269 |
An AST is either an atom (constant or variable) or a list of (at |
|
1270 |
least two) subtrees. Occasional diagnostic output of ASTs uses |
|
1271 |
notation that resembles S-expression of LISP. Constant atoms are |
|
1272 |
shown as quoted strings, variable atoms as non-quoted strings and |
|
1273 |
applications as a parenthesized list of subtrees. For example, the |
|
1274 |
AST |
|
1275 |
\begin{verbatim} |
|
1276 |
Ast.Appl |
|
1277 |
[Ast.Constant "_abs", Ast.Variable "x", Ast.Variable "t"] |
|
1278 |
\end{verbatim} |
|
1279 |
is pretty-printed as \verb|("_abs" x t)|. Note that |
|
1280 |
\verb|()| and \verb|(x)| are excluded as ASTs, because |
|
1281 |
they have too few subtrees. |
|
1282 |
||
1283 |
\medskip AST application is merely a pro-forma mechanism to indicate |
|
1284 |
certain syntactic structures. Thus \verb|(c a b)| could mean |
|
1285 |
either term application or type application, depending on the |
|
1286 |
syntactic context. |
|
1287 |
||
1288 |
Nested application like \verb|(("_abs" x t) u)| is also |
|
1289 |
possible, but ASTs are definitely first-order: the syntax constant |
|
1290 |
\verb|"_abs"| does not bind the \verb|x| in any way. |
|
1291 |
Proper bindings are introduced in later stages of the term syntax, |
|
1292 |
where \verb|("_abs" x t)| becomes an \verb|Abs| node and |
|
1293 |
occurrences of \verb|x| in \verb|t| are replaced by bound |
|
1294 |
variables (represented as de-Bruijn indices).% |
|
1295 |
\end{isamarkuptext}% |
|
1296 |
\isamarkuptrue% |
|
1297 |
% |
|
48115 | 1298 |
\isamarkupsubsubsection{AST constants versus variables% |
48114 | 1299 |
} |
1300 |
\isamarkuptrue% |
|
1301 |
% |
|
1302 |
\begin{isamarkuptext}% |
|
1303 |
Depending on the situation --- input syntax, output syntax, |
|
1304 |
translation patterns --- the distinction of atomic asts as \verb|Ast.Constant| versus \verb|Ast.Variable| serves slightly different |
|
1305 |
purposes. |
|
1306 |
||
1307 |
Input syntax of a term such as \isa{{\isaliteral{22}{\isachardoublequote}}f\ a\ b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequote}}} does not yet |
|
1308 |
indicate the scopes of atomic entities \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2C}{\isacharcomma}}\ a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{22}{\isachardoublequote}}}: they |
|
1309 |
could be global constants or local variables, even bound ones |
|
1310 |
depending on the context of the term. \verb|Ast.Variable| leaves |
|
1311 |
this choice still open: later syntax layers (or translation |
|
1312 |
functions) may capture such a variable to determine its role |
|
1313 |
specifically, to make it a constant, bound variable, free variable |
|
1314 |
etc. In contrast, syntax translations that introduce already known |
|
1315 |
constants would rather do it via \verb|Ast.Constant| to prevent |
|
1316 |
accidental re-interpretation later on. |
|
1317 |
||
1318 |
Output syntax turns term constants into \verb|Ast.Constant| and |
|
1319 |
variables (free or schematic) into \verb|Ast.Variable|. This |
|
1320 |
information is precise when printing fully formal \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-terms. |
|
1321 |
||
1322 |
In AST translation patterns (\secref{sec:syn-trans}) the system |
|
1323 |
guesses from the current theory context which atoms should be |
|
1324 |
treated as constant versus variable for the matching process. |
|
1325 |
Sometimes this needs to be indicated more explicitly using \isa{{\isaliteral{22}{\isachardoublequote}}CONST\ c{\isaliteral{22}{\isachardoublequote}}} inside the term language. It is also possible to use |
|
1326 |
\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} declarations (without mixfix annotation) to |
|
1327 |
enforce that certain unqualified names are always treated as |
|
1328 |
constant within the syntax machinery. |
|
1329 |
||
1330 |
\medskip For ASTs that represent the language of types or sorts, the |
|
1331 |
situation is much simpler, since the concrete syntax already |
|
1332 |
distinguishes type variables from type constants (constructors). So |
|
1333 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ foo{\isaliteral{22}{\isachardoublequote}}} corresponds to an AST application of some |
|
1334 |
constant for \isa{foo} and variable arguments for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}} and |
|
1335 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequote}}}. Note that the postfix application is merely a feature |
|
1336 |
of the concrete syntax, while in the AST the constructor occurs in |
|
1337 |
head position.% |
|
1338 |
\end{isamarkuptext}% |
|
1339 |
\isamarkuptrue% |
|
1340 |
% |
|
1341 |
\isamarkupsubsubsection{Authentic syntax names% |
|
1342 |
} |
|
1343 |
\isamarkuptrue% |
|
1344 |
% |
|
1345 |
\begin{isamarkuptext}% |
|
1346 |
Naming constant entities within ASTs is another delicate |
|
1347 |
issue. Unqualified names are looked up in the name space tables in |
|
1348 |
the last stage of parsing, after all translations have been applied. |
|
1349 |
Since syntax transformations do not know about this later name |
|
1350 |
resolution yet, there can be surprises in boundary cases. |
|
1351 |
||
1352 |
\emph{Authentic syntax names} for \verb|Ast.Constant| avoid this |
|
1353 |
problem: the fully-qualified constant name with a special prefix for |
|
1354 |
its formal category (\isa{{\isaliteral{22}{\isachardoublequote}}class{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}type{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}const{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}fixed{\isaliteral{22}{\isachardoublequote}}}) represents the information faithfully |
|
1355 |
within the untyped AST format. Accidental overlap with free or |
|
1356 |
bound variables is excluded as well. Authentic syntax names work |
|
1357 |
implicitly in the following situations: |
|
1358 |
||
1359 |
\begin{itemize} |
|
1360 |
||
1361 |
\item Input of term constants (or fixed variables) that are |
|
1362 |
introduced by concrete syntax via \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}: the |
|
1363 |
correspondence of a particular grammar production to some known term |
|
1364 |
entity is preserved. |
|
1365 |
||
48816 | 1366 |
\item Input of type constants (constructors) and type classes --- |
48114 | 1367 |
thanks to explicit syntactic distinction independently on the |
1368 |
context. |
|
1369 |
||
1370 |
\item Output of term constants, type constants, type classes --- |
|
1371 |
this information is already available from the internal term to be |
|
1372 |
printed. |
|
1373 |
||
1374 |
\end{itemize} |
|
1375 |
||
1376 |
In other words, syntax transformations that operate on input terms |
|
48816 | 1377 |
written as prefix applications are difficult to make robust. |
1378 |
Luckily, this case rarely occurs in practice, because syntax forms |
|
1379 |
to be translated usually correspond to some bits of concrete |
|
1380 |
notation.% |
|
48113 | 1381 |
\end{isamarkuptext}% |
1382 |
\isamarkuptrue% |
|
1383 |
% |
|
1384 |
\isamarkupsubsection{Raw syntax and translations \label{sec:syn-trans}% |
|
28762 | 1385 |
} |
1386 |
\isamarkuptrue% |
|
1387 |
% |
|
1388 |
\begin{isamarkuptext}% |
|
48117 | 1389 |
\begin{tabular}{rcll} |
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
40879
diff
changeset
|
1390 |
\indexdef{}{command}{nonterminal}\hypertarget{command.nonterminal}{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ |
40406 | 1391 |
\indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ |
1392 |
\indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}syntax}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
1393 |
\indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
1394 |
\indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}translations}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
48117 | 1395 |
\indexdef{}{attribute}{syntax\_ast\_trace}\hypertarget{attribute.syntax-ast-trace}{\hyperlink{attribute.syntax-ast-trace}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}trace}}}} & : & \isa{attribute} & default \isa{false} \\ |
1396 |
\indexdef{}{attribute}{syntax\_ast\_stats}\hypertarget{attribute.syntax-ast-stats}{\hyperlink{attribute.syntax-ast-stats}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}stats}}}} & : & \isa{attribute} & default \isa{false} \\ |
|
1397 |
\end{tabular} |
|
28762 | 1398 |
|
46292 | 1399 |
Unlike mixfix notation for existing formal entities |
1400 |
(\secref{sec:notation}), raw syntax declarations provide full access |
|
48115 | 1401 |
to the priority grammar of the inner syntax, without any sanity |
1402 |
checks. This includes additional syntactic categories (via |
|
1403 |
\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}) and free-form grammar productions (via |
|
1404 |
\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}). Additional syntax translations (or macros, via |
|
1405 |
\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}) are required to turn resulting parse trees |
|
1406 |
into proper representations of formal entities again. |
|
46292 | 1407 |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1408 |
\begin{railoutput} |
42662 | 1409 |
\rail@begin{2}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1410 |
\rail@term{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1411 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1412 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1413 |
\rail@nextplus{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1414 |
\rail@cterm{\isa{\isakeyword{and}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1415 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1416 |
\rail@end |
42662 | 1417 |
\rail@begin{2}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1418 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1419 |
\rail@term{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1420 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1421 |
\rail@term{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}syntax}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1422 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1423 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1424 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1425 |
\rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1426 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1427 |
\rail@plus |
46494
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1428 |
\rail@nont{\isa{constdecl}}[] |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1429 |
\rail@nextplus{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1430 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1431 |
\rail@end |
42662 | 1432 |
\rail@begin{7}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1433 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1434 |
\rail@term{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1435 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1436 |
\rail@term{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}translations}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1437 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1438 |
\rail@plus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1439 |
\rail@nont{\isa{transpat}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1440 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1441 |
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1442 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1443 |
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1444 |
\rail@nextbar{2} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1445 |
\rail@term{\isa{{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1446 |
\rail@nextbar{3} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1447 |
\rail@term{\isa{{\isaliteral{5C3C72696768746C656674686172706F6F6E733E}{\isasymrightleftharpoons}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1448 |
\rail@nextbar{4} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1449 |
\rail@term{\isa{{\isaliteral{5C3C7269676874686172706F6F6E75703E}{\isasymrightharpoonup}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1450 |
\rail@nextbar{5} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1451 |
\rail@term{\isa{{\isaliteral{5C3C6C656674686172706F6F6E646F776E3E}{\isasymleftharpoondown}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1452 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1453 |
\rail@nont{\isa{transpat}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1454 |
\rail@nextplus{6} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1455 |
\rail@endplus |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1456 |
\rail@end |
46494
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1457 |
\rail@begin{2}{\isa{constdecl}} |
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1458 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1459 |
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[] |
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1460 |
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[] |
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1461 |
\rail@bar |
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1462 |
\rail@nextbar{1} |
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1463 |
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[] |
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1464 |
\rail@endbar |
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1465 |
\rail@end |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1466 |
\rail@begin{3}{\isa{mode}} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1467 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1468 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1469 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1470 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1471 |
\rail@term{\isa{\isakeyword{output}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1472 |
\rail@nextbar{2} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1473 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1474 |
\rail@term{\isa{\isakeyword{output}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1475 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1476 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1477 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1478 |
\rail@begin{2}{\isa{transpat}} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1479 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1480 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1481 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1482 |
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1483 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1484 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1485 |
\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1486 |
\rail@end |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1487 |
\end{railoutput} |
28762 | 1488 |
|
1489 |
||
1490 |
\begin{description} |
|
46282 | 1491 |
|
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
40879
diff
changeset
|
1492 |
\item \hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}~\isa{c} declares a type |
28762 | 1493 |
constructor \isa{c} (without arguments) to act as purely syntactic |
1494 |
type: a nonterminal symbol of the inner syntax. |
|
1495 |
||
46292 | 1496 |
\item \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}\ c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} augments the |
1497 |
priority grammar and the pretty printer table for the given print |
|
1498 |
mode (default \verb|""|). An optional keyword \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} means that only the pretty printer table is affected. |
|
1499 |
||
1500 |
Following \secref{sec:mixfix}, the mixfix annotation \isa{{\isaliteral{22}{\isachardoublequote}}mx\ {\isaliteral{3D}{\isacharequal}}\ template\ ps\ q{\isaliteral{22}{\isachardoublequote}}} together with type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{3D}{\isacharequal}}\ {\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}}} and |
|
1501 |
specify a grammar production. The \isa{template} contains |
|
1502 |
delimiter tokens that surround \isa{{\isaliteral{22}{\isachardoublequote}}n{\isaliteral{22}{\isachardoublequote}}} argument positions |
|
1503 |
(\verb|_|). The latter correspond to nonterminal symbols |
|
1504 |
\isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} derived from the argument types \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} as |
|
1505 |
follows: |
|
1506 |
\begin{itemize} |
|
1507 |
||
1508 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}prop{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ prop{\isaliteral{22}{\isachardoublequote}}} |
|
1509 |
||
1510 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}logic{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}} for logical type |
|
1511 |
constructor \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ prop{\isaliteral{22}{\isachardoublequote}}} |
|
1512 |
||
1513 |
\item \isa{any} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequote}}} for type variables |
|
1514 |
||
1515 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}} for nonterminal \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}} |
|
1516 |
(syntactic type constructor) |
|
1517 |
||
1518 |
\end{itemize} |
|
1519 |
||
1520 |
Each \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} is decorated by priority \isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} from the |
|
1521 |
given list \isa{{\isaliteral{22}{\isachardoublequote}}ps{\isaliteral{22}{\isachardoublequote}}}; misssing priorities default to 0. |
|
1522 |
||
1523 |
The resulting nonterminal of the production is determined similarly |
|
1524 |
from type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}, with priority \isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}} and default 1000. |
|
1525 |
||
1526 |
\medskip Parsing via this production produces parse trees \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} for the argument slots. The resulting parse tree is |
|
1527 |
composed as \isa{{\isaliteral{22}{\isachardoublequote}}c\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, by using the syntax constant \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} of the syntax declaration. |
|
1528 |
||
1529 |
Such syntactic constants are invented on the spot, without formal |
|
1530 |
check wrt.\ existing declarations. It is conventional to use plain |
|
1531 |
identifiers prefixed by a single underscore (e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}foobar{\isaliteral{22}{\isachardoublequote}}}). Names should be chosen with care, to avoid clashes |
|
48816 | 1532 |
with other syntax declarations. |
46292 | 1533 |
|
1534 |
\medskip The special case of copy production is specified by \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|""| (empty string). It means that the |
|
1535 |
resulting parse tree \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is copied directly, without any |
|
1536 |
further decoration. |
|
46282 | 1537 |
|
40406 | 1538 |
\item \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}syntax}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}\ decls{\isaliteral{22}{\isachardoublequote}}} removes grammar |
28762 | 1539 |
declarations (and translations) resulting from \isa{decls}, which |
1540 |
are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above. |
|
46282 | 1541 |
|
28762 | 1542 |
\item \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules} specifies syntactic |
48115 | 1543 |
translation rules (i.e.\ macros) as first-order rewrite rules on |
48816 | 1544 |
ASTs (\secref{sec:ast}). The theory context maintains two |
48115 | 1545 |
independent lists translation rules: parse rules (\verb|=>| |
1546 |
or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7269676874686172706F6F6E75703E}{\isasymrightharpoonup}}{\isaliteral{22}{\isachardoublequote}}}) and print rules (\verb|<=| or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C656674686172706F6F6E646F776E3E}{\isasymleftharpoondown}}{\isaliteral{22}{\isachardoublequote}}}). |
|
1547 |
For convenience, both can be specified simultaneously as parse~/ |
|
1548 |
print rules (\verb|==| or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72696768746C656674686172706F6F6E733E}{\isasymrightleftharpoons}}{\isaliteral{22}{\isachardoublequote}}}). |
|
1549 |
||
28762 | 1550 |
Translation patterns may be prefixed by the syntactic category to be |
48115 | 1551 |
used for parsing; the default is \isa{logic} which means that |
1552 |
regular term syntax is used. Both sides of the syntax translation |
|
1553 |
rule undergo parsing and parse AST translations |
|
1554 |
\secref{sec:tr-funs}, in order to perform some fundamental |
|
1555 |
normalization like \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ b\ {\isaliteral{5C3C6C65616473746F3E}{\isasymleadsto}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}y{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{22}{\isachardoublequote}}}, but other AST |
|
1556 |
translation rules are \emph{not} applied recursively here. |
|
1557 |
||
1558 |
When processing AST patterns, the inner syntax lexer runs in a |
|
1559 |
different mode that allows identifiers to start with underscore. |
|
1560 |
This accommodates the usual naming convention for auxiliary syntax |
|
1561 |
constants --- those that do not have a logical counter part --- by |
|
1562 |
allowing to specify arbitrary AST applications within the term |
|
1563 |
syntax, independently of the corresponding concrete syntax. |
|
1564 |
||
1565 |
Atomic ASTs are distinguished as \verb|Ast.Constant| versus \verb|Ast.Variable| as follows: a qualified name or syntax constant |
|
1566 |
declared via \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}, or parse tree head of concrete |
|
1567 |
notation becomes \verb|Ast.Constant|, anything else \verb|Ast.Variable|. Note that \isa{CONST} and \isa{XCONST} within |
|
1568 |
the term language (\secref{sec:pure-grammar}) allow to enforce |
|
1569 |
treatment as constants. |
|
1570 |
||
1571 |
AST rewrite rules \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} need to obey the following |
|
1572 |
side-conditions: |
|
1573 |
||
1574 |
\begin{itemize} |
|
1575 |
||
1576 |
\item Rules must be left linear: \isa{{\isaliteral{22}{\isachardoublequote}}lhs{\isaliteral{22}{\isachardoublequote}}} must not contain |
|
1577 |
repeated variables.\footnote{The deeper reason for this is that AST |
|
1578 |
equality is not well-defined: different occurrences of the ``same'' |
|
1579 |
AST could be decorated differently by accidental type-constraints or |
|
1580 |
source position information, for example.} |
|
1581 |
||
1582 |
\item Every variable in \isa{{\isaliteral{22}{\isachardoublequote}}rhs{\isaliteral{22}{\isachardoublequote}}} must also occur in \isa{{\isaliteral{22}{\isachardoublequote}}lhs{\isaliteral{22}{\isachardoublequote}}}. |
|
1583 |
||
1584 |
\end{itemize} |
|
46282 | 1585 |
|
40406 | 1586 |
\item \hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}translations}}}}~\isa{rules} removes syntactic |
28762 | 1587 |
translation rules, which are interpreted in the same manner as for |
1588 |
\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above. |
|
1589 |
||
48117 | 1590 |
\item \hyperlink{attribute.syntax-ast-trace}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}trace}}} and \hyperlink{attribute.syntax-ast-stats}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}stats}}} control diagnostic output in the AST normalization |
1591 |
process, when translation rules are applied to concrete input or |
|
1592 |
output. |
|
1593 |
||
46293 | 1594 |
\end{description} |
1595 |
||
1596 |
Raw syntax and translations provides a slightly more low-level |
|
1597 |
access to the grammar and the form of resulting parse trees. It is |
|
1598 |
often possible to avoid this untyped macro mechanism, and use |
|
1599 |
type-safe \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}} or \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}} instead. |
|
1600 |
Some important situations where \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} are really need are as follows: |
|
1601 |
||
1602 |
\begin{itemize} |
|
1603 |
||
1604 |
\item Iterated replacement via recursive \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}. |
|
1605 |
For example, consider list enumeration \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{2C}{\isacharcomma}}\ d{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as |
|
46525 | 1606 |
defined in theory \isa{List} in Isabelle/HOL. |
46293 | 1607 |
|
1608 |
\item Change of binding status of variables: anything beyond the |
|
1609 |
built-in \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} mixfix annotation requires explicit |
|
1610 |
syntax translations. For example, consider list filter |
|
46525 | 1611 |
comprehension \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs\ {\isaliteral{2E}{\isachardot}}\ P{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as defined in theory \isa{List} in Isabelle/HOL. |
46293 | 1612 |
|
1613 |
\end{itemize}% |
|
28762 | 1614 |
\end{isamarkuptext}% |
1615 |
\isamarkuptrue% |
|
1616 |
% |
|
48117 | 1617 |
\isamarkupsubsubsection{Applying translation rules% |
1618 |
} |
|
1619 |
\isamarkuptrue% |
|
1620 |
% |
|
1621 |
\begin{isamarkuptext}% |
|
1622 |
As a term is being parsed or printed, an AST is generated as |
|
1623 |
an intermediate form according to \figref{fig:parse-print}. The AST |
|
1624 |
is normalized by applying translation rules in the manner of a |
|
1625 |
first-order term rewriting system. We first examine how a single |
|
1626 |
rule is applied. |
|
1627 |
||
1628 |
Let \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} be the abstract syntax tree to be normalized and |
|
1629 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} some translation rule. A subtree \isa{{\isaliteral{22}{\isachardoublequote}}u{\isaliteral{22}{\isachardoublequote}}} |
|
1630 |
of \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is called \emph{redex} if it is an instance of \isa{{\isaliteral{22}{\isachardoublequote}}lhs{\isaliteral{22}{\isachardoublequote}}}; in this case the pattern \isa{{\isaliteral{22}{\isachardoublequote}}lhs{\isaliteral{22}{\isachardoublequote}}} is said to match the |
|
1631 |
object \isa{{\isaliteral{22}{\isachardoublequote}}u{\isaliteral{22}{\isachardoublequote}}}. A redex matched by \isa{{\isaliteral{22}{\isachardoublequote}}lhs{\isaliteral{22}{\isachardoublequote}}} may be |
|
1632 |
replaced by the corresponding instance of \isa{{\isaliteral{22}{\isachardoublequote}}rhs{\isaliteral{22}{\isachardoublequote}}}, thus |
|
1633 |
\emph{rewriting} the AST \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}}. Matching requires some notion |
|
1634 |
of \emph{place-holders} in rule patterns: \verb|Ast.Variable| serves |
|
1635 |
this purpose. |
|
1636 |
||
1637 |
More precisely, the matching of the object \isa{{\isaliteral{22}{\isachardoublequote}}u{\isaliteral{22}{\isachardoublequote}}} against the |
|
1638 |
pattern \isa{{\isaliteral{22}{\isachardoublequote}}lhs{\isaliteral{22}{\isachardoublequote}}} is performed as follows: |
|
1639 |
||
1640 |
\begin{itemize} |
|
1641 |
||
1642 |
\item Objects of the form \verb|Ast.Variable|~\isa{{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}} or \verb|Ast.Constant|~\isa{{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}} are matched by pattern \verb|Ast.Constant|~\isa{{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}}. Thus all atomic ASTs in the object are |
|
1643 |
treated as (potential) constants, and a successful match makes them |
|
1644 |
actual constants even before name space resolution (see also |
|
1645 |
\secref{sec:ast}). |
|
1646 |
||
1647 |
\item Object \isa{{\isaliteral{22}{\isachardoublequote}}u{\isaliteral{22}{\isachardoublequote}}} is matched by pattern \verb|Ast.Variable|~\isa{{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}}, binding \isa{{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}} to \isa{{\isaliteral{22}{\isachardoublequote}}u{\isaliteral{22}{\isachardoublequote}}}. |
|
1648 |
||
1649 |
\item Object \verb|Ast.Appl|~\isa{{\isaliteral{22}{\isachardoublequote}}us{\isaliteral{22}{\isachardoublequote}}} is matched by \verb|Ast.Appl|~\isa{{\isaliteral{22}{\isachardoublequote}}ts{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}us{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}ts{\isaliteral{22}{\isachardoublequote}}} have the |
|
1650 |
same length and each corresponding subtree matches. |
|
1651 |
||
1652 |
\item In every other case, matching fails. |
|
1653 |
||
1654 |
\end{itemize} |
|
1655 |
||
1656 |
A successful match yields a substitution that is applied to \isa{{\isaliteral{22}{\isachardoublequote}}rhs{\isaliteral{22}{\isachardoublequote}}}, generating the instance that replaces \isa{{\isaliteral{22}{\isachardoublequote}}u{\isaliteral{22}{\isachardoublequote}}}. |
|
1657 |
||
1658 |
Normalizing an AST involves repeatedly applying translation rules |
|
1659 |
until none are applicable. This works yoyo-like: top-down, |
|
1660 |
bottom-up, top-down, etc. At each subtree position, rules are |
|
1661 |
chosen in order of appearance in the theory definitions. |
|
1662 |
||
1663 |
The configuration options \hyperlink{attribute.syntax-ast-trace}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}trace}}} and |
|
48816 | 1664 |
\hyperlink{attribute.syntax-ast-stats}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}stats}}} might help to understand this process |
48117 | 1665 |
and diagnose problems. |
1666 |
||
1667 |
\begin{warn} |
|
1668 |
If syntax translation rules work incorrectly, the output of |
|
48118 | 1669 |
\indexref{}{command}{print\_syntax}\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}syntax}}}} with its \emph{rules} sections reveals the |
48117 | 1670 |
actual internal forms of AST pattern, without potentially confusing |
1671 |
concrete syntax. Recall that AST constants appear as quoted strings |
|
1672 |
and variables without quotes. |
|
1673 |
\end{warn} |
|
1674 |
||
1675 |
\begin{warn} |
|
1676 |
If \indexref{}{attribute}{eta\_contract}\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}} is set to \isa{{\isaliteral{22}{\isachardoublequote}}true{\isaliteral{22}{\isachardoublequote}}}, terms |
|
1677 |
will be \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted \emph{before} the AST rewriter sees |
|
1678 |
them. Thus some abstraction nodes needed for print rules to match |
|
1679 |
may vanish. For example, \isa{{\isaliteral{22}{\isachardoublequote}}Ball\ A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} would contract |
|
1680 |
to \isa{{\isaliteral{22}{\isachardoublequote}}Ball\ A\ P{\isaliteral{22}{\isachardoublequote}}} and the standard print rule would fail to |
|
1681 |
apply. This problem can be avoided by hand-written ML translation |
|
1682 |
functions (see also \secref{sec:tr-funs}), which is in fact the same |
|
1683 |
mechanism used in built-in \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} declarations. |
|
1684 |
\end{warn}% |
|
1685 |
\end{isamarkuptext}% |
|
1686 |
\isamarkuptrue% |
|
1687 |
% |
|
48113 | 1688 |
\isamarkupsubsection{Syntax translation functions \label{sec:tr-funs}% |
28762 | 1689 |
} |
1690 |
\isamarkuptrue% |
|
1691 |
% |
|
1692 |
\begin{isamarkuptext}% |
|
1693 |
\begin{matharray}{rcl} |
|
40406 | 1694 |
\indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ |
1695 |
\indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
1696 |
\indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
1697 |
\indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isaliteral{5F}{\isacharunderscore}}print{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
1698 |
\indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\ |
|
48119
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1699 |
\indexdef{}{ML antiquotation}{class\_syntax}\hypertarget{ML antiquotation.class-syntax}{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1700 |
\indexdef{}{ML antiquotation}{type\_syntax}\hypertarget{ML antiquotation.type-syntax}{\hyperlink{ML antiquotation.type-syntax}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}syntax}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1701 |
\indexdef{}{ML antiquotation}{const\_syntax}\hypertarget{ML antiquotation.const-syntax}{\hyperlink{ML antiquotation.const-syntax}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}syntax}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1702 |
\indexdef{}{ML antiquotation}{syntax\_const}\hypertarget{ML antiquotation.syntax-const}{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}const}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\ |
28762 | 1703 |
\end{matharray} |
1704 |
||
48118 | 1705 |
Syntax translation functions written in ML admit almost arbitrary |
1706 |
manipulations of inner syntax, at the expense of some complexity and |
|
1707 |
obscurity in the implementation. |
|
1708 |
||
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1709 |
\begin{railoutput} |
42662 | 1710 |
\rail@begin{5}{} |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1711 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1712 |
\rail@term{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1713 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1714 |
\rail@term{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1715 |
\rail@nextbar{2} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1716 |
\rail@term{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1717 |
\rail@nextbar{3} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1718 |
\rail@term{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isaliteral{5F}{\isacharunderscore}}print{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1719 |
\rail@nextbar{4} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1720 |
\rail@term{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1721 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1722 |
\rail@bar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1723 |
\rail@nextbar{1} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1724 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1725 |
\rail@term{\isa{\isakeyword{advanced}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1726 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1727 |
\rail@endbar |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1728 |
\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[] |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1729 |
\rail@end |
48119
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1730 |
\rail@begin{4}{} |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1731 |
\rail@bar |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1732 |
\rail@term{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[] |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1733 |
\rail@nextbar{1} |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1734 |
\rail@term{\hyperlink{ML antiquotation.type-syntax}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[] |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1735 |
\rail@nextbar{2} |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1736 |
\rail@term{\hyperlink{ML antiquotation.const-syntax}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[] |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1737 |
\rail@nextbar{3} |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1738 |
\rail@term{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}const}}}}[] |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1739 |
\rail@endbar |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1740 |
\rail@nont{\isa{name}}[] |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1741 |
\rail@end |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1742 |
\end{railoutput} |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1743 |
|
28762 | 1744 |
|
48119
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1745 |
\begin{description} |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1746 |
|
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1747 |
\item \hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}translation}}}} etc. declare syntax translation |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1748 |
functions to the theory. Any of these commands have a single |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1749 |
\hyperlink{syntax.text}{\mbox{\isa{text}}} argument that refers to an ML expression of |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1750 |
appropriate type, which are as follows by default: |
28762 | 1751 |
|
48118 | 1752 |
\medskip |
48119
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1753 |
{\footnotesize |
48118 | 1754 |
\begin{tabular}{ll} |
1755 |
\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (Ast.ast list -> Ast.ast)) list| \\ |
|
1756 |
\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (term list -> term)) list| \\ |
|
1757 |
\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (term list -> term)) list| \\ |
|
1758 |
\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isaliteral{5F}{\isacharunderscore}}print{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (typ -> term list -> term)) list| \\ |
|
1759 |
\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (Ast.ast list -> Ast.ast)) list| \\ |
|
1760 |
\end{tabular}} |
|
1761 |
\medskip |
|
1762 |
||
48816 | 1763 |
The argument list consists of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ tr{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} pairs, where \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} is the syntax name of the formal entity involved, and \isa{{\isaliteral{22}{\isachardoublequote}}tr{\isaliteral{22}{\isachardoublequote}}} a function that translates a syntax form \isa{{\isaliteral{22}{\isachardoublequote}}c\ args{\isaliteral{22}{\isachardoublequote}}} into |
1764 |
\isa{{\isaliteral{22}{\isachardoublequote}}tr\ args{\isaliteral{22}{\isachardoublequote}}}. The ML naming convention for parse translations |
|
1765 |
is \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}tr{\isaliteral{22}{\isachardoublequote}}} and for print translations \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}tr{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}}. |
|
48118 | 1766 |
|
1767 |
The \indexref{}{command}{print\_syntax}\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}syntax}}}} command displays the sets of names |
|
1768 |
associated with the translation functions of a theory under \isa{{\isaliteral{22}{\isachardoublequote}}parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation{\isaliteral{22}{\isachardoublequote}}} etc. |
|
28762 | 1769 |
|
48118 | 1770 |
If the \verb|(|\hyperlink{keyword.advanced}{\mbox{\isa{\isakeyword{advanced}}}}\verb|)| option is |
1771 |
given, the corresponding translation functions depend on the current |
|
1772 |
theory or proof context as additional argument. This allows to |
|
1773 |
implement advanced syntax mechanisms, as translations functions may |
|
48119
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1774 |
refer to specific theory declarations or auxiliary proof data. |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1775 |
|
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1776 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}class{\isaliteral{5F}{\isacharunderscore}}syntax\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}type{\isaliteral{5F}{\isacharunderscore}}syntax\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1777 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const{\isaliteral{5F}{\isacharunderscore}}syntax\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} inline the authentic syntax name of the |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1778 |
given formal entities into the ML source. This is the |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1779 |
fully-qualified logical name prefixed by a special marker to |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1780 |
indicate its kind: thus different logical name spaces are properly |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1781 |
distinguished within parse trees. |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1782 |
|
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1783 |
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const{\isaliteral{5F}{\isacharunderscore}}syntax\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} inlines the name \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} of |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1784 |
the given syntax constant, having checked that it has been declared |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1785 |
via some \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} commands within the theory context. Note |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1786 |
that the usual naming convention makes syntax constants start with |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1787 |
underscore, to reduce the chance of accidental clashes with other |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1788 |
names occurring in parse trees (unqualified constants etc.). |
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1789 |
|
55c305e29f4b
cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;
wenzelm
parents:
48118
diff
changeset
|
1790 |
\end{description}% |
48118 | 1791 |
\end{isamarkuptext}% |
1792 |
\isamarkuptrue% |
|
1793 |
% |
|
1794 |
\isamarkupsubsubsection{The translation strategy% |
|
1795 |
} |
|
1796 |
\isamarkuptrue% |
|
1797 |
% |
|
1798 |
\begin{isamarkuptext}% |
|
48816 | 1799 |
The different kinds of translation functions are invoked during |
48118 | 1800 |
the transformations between parse trees, ASTs and syntactic terms |
1801 |
(cf.\ \figref{fig:parse-print}). Whenever a combination of the form |
|
1802 |
\isa{{\isaliteral{22}{\isachardoublequote}}c\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} is encountered, and a translation function |
|
1803 |
\isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}} of appropriate kind is declared for \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}}, the |
|
1804 |
result is produced by evaluation of \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5B}{\isacharbrackleft}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} in ML. |
|
1805 |
||
1806 |
For AST translations, the arguments \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are ASTs. A |
|
1807 |
combination has the form \verb|Ast.Constant|~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} or \verb|Ast.Appl|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}}\verb|Ast.Constant|~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}. |
|
1808 |
For term translations, the arguments are terms and a combination has |
|
1809 |
the form \verb|Const|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} or \verb|Const|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{24}{\isachardollar}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}. Terms allow more sophisticated transformations |
|
1810 |
than ASTs do, typically involving abstractions and bound |
|
1811 |
variables. \emph{Typed} print translations may even peek at the type |
|
48816 | 1812 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} of the constant they are invoked on, although that information |
1813 |
may be inaccurate. |
|
28762 | 1814 |
|
48118 | 1815 |
Regardless of whether they act on ASTs or terms, translation |
1816 |
functions called during the parsing process differ from those for |
|
1817 |
printing in their overall behaviour: |
|
1818 |
||
1819 |
\begin{description} |
|
1820 |
||
1821 |
\item [Parse translations] are applied bottom-up. The arguments are |
|
1822 |
already in translated form. The translations must not fail; |
|
1823 |
exceptions trigger an error message. There may be at most one |
|
1824 |
function associated with any syntactic name. |
|
46294 | 1825 |
|
48118 | 1826 |
\item [Print translations] are applied top-down. They are supplied |
1827 |
with arguments that are partly still in internal form. The result |
|
1828 |
again undergoes translation; therefore a print translation should |
|
1829 |
not introduce as head the very constant that invoked it. The |
|
1830 |
function may raise exception \verb|Match| to indicate failure; in |
|
1831 |
this event it has no effect. Multiple functions associated with |
|
1832 |
some syntactic name are tried in the order of declaration in the |
|
1833 |
theory. |
|
1834 |
||
1835 |
\end{description} |
|
1836 |
||
1837 |
Only constant atoms --- constructor \verb|Ast.Constant| for ASTs and |
|
1838 |
\verb|Const| for terms --- can invoke translation functions. This |
|
1839 |
means that parse translations can only be associated with parse tree |
|
1840 |
heads of concrete syntax, or syntactic constants introduced via |
|
1841 |
other translations. For plain identifiers within the term language, |
|
1842 |
the status of constant versus variable is not yet know during |
|
1843 |
parsing. This is in contrast to print translations, where constants |
|
1844 |
are explicitly known from the given term in its fully internal form.% |
|
28762 | 1845 |
\end{isamarkuptext}% |
1846 |
\isamarkuptrue% |
|
1847 |
% |
|
1848 |
\isadelimtheory |
|
1849 |
% |
|
1850 |
\endisadelimtheory |
|
1851 |
% |
|
1852 |
\isatagtheory |
|
1853 |
\isacommand{end}\isamarkupfalse% |
|
1854 |
% |
|
1855 |
\endisatagtheory |
|
1856 |
{\isafoldtheory}% |
|
1857 |
% |
|
1858 |
\isadelimtheory |
|
1859 |
% |
|
1860 |
\endisadelimtheory |
|
1861 |
\isanewline |
|
1862 |
\end{isabellebody}% |
|
1863 |
%%% Local Variables: |
|
1864 |
%%% mode: latex |
|
1865 |
%%% TeX-master: "root" |
|
1866 |
%%% End: |