wenzelm@28762
|
1 |
theory Inner_Syntax
|
wenzelm@28762
|
2 |
imports Main
|
wenzelm@28762
|
3 |
begin
|
wenzelm@28762
|
4 |
|
wenzelm@28778
|
5 |
chapter {* Inner syntax --- the term language \label{ch:inner-syntax} *}
|
wenzelm@28762
|
6 |
|
wenzelm@28762
|
7 |
section {* Printing logical entities *}
|
wenzelm@28762
|
8 |
|
wenzelm@28762
|
9 |
subsection {* Diagnostic commands *}
|
wenzelm@28762
|
10 |
|
wenzelm@28762
|
11 |
text {*
|
wenzelm@28762
|
12 |
\begin{matharray}{rcl}
|
wenzelm@28766
|
13 |
@{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28762
|
14 |
@{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28762
|
15 |
@{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28766
|
16 |
@{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28762
|
17 |
@{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28762
|
18 |
@{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28766
|
19 |
@{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
|
wenzelm@28762
|
20 |
\end{matharray}
|
wenzelm@28762
|
21 |
|
wenzelm@28762
|
22 |
These diagnostic commands assist interactive development by printing
|
wenzelm@28762
|
23 |
internal logical entities in a human-readable fashion.
|
wenzelm@28762
|
24 |
|
wenzelm@28762
|
25 |
\begin{rail}
|
wenzelm@28766
|
26 |
'typ' modes? type
|
wenzelm@28762
|
27 |
;
|
wenzelm@28762
|
28 |
'term' modes? term
|
wenzelm@28762
|
29 |
;
|
wenzelm@28762
|
30 |
'prop' modes? prop
|
wenzelm@28762
|
31 |
;
|
wenzelm@28766
|
32 |
'thm' modes? thmrefs
|
wenzelm@28762
|
33 |
;
|
wenzelm@28766
|
34 |
( 'prf' | 'full\_prf' ) modes? thmrefs?
|
wenzelm@28762
|
35 |
;
|
wenzelm@28766
|
36 |
'pr' modes? nat? (',' nat)?
|
wenzelm@28762
|
37 |
;
|
wenzelm@28762
|
38 |
|
wenzelm@28762
|
39 |
modes: '(' (name + ) ')'
|
wenzelm@28762
|
40 |
;
|
wenzelm@28762
|
41 |
\end{rail}
|
wenzelm@28762
|
42 |
|
wenzelm@28762
|
43 |
\begin{description}
|
wenzelm@28762
|
44 |
|
wenzelm@28766
|
45 |
\item @{command "typ"}~@{text \<tau>} reads and prints types of the
|
wenzelm@28766
|
46 |
meta-logic according to the current theory or proof context.
|
wenzelm@28766
|
47 |
|
wenzelm@28766
|
48 |
\item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
|
wenzelm@28766
|
49 |
read, type-check and print terms or propositions according to the
|
wenzelm@28766
|
50 |
current theory or proof context; the inferred type of @{text t} is
|
wenzelm@28766
|
51 |
output as well. Note that these commands are also useful in
|
wenzelm@28766
|
52 |
inspecting the current environment of term abbreviations.
|
wenzelm@28762
|
53 |
|
wenzelm@28762
|
54 |
\item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves
|
wenzelm@28762
|
55 |
theorems from the current theory or proof context. Note that any
|
wenzelm@28762
|
56 |
attributes included in the theorem specifications are applied to a
|
wenzelm@28762
|
57 |
temporary context derived from the current theory or proof; the
|
wenzelm@28762
|
58 |
result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
|
wenzelm@28762
|
59 |
\<dots>, a\<^sub>n"} do not have any permanent effect.
|
wenzelm@28762
|
60 |
|
wenzelm@28762
|
61 |
\item @{command "prf"} displays the (compact) proof term of the
|
wenzelm@28762
|
62 |
current proof state (if present), or of the given theorems. Note
|
wenzelm@28762
|
63 |
that this requires proof terms to be switched on for the current
|
wenzelm@28762
|
64 |
object logic (see the ``Proof terms'' section of the Isabelle
|
wenzelm@28762
|
65 |
reference manual for information on how to do this).
|
wenzelm@28762
|
66 |
|
wenzelm@28762
|
67 |
\item @{command "full_prf"} is like @{command "prf"}, but displays
|
wenzelm@28762
|
68 |
the full proof term, i.e.\ also displays information omitted in the
|
wenzelm@28762
|
69 |
compact proof term, which is denoted by ``@{text _}'' placeholders
|
wenzelm@28762
|
70 |
there.
|
wenzelm@28762
|
71 |
|
wenzelm@28766
|
72 |
\item @{command "pr"}~@{text "goals, prems"} prints the current
|
wenzelm@28766
|
73 |
proof state (if present), including the proof context, current facts
|
wenzelm@28766
|
74 |
and goals. The optional limit arguments affect the number of goals
|
wenzelm@28766
|
75 |
and premises to be displayed, which is initially 10 for both.
|
wenzelm@28766
|
76 |
Omitting limit values leaves the current setting unchanged.
|
wenzelm@28766
|
77 |
|
wenzelm@28762
|
78 |
\end{description}
|
wenzelm@28762
|
79 |
|
wenzelm@28762
|
80 |
All of the diagnostic commands above admit a list of @{text modes}
|
wenzelm@28762
|
81 |
to be specified, which is appended to the current print mode (see
|
wenzelm@28762
|
82 |
also \cite{isabelle-ref}). Thus the output behavior may be modified
|
wenzelm@28762
|
83 |
according particular print mode features. For example, @{command
|
wenzelm@28762
|
84 |
"pr"}~@{text "(latex xsymbols)"} would print the current proof state
|
wenzelm@28762
|
85 |
with mathematical symbols and special characters represented in
|
wenzelm@28762
|
86 |
{\LaTeX} source, according to the Isabelle style
|
wenzelm@28762
|
87 |
\cite{isabelle-sys}.
|
wenzelm@28762
|
88 |
|
wenzelm@28762
|
89 |
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
|
wenzelm@28762
|
90 |
systematic way to include formal items into the printed text
|
wenzelm@28762
|
91 |
document.
|
wenzelm@28762
|
92 |
*}
|
wenzelm@28762
|
93 |
|
wenzelm@28762
|
94 |
|
wenzelm@28763
|
95 |
subsection {* Details of printed content *}
|
wenzelm@28763
|
96 |
|
wenzelm@28763
|
97 |
text {*
|
wenzelm@28763
|
98 |
\begin{mldecls}
|
wenzelm@32833
|
99 |
@{index_ML show_types: "bool Unsynchronized.ref"} & default @{ML false} \\
|
wenzelm@32833
|
100 |
@{index_ML show_sorts: "bool Unsynchronized.ref"} & default @{ML false} \\
|
wenzelm@32833
|
101 |
@{index_ML show_consts: "bool Unsynchronized.ref"} & default @{ML false} \\
|
wenzelm@32833
|
102 |
@{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
|
wenzelm@32833
|
103 |
@{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
|
wenzelm@32833
|
104 |
@{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
|
wenzelm@32833
|
105 |
@{index_ML show_brackets: "bool Unsynchronized.ref"} & default @{ML false} \\
|
wenzelm@32833
|
106 |
@{index_ML eta_contract: "bool Unsynchronized.ref"} & default @{ML true} \\
|
wenzelm@32833
|
107 |
@{index_ML goals_limit: "int Unsynchronized.ref"} & default @{ML 10} \\
|
wenzelm@32833
|
108 |
@{index_ML Proof.show_main_goal: "bool Unsynchronized.ref"} & default @{ML false} \\
|
wenzelm@32833
|
109 |
@{index_ML show_hyps: "bool Unsynchronized.ref"} & default @{ML false} \\
|
wenzelm@32833
|
110 |
@{index_ML show_tags: "bool Unsynchronized.ref"} & default @{ML false} \\
|
wenzelm@32833
|
111 |
@{index_ML show_question_marks: "bool Unsynchronized.ref"} & default @{ML true} \\
|
wenzelm@28763
|
112 |
\end{mldecls}
|
wenzelm@28763
|
113 |
|
wenzelm@28763
|
114 |
These global ML variables control the detail of information that is
|
wenzelm@28763
|
115 |
displayed for types, terms, theorems, goals etc.
|
wenzelm@28763
|
116 |
|
wenzelm@28765
|
117 |
In interactive sessions, the user interface usually manages these
|
wenzelm@28765
|
118 |
global parameters of the Isabelle process, even with some concept of
|
wenzelm@28765
|
119 |
persistence. Nonetheless it is occasionally useful to manipulate ML
|
wenzelm@28765
|
120 |
variables directly, e.g.\ using @{command "ML_val"} or @{command
|
wenzelm@28765
|
121 |
"ML_command"}.
|
wenzelm@28765
|
122 |
|
wenzelm@28765
|
123 |
Batch-mode logic sessions may be configured by putting appropriate
|
wenzelm@28765
|
124 |
ML text directly into the @{verbatim ROOT.ML} file.
|
wenzelm@28765
|
125 |
|
wenzelm@28763
|
126 |
\begin{description}
|
wenzelm@28763
|
127 |
|
wenzelm@28763
|
128 |
\item @{ML show_types} and @{ML show_sorts} control printing of type
|
wenzelm@28763
|
129 |
constraints for term variables, and sort constraints for type
|
wenzelm@28763
|
130 |
variables. By default, neither of these are shown in output. If
|
wenzelm@28763
|
131 |
@{ML show_sorts} is set to @{ML true}, types are always shown as
|
wenzelm@28763
|
132 |
well.
|
wenzelm@28763
|
133 |
|
wenzelm@28763
|
134 |
Note that displaying types and sorts may explain why a polymorphic
|
wenzelm@28763
|
135 |
inference rule fails to resolve with some goal, or why a rewrite
|
wenzelm@28763
|
136 |
rule does not apply as expected.
|
wenzelm@28763
|
137 |
|
wenzelm@28763
|
138 |
\item @{ML show_consts} controls printing of types of constants when
|
wenzelm@28765
|
139 |
displaying a goal state.
|
wenzelm@28765
|
140 |
|
wenzelm@28765
|
141 |
Note that the output can be enormous, because polymorphic constants
|
wenzelm@28765
|
142 |
often occur at several different type instances.
|
wenzelm@28763
|
143 |
|
wenzelm@28763
|
144 |
\item @{ML long_names}, @{ML short_names}, and @{ML unique_names}
|
wenzelm@28765
|
145 |
control the way of printing fully qualified internal names in
|
wenzelm@28765
|
146 |
external form. See also \secref{sec:antiq} for the document
|
wenzelm@28765
|
147 |
antiquotation options of the same names.
|
wenzelm@28763
|
148 |
|
wenzelm@28765
|
149 |
\item @{ML show_brackets} controls bracketing in pretty printed
|
wenzelm@28765
|
150 |
output. If set to @{ML true}, all sub-expressions of the pretty
|
wenzelm@28765
|
151 |
printing tree will be parenthesized, even if this produces malformed
|
wenzelm@28765
|
152 |
term syntax! This crude way of showing the internal structure of
|
wenzelm@28765
|
153 |
pretty printed entities may occasionally help to diagnose problems
|
wenzelm@28765
|
154 |
with operator priorities, for example.
|
wenzelm@28763
|
155 |
|
wenzelm@28763
|
156 |
\item @{ML eta_contract} controls @{text "\<eta>"}-contracted printing of
|
wenzelm@28763
|
157 |
terms.
|
wenzelm@28763
|
158 |
|
wenzelm@28763
|
159 |
The @{text \<eta>}-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"},
|
wenzelm@28763
|
160 |
provided @{text x} is not free in @{text f}. It asserts
|
wenzelm@28763
|
161 |
\emph{extensionality} of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv>
|
wenzelm@28763
|
162 |
g x"} for all @{text x}. Higher-order unification frequently puts
|
wenzelm@28763
|
163 |
terms into a fully @{text \<eta>}-expanded form. For example, if @{text
|
wenzelm@28763
|
164 |
F} has type @{text "(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>"} then its expanded form is @{term
|
wenzelm@28763
|
165 |
"\<lambda>h. F (\<lambda>x. h x)"}.
|
wenzelm@28763
|
166 |
|
wenzelm@28763
|
167 |
Setting @{ML eta_contract} makes Isabelle perform @{text
|
wenzelm@28763
|
168 |
\<eta>}-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"}
|
wenzelm@28763
|
169 |
appears simply as @{text F}.
|
wenzelm@28763
|
170 |
|
wenzelm@28763
|
171 |
Note that the distinction between a term and its @{text \<eta>}-expanded
|
wenzelm@28765
|
172 |
form occasionally matters. While higher-order resolution and
|
wenzelm@28765
|
173 |
rewriting operate modulo @{text "\<alpha>\<beta>\<eta>"}-conversion, some other tools
|
wenzelm@28765
|
174 |
might look at terms more discretely.
|
wenzelm@28763
|
175 |
|
wenzelm@28763
|
176 |
\item @{ML goals_limit} controls the maximum number of subgoals to
|
wenzelm@28765
|
177 |
be shown in goal output.
|
wenzelm@28763
|
178 |
|
wenzelm@28763
|
179 |
\item @{ML Proof.show_main_goal} controls whether the main result to
|
wenzelm@28763
|
180 |
be proven should be displayed. This information might be relevant
|
wenzelm@28765
|
181 |
for schematic goals, to inspect the current claim that has been
|
wenzelm@28765
|
182 |
synthesized so far.
|
wenzelm@28763
|
183 |
|
wenzelm@28763
|
184 |
\item @{ML show_hyps} controls printing of implicit hypotheses of
|
wenzelm@28763
|
185 |
local facts. Normally, only those hypotheses are displayed that are
|
wenzelm@28763
|
186 |
\emph{not} covered by the assumptions of the current context: this
|
wenzelm@28763
|
187 |
situation indicates a fault in some tool being used.
|
wenzelm@28763
|
188 |
|
wenzelm@28765
|
189 |
By setting @{ML show_hyps} to @{ML true}, output of \emph{all}
|
wenzelm@28765
|
190 |
hypotheses can be enforced, which is occasionally useful for
|
wenzelm@28765
|
191 |
diagnostic purposes.
|
wenzelm@28763
|
192 |
|
wenzelm@28763
|
193 |
\item @{ML show_tags} controls printing of extra annotations within
|
wenzelm@28765
|
194 |
theorems, such as internal position information, or the case names
|
wenzelm@28765
|
195 |
being attached by the attribute @{attribute case_names}.
|
wenzelm@28765
|
196 |
|
wenzelm@28765
|
197 |
Note that the @{attribute tagged} and @{attribute untagged}
|
wenzelm@28765
|
198 |
attributes provide low-level access to the collection of tags
|
wenzelm@28765
|
199 |
associated with a theorem.
|
wenzelm@28765
|
200 |
|
wenzelm@28765
|
201 |
\item @{ML show_question_marks} controls printing of question marks
|
wenzelm@28765
|
202 |
for schematic variables, such as @{text ?x}. Only the leading
|
wenzelm@28765
|
203 |
question mark is affected, the remaining text is unchanged
|
wenzelm@28765
|
204 |
(including proper markup for schematic variables that might be
|
wenzelm@28765
|
205 |
relevant for user interfaces).
|
wenzelm@28765
|
206 |
|
wenzelm@28765
|
207 |
\end{description}
|
wenzelm@28765
|
208 |
*}
|
wenzelm@28765
|
209 |
|
wenzelm@28765
|
210 |
|
wenzelm@28765
|
211 |
subsection {* Printing limits *}
|
wenzelm@28765
|
212 |
|
wenzelm@28765
|
213 |
text {*
|
wenzelm@28765
|
214 |
\begin{mldecls}
|
wenzelm@36754
|
215 |
@{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
|
wenzelm@28765
|
216 |
@{index_ML print_depth: "int -> unit"} \\
|
wenzelm@28765
|
217 |
\end{mldecls}
|
wenzelm@28765
|
218 |
|
wenzelm@28765
|
219 |
These ML functions set limits for pretty printed text.
|
wenzelm@28765
|
220 |
|
wenzelm@28765
|
221 |
\begin{description}
|
wenzelm@28765
|
222 |
|
wenzelm@36754
|
223 |
\item @{ML Pretty.margin_default} indicates the global default for
|
wenzelm@36754
|
224 |
the right margin of the built-in pretty printer, with initial value
|
wenzelm@36754
|
225 |
76. Note that user-interfaces typically control margins
|
wenzelm@36754
|
226 |
automatically when resizing windows, or even bypass the formatting
|
wenzelm@36754
|
227 |
engine of Isabelle/ML altogether and do it within the front end via
|
wenzelm@36754
|
228 |
Isabelle/Scala.
|
wenzelm@28765
|
229 |
|
wenzelm@28765
|
230 |
\item @{ML print_depth}~@{text n} limits the printing depth of the
|
wenzelm@28765
|
231 |
ML toplevel pretty printer; the precise effect depends on the ML
|
wenzelm@28765
|
232 |
compiler and run-time system. Typically @{text n} should be less
|
wenzelm@28765
|
233 |
than 10. Bigger values such as 100--1000 are useful for debugging.
|
wenzelm@28763
|
234 |
|
wenzelm@28763
|
235 |
\end{description}
|
wenzelm@28763
|
236 |
*}
|
wenzelm@28763
|
237 |
|
wenzelm@28763
|
238 |
|
wenzelm@28762
|
239 |
section {* Mixfix annotations *}
|
wenzelm@28762
|
240 |
|
wenzelm@28762
|
241 |
text {* Mixfix annotations specify concrete \emph{inner syntax} of
|
wenzelm@35352
|
242 |
Isabelle types and terms. Locally fixed parameters in toplevel
|
wenzelm@35352
|
243 |
theorem statements, locale specifications etc.\ also admit mixfix
|
wenzelm@35352
|
244 |
annotations.
|
wenzelm@28762
|
245 |
|
wenzelm@28762
|
246 |
\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
|
wenzelm@28762
|
247 |
\begin{rail}
|
wenzelm@28762
|
248 |
infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
|
wenzelm@28762
|
249 |
;
|
wenzelm@28762
|
250 |
mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
|
wenzelm@28762
|
251 |
;
|
wenzelm@28762
|
252 |
structmixfix: mixfix | '(' 'structure' ')'
|
wenzelm@28762
|
253 |
;
|
wenzelm@28762
|
254 |
|
wenzelm@28762
|
255 |
prios: '[' (nat + ',') ']'
|
wenzelm@28762
|
256 |
;
|
wenzelm@28762
|
257 |
\end{rail}
|
wenzelm@28762
|
258 |
|
wenzelm@28762
|
259 |
Here the \railtok{string} specifications refer to the actual mixfix
|
wenzelm@28762
|
260 |
template, which may include literal text, spacing, blocks, and
|
wenzelm@28762
|
261 |
arguments (denoted by ``@{text _}''); the special symbol
|
wenzelm@28762
|
262 |
``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index
|
wenzelm@28762
|
263 |
argument that specifies an implicit structure reference (see also
|
wenzelm@28762
|
264 |
\secref{sec:locale}). Infix and binder declarations provide common
|
wenzelm@28762
|
265 |
abbreviations for particular mixfix declarations. So in practice,
|
wenzelm@28762
|
266 |
mixfix templates mostly degenerate to literal text for concrete
|
wenzelm@28762
|
267 |
syntax, such as ``@{verbatim "++"}'' for an infix symbol.
|
wenzelm@28762
|
268 |
|
wenzelm@28762
|
269 |
\medskip In full generality, mixfix declarations work as follows.
|
wenzelm@28762
|
270 |
Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is
|
wenzelm@28762
|
271 |
annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text
|
wenzelm@28762
|
272 |
"mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of
|
wenzelm@28762
|
273 |
delimiters that surround argument positions as indicated by
|
wenzelm@28762
|
274 |
underscores.
|
wenzelm@28762
|
275 |
|
wenzelm@28762
|
276 |
Altogether this determines a production for a context-free priority
|
wenzelm@28762
|
277 |
grammar, where for each argument @{text "i"} the syntactic category
|
wenzelm@28762
|
278 |
is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and
|
wenzelm@28762
|
279 |
the result category is determined from @{text "\<tau>"} (with
|
wenzelm@28762
|
280 |
priority @{text "p"}). Priority specifications are optional, with
|
wenzelm@28762
|
281 |
default 0 for arguments and 1000 for the result.
|
wenzelm@28762
|
282 |
|
wenzelm@28762
|
283 |
Since @{text "\<tau>"} may be again a function type, the constant
|
wenzelm@28762
|
284 |
type scheme may have more argument positions than the mixfix
|
wenzelm@28762
|
285 |
pattern. Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
|
wenzelm@28762
|
286 |
@{text "m > n"} works by attaching concrete notation only to the
|
wenzelm@28762
|
287 |
innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
|
wenzelm@28762
|
288 |
instead. If a term has fewer arguments than specified in the mixfix
|
wenzelm@28762
|
289 |
template, the concrete syntax is ignored.
|
wenzelm@28762
|
290 |
|
wenzelm@28762
|
291 |
\medskip A mixfix template may also contain additional directives
|
wenzelm@28762
|
292 |
for pretty printing, notably spaces, blocks, and breaks. The
|
wenzelm@28762
|
293 |
general template format is a sequence over any of the following
|
wenzelm@28762
|
294 |
entities.
|
wenzelm@28762
|
295 |
|
wenzelm@28778
|
296 |
\begin{description}
|
wenzelm@28762
|
297 |
|
wenzelm@28771
|
298 |
\item @{text "d"} is a delimiter, namely a non-empty sequence of
|
wenzelm@28771
|
299 |
characters other than the following special characters:
|
wenzelm@28762
|
300 |
|
wenzelm@28771
|
301 |
\smallskip
|
wenzelm@28771
|
302 |
\begin{tabular}{ll}
|
wenzelm@28771
|
303 |
@{verbatim "'"} & single quote \\
|
wenzelm@28771
|
304 |
@{verbatim "_"} & underscore \\
|
wenzelm@28771
|
305 |
@{text "\<index>"} & index symbol \\
|
wenzelm@28771
|
306 |
@{verbatim "("} & open parenthesis \\
|
wenzelm@28771
|
307 |
@{verbatim ")"} & close parenthesis \\
|
wenzelm@28771
|
308 |
@{verbatim "/"} & slash \\
|
wenzelm@28771
|
309 |
\end{tabular}
|
wenzelm@28771
|
310 |
\medskip
|
wenzelm@28762
|
311 |
|
wenzelm@28771
|
312 |
\item @{verbatim "'"} escapes the special meaning of these
|
wenzelm@28771
|
313 |
meta-characters, producing a literal version of the following
|
wenzelm@28771
|
314 |
character, unless that is a blank.
|
wenzelm@28771
|
315 |
|
wenzelm@28771
|
316 |
A single quote followed by a blank separates delimiters, without
|
wenzelm@28771
|
317 |
affecting printing, but input tokens may have additional white space
|
wenzelm@28771
|
318 |
here.
|
wenzelm@28771
|
319 |
|
wenzelm@28771
|
320 |
\item @{verbatim "_"} is an argument position, which stands for a
|
wenzelm@28762
|
321 |
certain syntactic category in the underlying grammar.
|
wenzelm@28762
|
322 |
|
wenzelm@28771
|
323 |
\item @{text "\<index>"} is an indexed argument position; this is the place
|
wenzelm@28771
|
324 |
where implicit structure arguments can be attached.
|
wenzelm@28762
|
325 |
|
wenzelm@28771
|
326 |
\item @{text "s"} is a non-empty sequence of spaces for printing.
|
wenzelm@28771
|
327 |
This and the following specifications do not affect parsing at all.
|
wenzelm@28762
|
328 |
|
wenzelm@28771
|
329 |
\item @{verbatim "("}@{text n} opens a pretty printing block. The
|
wenzelm@28762
|
330 |
optional number specifies how much indentation to add when a line
|
wenzelm@28762
|
331 |
break occurs within the block. If the parenthesis is not followed
|
wenzelm@28762
|
332 |
by digits, the indentation defaults to 0. A block specified via
|
wenzelm@28771
|
333 |
@{verbatim "(00"} is unbreakable.
|
wenzelm@28762
|
334 |
|
wenzelm@28771
|
335 |
\item @{verbatim ")"} closes a pretty printing block.
|
wenzelm@28762
|
336 |
|
wenzelm@28771
|
337 |
\item @{verbatim "//"} forces a line break.
|
wenzelm@28762
|
338 |
|
wenzelm@28771
|
339 |
\item @{verbatim "/"}@{text s} allows a line break. Here @{text s}
|
wenzelm@28771
|
340 |
stands for the string of spaces (zero or more) right after the
|
wenzelm@28771
|
341 |
slash. These spaces are printed if the break is \emph{not} taken.
|
wenzelm@28762
|
342 |
|
wenzelm@28778
|
343 |
\end{description}
|
wenzelm@28762
|
344 |
|
wenzelm@28771
|
345 |
For example, the template @{verbatim "(_ +/ _)"} specifies an infix
|
wenzelm@28771
|
346 |
operator. There are two argument positions; the delimiter
|
wenzelm@28771
|
347 |
@{verbatim "+"} is preceded by a space and followed by a space or
|
wenzelm@28771
|
348 |
line break; the entire phrase is a pretty printing block.
|
wenzelm@28762
|
349 |
|
wenzelm@28762
|
350 |
The general idea of pretty printing with blocks and breaks is also
|
wenzelm@28762
|
351 |
described in \cite{paulson-ml2}.
|
wenzelm@28762
|
352 |
*}
|
wenzelm@28762
|
353 |
|
wenzelm@28762
|
354 |
|
wenzelm@35418
|
355 |
section {* Explicit notation *}
|
wenzelm@28762
|
356 |
|
wenzelm@28762
|
357 |
text {*
|
wenzelm@28762
|
358 |
\begin{matharray}{rcll}
|
wenzelm@35418
|
359 |
@{command_def "type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
|
wenzelm@35418
|
360 |
@{command_def "no_type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
|
wenzelm@28762
|
361 |
@{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
|
wenzelm@28762
|
362 |
@{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
|
wenzelm@36524
|
363 |
@{command_def "write"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
|
wenzelm@28762
|
364 |
\end{matharray}
|
wenzelm@28762
|
365 |
|
wenzelm@28762
|
366 |
\begin{rail}
|
wenzelm@35418
|
367 |
('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
|
wenzelm@35418
|
368 |
;
|
wenzelm@30067
|
369 |
('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
|
wenzelm@28762
|
370 |
;
|
wenzelm@36524
|
371 |
'write' mode? (nameref structmixfix + 'and')
|
wenzelm@36524
|
372 |
;
|
wenzelm@28762
|
373 |
\end{rail}
|
wenzelm@28762
|
374 |
|
wenzelm@28762
|
375 |
\begin{description}
|
wenzelm@28762
|
376 |
|
wenzelm@35418
|
377 |
\item @{command "type_notation"}~@{text "c (mx)"} associates mixfix
|
wenzelm@35418
|
378 |
syntax with an existing type constructor. The arity of the
|
wenzelm@35418
|
379 |
constructor is retrieved from the context.
|
wenzelm@35418
|
380 |
|
wenzelm@35418
|
381 |
\item @{command "no_type_notation"} is similar to @{command
|
wenzelm@35418
|
382 |
"type_notation"}, but removes the specified syntax annotation from
|
wenzelm@35418
|
383 |
the present context.
|
wenzelm@35418
|
384 |
|
wenzelm@28762
|
385 |
\item @{command "notation"}~@{text "c (mx)"} associates mixfix
|
wenzelm@35418
|
386 |
syntax with an existing constant or fixed variable. The type
|
wenzelm@35418
|
387 |
declaration of the given entity is retrieved from the context.
|
wenzelm@28762
|
388 |
|
wenzelm@28762
|
389 |
\item @{command "no_notation"} is similar to @{command "notation"},
|
wenzelm@28762
|
390 |
but removes the specified syntax annotation from the present
|
wenzelm@28762
|
391 |
context.
|
wenzelm@28762
|
392 |
|
wenzelm@36524
|
393 |
\item @{command "write"} is similar to @{command "notation"}, but
|
wenzelm@36524
|
394 |
works within an Isar proof body.
|
wenzelm@36524
|
395 |
|
wenzelm@28762
|
396 |
\end{description}
|
wenzelm@35418
|
397 |
|
wenzelm@36524
|
398 |
Note that the more primitive commands @{command "syntax"} and
|
wenzelm@36524
|
399 |
@{command "no_syntax"} (\secref{sec:syn-trans}) provide raw access
|
wenzelm@36524
|
400 |
to the syntax tables of a global theory.
|
wenzelm@28762
|
401 |
*}
|
wenzelm@28762
|
402 |
|
wenzelm@28778
|
403 |
|
wenzelm@28778
|
404 |
section {* The Pure syntax \label{sec:pure-syntax} *}
|
wenzelm@28769
|
405 |
|
wenzelm@28777
|
406 |
subsection {* Priority grammars \label{sec:priority-grammar} *}
|
wenzelm@28769
|
407 |
|
wenzelm@28769
|
408 |
text {* A context-free grammar consists of a set of \emph{terminal
|
wenzelm@28769
|
409 |
symbols}, a set of \emph{nonterminal symbols} and a set of
|
wenzelm@28769
|
410 |
\emph{productions}. Productions have the form @{text "A = \<gamma>"},
|
wenzelm@28769
|
411 |
where @{text A} is a nonterminal and @{text \<gamma>} is a string of
|
wenzelm@28769
|
412 |
terminals and nonterminals. One designated nonterminal is called
|
wenzelm@28769
|
413 |
the \emph{root symbol}. The language defined by the grammar
|
wenzelm@28769
|
414 |
consists of all strings of terminals that can be derived from the
|
wenzelm@28769
|
415 |
root symbol by applying productions as rewrite rules.
|
wenzelm@28769
|
416 |
|
wenzelm@28769
|
417 |
The standard Isabelle parser for inner syntax uses a \emph{priority
|
wenzelm@28769
|
418 |
grammar}. Each nonterminal is decorated by an integer priority:
|
wenzelm@28769
|
419 |
@{text "A\<^sup>(\<^sup>p\<^sup>)"}. In a derivation, @{text "A\<^sup>(\<^sup>p\<^sup>)"} may be rewritten
|
wenzelm@28769
|
420 |
using a production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} only if @{text "p \<le> q"}. Any
|
wenzelm@28769
|
421 |
priority grammar can be translated into a normal context-free
|
wenzelm@28769
|
422 |
grammar by introducing new nonterminals and productions.
|
wenzelm@28769
|
423 |
|
wenzelm@28769
|
424 |
\medskip Formally, a set of context free productions @{text G}
|
wenzelm@28769
|
425 |
induces a derivation relation @{text "\<longrightarrow>\<^sub>G"} as follows. Let @{text
|
wenzelm@28769
|
426 |
\<alpha>} and @{text \<beta>} denote strings of terminal or nonterminal symbols.
|
wenzelm@28774
|
427 |
Then @{text "\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>"} holds if and only if @{text G}
|
wenzelm@28774
|
428 |
contains some production @{text "A\<^sup>(\<^sup>q\<^sup>) = \<gamma>"} for @{text "p \<le> q"}.
|
wenzelm@28769
|
429 |
|
wenzelm@28769
|
430 |
\medskip The following grammar for arithmetic expressions
|
wenzelm@28769
|
431 |
demonstrates how binding power and associativity of operators can be
|
wenzelm@28769
|
432 |
enforced by priorities.
|
wenzelm@28769
|
433 |
|
wenzelm@28769
|
434 |
\begin{center}
|
wenzelm@28769
|
435 |
\begin{tabular}{rclr}
|
wenzelm@28774
|
436 |
@{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim "("} @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim ")"} \\
|
wenzelm@28769
|
437 |
@{text "A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "="} & @{verbatim 0} \\
|
wenzelm@28769
|
438 |
@{text "A\<^sup>(\<^sup>0\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} \\
|
wenzelm@28769
|
439 |
@{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "="} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} \\
|
wenzelm@28769
|
440 |
@{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "="} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} \\
|
wenzelm@28769
|
441 |
\end{tabular}
|
wenzelm@28769
|
442 |
\end{center}
|
wenzelm@28769
|
443 |
The choice of priorities determines that @{verbatim "-"} binds
|
wenzelm@28769
|
444 |
tighter than @{verbatim "*"}, which binds tighter than @{verbatim
|
wenzelm@28769
|
445 |
"+"}. Furthermore @{verbatim "+"} associates to the left and
|
wenzelm@28769
|
446 |
@{verbatim "*"} to the right.
|
wenzelm@28769
|
447 |
|
wenzelm@28769
|
448 |
\medskip For clarity, grammars obey these conventions:
|
wenzelm@28769
|
449 |
\begin{itemize}
|
wenzelm@28769
|
450 |
|
wenzelm@28769
|
451 |
\item All priorities must lie between 0 and 1000.
|
wenzelm@28769
|
452 |
|
wenzelm@28769
|
453 |
\item Priority 0 on the right-hand side and priority 1000 on the
|
wenzelm@28769
|
454 |
left-hand side may be omitted.
|
wenzelm@28769
|
455 |
|
wenzelm@28769
|
456 |
\item The production @{text "A\<^sup>(\<^sup>p\<^sup>) = \<alpha>"} is written as @{text "A = \<alpha>
|
wenzelm@28769
|
457 |
(p)"}, i.e.\ the priority of the left-hand side actually appears in
|
wenzelm@28769
|
458 |
a column on the far right.
|
wenzelm@28769
|
459 |
|
wenzelm@28769
|
460 |
\item Alternatives are separated by @{text "|"}.
|
wenzelm@28769
|
461 |
|
wenzelm@28769
|
462 |
\item Repetition is indicated by dots @{text "(\<dots>)"} in an informal
|
wenzelm@28769
|
463 |
but obvious way.
|
wenzelm@28769
|
464 |
|
wenzelm@28769
|
465 |
\end{itemize}
|
wenzelm@28769
|
466 |
|
wenzelm@28769
|
467 |
Using these conventions, the example grammar specification above
|
wenzelm@28769
|
468 |
takes the form:
|
wenzelm@28769
|
469 |
\begin{center}
|
wenzelm@28769
|
470 |
\begin{tabular}{rclc}
|
wenzelm@28774
|
471 |
@{text A} & @{text "="} & @{verbatim "("} @{text A} @{verbatim ")"} \\
|
wenzelm@28774
|
472 |
& @{text "|"} & @{verbatim 0} & \qquad\qquad \\
|
wenzelm@28769
|
473 |
& @{text "|"} & @{text A} @{verbatim "+"} @{text "A\<^sup>(\<^sup>1\<^sup>)"} & @{text "(0)"} \\
|
wenzelm@28769
|
474 |
& @{text "|"} & @{text "A\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "*"} @{text "A\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
|
wenzelm@28769
|
475 |
& @{text "|"} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
|
wenzelm@28769
|
476 |
\end{tabular}
|
wenzelm@28769
|
477 |
\end{center}
|
wenzelm@28769
|
478 |
*}
|
wenzelm@28769
|
479 |
|
wenzelm@28769
|
480 |
|
wenzelm@28770
|
481 |
subsection {* The Pure grammar *}
|
wenzelm@28770
|
482 |
|
wenzelm@28770
|
483 |
text {*
|
wenzelm@28773
|
484 |
The priority grammar of the @{text "Pure"} theory is defined as follows:
|
wenzelm@28773
|
485 |
|
wenzelm@28774
|
486 |
%FIXME syntax for "index" (?)
|
wenzelm@28774
|
487 |
%FIXME "op" versions of ==> etc. (?)
|
wenzelm@28774
|
488 |
|
wenzelm@28770
|
489 |
\begin{center}
|
wenzelm@28773
|
490 |
\begin{supertabular}{rclr}
|
wenzelm@28770
|
491 |
|
wenzelm@28778
|
492 |
@{syntax_def (inner) any} & = & @{text "prop | logic"} \\\\
|
wenzelm@28770
|
493 |
|
wenzelm@28778
|
494 |
@{syntax_def (inner) prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\
|
wenzelm@28772
|
495 |
& @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
|
wenzelm@28773
|
496 |
& @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
|
wenzelm@28772
|
497 |
& @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
|
wenzelm@28773
|
498 |
& @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
|
wenzelm@28856
|
499 |
& @{text "|"} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
|
wenzelm@28772
|
500 |
& @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
|
wenzelm@28773
|
501 |
& @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
|
wenzelm@28772
|
502 |
& @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
|
wenzelm@28773
|
503 |
& @{text "|"} & @{text "\<lbrakk>"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{text "\<rbrakk>"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
|
wenzelm@28772
|
504 |
& @{text "|"} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
|
wenzelm@28773
|
505 |
& @{text "|"} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
|
wenzelm@28773
|
506 |
& @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\
|
wenzelm@28773
|
507 |
& @{text "|"} & @{verbatim SORT_CONSTRAINT} @{verbatim "("} @{text type} @{verbatim ")"} \\
|
wenzelm@28856
|
508 |
& @{text "|"} & @{verbatim TERM} @{text logic} \\
|
wenzelm@28773
|
509 |
& @{text "|"} & @{verbatim PROP} @{text aprop} \\\\
|
wenzelm@28772
|
510 |
|
wenzelm@28856
|
511 |
@{syntax_def (inner) aprop} & = & @{verbatim "("} @{text aprop} @{verbatim ")"} \\
|
wenzelm@28856
|
512 |
& @{text "|"} & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\
|
wenzelm@28856
|
513 |
& @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\
|
wenzelm@28773
|
514 |
& @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\\\
|
wenzelm@28772
|
515 |
|
wenzelm@28778
|
516 |
@{syntax_def (inner) logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\
|
wenzelm@28772
|
517 |
& @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
|
wenzelm@28773
|
518 |
& @{text "|"} & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\
|
wenzelm@28856
|
519 |
& @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\
|
wenzelm@28773
|
520 |
& @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\
|
wenzelm@28772
|
521 |
& @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
|
wenzelm@28773
|
522 |
& @{text "|"} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
|
wenzelm@28772
|
523 |
& @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\
|
wenzelm@28772
|
524 |
|
wenzelm@28778
|
525 |
@{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text " | id | "}@{verbatim "_"} \\
|
wenzelm@28773
|
526 |
& @{text "|"} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\
|
wenzelm@28773
|
527 |
& @{text "|"} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\
|
wenzelm@28772
|
528 |
|
wenzelm@28778
|
529 |
@{syntax_def (inner) idts} & = & @{text "idt | idt\<^sup>(\<^sup>1\<^sup>) idts"} & @{text "(0)"} \\\\
|
wenzelm@28772
|
530 |
|
wenzelm@28778
|
531 |
@{syntax_def (inner) pttrn} & = & @{text idt} \\\\
|
wenzelm@28772
|
532 |
|
wenzelm@28778
|
533 |
@{syntax_def (inner) pttrns} & = & @{text "pttrn | pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} & @{text "(0)"} \\\\
|
wenzelm@28774
|
534 |
|
wenzelm@28778
|
535 |
@{syntax_def (inner) type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\
|
wenzelm@28773
|
536 |
& @{text "|"} & @{text "tid | tvar | "}@{verbatim "_"} \\
|
wenzelm@28773
|
537 |
& @{text "|"} & @{text "tid"} @{verbatim "::"} @{text "sort | tvar "}@{verbatim "::"} @{text "sort | "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\
|
wenzelm@28772
|
538 |
& @{text "|"} & @{text "id | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) id | "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text id} \\
|
wenzelm@30067
|
539 |
& @{text "|"} & @{text "longid | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) longid"} \\
|
wenzelm@30067
|
540 |
& @{text "|"} & @{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text longid} \\
|
wenzelm@28772
|
541 |
& @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
|
wenzelm@28773
|
542 |
& @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\
|
wenzelm@28773
|
543 |
& @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
|
wenzelm@28773
|
544 |
& @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\\\
|
wenzelm@28772
|
545 |
|
wenzelm@30067
|
546 |
@{syntax_def (inner) sort} & = & @{text "id | longid | "}@{verbatim "{}"} \\
|
wenzelm@30067
|
547 |
& @{text "|"} & @{verbatim "{"} @{text "(id | longid)"} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text "(id | longid)"} @{verbatim "}"} \\
|
wenzelm@28773
|
548 |
\end{supertabular}
|
wenzelm@28770
|
549 |
\end{center}
|
wenzelm@28770
|
550 |
|
wenzelm@28774
|
551 |
\medskip Here literal terminals are printed @{verbatim "verbatim"};
|
wenzelm@28774
|
552 |
see also \secref{sec:inner-lex} for further token categories of the
|
wenzelm@28774
|
553 |
inner syntax. The meaning of the nonterminals defined by the above
|
wenzelm@28774
|
554 |
grammar is as follows:
|
wenzelm@28770
|
555 |
|
wenzelm@28770
|
556 |
\begin{description}
|
wenzelm@28770
|
557 |
|
wenzelm@28778
|
558 |
\item @{syntax_ref (inner) any} denotes any term.
|
wenzelm@28770
|
559 |
|
wenzelm@28778
|
560 |
\item @{syntax_ref (inner) prop} denotes meta-level propositions,
|
wenzelm@28778
|
561 |
which are terms of type @{typ prop}. The syntax of such formulae of
|
wenzelm@28778
|
562 |
the meta-logic is carefully distinguished from usual conventions for
|
wenzelm@28778
|
563 |
object-logics. In particular, plain @{text "\<lambda>"}-term notation is
|
wenzelm@28778
|
564 |
\emph{not} recognized as @{syntax (inner) prop}.
|
wenzelm@28770
|
565 |
|
wenzelm@28778
|
566 |
\item @{syntax_ref (inner) aprop} denotes atomic propositions, which
|
wenzelm@28778
|
567 |
are embedded into regular @{syntax (inner) prop} by means of an
|
wenzelm@28778
|
568 |
explicit @{verbatim PROP} token.
|
wenzelm@28770
|
569 |
|
wenzelm@28770
|
570 |
Terms of type @{typ prop} with non-constant head, e.g.\ a plain
|
wenzelm@28770
|
571 |
variable, are printed in this form. Constants that yield type @{typ
|
wenzelm@28770
|
572 |
prop} are expected to provide their own concrete syntax; otherwise
|
wenzelm@28778
|
573 |
the printed version will appear like @{syntax (inner) logic} and
|
wenzelm@28778
|
574 |
cannot be parsed again as @{syntax (inner) prop}.
|
wenzelm@28770
|
575 |
|
wenzelm@28778
|
576 |
\item @{syntax_ref (inner) logic} denotes arbitrary terms of a
|
wenzelm@28778
|
577 |
logical type, excluding type @{typ prop}. This is the main
|
wenzelm@28778
|
578 |
syntactic category of object-logic entities, covering plain @{text
|
wenzelm@28778
|
579 |
\<lambda>}-term notation (variables, abstraction, application), plus
|
wenzelm@28778
|
580 |
anything defined by the user.
|
wenzelm@28770
|
581 |
|
wenzelm@28770
|
582 |
When specifying notation for logical entities, all logical types
|
wenzelm@28770
|
583 |
(excluding @{typ prop}) are \emph{collapsed} to this single category
|
wenzelm@28778
|
584 |
of @{syntax (inner) logic}.
|
wenzelm@28770
|
585 |
|
wenzelm@28778
|
586 |
\item @{syntax_ref (inner) idt} denotes identifiers, possibly
|
wenzelm@28778
|
587 |
constrained by types.
|
wenzelm@28770
|
588 |
|
wenzelm@28778
|
589 |
\item @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref
|
wenzelm@28778
|
590 |
(inner) idt}. This is the most basic category for variables in
|
wenzelm@28778
|
591 |
iterated binders, such as @{text "\<lambda>"} or @{text "\<And>"}.
|
wenzelm@28770
|
592 |
|
wenzelm@28778
|
593 |
\item @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns}
|
wenzelm@28778
|
594 |
denote patterns for abstraction, cases bindings etc. In Pure, these
|
wenzelm@28778
|
595 |
categories start as a merely copy of @{syntax (inner) idt} and
|
wenzelm@28778
|
596 |
@{syntax (inner) idts}, respectively. Object-logics may add
|
wenzelm@28778
|
597 |
additional productions for binding forms.
|
wenzelm@28770
|
598 |
|
wenzelm@28778
|
599 |
\item @{syntax_ref (inner) type} denotes types of the meta-logic.
|
wenzelm@28770
|
600 |
|
wenzelm@28778
|
601 |
\item @{syntax_ref (inner) sort} denotes meta-level sorts.
|
wenzelm@28770
|
602 |
|
wenzelm@28770
|
603 |
\end{description}
|
wenzelm@28770
|
604 |
|
wenzelm@28774
|
605 |
Here are some further explanations of certain syntax features.
|
wenzelm@28770
|
606 |
|
wenzelm@28773
|
607 |
\begin{itemize}
|
wenzelm@28773
|
608 |
|
wenzelm@28778
|
609 |
\item In @{syntax (inner) idts}, note that @{text "x :: nat y"} is
|
wenzelm@28778
|
610 |
parsed as @{text "x :: (nat y)"}, treating @{text y} like a type
|
wenzelm@28778
|
611 |
constructor applied to @{text nat}. To avoid this interpretation,
|
wenzelm@28778
|
612 |
write @{text "(x :: nat) y"} with explicit parentheses.
|
wenzelm@28773
|
613 |
|
wenzelm@28773
|
614 |
\item Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x ::
|
wenzelm@28770
|
615 |
(nat y :: nat)"}. The correct form is @{text "(x :: nat) (y ::
|
wenzelm@28770
|
616 |
nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the
|
wenzelm@28770
|
617 |
sequence of identifiers.
|
wenzelm@28770
|
618 |
|
wenzelm@28773
|
619 |
\item Type constraints for terms bind very weakly. For example,
|
wenzelm@28773
|
620 |
@{text "x < y :: nat"} is normally parsed as @{text "(x < y) ::
|
wenzelm@28773
|
621 |
nat"}, unless @{text "<"} has a very low priority, in which case the
|
wenzelm@28773
|
622 |
input is likely to be ambiguous. The correct form is @{text "x < (y
|
wenzelm@28773
|
623 |
:: nat)"}.
|
wenzelm@28773
|
624 |
|
wenzelm@28773
|
625 |
\item Constraints may be either written with two literal colons
|
wenzelm@28773
|
626 |
``@{verbatim "::"}'' or the double-colon symbol @{verbatim "\<Colon>"},
|
wenzelm@28774
|
627 |
which actually looks exactly the same in some {\LaTeX} styles.
|
wenzelm@28773
|
628 |
|
wenzelm@28774
|
629 |
\item Dummy variables (written as underscore) may occur in different
|
wenzelm@28774
|
630 |
roles.
|
wenzelm@28773
|
631 |
|
wenzelm@28773
|
632 |
\begin{description}
|
wenzelm@28773
|
633 |
|
wenzelm@28774
|
634 |
\item A type ``@{text "_"}'' or ``@{text "_ :: sort"}'' acts like an
|
wenzelm@28774
|
635 |
anonymous inference parameter, which is filled-in according to the
|
wenzelm@28774
|
636 |
most general type produced by the type-checking phase.
|
wenzelm@28773
|
637 |
|
wenzelm@28774
|
638 |
\item A bound ``@{text "_"}'' refers to a vacuous abstraction, where
|
wenzelm@28774
|
639 |
the body does not refer to the binding introduced here. As in the
|
wenzelm@28774
|
640 |
term @{term "\<lambda>x _. x"}, which is @{text "\<alpha>"}-equivalent to @{text
|
wenzelm@28774
|
641 |
"\<lambda>x y. x"}.
|
wenzelm@28773
|
642 |
|
wenzelm@28774
|
643 |
\item A free ``@{text "_"}'' refers to an implicit outer binding.
|
wenzelm@28773
|
644 |
Higher definitional packages usually allow forms like @{text "f x _
|
wenzelm@28774
|
645 |
= x"}.
|
wenzelm@28773
|
646 |
|
wenzelm@28774
|
647 |
\item A schematic ``@{text "_"}'' (within a term pattern, see
|
wenzelm@28774
|
648 |
\secref{sec:term-decls}) refers to an anonymous variable that is
|
wenzelm@28774
|
649 |
implicitly abstracted over its context of locally bound variables.
|
wenzelm@28774
|
650 |
For example, this allows pattern matching of @{text "{x. f x = g
|
wenzelm@28774
|
651 |
x}"} against @{text "{x. _ = _}"}, or even @{text "{_. _ = _}"} by
|
wenzelm@28774
|
652 |
using both bound and schematic dummies.
|
wenzelm@28773
|
653 |
|
wenzelm@28773
|
654 |
\end{description}
|
wenzelm@28773
|
655 |
|
wenzelm@28774
|
656 |
\item The three literal dots ``@{verbatim "..."}'' may be also
|
wenzelm@28774
|
657 |
written as ellipsis symbol @{verbatim "\<dots>"}. In both cases this
|
wenzelm@28774
|
658 |
refers to a special schematic variable, which is bound in the
|
wenzelm@28774
|
659 |
context. This special term abbreviation works nicely with
|
wenzelm@28774
|
660 |
calculational reasoning (\secref{sec:calculation}).
|
wenzelm@28774
|
661 |
|
wenzelm@28773
|
662 |
\end{itemize}
|
wenzelm@28770
|
663 |
*}
|
wenzelm@28770
|
664 |
|
wenzelm@28777
|
665 |
|
wenzelm@28774
|
666 |
section {* Lexical matters \label{sec:inner-lex} *}
|
wenzelm@28774
|
667 |
|
wenzelm@28777
|
668 |
text {* The inner lexical syntax vaguely resembles the outer one
|
wenzelm@28777
|
669 |
(\secref{sec:outer-lex}), but some details are different. There are
|
wenzelm@28777
|
670 |
two main categories of inner syntax tokens:
|
wenzelm@28777
|
671 |
|
wenzelm@28777
|
672 |
\begin{enumerate}
|
wenzelm@28777
|
673 |
|
wenzelm@28777
|
674 |
\item \emph{delimiters} --- the literal tokens occurring in
|
wenzelm@28777
|
675 |
productions of the given priority grammar (cf.\
|
wenzelm@28777
|
676 |
\secref{sec:priority-grammar});
|
wenzelm@28777
|
677 |
|
wenzelm@28777
|
678 |
\item \emph{named tokens} --- various categories of identifiers etc.
|
wenzelm@28777
|
679 |
|
wenzelm@28777
|
680 |
\end{enumerate}
|
wenzelm@28777
|
681 |
|
wenzelm@28777
|
682 |
Delimiters override named tokens and may thus render certain
|
wenzelm@28777
|
683 |
identifiers inaccessible. Sometimes the logical context admits
|
wenzelm@28777
|
684 |
alternative ways to refer to the same entity, potentially via
|
wenzelm@28777
|
685 |
qualified names.
|
wenzelm@28777
|
686 |
|
wenzelm@28777
|
687 |
\medskip The categories for named tokens are defined once and for
|
wenzelm@28777
|
688 |
all as follows, reusing some categories of the outer token syntax
|
wenzelm@28777
|
689 |
(\secref{sec:outer-lex}).
|
wenzelm@28777
|
690 |
|
wenzelm@28777
|
691 |
\begin{center}
|
wenzelm@28777
|
692 |
\begin{supertabular}{rcl}
|
wenzelm@28777
|
693 |
@{syntax_def (inner) id} & = & @{syntax_ref ident} \\
|
wenzelm@28777
|
694 |
@{syntax_def (inner) longid} & = & @{syntax_ref longident} \\
|
wenzelm@28777
|
695 |
@{syntax_def (inner) var} & = & @{syntax_ref var} \\
|
wenzelm@28777
|
696 |
@{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
|
wenzelm@28777
|
697 |
@{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
|
wenzelm@28777
|
698 |
@{syntax_def (inner) num} & = & @{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat} \\
|
wenzelm@29157
|
699 |
@{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
|
wenzelm@28777
|
700 |
@{syntax_def (inner) xnum} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\
|
wenzelm@28777
|
701 |
|
wenzelm@28777
|
702 |
@{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
|
wenzelm@28777
|
703 |
\end{supertabular}
|
wenzelm@28777
|
704 |
\end{center}
|
wenzelm@28777
|
705 |
|
wenzelm@29157
|
706 |
The token categories @{syntax (inner) num}, @{syntax (inner)
|
wenzelm@29157
|
707 |
float_token}, @{syntax (inner) xnum}, and @{syntax (inner) xstr} are
|
wenzelm@29157
|
708 |
not used in Pure. Object-logics may implement numerals and string
|
wenzelm@29157
|
709 |
constants by adding appropriate syntax declarations, together with
|
wenzelm@29157
|
710 |
some translation functions (e.g.\ see Isabelle/HOL).
|
wenzelm@29157
|
711 |
|
wenzelm@29157
|
712 |
The derived categories @{syntax_def (inner) num_const} and
|
wenzelm@29157
|
713 |
@{syntax_def (inner) float_const} provide robust access to @{syntax
|
wenzelm@29157
|
714 |
(inner) num}, and @{syntax (inner) float_token}, respectively: the
|
wenzelm@29157
|
715 |
syntax tree holds a syntactic constant instead of a free variable.
|
wenzelm@28777
|
716 |
*}
|
wenzelm@28774
|
717 |
|
wenzelm@28770
|
718 |
|
wenzelm@28762
|
719 |
section {* Syntax and translations \label{sec:syn-trans} *}
|
wenzelm@28762
|
720 |
|
wenzelm@28762
|
721 |
text {*
|
wenzelm@28762
|
722 |
\begin{matharray}{rcl}
|
wenzelm@28762
|
723 |
@{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\
|
wenzelm@28762
|
724 |
@{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
|
wenzelm@28762
|
725 |
@{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\
|
wenzelm@28762
|
726 |
@{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\
|
wenzelm@28762
|
727 |
@{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
|
wenzelm@28762
|
728 |
\end{matharray}
|
wenzelm@28762
|
729 |
|
wenzelm@28762
|
730 |
\begin{rail}
|
wenzelm@28762
|
731 |
'nonterminals' (name +)
|
wenzelm@28762
|
732 |
;
|
wenzelm@28762
|
733 |
('syntax' | 'no\_syntax') mode? (constdecl +)
|
wenzelm@28762
|
734 |
;
|
wenzelm@28762
|
735 |
('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
|
wenzelm@28762
|
736 |
;
|
wenzelm@28762
|
737 |
|
wenzelm@28762
|
738 |
mode: ('(' ( name | 'output' | name 'output' ) ')')
|
wenzelm@28762
|
739 |
;
|
wenzelm@28762
|
740 |
transpat: ('(' nameref ')')? string
|
wenzelm@28762
|
741 |
;
|
wenzelm@28762
|
742 |
\end{rail}
|
wenzelm@28762
|
743 |
|
wenzelm@28762
|
744 |
\begin{description}
|
wenzelm@28762
|
745 |
|
wenzelm@28762
|
746 |
\item @{command "nonterminals"}~@{text c} declares a type
|
wenzelm@28762
|
747 |
constructor @{text c} (without arguments) to act as purely syntactic
|
wenzelm@28762
|
748 |
type: a nonterminal symbol of the inner syntax.
|
wenzelm@28762
|
749 |
|
wenzelm@28762
|
750 |
\item @{command "syntax"}~@{text "(mode) decls"} is similar to
|
wenzelm@28762
|
751 |
@{command "consts"}~@{text decls}, except that the actual logical
|
wenzelm@28762
|
752 |
signature extension is omitted. Thus the context free grammar of
|
wenzelm@28762
|
753 |
Isabelle's inner syntax may be augmented in arbitrary ways,
|
wenzelm@28762
|
754 |
independently of the logic. The @{text mode} argument refers to the
|
wenzelm@28762
|
755 |
print mode that the grammar rules belong; unless the @{keyword_ref
|
wenzelm@28762
|
756 |
"output"} indicator is given, all productions are added both to the
|
wenzelm@28762
|
757 |
input and output grammar.
|
wenzelm@28762
|
758 |
|
wenzelm@28762
|
759 |
\item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar
|
wenzelm@28762
|
760 |
declarations (and translations) resulting from @{text decls}, which
|
wenzelm@28762
|
761 |
are interpreted in the same manner as for @{command "syntax"} above.
|
wenzelm@28762
|
762 |
|
wenzelm@28762
|
763 |
\item @{command "translations"}~@{text rules} specifies syntactic
|
wenzelm@28762
|
764 |
translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
|
wenzelm@28762
|
765 |
parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
|
wenzelm@28762
|
766 |
Translation patterns may be prefixed by the syntactic category to be
|
wenzelm@28762
|
767 |
used for parsing; the default is @{text logic}.
|
wenzelm@28762
|
768 |
|
wenzelm@28762
|
769 |
\item @{command "no_translations"}~@{text rules} removes syntactic
|
wenzelm@28762
|
770 |
translation rules, which are interpreted in the same manner as for
|
wenzelm@28762
|
771 |
@{command "translations"} above.
|
wenzelm@28762
|
772 |
|
wenzelm@28762
|
773 |
\end{description}
|
wenzelm@28762
|
774 |
*}
|
wenzelm@28762
|
775 |
|
wenzelm@28762
|
776 |
|
wenzelm@28779
|
777 |
section {* Syntax translation functions \label{sec:tr-funs} *}
|
wenzelm@28762
|
778 |
|
wenzelm@28762
|
779 |
text {*
|
wenzelm@28762
|
780 |
\begin{matharray}{rcl}
|
wenzelm@28762
|
781 |
@{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
|
wenzelm@28762
|
782 |
@{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
|
wenzelm@28762
|
783 |
@{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
|
wenzelm@28762
|
784 |
@{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
|
wenzelm@28762
|
785 |
@{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
|
wenzelm@28762
|
786 |
\end{matharray}
|
wenzelm@28762
|
787 |
|
wenzelm@28762
|
788 |
\begin{rail}
|
wenzelm@28762
|
789 |
( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
|
wenzelm@28762
|
790 |
'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
|
wenzelm@28762
|
791 |
;
|
wenzelm@28762
|
792 |
\end{rail}
|
wenzelm@28762
|
793 |
|
wenzelm@28762
|
794 |
Syntax translation functions written in ML admit almost arbitrary
|
wenzelm@28762
|
795 |
manipulations of Isabelle's inner syntax. Any of the above commands
|
wenzelm@28762
|
796 |
have a single \railqtok{text} argument that refers to an ML
|
wenzelm@28762
|
797 |
expression of appropriate type, which are as follows by default:
|
wenzelm@28762
|
798 |
|
wenzelm@28762
|
799 |
%FIXME proper antiquotations
|
wenzelm@28762
|
800 |
\begin{ttbox}
|
wenzelm@28762
|
801 |
val parse_ast_translation : (string * (ast list -> ast)) list
|
wenzelm@28762
|
802 |
val parse_translation : (string * (term list -> term)) list
|
wenzelm@28762
|
803 |
val print_translation : (string * (term list -> term)) list
|
wenzelm@28762
|
804 |
val typed_print_translation :
|
wenzelm@28762
|
805 |
(string * (bool -> typ -> term list -> term)) list
|
wenzelm@28762
|
806 |
val print_ast_translation : (string * (ast list -> ast)) list
|
wenzelm@28762
|
807 |
\end{ttbox}
|
wenzelm@28762
|
808 |
|
wenzelm@28762
|
809 |
If the @{text "(advanced)"} option is given, the corresponding
|
wenzelm@28762
|
810 |
translation functions may depend on the current theory or proof
|
wenzelm@28762
|
811 |
context. This allows to implement advanced syntax mechanisms, as
|
wenzelm@28762
|
812 |
translations functions may refer to specific theory declarations or
|
wenzelm@28762
|
813 |
auxiliary proof data.
|
wenzelm@28762
|
814 |
|
wenzelm@30397
|
815 |
See also \cite{isabelle-ref} for more information on the general
|
wenzelm@30397
|
816 |
concept of syntax transformations in Isabelle.
|
wenzelm@28762
|
817 |
|
wenzelm@28762
|
818 |
%FIXME proper antiquotations
|
wenzelm@28762
|
819 |
\begin{ttbox}
|
wenzelm@28762
|
820 |
val parse_ast_translation:
|
wenzelm@28762
|
821 |
(string * (Proof.context -> ast list -> ast)) list
|
wenzelm@28762
|
822 |
val parse_translation:
|
wenzelm@28762
|
823 |
(string * (Proof.context -> term list -> term)) list
|
wenzelm@28762
|
824 |
val print_translation:
|
wenzelm@28762
|
825 |
(string * (Proof.context -> term list -> term)) list
|
wenzelm@28762
|
826 |
val typed_print_translation:
|
wenzelm@28762
|
827 |
(string * (Proof.context -> bool -> typ -> term list -> term)) list
|
wenzelm@28762
|
828 |
val print_ast_translation:
|
wenzelm@28762
|
829 |
(string * (Proof.context -> ast list -> ast)) list
|
wenzelm@28762
|
830 |
\end{ttbox}
|
wenzelm@28762
|
831 |
*}
|
wenzelm@28762
|
832 |
|
wenzelm@28779
|
833 |
|
wenzelm@28779
|
834 |
section {* Inspecting the syntax *}
|
wenzelm@28779
|
835 |
|
wenzelm@28779
|
836 |
text {*
|
wenzelm@28779
|
837 |
\begin{matharray}{rcl}
|
wenzelm@28779
|
838 |
@{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
|
wenzelm@28779
|
839 |
\end{matharray}
|
wenzelm@28779
|
840 |
|
wenzelm@28779
|
841 |
\begin{description}
|
wenzelm@28779
|
842 |
|
wenzelm@28779
|
843 |
\item @{command "print_syntax"} prints the inner syntax of the
|
wenzelm@28779
|
844 |
current context. The output can be quite large; the most important
|
wenzelm@28779
|
845 |
sections are explained below.
|
wenzelm@28779
|
846 |
|
wenzelm@28779
|
847 |
\begin{description}
|
wenzelm@28779
|
848 |
|
wenzelm@28779
|
849 |
\item @{text "lexicon"} lists the delimiters of the inner token
|
wenzelm@28779
|
850 |
language; see \secref{sec:inner-lex}.
|
wenzelm@28779
|
851 |
|
wenzelm@28779
|
852 |
\item @{text "prods"} lists the productions of the underlying
|
wenzelm@28779
|
853 |
priority grammar; see \secref{sec:priority-grammar}.
|
wenzelm@28779
|
854 |
|
wenzelm@28779
|
855 |
The nonterminal @{text "A\<^sup>(\<^sup>p\<^sup>)"} is rendered in plain text as @{text
|
wenzelm@28779
|
856 |
"A[p]"}; delimiters are quoted. Many productions have an extra
|
wenzelm@28779
|
857 |
@{text "\<dots> => name"}. These names later become the heads of parse
|
wenzelm@28779
|
858 |
trees; they also guide the pretty printer.
|
wenzelm@28779
|
859 |
|
wenzelm@28779
|
860 |
Productions without such parse tree names are called \emph{copy
|
wenzelm@28779
|
861 |
productions}. Their right-hand side must have exactly one
|
wenzelm@28779
|
862 |
nonterminal symbol (or named token). The parser does not create a
|
wenzelm@28779
|
863 |
new parse tree node for copy productions, but simply returns the
|
wenzelm@28779
|
864 |
parse tree of the right-hand symbol.
|
wenzelm@28779
|
865 |
|
wenzelm@28779
|
866 |
If the right-hand side of a copy production consists of a single
|
wenzelm@28779
|
867 |
nonterminal without any delimiters, then it is called a \emph{chain
|
wenzelm@28779
|
868 |
production}. Chain productions act as abbreviations: conceptually,
|
wenzelm@28779
|
869 |
they are removed from the grammar by adding new productions.
|
wenzelm@28779
|
870 |
Priority information attached to chain productions is ignored; only
|
wenzelm@28779
|
871 |
the dummy value @{text "-1"} is displayed.
|
wenzelm@28779
|
872 |
|
wenzelm@28856
|
873 |
\item @{text "print modes"} lists the alternative print modes
|
wenzelm@28779
|
874 |
provided by this grammar; see \secref{sec:print-modes}.
|
wenzelm@28779
|
875 |
|
wenzelm@28779
|
876 |
\item @{text "parse_rules"} and @{text "print_rules"} relate to
|
wenzelm@28779
|
877 |
syntax translations (macros); see \secref{sec:syn-trans}.
|
wenzelm@28779
|
878 |
|
wenzelm@28779
|
879 |
\item @{text "parse_ast_translation"} and @{text
|
wenzelm@28779
|
880 |
"print_ast_translation"} list sets of constants that invoke
|
wenzelm@28779
|
881 |
translation functions for abstract syntax trees, which are only
|
wenzelm@28779
|
882 |
required in very special situations; see \secref{sec:tr-funs}.
|
wenzelm@28779
|
883 |
|
wenzelm@28779
|
884 |
\item @{text "parse_translation"} and @{text "print_translation"}
|
wenzelm@28779
|
885 |
list the sets of constants that invoke regular translation
|
wenzelm@28779
|
886 |
functions; see \secref{sec:tr-funs}.
|
wenzelm@28779
|
887 |
|
wenzelm@28779
|
888 |
\end{description}
|
wenzelm@28779
|
889 |
|
wenzelm@28779
|
890 |
\end{description}
|
wenzelm@28779
|
891 |
*}
|
wenzelm@28779
|
892 |
|
wenzelm@28762
|
893 |
end
|