author | wenzelm |
Tue, 20 Oct 2015 23:53:40 +0200 | |
changeset 61493 | 0debd22f0c0e |
parent 61477 | e467ae7aa808 |
child 61494 | 63b18f758874 |
permissions | -rw-r--r-- |
28762 | 1 |
theory Inner_Syntax |
42651 | 2 |
imports Base Main |
28762 | 3 |
begin |
4 |
||
58618 | 5 |
chapter \<open>Inner syntax --- the term language \label{ch:inner-syntax}\<close> |
28762 | 6 |
|
58618 | 7 |
text \<open>The inner syntax of Isabelle provides concrete notation for |
61493 | 8 |
the main entities of the logical framework, notably \<open>\<lambda>\<close>-terms with types and type classes. Applications may either |
46282 | 9 |
extend existing syntactic categories by additional notation, or |
10 |
define new sub-languages that are linked to the standard term |
|
11 |
language via some explicit markers. For example @{verbatim |
|
61493 | 12 |
FOO}~\<open>foo\<close> could embed the syntax corresponding for some |
13 |
user-defined nonterminal \<open>foo\<close> --- within the bounds of the |
|
46282 | 14 |
given lexical syntax of Isabelle/Pure. |
15 |
||
16 |
The most basic way to specify concrete syntax for logical entities |
|
17 |
works via mixfix annotations (\secref{sec:mixfix}), which may be |
|
18 |
usually given as part of the original declaration or via explicit |
|
19 |
notation commands later on (\secref{sec:notation}). This already |
|
20 |
covers many needs of concrete syntax without having to understand |
|
21 |
the full complexity of inner syntax layers. |
|
22 |
||
23 |
Further details of the syntax engine involves the classical |
|
24 |
distinction of lexical language versus context-free grammar (see |
|
61477 | 25 |
\secref{sec:pure-syntax}), and various mechanisms for \<^emph>\<open>syntax |
26 |
transformations\<close> (see \secref{sec:syntax-transformations}). |
|
58618 | 27 |
\<close> |
46282 | 28 |
|
29 |
||
58618 | 30 |
section \<open>Printing logical entities\<close> |
28762 | 31 |
|
58618 | 32 |
subsection \<open>Diagnostic commands \label{sec:print-diag}\<close> |
28762 | 33 |
|
58618 | 34 |
text \<open> |
28762 | 35 |
\begin{matharray}{rcl} |
61493 | 36 |
@{command_def "typ"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
37 |
@{command_def "term"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
38 |
@{command_def "prop"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
39 |
@{command_def "thm"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
40 |
@{command_def "prf"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
41 |
@{command_def "full_prf"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
42 |
@{command_def "print_state"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\ |
|
28762 | 43 |
\end{matharray} |
44 |
||
45 |
These diagnostic commands assist interactive development by printing |
|
46 |
internal logical entities in a human-readable fashion. |
|
47 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55108
diff
changeset
|
48 |
@{rail \<open> |
48792 | 49 |
@@{command typ} @{syntax modes}? @{syntax type} ('::' @{syntax sort})? |
28762 | 50 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
51 |
@@{command term} @{syntax modes}? @{syntax term} |
28762 | 52 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
53 |
@@{command prop} @{syntax modes}? @{syntax prop} |
28762 | 54 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
55 |
@@{command thm} @{syntax modes}? @{syntax thmrefs} |
28762 | 56 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
57 |
( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thmrefs}? |
28762 | 58 |
; |
52430 | 59 |
@@{command print_state} @{syntax modes}? |
28762 | 60 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
61 |
@{syntax_def modes}: '(' (@{syntax name} + ) ')' |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55108
diff
changeset
|
62 |
\<close>} |
28762 | 63 |
|
61493 | 64 |
\<^descr> @{command "typ"}~\<open>\<tau>\<close> reads and prints a type expression |
48792 | 65 |
according to the current context. |
66 |
||
61493 | 67 |
\<^descr> @{command "typ"}~\<open>\<tau> :: s\<close> uses type-inference to |
68 |
determine the most general way to make \<open>\<tau>\<close> conform to sort |
|
69 |
\<open>s\<close>. For concrete \<open>\<tau>\<close> this checks if the type |
|
70 |
belongs to that sort. Dummy type parameters ``\<open>_\<close>'' |
|
48792 | 71 |
(underscore) are assigned to fresh type variables with most general |
72 |
sorts, according the the principles of type-inference. |
|
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
73 |
|
61493 | 74 |
\<^descr> @{command "term"}~\<open>t\<close> and @{command "prop"}~\<open>\<phi>\<close> |
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
75 |
read, type-check and print terms or propositions according to the |
61493 | 76 |
current theory or proof context; the inferred type of \<open>t\<close> is |
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
77 |
output as well. Note that these commands are also useful in |
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
78 |
inspecting the current environment of term abbreviations. |
28762 | 79 |
|
61493 | 80 |
\<^descr> @{command "thm"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> retrieves |
28762 | 81 |
theorems from the current theory or proof context. Note that any |
82 |
attributes included in the theorem specifications are applied to a |
|
83 |
temporary context derived from the current theory or proof; the |
|
61493 | 84 |
result is discarded, i.e.\ attributes involved in \<open>a\<^sub>1, |
85 |
\<dots>, a\<^sub>n\<close> do not have any permanent effect. |
|
28762 | 86 |
|
61439 | 87 |
\<^descr> @{command "prf"} displays the (compact) proof term of the |
28762 | 88 |
current proof state (if present), or of the given theorems. Note |
89 |
that this requires proof terms to be switched on for the current |
|
90 |
object logic (see the ``Proof terms'' section of the Isabelle |
|
91 |
reference manual for information on how to do this). |
|
92 |
||
61439 | 93 |
\<^descr> @{command "full_prf"} is like @{command "prf"}, but displays |
28762 | 94 |
the full proof term, i.e.\ also displays information omitted in the |
61493 | 95 |
compact proof term, which is denoted by ``\<open>_\<close>'' placeholders |
28762 | 96 |
there. |
97 |
||
61439 | 98 |
\<^descr> @{command "print_state"} prints the current proof state (if |
52430 | 99 |
present), including current facts and goals. |
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset
|
100 |
|
28762 | 101 |
|
61493 | 102 |
All of the diagnostic commands above admit a list of \<open>modes\<close> |
42926 | 103 |
to be specified, which is appended to the current print mode; see |
46284 | 104 |
also \secref{sec:print-modes}. Thus the output behavior may be |
105 |
modified according particular print mode features. For example, |
|
61493 | 106 |
@{command "print_state"}~\<open>(latex xsymbols)\<close> prints the |
52430 | 107 |
current proof state with mathematical symbols and special characters |
46284 | 108 |
represented in {\LaTeX} source, according to the Isabelle style |
60270 | 109 |
@{cite "isabelle-system"}. |
28762 | 110 |
|
111 |
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
|
112 |
systematic way to include formal items into the printed text |
|
113 |
document. |
|
58618 | 114 |
\<close> |
28762 | 115 |
|
116 |
||
58618 | 117 |
subsection \<open>Details of printed content\<close> |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
118 |
|
58618 | 119 |
text \<open> |
42655 | 120 |
\begin{tabular}{rcll} |
61493 | 121 |
@{attribute_def show_markup} & : & \<open>attribute\<close> \\ |
122 |
@{attribute_def show_types} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
123 |
@{attribute_def show_sorts} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
124 |
@{attribute_def show_consts} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
125 |
@{attribute_def show_abbrevs} & : & \<open>attribute\<close> & default \<open>true\<close> \\ |
|
126 |
@{attribute_def show_brackets} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
127 |
@{attribute_def names_long} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
128 |
@{attribute_def names_short} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
129 |
@{attribute_def names_unique} & : & \<open>attribute\<close> & default \<open>true\<close> \\ |
|
130 |
@{attribute_def eta_contract} & : & \<open>attribute\<close> & default \<open>true\<close> \\ |
|
131 |
@{attribute_def goals_limit} & : & \<open>attribute\<close> & default \<open>10\<close> \\ |
|
132 |
@{attribute_def show_main_goal} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
133 |
@{attribute_def show_hyps} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
134 |
@{attribute_def show_tags} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
135 |
@{attribute_def show_question_marks} & : & \<open>attribute\<close> & default \<open>true\<close> \\ |
|
42655 | 136 |
\end{tabular} |
61421 | 137 |
\<^medskip> |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
138 |
|
42655 | 139 |
These configuration options control the detail of information that |
140 |
is displayed for types, terms, theorems, goals etc. See also |
|
141 |
\secref{sec:config}. |
|
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
142 |
|
61439 | 143 |
\<^descr> @{attribute show_markup} controls direct inlining of markup |
49699 | 144 |
into the printed representation of formal entities --- notably type |
145 |
and sort constraints. This enables Prover IDE users to retrieve |
|
146 |
that information via tooltips or popups while hovering with the |
|
147 |
mouse over the output window, for example. Consequently, this |
|
58842 | 148 |
option is enabled by default for Isabelle/jEdit. |
49699 | 149 |
|
61439 | 150 |
\<^descr> @{attribute show_types} and @{attribute show_sorts} control |
42655 | 151 |
printing of type constraints for term variables, and sort |
152 |
constraints for type variables. By default, neither of these are |
|
153 |
shown in output. If @{attribute show_sorts} is enabled, types are |
|
49699 | 154 |
always shown as well. In Isabelle/jEdit, manual setting of these |
155 |
options is normally not required thanks to @{attribute show_markup} |
|
156 |
above. |
|
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
157 |
|
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
158 |
Note that displaying types and sorts may explain why a polymorphic |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
159 |
inference rule fails to resolve with some goal, or why a rewrite |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
160 |
rule does not apply as expected. |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
161 |
|
61439 | 162 |
\<^descr> @{attribute show_consts} controls printing of types of |
42655 | 163 |
constants when displaying a goal state. |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
164 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
165 |
Note that the output can be enormous, because polymorphic constants |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
166 |
often occur at several different type instances. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
167 |
|
61439 | 168 |
\<^descr> @{attribute show_abbrevs} controls folding of constant |
42655 | 169 |
abbreviations. |
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40255
diff
changeset
|
170 |
|
61439 | 171 |
\<^descr> @{attribute show_brackets} controls bracketing in pretty |
42655 | 172 |
printed output. If enabled, all sub-expressions of the pretty |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
173 |
printing tree will be parenthesized, even if this produces malformed |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
174 |
term syntax! This crude way of showing the internal structure of |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
175 |
pretty printed entities may occasionally help to diagnose problems |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
176 |
with operator priorities, for example. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
177 |
|
61439 | 178 |
\<^descr> @{attribute names_long}, @{attribute names_short}, and |
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42655
diff
changeset
|
179 |
@{attribute names_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
|
180 |
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
|
181 |
\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
|
182 |
same names. |
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42279
diff
changeset
|
183 |
|
61493 | 184 |
\<^descr> @{attribute eta_contract} controls \<open>\<eta>\<close>-contracted |
42655 | 185 |
printing of terms. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
186 |
|
61493 | 187 |
The \<open>\<eta>\<close>-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"}, |
188 |
provided \<open>x\<close> is not free in \<open>f\<close>. It asserts |
|
61477 | 189 |
\<^emph>\<open>extensionality\<close> of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv> |
61493 | 190 |
g x"} for all \<open>x\<close>. Higher-order unification frequently puts |
191 |
terms into a fully \<open>\<eta>\<close>-expanded form. For example, if \<open>F\<close> has type \<open>(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>\<close> then its expanded form is @{term |
|
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
192 |
"\<lambda>h. F (\<lambda>x. h x)"}. |
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
193 |
|
61493 | 194 |
Enabling @{attribute eta_contract} makes Isabelle perform \<open>\<eta>\<close>-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"} |
195 |
appears simply as \<open>F\<close>. |
|
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
196 |
|
61493 | 197 |
Note that the distinction between a term and its \<open>\<eta>\<close>-expanded |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
198 |
form occasionally matters. While higher-order resolution and |
61493 | 199 |
rewriting operate modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion, some other tools |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
200 |
might look at terms more discretely. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
201 |
|
61439 | 202 |
\<^descr> @{attribute goals_limit} controls the maximum number of |
51960
61ac1efe02c3
option "goals_limit", with more uniform description;
wenzelm
parents:
51657
diff
changeset
|
203 |
subgoals to be printed. |
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
204 |
|
61439 | 205 |
\<^descr> @{attribute show_main_goal} controls whether the main result |
42655 | 206 |
to be proven should be displayed. This information might be |
39130 | 207 |
relevant for schematic goals, to inspect the current claim that has |
208 |
been synthesized so far. |
|
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
209 |
|
61439 | 210 |
\<^descr> @{attribute show_hyps} controls printing of implicit |
42655 | 211 |
hypotheses of local facts. Normally, only those hypotheses are |
61477 | 212 |
displayed that are \<^emph>\<open>not\<close> covered by the assumptions of the |
42655 | 213 |
current context: this situation indicates a fault in some tool being |
214 |
used. |
|
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
215 |
|
61477 | 216 |
By enabling @{attribute show_hyps}, output of \<^emph>\<open>all\<close> hypotheses |
42655 | 217 |
can be enforced, which is occasionally useful for diagnostic |
218 |
purposes. |
|
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset
|
219 |
|
61439 | 220 |
\<^descr> @{attribute show_tags} controls printing of extra annotations |
42655 | 221 |
within theorems, such as internal position information, or the case |
222 |
names being attached by the attribute @{attribute case_names}. |
|
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
223 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
224 |
Note that the @{attribute tagged} and @{attribute untagged} |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
225 |
attributes provide low-level access to the collection of tags |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
226 |
associated with a theorem. |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
227 |
|
61439 | 228 |
\<^descr> @{attribute show_question_marks} controls printing of question |
61493 | 229 |
marks for schematic variables, such as \<open>?x\<close>. Only the leading |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
230 |
question mark is affected, the remaining text is unchanged |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
231 |
(including proper markup for schematic variables that might be |
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
232 |
relevant for user interfaces). |
58618 | 233 |
\<close> |
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
234 |
|
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset
|
235 |
|
58618 | 236 |
subsection \<open>Alternative print modes \label{sec:print-modes}\<close> |
46284 | 237 |
|
58618 | 238 |
text \<open> |
46284 | 239 |
\begin{mldecls} |
240 |
@{index_ML print_mode_value: "unit -> string list"} \\ |
|
241 |
@{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\ |
|
242 |
\end{mldecls} |
|
243 |
||
61477 | 244 |
The \<^emph>\<open>print mode\<close> facility allows to modify various operations |
46284 | 245 |
for printing. Commands like @{command typ}, @{command term}, |
246 |
@{command thm} (see \secref{sec:print-diag}) take additional print |
|
247 |
modes as optional argument. The underlying ML operations are as |
|
248 |
follows. |
|
249 |
||
61439 | 250 |
\<^descr> @{ML "print_mode_value ()"} yields the list of currently |
46284 | 251 |
active print mode names. This should be understood as symbolic |
252 |
representation of certain individual features for printing (with |
|
253 |
precedence from left to right). |
|
254 |
||
61493 | 255 |
\<^descr> @{ML Print_Mode.with_modes}~\<open>modes f x\<close> evaluates |
256 |
\<open>f x\<close> in an execution context where the print mode is |
|
257 |
prepended by the given \<open>modes\<close>. This provides a thread-safe |
|
46284 | 258 |
way to augment print modes. It is also monotonic in the set of mode |
259 |
names: it retains the default print mode that certain |
|
260 |
user-interfaces might have installed for their proper functioning! |
|
261 |
||
262 |
||
61421 | 263 |
\<^medskip> |
264 |
The pretty printer for inner syntax maintains alternative |
|
46284 | 265 |
mixfix productions for any print mode name invented by the user, say |
266 |
in commands like @{command notation} or @{command abbreviation}. |
|
267 |
Mode names can be arbitrary, but the following ones have a specific |
|
268 |
meaning by convention: |
|
269 |
||
61421 | 270 |
\<^item> @{verbatim \<open>""\<close>} (the empty string): default mode; |
46284 | 271 |
implicitly active as last element in the list of modes. |
272 |
||
61421 | 273 |
\<^item> @{verbatim input}: dummy print mode that is never active; may |
46284 | 274 |
be used to specify notation that is only available for input. |
275 |
||
61421 | 276 |
\<^item> @{verbatim internal} dummy print mode that is never active; |
46284 | 277 |
used internally in Isabelle/Pure. |
278 |
||
61421 | 279 |
\<^item> @{verbatim xsymbols}: enable proper mathematical symbols |
46284 | 280 |
instead of ASCII art.\footnote{This traditional mode name stems from |
58842 | 281 |
the ``X-Symbol'' package for classic Proof~General with XEmacs.} |
46284 | 282 |
|
61421 | 283 |
\<^item> @{verbatim HTML}: additional mode that is active in HTML |
46284 | 284 |
presentation of Isabelle theory sources; allows to provide |
285 |
alternative output notation. |
|
286 |
||
61421 | 287 |
\<^item> @{verbatim latex}: additional mode that is active in {\LaTeX} |
46284 | 288 |
document preparation of Isabelle theory sources; allows to provide |
289 |
alternative output notation. |
|
58618 | 290 |
\<close> |
46284 | 291 |
|
292 |
||
58618 | 293 |
section \<open>Mixfix annotations \label{sec:mixfix}\<close> |
28762 | 294 |
|
61477 | 295 |
text \<open>Mixfix annotations specify concrete \<^emph>\<open>inner syntax\<close> of |
35351
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
32833
diff
changeset
|
296 |
Isabelle types and terms. Locally fixed parameters in toplevel |
46290 | 297 |
theorem statements, locale and class specifications also admit |
298 |
mixfix annotations in a fairly uniform manner. A mixfix annotation |
|
50635 | 299 |
describes the concrete syntax, the translation to abstract |
46290 | 300 |
syntax, and the pretty printing. Special case annotations provide a |
301 |
simple means of specifying infix operators and binders. |
|
302 |
||
58552 | 303 |
Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}. It allows |
46290 | 304 |
to specify any context-free priority grammar, which is more general |
305 |
than the fixity declarations of ML and Prolog. |
|
28762 | 306 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55108
diff
changeset
|
307 |
@{rail \<open> |
51654
8450b944e58a
just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents:
50636
diff
changeset
|
308 |
@{syntax_def mixfix}: '(' |
58761 | 309 |
(@{syntax template} prios? @{syntax nat}? | |
310 |
(@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} | |
|
311 |
@'binder' @{syntax template} prios? @{syntax nat} | |
|
312 |
@'structure') ')' |
|
46290 | 313 |
; |
314 |
template: string |
|
46289 | 315 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
316 |
prios: '[' (@{syntax nat} + ',') ']' |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55108
diff
changeset
|
317 |
\<close>} |
28762 | 318 |
|
61493 | 319 |
The string given as \<open>template\<close> may include literal text, |
320 |
spacing, blocks, and arguments (denoted by ``\<open>_\<close>''); the |
|
321 |
special symbol ``@{verbatim "\<index>"}'' (printed as ``\<open>\<index>\<close>'') |
|
51657
3db1bbc82d8d
more accurate documentation of "(structure)" mixfix;
wenzelm
parents:
51654
diff
changeset
|
322 |
represents an index argument that specifies an implicit @{keyword |
3db1bbc82d8d
more accurate documentation of "(structure)" mixfix;
wenzelm
parents:
51654
diff
changeset
|
323 |
"structure"} reference (see also \secref{sec:locale}). Only locally |
3db1bbc82d8d
more accurate documentation of "(structure)" mixfix;
wenzelm
parents:
51654
diff
changeset
|
324 |
fixed variables may be declared as @{keyword "structure"}. |
3db1bbc82d8d
more accurate documentation of "(structure)" mixfix;
wenzelm
parents:
51654
diff
changeset
|
325 |
|
3db1bbc82d8d
more accurate documentation of "(structure)" mixfix;
wenzelm
parents:
51654
diff
changeset
|
326 |
Infix and binder declarations provide common abbreviations for |
3db1bbc82d8d
more accurate documentation of "(structure)" mixfix;
wenzelm
parents:
51654
diff
changeset
|
327 |
particular mixfix declarations. So in practice, mixfix templates |
3db1bbc82d8d
more accurate documentation of "(structure)" mixfix;
wenzelm
parents:
51654
diff
changeset
|
328 |
mostly degenerate to literal text for concrete syntax, such as |
58618 | 329 |
``@{verbatim "++"}'' for an infix symbol.\<close> |
28762 | 330 |
|
46290 | 331 |
|
58618 | 332 |
subsection \<open>The general mixfix form\<close> |
46290 | 333 |
|
58618 | 334 |
text \<open>In full generality, mixfix declarations work as follows. |
61493 | 335 |
Suppose a constant \<open>c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> is annotated by |
336 |
\<open>(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)\<close>, where \<open>mixfix\<close> is a string |
|
337 |
\<open>d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n\<close> consisting of delimiters that surround |
|
46290 | 338 |
argument positions as indicated by underscores. |
28762 | 339 |
|
340 |
Altogether this determines a production for a context-free priority |
|
61493 | 341 |
grammar, where for each argument \<open>i\<close> the syntactic category |
342 |
is determined by \<open>\<tau>\<^sub>i\<close> (with priority \<open>p\<^sub>i\<close>), and the |
|
343 |
result category is determined from \<open>\<tau>\<close> (with priority \<open>p\<close>). Priority specifications are optional, with default 0 for |
|
46292 | 344 |
arguments and 1000 for the result.\footnote{Omitting priorities is |
345 |
prone to syntactic ambiguities unless the delimiter tokens determine |
|
61493 | 346 |
fully bracketed notation, as in \<open>if _ then _ else _ fi\<close>.} |
28762 | 347 |
|
61493 | 348 |
Since \<open>\<tau>\<close> may be again a function type, the constant |
28762 | 349 |
type scheme may have more argument positions than the mixfix |
61493 | 350 |
pattern. Printing a nested application \<open>c t\<^sub>1 \<dots> t\<^sub>m\<close> for |
351 |
\<open>m > n\<close> works by attaching concrete notation only to the |
|
352 |
innermost part, essentially by printing \<open>(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m\<close> |
|
28762 | 353 |
instead. If a term has fewer arguments than specified in the mixfix |
354 |
template, the concrete syntax is ignored. |
|
355 |
||
61421 | 356 |
\<^medskip> |
357 |
A mixfix template may also contain additional directives |
|
28762 | 358 |
for pretty printing, notably spaces, blocks, and breaks. The |
359 |
general template format is a sequence over any of the following |
|
360 |
entities. |
|
361 |
||
61493 | 362 |
\<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of |
28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
363 |
characters other than the following special characters: |
28762 | 364 |
|
61421 | 365 |
\<^medskip> |
28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
366 |
\begin{tabular}{ll} |
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
367 |
@{verbatim "'"} & single quote \\ |
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
368 |
@{verbatim "_"} & underscore \\ |
61493 | 369 |
\<open>\<index>\<close> & index symbol \\ |
28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
370 |
@{verbatim "("} & open parenthesis \\ |
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
371 |
@{verbatim ")"} & close parenthesis \\ |
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
372 |
@{verbatim "/"} & slash \\ |
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
373 |
\end{tabular} |
61421 | 374 |
\<^medskip> |
28762 | 375 |
|
61439 | 376 |
\<^descr> @{verbatim "'"} escapes the special meaning of these |
28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
377 |
meta-characters, producing a literal version of the following |
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
378 |
character, unless that is a blank. |
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
379 |
|
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
380 |
A single quote followed by a blank separates delimiters, without |
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
381 |
affecting printing, but input tokens may have additional white space |
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
382 |
here. |
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
383 |
|
61439 | 384 |
\<^descr> @{verbatim "_"} is an argument position, which stands for a |
28762 | 385 |
certain syntactic category in the underlying grammar. |
386 |
||
61493 | 387 |
\<^descr> \<open>\<index>\<close> is an indexed argument position; this is the place |
28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
388 |
where implicit structure arguments can be attached. |
28762 | 389 |
|
61493 | 390 |
\<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing. |
28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
391 |
This and the following specifications do not affect parsing at all. |
28762 | 392 |
|
61493 | 393 |
\<^descr> @{verbatim "("}\<open>n\<close> opens a pretty printing block. The |
28762 | 394 |
optional number specifies how much indentation to add when a line |
395 |
break occurs within the block. If the parenthesis is not followed |
|
396 |
by digits, the indentation defaults to 0. A block specified via |
|
28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
397 |
@{verbatim "(00"} is unbreakable. |
28762 | 398 |
|
61439 | 399 |
\<^descr> @{verbatim ")"} closes a pretty printing block. |
28762 | 400 |
|
61439 | 401 |
\<^descr> @{verbatim "//"} forces a line break. |
28762 | 402 |
|
61493 | 403 |
\<^descr> @{verbatim "/"}\<open>s\<close> allows a line break. Here \<open>s\<close> |
28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset
|
404 |
stands for the string of spaces (zero or more) right after the |
61477 | 405 |
slash. These spaces are printed if the break is \<^emph>\<open>not\<close> taken. |
28762 | 406 |
|
407 |
||
408 |
The general idea of pretty printing with blocks and breaks is also |
|
58552 | 409 |
described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}. |
58618 | 410 |
\<close> |
28762 | 411 |
|
412 |
||
58618 | 413 |
subsection \<open>Infixes\<close> |
46290 | 414 |
|
58618 | 415 |
text \<open>Infix operators are specified by convenient short forms that |
46290 | 416 |
abbreviate general mixfix annotations as follows: |
417 |
||
418 |
\begin{center} |
|
419 |
\begin{tabular}{lll} |
|
420 |
||
61493 | 421 |
@{verbatim "("}@{keyword_def "infix"}~@{verbatim \<open>"\<close>}\<open>sy\<close>@{verbatim \<open>"\<close>} \<open>p\<close>@{verbatim ")"} |
422 |
& \<open>\<mapsto>\<close> & |
|
423 |
@{verbatim \<open>("(_\<close>}~\<open>sy\<close>@{verbatim \<open>/ _)" [\<close>}\<open>p + 1\<close>@{verbatim ","}~\<open>p + 1\<close>@{verbatim "]"}~\<open>p\<close>@{verbatim ")"} \\ |
|
424 |
@{verbatim "("}@{keyword_def "infixl"}~@{verbatim \<open>"\<close>}\<open>sy\<close>@{verbatim \<open>"\<close>} \<open>p\<close>@{verbatim ")"} |
|
425 |
& \<open>\<mapsto>\<close> & |
|
426 |
@{verbatim \<open>("(_\<close>}~\<open>sy\<close>@{verbatim \<open>/ _)" [\<close>}\<open>p\<close>@{verbatim ","}~\<open>p + 1\<close>@{verbatim "]"}~\<open>p\<close>@{verbatim ")"} \\ |
|
427 |
@{verbatim "("}@{keyword_def "infixr"}~@{verbatim \<open>"\<close>}\<open>sy\<close>@{verbatim \<open>"\<close>}~\<open>p\<close>@{verbatim ")"} |
|
428 |
& \<open>\<mapsto>\<close> & |
|
429 |
@{verbatim \<open>("(_\<close>}~\<open>sy\<close>@{verbatim \<open>/ _)" [\<close>}\<open>p + 1\<close>@{verbatim ","}~\<open>p\<close>@{verbatim "]"}~\<open>p\<close>@{verbatim ")"} \\ |
|
46290 | 430 |
|
431 |
\end{tabular} |
|
432 |
\end{center} |
|
433 |
||
61493 | 434 |
The mixfix template @{verbatim \<open>"(_\<close>}~\<open>sy\<close>@{verbatim \<open>/ _)"\<close>} |
46292 | 435 |
specifies two argument positions; the delimiter is preceded by a |
436 |
space and followed by a space or line break; the entire phrase is a |
|
437 |
pretty printing block. |
|
46290 | 438 |
|
61493 | 439 |
The alternative notation @{verbatim "op"}~\<open>sy\<close> is introduced |
46290 | 440 |
in addition. Thus any infix operator may be written in prefix form |
441 |
(as in ML), independently of the number of arguments in the term. |
|
58618 | 442 |
\<close> |
46290 | 443 |
|
444 |
||
58618 | 445 |
subsection \<open>Binders\<close> |
46290 | 446 |
|
61477 | 447 |
text \<open>A \<^emph>\<open>binder\<close> is a variable-binding construct such as a |
61493 | 448 |
quantifier. The idea to formalize \<open>\<forall>x. b\<close> as \<open>All |
449 |
(\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close> already goes back |
|
58552 | 450 |
to @{cite church40}. Isabelle declarations of certain higher-order |
46292 | 451 |
operators may be annotated with @{keyword_def "binder"} annotations |
452 |
as follows: |
|
46290 | 453 |
|
454 |
\begin{center} |
|
61493 | 455 |
\<open>c :: \<close>@{verbatim \<open>"\<close>}\<open>(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3\<close>@{verbatim \<open>" (\<close>}@{keyword "binder"}~@{verbatim \<open>"\<close>}\<open>sy\<close>@{verbatim \<open>" [\<close>}\<open>p\<close>@{verbatim "]"}~\<open>q\<close>@{verbatim ")"} |
46290 | 456 |
\end{center} |
457 |
||
61493 | 458 |
This introduces concrete binder syntax \<open>sy x. b\<close>, where |
459 |
\<open>x\<close> is a bound variable of type \<open>\<tau>\<^sub>1\<close>, the body \<open>b\<close> has type \<open>\<tau>\<^sub>2\<close> and the whole term has type \<open>\<tau>\<^sub>3\<close>. |
|
460 |
The optional integer \<open>p\<close> specifies the syntactic priority of |
|
461 |
the body; the default is \<open>q\<close>, which is also the priority of |
|
46290 | 462 |
the whole construct. |
463 |
||
464 |
Internally, the binder syntax is expanded to something like this: |
|
465 |
\begin{center} |
|
61493 | 466 |
\<open>c_binder :: \<close>@{verbatim \<open>"\<close>}\<open>idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3\<close>@{verbatim \<open>" ("(3\<close>}\<open>sy\<close>@{verbatim \<open>_./ _)" [0,\<close>}~\<open>p\<close>@{verbatim "]"}~\<open>q\<close>@{verbatim ")"} |
46290 | 467 |
\end{center} |
468 |
||
469 |
Here @{syntax (inner) idts} is the nonterminal symbol for a list of |
|
470 |
identifiers with optional type constraints (see also |
|
471 |
\secref{sec:pure-grammar}). The mixfix template @{verbatim |
|
61493 | 472 |
\<open>"(3\<close>}\<open>sy\<close>@{verbatim \<open>_./ _)"\<close>} defines argument positions |
46290 | 473 |
for the bound identifiers and the body, separated by a dot with |
474 |
optional line break; the entire phrase is a pretty printing block of |
|
61493 | 475 |
indentation level 3. Note that there is no extra space after \<open>sy\<close>, so it needs to be included user specification if the binder |
46290 | 476 |
syntax ends with a token that may be continued by an identifier |
477 |
token at the start of @{syntax (inner) idts}. |
|
478 |
||
61493 | 479 |
Furthermore, a syntax translation to transforms \<open>c_binder x\<^sub>1 |
480 |
\<dots> x\<^sub>n b\<close> into iterated application \<open>c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)\<close>. |
|
58618 | 481 |
This works in both directions, for parsing and printing.\<close> |
46290 | 482 |
|
483 |
||
58618 | 484 |
section \<open>Explicit notation \label{sec:notation}\<close> |
28762 | 485 |
|
58618 | 486 |
text \<open> |
28762 | 487 |
\begin{matharray}{rcll} |
61493 | 488 |
@{command_def "type_notation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
489 |
@{command_def "no_type_notation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
490 |
@{command_def "notation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
491 |
@{command_def "no_notation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
492 |
@{command_def "write"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
|
28762 | 493 |
\end{matharray} |
494 |
||
46288 | 495 |
Commands that introduce new logical entities (terms or types) |
496 |
usually allow to provide mixfix annotations on the spot, which is |
|
497 |
convenient for default notation. Nonetheless, the syntax may be |
|
498 |
modified later on by declarations for explicit notation. This |
|
499 |
allows to add or delete mixfix annotations for of existing logical |
|
500 |
entities within the current context. |
|
501 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55108
diff
changeset
|
502 |
@{rail \<open> |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
58842
diff
changeset
|
503 |
(@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline> |
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
58842
diff
changeset
|
504 |
(@{syntax nameref} @{syntax mixfix} + @'and') |
35413 | 505 |
; |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
58842
diff
changeset
|
506 |
(@@{command notation} | @@{command no_notation}) @{syntax mode}? \<newline> |
51654
8450b944e58a
just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents:
50636
diff
changeset
|
507 |
(@{syntax nameref} @{syntax mixfix} + @'and') |
28762 | 508 |
; |
51654
8450b944e58a
just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents:
50636
diff
changeset
|
509 |
@@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55108
diff
changeset
|
510 |
\<close>} |
28762 | 511 |
|
61493 | 512 |
\<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix |
35413 | 513 |
syntax with an existing type constructor. The arity of the |
514 |
constructor is retrieved from the context. |
|
46282 | 515 |
|
61439 | 516 |
\<^descr> @{command "no_type_notation"} is similar to @{command |
35413 | 517 |
"type_notation"}, but removes the specified syntax annotation from |
518 |
the present context. |
|
519 |
||
61493 | 520 |
\<^descr> @{command "notation"}~\<open>c (mx)\<close> associates mixfix |
35413 | 521 |
syntax with an existing constant or fixed variable. The type |
522 |
declaration of the given entity is retrieved from the context. |
|
46282 | 523 |
|
61439 | 524 |
\<^descr> @{command "no_notation"} is similar to @{command "notation"}, |
28762 | 525 |
but removes the specified syntax annotation from the present |
526 |
context. |
|
527 |
||
61439 | 528 |
\<^descr> @{command "write"} is similar to @{command "notation"}, but |
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:
35413
diff
changeset
|
529 |
works within an Isar proof body. |
58618 | 530 |
\<close> |
28762 | 531 |
|
28778 | 532 |
|
58618 | 533 |
section \<open>The Pure syntax \label{sec:pure-syntax}\<close> |
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
534 |
|
58618 | 535 |
subsection \<open>Lexical matters \label{sec:inner-lex}\<close> |
46282 | 536 |
|
58618 | 537 |
text \<open>The inner lexical syntax vaguely resembles the outer one |
46282 | 538 |
(\secref{sec:outer-lex}), but some details are different. There are |
539 |
two main categories of inner syntax tokens: |
|
540 |
||
61477 | 541 |
\<^enum> \<^emph>\<open>delimiters\<close> --- the literal tokens occurring in |
46282 | 542 |
productions of the given priority grammar (cf.\ |
543 |
\secref{sec:priority-grammar}); |
|
544 |
||
61477 | 545 |
\<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc. |
46282 | 546 |
|
547 |
||
548 |
Delimiters override named tokens and may thus render certain |
|
549 |
identifiers inaccessible. Sometimes the logical context admits |
|
550 |
alternative ways to refer to the same entity, potentially via |
|
551 |
qualified names. |
|
552 |
||
61421 | 553 |
\<^medskip> |
554 |
The categories for named tokens are defined once and for |
|
46282 | 555 |
all as follows, reusing some categories of the outer token syntax |
556 |
(\secref{sec:outer-lex}). |
|
557 |
||
558 |
\begin{center} |
|
559 |
\begin{supertabular}{rcl} |
|
560 |
@{syntax_def (inner) id} & = & @{syntax_ref ident} \\ |
|
561 |
@{syntax_def (inner) longid} & = & @{syntax_ref longident} \\ |
|
562 |
@{syntax_def (inner) var} & = & @{syntax_ref var} \\ |
|
563 |
@{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\ |
|
564 |
@{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\ |
|
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58409
diff
changeset
|
565 |
@{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\ |
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58409
diff
changeset
|
566 |
@{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ |
61493 | 567 |
@{syntax_def (inner) str_token} & = & @{verbatim "''"} \<open>\<dots>\<close> @{verbatim "''"} \\ |
568 |
@{syntax_def (inner) string_token} & = & @{verbatim \<open>"\<close>} \<open>\<dots>\<close> @{verbatim \<open>"\<close>} \\ |
|
569 |
@{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\ |
|
46282 | 570 |
\end{supertabular} |
571 |
\end{center} |
|
572 |
||
573 |
The token categories @{syntax (inner) num_token}, @{syntax (inner) |
|
58421 | 574 |
float_token}, @{syntax (inner) str_token}, @{syntax (inner) string_token}, |
575 |
and @{syntax (inner) cartouche} are not used in Pure. Object-logics may |
|
576 |
implement numerals and string literals by adding appropriate syntax |
|
577 |
declarations, together with some translation functions (e.g.\ see @{file |
|
578 |
"~~/src/HOL/Tools/string_syntax.ML"}). |
|
46282 | 579 |
|
58421 | 580 |
The derived categories @{syntax_def (inner) num_const}, and @{syntax_def |
581 |
(inner) float_const}, provide robust access to the respective tokens: the |
|
582 |
syntax tree holds a syntactic constant instead of a free variable. |
|
58618 | 583 |
\<close> |
46282 | 584 |
|
585 |
||
58618 | 586 |
subsection \<open>Priority grammars \label{sec:priority-grammar}\<close> |
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
587 |
|
61477 | 588 |
text \<open>A context-free grammar consists of a set of \<^emph>\<open>terminal |
589 |
symbols\<close>, a set of \<^emph>\<open>nonterminal symbols\<close> and a set of |
|
61493 | 590 |
\<^emph>\<open>productions\<close>. Productions have the form \<open>A = \<gamma>\<close>, |
591 |
where \<open>A\<close> is a nonterminal and \<open>\<gamma>\<close> is a string of |
|
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
592 |
terminals and nonterminals. One designated nonterminal is called |
61477 | 593 |
the \<^emph>\<open>root symbol\<close>. The language defined by the grammar |
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
594 |
consists of all strings of terminals that can be derived from the |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
595 |
root symbol by applying productions as rewrite rules. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
596 |
|
61477 | 597 |
The standard Isabelle parser for inner syntax uses a \<^emph>\<open>priority |
598 |
grammar\<close>. Each nonterminal is decorated by an integer priority: |
|
61493 | 599 |
\<open>A\<^sup>(\<^sup>p\<^sup>)\<close>. In a derivation, \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> may be rewritten |
600 |
using a production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> only if \<open>p \<le> q\<close>. Any |
|
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
601 |
priority grammar can be translated into a normal context-free |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
602 |
grammar by introducing new nonterminals and productions. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
603 |
|
61421 | 604 |
\<^medskip> |
61493 | 605 |
Formally, a set of context free productions \<open>G\<close> |
606 |
induces a derivation relation \<open>\<longrightarrow>\<^sub>G\<close> as follows. Let \<open>\<alpha>\<close> and \<open>\<beta>\<close> denote strings of terminal or nonterminal symbols. |
|
607 |
Then \<open>\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>\<close> holds if and only if \<open>G\<close> |
|
608 |
contains some production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> for \<open>p \<le> q\<close>. |
|
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
609 |
|
61421 | 610 |
\<^medskip> |
611 |
The following grammar for arithmetic expressions |
|
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
612 |
demonstrates how binding power and associativity of operators can be |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
613 |
enforced by priorities. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
614 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
615 |
\begin{center} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
616 |
\begin{tabular}{rclr} |
61493 | 617 |
\<open>A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>=\<close> & @{verbatim "("} \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> @{verbatim ")"} \\ |
618 |
\<open>A\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>=\<close> & @{verbatim 0} \\ |
|
619 |
\<open>A\<^sup>(\<^sup>0\<^sup>)\<close> & \<open>=\<close> & \<open>A\<^sup>(\<^sup>0\<^sup>)\<close> @{verbatim "+"} \<open>A\<^sup>(\<^sup>1\<^sup>)\<close> \\ |
|
620 |
\<open>A\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>=\<close> & \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> @{verbatim "*"} \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> \\ |
|
621 |
\<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>=\<close> & @{verbatim "-"} \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \\ |
|
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
622 |
\end{tabular} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
623 |
\end{center} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
624 |
The choice of priorities determines that @{verbatim "-"} binds |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
625 |
tighter than @{verbatim "*"}, which binds tighter than @{verbatim |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
626 |
"+"}. Furthermore @{verbatim "+"} associates to the left and |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
627 |
@{verbatim "*"} to the right. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
628 |
|
61421 | 629 |
\<^medskip> |
630 |
For clarity, grammars obey these conventions: |
|
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
631 |
|
61421 | 632 |
\<^item> All priorities must lie between 0 and 1000. |
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
633 |
|
61421 | 634 |
\<^item> Priority 0 on the right-hand side and priority 1000 on the |
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
635 |
left-hand side may be omitted. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
636 |
|
61493 | 637 |
\<^item> The production \<open>A\<^sup>(\<^sup>p\<^sup>) = \<alpha>\<close> is written as \<open>A = \<alpha> |
638 |
(p)\<close>, i.e.\ the priority of the left-hand side actually appears in |
|
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
639 |
a column on the far right. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
640 |
|
61493 | 641 |
\<^item> Alternatives are separated by \<open>|\<close>. |
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
642 |
|
61493 | 643 |
\<^item> Repetition is indicated by dots \<open>(\<dots>)\<close> in an informal |
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
644 |
but obvious way. |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
645 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
646 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
647 |
Using these conventions, the example grammar specification above |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
648 |
takes the form: |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
649 |
\begin{center} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
650 |
\begin{tabular}{rclc} |
61493 | 651 |
\<open>A\<close> & \<open>=\<close> & @{verbatim "("} \<open>A\<close> @{verbatim ")"} \\ |
652 |
& \<open>|\<close> & @{verbatim 0} & \qquad\qquad \\ |
|
653 |
& \<open>|\<close> & \<open>A\<close> @{verbatim "+"} \<open>A\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(0)\<close> \\ |
|
654 |
& \<open>|\<close> & \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> @{verbatim "*"} \<open>A\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>(2)\<close> \\ |
|
655 |
& \<open>|\<close> & @{verbatim "-"} \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\ |
|
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
656 |
\end{tabular} |
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
657 |
\end{center} |
58618 | 658 |
\<close> |
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
659 |
|
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset
|
660 |
|
58618 | 661 |
subsection \<open>The Pure grammar \label{sec:pure-grammar}\<close> |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
662 |
|
61493 | 663 |
text \<open>The priority grammar of the \<open>Pure\<close> theory is defined |
46287 | 664 |
approximately like this: |
28774 | 665 |
|
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
666 |
\begin{center} |
28773 | 667 |
\begin{supertabular}{rclr} |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
668 |
|
61493 | 669 |
@{syntax_def (inner) any} & = & \<open>prop | logic\<close> \\\\ |
28772 | 670 |
|
61493 | 671 |
@{syntax_def (inner) prop} & = & @{verbatim "("} \<open>prop\<close> @{verbatim ")"} \\ |
672 |
& \<open>|\<close> & \<open>prop\<^sup>(\<^sup>4\<^sup>)\<close> @{verbatim "::"} \<open>type\<close> & \<open>(3)\<close> \\ |
|
673 |
& \<open>|\<close> & \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> @{verbatim "=="} \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(2)\<close> \\ |
|
674 |
& \<open>|\<close> & \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> \<open>\<equiv>\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(2)\<close> \\ |
|
675 |
& \<open>|\<close> & \<open>prop\<^sup>(\<^sup>3\<^sup>)\<close> @{verbatim "&&&"} \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> & \<open>(2)\<close> \\ |
|
676 |
& \<open>|\<close> & \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> @{verbatim "==>"} \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\ |
|
677 |
& \<open>|\<close> & \<open>prop\<^sup>(\<^sup>2\<^sup>)\<close> \<open>\<Longrightarrow>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\ |
|
678 |
& \<open>|\<close> & @{verbatim "[|"} \<open>prop\<close> @{verbatim ";"} \<open>\<dots>\<close> @{verbatim ";"} \<open>prop\<close> @{verbatim "|]"} @{verbatim "==>"} \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\ |
|
679 |
& \<open>|\<close> & \<open>\<lbrakk>\<close> \<open>prop\<close> @{verbatim ";"} \<open>\<dots>\<close> @{verbatim ";"} \<open>prop\<close> \<open>\<rbrakk>\<close> \<open>\<Longrightarrow>\<close> \<open>prop\<^sup>(\<^sup>1\<^sup>)\<close> & \<open>(1)\<close> \\ |
|
680 |
& \<open>|\<close> & @{verbatim "!!"} \<open>idts\<close> @{verbatim "."} \<open>prop\<close> & \<open>(0)\<close> \\ |
|
681 |
& \<open>|\<close> & \<open>\<And>\<close> \<open>idts\<close> @{verbatim "."} \<open>prop\<close> & \<open>(0)\<close> \\ |
|
682 |
& \<open>|\<close> & @{verbatim OFCLASS} @{verbatim "("} \<open>type\<close> @{verbatim ","} \<open>logic\<close> @{verbatim ")"} \\ |
|
683 |
& \<open>|\<close> & @{verbatim SORT_CONSTRAINT} @{verbatim "("} \<open>type\<close> @{verbatim ")"} \\ |
|
684 |
& \<open>|\<close> & @{verbatim TERM} \<open>logic\<close> \\ |
|
685 |
& \<open>|\<close> & @{verbatim PROP} \<open>aprop\<close> \\\\ |
|
28772 | 686 |
|
61493 | 687 |
@{syntax_def (inner) aprop} & = & @{verbatim "("} \<open>aprop\<close> @{verbatim ")"} \\ |
688 |
& \<open>|\<close> & \<open>id | longid | var | \<close>@{verbatim "_"}\<open> | \<close>@{verbatim "..."} \\ |
|
689 |
& \<open>|\<close> & @{verbatim CONST} \<open>id | \<close>@{verbatim CONST} \<open>longid\<close> \\ |
|
690 |
& \<open>|\<close> & @{verbatim XCONST} \<open>id | \<close>@{verbatim XCONST} \<open>longid\<close> \\ |
|
691 |
& \<open>|\<close> & \<open>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>)\<close> & \<open>(999)\<close> \\\\ |
|
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
692 |
|
61493 | 693 |
@{syntax_def (inner) logic} & = & @{verbatim "("} \<open>logic\<close> @{verbatim ")"} \\ |
694 |
& \<open>|\<close> & \<open>logic\<^sup>(\<^sup>4\<^sup>)\<close> @{verbatim "::"} \<open>type\<close> & \<open>(3)\<close> \\ |
|
695 |
& \<open>|\<close> & \<open>id | longid | var | \<close>@{verbatim "_"}\<open> | \<close>@{verbatim "..."} \\ |
|
696 |
& \<open>|\<close> & @{verbatim CONST} \<open>id | \<close>@{verbatim CONST} \<open>longid\<close> \\ |
|
697 |
& \<open>|\<close> & @{verbatim XCONST} \<open>id | \<close>@{verbatim XCONST} \<open>longid\<close> \\ |
|
698 |
& \<open>|\<close> & \<open>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>)\<close> & \<open>(999)\<close> \\ |
|
699 |
& \<open>|\<close> & \<open>\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> \\ |
|
700 |
& \<open>|\<close> & @{verbatim "%"} \<open>pttrns\<close> @{verbatim "."} \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\ |
|
701 |
& \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> @{verbatim "."} \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\ |
|
702 |
& \<open>|\<close> & @{verbatim op} @{verbatim "=="}\<open> | \<close>@{verbatim op} \<open>\<equiv>\<close>\<open> | \<close>@{verbatim op} @{verbatim "&&&"} \\ |
|
703 |
& \<open>|\<close> & @{verbatim op} @{verbatim "==>"}\<open> | \<close>@{verbatim op} \<open>\<Longrightarrow>\<close> \\ |
|
704 |
& \<open>|\<close> & @{verbatim TYPE} @{verbatim "("} \<open>type\<close> @{verbatim ")"} \\\\ |
|
28772 | 705 |
|
61493 | 706 |
@{syntax_def (inner) idt} & = & @{verbatim "("} \<open>idt\<close> @{verbatim ")"}\<open> | id | \<close>@{verbatim "_"} \\ |
707 |
& \<open>|\<close> & \<open>id\<close> @{verbatim "::"} \<open>type\<close> & \<open>(0)\<close> \\ |
|
708 |
& \<open>|\<close> & @{verbatim "_"} @{verbatim "::"} \<open>type\<close> & \<open>(0)\<close> \\\\ |
|
28772 | 709 |
|
61493 | 710 |
@{syntax_def (inner) index} & = & @{verbatim "\<^bsub>"} \<open>logic\<^sup>(\<^sup>0\<^sup>)\<close> @{verbatim "\<^esub>"}\<open> | | \<index>\<close> \\\\ |
46287 | 711 |
|
61493 | 712 |
@{syntax_def (inner) idts} & = & \<open>idt | idt\<^sup>(\<^sup>1\<^sup>) idts\<close> & \<open>(0)\<close> \\\\ |
28772 | 713 |
|
61493 | 714 |
@{syntax_def (inner) pttrn} & = & \<open>idt\<close> \\\\ |
28772 | 715 |
|
61493 | 716 |
@{syntax_def (inner) pttrns} & = & \<open>pttrn | pttrn\<^sup>(\<^sup>1\<^sup>) pttrns\<close> & \<open>(0)\<close> \\\\ |
28774 | 717 |
|
61493 | 718 |
@{syntax_def (inner) type} & = & @{verbatim "("} \<open>type\<close> @{verbatim ")"} \\ |
719 |
& \<open>|\<close> & \<open>tid | tvar | \<close>@{verbatim "_"} \\ |
|
720 |
& \<open>|\<close> & \<open>tid\<close> @{verbatim "::"} \<open>sort | tvar \<close>@{verbatim "::"} \<open>sort | \<close>@{verbatim "_"} @{verbatim "::"} \<open>sort\<close> \\ |
|
721 |
& \<open>|\<close> & \<open>type_name | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) type_name\<close> \\ |
|
722 |
& \<open>|\<close> & @{verbatim "("} \<open>type\<close> @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} \<open>type\<close> @{verbatim ")"} \<open>type_name\<close> \\ |
|
723 |
& \<open>|\<close> & \<open>type\<^sup>(\<^sup>1\<^sup>)\<close> @{verbatim "=>"} \<open>type\<close> & \<open>(0)\<close> \\ |
|
724 |
& \<open>|\<close> & \<open>type\<^sup>(\<^sup>1\<^sup>)\<close> \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\ |
|
725 |
& \<open>|\<close> & @{verbatim "["} \<open>type\<close> @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} \<open>type\<close> @{verbatim "]"} @{verbatim "=>"} \<open>type\<close> & \<open>(0)\<close> \\ |
|
726 |
& \<open>|\<close> & @{verbatim "["} \<open>type\<close> @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} \<open>type\<close> @{verbatim "]"} \<open>\<Rightarrow>\<close> \<open>type\<close> & \<open>(0)\<close> \\ |
|
727 |
@{syntax_def (inner) type_name} & = & \<open>id | longid\<close> \\\\ |
|
28772 | 728 |
|
61493 | 729 |
@{syntax_def (inner) sort} & = & @{syntax class_name}~\<open> | \<close>@{verbatim "{}"} \\ |
730 |
& \<open>|\<close> & @{verbatim "{"} @{syntax class_name} @{verbatim ","} \<open>\<dots>\<close> @{verbatim ","} @{syntax class_name} @{verbatim "}"} \\ |
|
731 |
@{syntax_def (inner) class_name} & = & \<open>id | longid\<close> \\ |
|
28773 | 732 |
\end{supertabular} |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
733 |
\end{center} |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
734 |
|
61421 | 735 |
\<^medskip> |
736 |
Here literal terminals are printed @{verbatim "verbatim"}; |
|
28774 | 737 |
see also \secref{sec:inner-lex} for further token categories of the |
738 |
inner syntax. The meaning of the nonterminals defined by the above |
|
739 |
grammar is as follows: |
|
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
740 |
|
61439 | 741 |
\<^descr> @{syntax_ref (inner) any} denotes any term. |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
742 |
|
61439 | 743 |
\<^descr> @{syntax_ref (inner) prop} denotes meta-level propositions, |
28778 | 744 |
which are terms of type @{typ prop}. The syntax of such formulae of |
745 |
the meta-logic is carefully distinguished from usual conventions for |
|
61493 | 746 |
object-logics. In particular, plain \<open>\<lambda>\<close>-term notation is |
61477 | 747 |
\<^emph>\<open>not\<close> recognized as @{syntax (inner) prop}. |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
748 |
|
61439 | 749 |
\<^descr> @{syntax_ref (inner) aprop} denotes atomic propositions, which |
28778 | 750 |
are embedded into regular @{syntax (inner) prop} by means of an |
751 |
explicit @{verbatim PROP} token. |
|
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
752 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
753 |
Terms of type @{typ prop} with non-constant head, e.g.\ a plain |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
754 |
variable, are printed in this form. Constants that yield type @{typ |
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
755 |
prop} are expected to provide their own concrete syntax; otherwise |
28778 | 756 |
the printed version will appear like @{syntax (inner) logic} and |
757 |
cannot be parsed again as @{syntax (inner) prop}. |
|
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
758 |
|
61439 | 759 |
\<^descr> @{syntax_ref (inner) logic} denotes arbitrary terms of a |
28778 | 760 |
logical type, excluding type @{typ prop}. This is the main |
61493 | 761 |
syntactic category of object-logic entities, covering plain \<open>\<lambda>\<close>-term notation (variables, abstraction, application), plus |
28778 | 762 |
anything defined by the user. |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
763 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
764 |
When specifying notation for logical entities, all logical types |
61477 | 765 |
(excluding @{typ prop}) are \<^emph>\<open>collapsed\<close> to this single category |
28778 | 766 |
of @{syntax (inner) logic}. |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
767 |
|
61439 | 768 |
\<^descr> @{syntax_ref (inner) index} denotes an optional index term for |
51657
3db1bbc82d8d
more accurate documentation of "(structure)" mixfix;
wenzelm
parents:
51654
diff
changeset
|
769 |
indexed syntax. If omitted, it refers to the first @{keyword_ref |
61493 | 770 |
"structure"} variable in the context. The special dummy ``\<open>\<index>\<close>'' serves as pattern variable in mixfix annotations that |
46287 | 771 |
introduce indexed notation. |
772 |
||
61439 | 773 |
\<^descr> @{syntax_ref (inner) idt} denotes identifiers, possibly |
28778 | 774 |
constrained by types. |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
775 |
|
61439 | 776 |
\<^descr> @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref |
28778 | 777 |
(inner) idt}. This is the most basic category for variables in |
61493 | 778 |
iterated binders, such as \<open>\<lambda>\<close> or \<open>\<And>\<close>. |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
779 |
|
61439 | 780 |
\<^descr> @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns} |
28778 | 781 |
denote patterns for abstraction, cases bindings etc. In Pure, these |
782 |
categories start as a merely copy of @{syntax (inner) idt} and |
|
783 |
@{syntax (inner) idts}, respectively. Object-logics may add |
|
784 |
additional productions for binding forms. |
|
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
785 |
|
61439 | 786 |
\<^descr> @{syntax_ref (inner) type} denotes types of the meta-logic. |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
787 |
|
61439 | 788 |
\<^descr> @{syntax_ref (inner) sort} denotes meta-level sorts. |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
789 |
|
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
790 |
|
28774 | 791 |
Here are some further explanations of certain syntax features. |
28773 | 792 |
|
61493 | 793 |
\<^item> In @{syntax (inner) idts}, note that \<open>x :: nat y\<close> is |
794 |
parsed as \<open>x :: (nat y)\<close>, treating \<open>y\<close> like a type |
|
795 |
constructor applied to \<open>nat\<close>. To avoid this interpretation, |
|
796 |
write \<open>(x :: nat) y\<close> with explicit parentheses. |
|
28773 | 797 |
|
61493 | 798 |
\<^item> Similarly, \<open>x :: nat y :: nat\<close> is parsed as \<open>x :: |
799 |
(nat y :: nat)\<close>. The correct form is \<open>(x :: nat) (y :: |
|
800 |
nat)\<close>, or \<open>(x :: nat) y :: nat\<close> if \<open>y\<close> is last in the |
|
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
801 |
sequence of identifiers. |
28773 | 802 |
|
61421 | 803 |
\<^item> Type constraints for terms bind very weakly. For example, |
61493 | 804 |
\<open>x < y :: nat\<close> is normally parsed as \<open>(x < y) :: |
805 |
nat\<close>, unless \<open><\<close> has a very low priority, in which case the |
|
806 |
input is likely to be ambiguous. The correct form is \<open>x < (y |
|
807 |
:: nat)\<close>. |
|
28773 | 808 |
|
61421 | 809 |
\<^item> Dummy variables (written as underscore) may occur in different |
28774 | 810 |
roles. |
28773 | 811 |
|
61493 | 812 |
\<^descr> A type ``\<open>_\<close>'' or ``\<open>_ :: sort\<close>'' acts like an |
61458 | 813 |
anonymous inference parameter, which is filled-in according to the |
814 |
most general type produced by the type-checking phase. |
|
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
815 |
|
61493 | 816 |
\<^descr> A bound ``\<open>_\<close>'' refers to a vacuous abstraction, where |
61458 | 817 |
the body does not refer to the binding introduced here. As in the |
61493 | 818 |
term @{term "\<lambda>x _. x"}, which is \<open>\<alpha>\<close>-equivalent to \<open>\<lambda>x y. x\<close>. |
28773 | 819 |
|
61493 | 820 |
\<^descr> A free ``\<open>_\<close>'' refers to an implicit outer binding. |
821 |
Higher definitional packages usually allow forms like \<open>f x _ |
|
822 |
= x\<close>. |
|
28773 | 823 |
|
61493 | 824 |
\<^descr> A schematic ``\<open>_\<close>'' (within a term pattern, see |
61458 | 825 |
\secref{sec:term-decls}) refers to an anonymous variable that is |
826 |
implicitly abstracted over its context of locally bound variables. |
|
61493 | 827 |
For example, this allows pattern matching of \<open>{x. f x = g |
828 |
x}\<close> against \<open>{x. _ = _}\<close>, or even \<open>{_. _ = _}\<close> by |
|
61458 | 829 |
using both bound and schematic dummies. |
28773 | 830 |
|
61439 | 831 |
\<^descr> The three literal dots ``@{verbatim "..."}'' may be also |
28774 | 832 |
written as ellipsis symbol @{verbatim "\<dots>"}. In both cases this |
833 |
refers to a special schematic variable, which is bound in the |
|
834 |
context. This special term abbreviation works nicely with |
|
835 |
calculational reasoning (\secref{sec:calculation}). |
|
836 |
||
61439 | 837 |
\<^descr> @{verbatim CONST} ensures that the given identifier is treated |
46287 | 838 |
as constant term, and passed through the parse tree in fully |
839 |
internalized form. This is particularly relevant for translation |
|
840 |
rules (\secref{sec:syn-trans}), notably on the RHS. |
|
841 |
||
61439 | 842 |
\<^descr> @{verbatim XCONST} is similar to @{verbatim CONST}, but |
46287 | 843 |
retains the constant name as given. This is only relevant to |
844 |
translation rules (\secref{sec:syn-trans}), notably on the LHS. |
|
58618 | 845 |
\<close> |
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
846 |
|
28777 | 847 |
|
58618 | 848 |
subsection \<open>Inspecting the syntax\<close> |
28777 | 849 |
|
58618 | 850 |
text \<open> |
46282 | 851 |
\begin{matharray}{rcl} |
61493 | 852 |
@{command_def "print_syntax"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
46282 | 853 |
\end{matharray} |
28777 | 854 |
|
61439 | 855 |
\<^descr> @{command "print_syntax"} prints the inner syntax of the |
46282 | 856 |
current context. The output can be quite large; the most important |
857 |
sections are explained below. |
|
28777 | 858 |
|
61493 | 859 |
\<^descr> \<open>lexicon\<close> lists the delimiters of the inner token |
61458 | 860 |
language; see \secref{sec:inner-lex}. |
28777 | 861 |
|
61493 | 862 |
\<^descr> \<open>prods\<close> lists the productions of the underlying |
61458 | 863 |
priority grammar; see \secref{sec:priority-grammar}. |
28777 | 864 |
|
61493 | 865 |
The nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is rendered in plain text as \<open>A[p]\<close>; delimiters are quoted. Many productions have an extra |
866 |
\<open>\<dots> => name\<close>. These names later become the heads of parse |
|
61458 | 867 |
trees; they also guide the pretty printer. |
28777 | 868 |
|
61477 | 869 |
Productions without such parse tree names are called \<^emph>\<open>copy |
870 |
productions\<close>. Their right-hand side must have exactly one |
|
61458 | 871 |
nonterminal symbol (or named token). The parser does not create a |
872 |
new parse tree node for copy productions, but simply returns the |
|
873 |
parse tree of the right-hand symbol. |
|
46282 | 874 |
|
61458 | 875 |
If the right-hand side of a copy production consists of a single |
61477 | 876 |
nonterminal without any delimiters, then it is called a \<^emph>\<open>chain |
877 |
production\<close>. Chain productions act as abbreviations: conceptually, |
|
61458 | 878 |
they are removed from the grammar by adding new productions. |
879 |
Priority information attached to chain productions is ignored; only |
|
61493 | 880 |
the dummy value \<open>-1\<close> is displayed. |
46282 | 881 |
|
61493 | 882 |
\<^descr> \<open>print modes\<close> lists the alternative print modes |
61458 | 883 |
provided by this grammar; see \secref{sec:print-modes}. |
28777 | 884 |
|
61493 | 885 |
\<^descr> \<open>parse_rules\<close> and \<open>print_rules\<close> relate to |
61458 | 886 |
syntax translations (macros); see \secref{sec:syn-trans}. |
46282 | 887 |
|
61493 | 888 |
\<^descr> \<open>parse_ast_translation\<close> and \<open>print_ast_translation\<close> list sets of constants that invoke |
61458 | 889 |
translation functions for abstract syntax trees, which are only |
890 |
required in very special situations; see \secref{sec:tr-funs}. |
|
28777 | 891 |
|
61493 | 892 |
\<^descr> \<open>parse_translation\<close> and \<open>print_translation\<close> |
61458 | 893 |
list the sets of constants that invoke regular translation |
894 |
functions; see \secref{sec:tr-funs}. |
|
58618 | 895 |
\<close> |
28774 | 896 |
|
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset
|
897 |
|
58618 | 898 |
subsection \<open>Ambiguity of parsed expressions\<close> |
46291 | 899 |
|
58618 | 900 |
text \<open> |
46291 | 901 |
\begin{tabular}{rcll} |
61493 | 902 |
@{attribute_def syntax_ambiguity_warning} & : & \<open>attribute\<close> & default \<open>true\<close> \\ |
903 |
@{attribute_def syntax_ambiguity_limit} & : & \<open>attribute\<close> & default \<open>10\<close> \\ |
|
46291 | 904 |
\end{tabular} |
905 |
||
906 |
Depending on the grammar and the given input, parsing may be |
|
907 |
ambiguous. Isabelle lets the Earley parser enumerate all possible |
|
908 |
parse trees, and then tries to make the best out of the situation. |
|
909 |
Terms that cannot be type-checked are filtered out, which often |
|
910 |
leads to a unique result in the end. Unlike regular type |
|
911 |
reconstruction, which is applied to the whole collection of input |
|
912 |
terms simultaneously, the filtering stage only treats each given |
|
913 |
term in isolation. Filtering is also not attempted for individual |
|
914 |
types or raw ASTs (as required for @{command translations}). |
|
915 |
||
916 |
Certain warning or error messages are printed, depending on the |
|
917 |
situation and the given configuration options. Parsing ultimately |
|
918 |
fails, if multiple results remain after the filtering phase. |
|
919 |
||
61439 | 920 |
\<^descr> @{attribute syntax_ambiguity_warning} controls output of |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
921 |
explicit warning messages about syntax ambiguity. |
46291 | 922 |
|
61439 | 923 |
\<^descr> @{attribute syntax_ambiguity_limit} determines the number of |
46291 | 924 |
resulting parse trees that are shown as part of the printed message |
925 |
in case of an ambiguity. |
|
58618 | 926 |
\<close> |
46291 | 927 |
|
928 |
||
58618 | 929 |
section \<open>Syntax transformations \label{sec:syntax-transformations}\<close> |
48113 | 930 |
|
58618 | 931 |
text \<open>The inner syntax engine of Isabelle provides separate |
52413 | 932 |
mechanisms to transform parse trees either via rewrite systems on |
48113 | 933 |
first-order ASTs (\secref{sec:syn-trans}), or ML functions on ASTs |
61493 | 934 |
or syntactic \<open>\<lambda>\<close>-terms (\secref{sec:tr-funs}). This works |
48113 | 935 |
both for parsing and printing, as outlined in |
936 |
\figref{fig:parse-print}. |
|
937 |
||
938 |
\begin{figure}[htbp] |
|
939 |
\begin{center} |
|
940 |
\begin{tabular}{cl} |
|
941 |
string & \\ |
|
61493 | 942 |
\<open>\<down>\<close> & lexer + parser \\ |
48113 | 943 |
parse tree & \\ |
61493 | 944 |
\<open>\<down>\<close> & parse AST translation \\ |
48113 | 945 |
AST & \\ |
61493 | 946 |
\<open>\<down>\<close> & AST rewriting (macros) \\ |
48113 | 947 |
AST & \\ |
61493 | 948 |
\<open>\<down>\<close> & parse translation \\ |
48113 | 949 |
--- pre-term --- & \\ |
61493 | 950 |
\<open>\<down>\<close> & print translation \\ |
48113 | 951 |
AST & \\ |
61493 | 952 |
\<open>\<down>\<close> & AST rewriting (macros) \\ |
48113 | 953 |
AST & \\ |
61493 | 954 |
\<open>\<down>\<close> & print AST translation \\ |
48113 | 955 |
string & |
956 |
\end{tabular} |
|
957 |
\end{center} |
|
958 |
\caption{Parsing and printing with translations}\label{fig:parse-print} |
|
959 |
\end{figure} |
|
960 |
||
961 |
These intermediate syntax tree formats eventually lead to a pre-term |
|
962 |
with all names and binding scopes resolved, but most type |
|
963 |
information still missing. Explicit type constraints might be given by |
|
964 |
the user, or implicit position information by the system --- both |
|
48816 | 965 |
need to be passed-through carefully by syntax transformations. |
48113 | 966 |
|
61477 | 967 |
Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and |
968 |
\<^emph>\<open>uncheck\<close> phases that are intertwined with type-inference (see |
|
58552 | 969 |
also @{cite "isabelle-implementation"}). The latter allows to operate |
48113 | 970 |
on higher-order abstract syntax with proper binding and type |
971 |
information already available. |
|
972 |
||
973 |
As a rule of thumb, anything that manipulates bindings of variables |
|
974 |
or constants needs to be implemented as syntax transformation (see |
|
975 |
below). Anything else is better done via check/uncheck: a prominent |
|
976 |
example application is the @{command abbreviation} concept of |
|
58618 | 977 |
Isabelle/Pure.\<close> |
48113 | 978 |
|
979 |
||
58618 | 980 |
subsection \<open>Abstract syntax trees \label{sec:ast}\<close> |
48113 | 981 |
|
58618 | 982 |
text \<open>The ML datatype @{ML_type Ast.ast} explicitly represents the |
48114 | 983 |
intermediate AST format that is used for syntax rewriting |
984 |
(\secref{sec:syn-trans}). It is defined in ML as follows: |
|
61408
9020a3ba6c9a
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61143
diff
changeset
|
985 |
@{verbatim [display] |
9020a3ba6c9a
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61143
diff
changeset
|
986 |
\<open>datatype ast = |
9020a3ba6c9a
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61143
diff
changeset
|
987 |
Constant of string | |
9020a3ba6c9a
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61143
diff
changeset
|
988 |
Variable of string | |
9020a3ba6c9a
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61143
diff
changeset
|
989 |
Appl of ast list\<close>} |
48114 | 990 |
|
991 |
An AST is either an atom (constant or variable) or a list of (at |
|
992 |
least two) subtrees. Occasional diagnostic output of ASTs uses |
|
993 |
notation that resembles S-expression of LISP. Constant atoms are |
|
994 |
shown as quoted strings, variable atoms as non-quoted strings and |
|
995 |
applications as a parenthesized list of subtrees. For example, the |
|
996 |
AST |
|
58724 | 997 |
@{ML [display] \<open>Ast.Appl [Ast.Constant "_abs", Ast.Variable "x", Ast.Variable "t"]\<close>} |
998 |
is pretty-printed as @{verbatim \<open>("_abs" x t)\<close>}. Note that |
|
48114 | 999 |
@{verbatim "()"} and @{verbatim "(x)"} are excluded as ASTs, because |
1000 |
they have too few subtrees. |
|
1001 |
||
61421 | 1002 |
\<^medskip> |
1003 |
AST application is merely a pro-forma mechanism to indicate |
|
48114 | 1004 |
certain syntactic structures. Thus @{verbatim "(c a b)"} could mean |
1005 |
either term application or type application, depending on the |
|
1006 |
syntactic context. |
|
1007 |
||
58724 | 1008 |
Nested application like @{verbatim \<open>(("_abs" x t) u)\<close>} is also |
48114 | 1009 |
possible, but ASTs are definitely first-order: the syntax constant |
58724 | 1010 |
@{verbatim \<open>"_abs"\<close>} does not bind the @{verbatim x} in any way. |
48114 | 1011 |
Proper bindings are introduced in later stages of the term syntax, |
58724 | 1012 |
where @{verbatim \<open>("_abs" x t)\<close>} becomes an @{ML Abs} node and |
48114 | 1013 |
occurrences of @{verbatim x} in @{verbatim t} are replaced by bound |
1014 |
variables (represented as de-Bruijn indices). |
|
58618 | 1015 |
\<close> |
48113 | 1016 |
|
1017 |
||
58618 | 1018 |
subsubsection \<open>AST constants versus variables\<close> |
48114 | 1019 |
|
58618 | 1020 |
text \<open>Depending on the situation --- input syntax, output syntax, |
56582 | 1021 |
translation patterns --- the distinction of atomic ASTs as @{ML |
48114 | 1022 |
Ast.Constant} versus @{ML Ast.Variable} serves slightly different |
1023 |
purposes. |
|
1024 |
||
61493 | 1025 |
Input syntax of a term such as \<open>f a b = c\<close> does not yet |
1026 |
indicate the scopes of atomic entities \<open>f, a, b, c\<close>: they |
|
48114 | 1027 |
could be global constants or local variables, even bound ones |
1028 |
depending on the context of the term. @{ML Ast.Variable} leaves |
|
1029 |
this choice still open: later syntax layers (or translation |
|
1030 |
functions) may capture such a variable to determine its role |
|
1031 |
specifically, to make it a constant, bound variable, free variable |
|
1032 |
etc. In contrast, syntax translations that introduce already known |
|
1033 |
constants would rather do it via @{ML Ast.Constant} to prevent |
|
1034 |
accidental re-interpretation later on. |
|
1035 |
||
1036 |
Output syntax turns term constants into @{ML Ast.Constant} and |
|
1037 |
variables (free or schematic) into @{ML Ast.Variable}. This |
|
61493 | 1038 |
information is precise when printing fully formal \<open>\<lambda>\<close>-terms. |
48114 | 1039 |
|
61421 | 1040 |
\<^medskip> |
1041 |
AST translation patterns (\secref{sec:syn-trans}) that |
|
52413 | 1042 |
represent terms cannot distinguish constants and variables |
61493 | 1043 |
syntactically. Explicit indication of \<open>CONST c\<close> inside the |
1044 |
term language is required, unless \<open>c\<close> is known as special |
|
61477 | 1045 |
\<^emph>\<open>syntax constant\<close> (see also @{command syntax}). It is also |
52413 | 1046 |
possible to use @{command syntax} declarations (without mixfix |
1047 |
annotation) to enforce that certain unqualified names are always |
|
1048 |
treated as constant within the syntax machinery. |
|
48114 | 1049 |
|
52413 | 1050 |
The situation is simpler for ASTs that represent types or sorts, |
1051 |
since the concrete syntax already distinguishes type variables from |
|
61493 | 1052 |
type constants (constructors). So \<open>('a, 'b) foo\<close> |
1053 |
corresponds to an AST application of some constant for \<open>foo\<close> |
|
1054 |
and variable arguments for \<open>'a\<close> and \<open>'b\<close>. Note that |
|
52413 | 1055 |
the postfix application is merely a feature of the concrete syntax, |
58618 | 1056 |
while in the AST the constructor occurs in head position.\<close> |
48114 | 1057 |
|
1058 |
||
58618 | 1059 |
subsubsection \<open>Authentic syntax names\<close> |
48114 | 1060 |
|
58618 | 1061 |
text \<open>Naming constant entities within ASTs is another delicate |
52413 | 1062 |
issue. Unqualified names are resolved in the name space tables in |
48114 | 1063 |
the last stage of parsing, after all translations have been applied. |
1064 |
Since syntax transformations do not know about this later name |
|
52413 | 1065 |
resolution, there can be surprises in boundary cases. |
48114 | 1066 |
|
61477 | 1067 |
\<^emph>\<open>Authentic syntax names\<close> for @{ML Ast.Constant} avoid this |
48114 | 1068 |
problem: the fully-qualified constant name with a special prefix for |
61493 | 1069 |
its formal category (\<open>class\<close>, \<open>type\<close>, \<open>const\<close>, \<open>fixed\<close>) represents the information faithfully |
48114 | 1070 |
within the untyped AST format. Accidental overlap with free or |
1071 |
bound variables is excluded as well. Authentic syntax names work |
|
1072 |
implicitly in the following situations: |
|
1073 |
||
61421 | 1074 |
\<^item> Input of term constants (or fixed variables) that are |
48114 | 1075 |
introduced by concrete syntax via @{command notation}: the |
1076 |
correspondence of a particular grammar production to some known term |
|
1077 |
entity is preserved. |
|
1078 |
||
61421 | 1079 |
\<^item> Input of type constants (constructors) and type classes --- |
48114 | 1080 |
thanks to explicit syntactic distinction independently on the |
1081 |
context. |
|
1082 |
||
61421 | 1083 |
\<^item> Output of term constants, type constants, type classes --- |
48114 | 1084 |
this information is already available from the internal term to be |
1085 |
printed. |
|
1086 |
||
1087 |
||
1088 |
In other words, syntax transformations that operate on input terms |
|
48816 | 1089 |
written as prefix applications are difficult to make robust. |
1090 |
Luckily, this case rarely occurs in practice, because syntax forms |
|
58618 | 1091 |
to be translated usually correspond to some concrete notation.\<close> |
48114 | 1092 |
|
1093 |
||
58618 | 1094 |
subsection \<open>Raw syntax and translations \label{sec:syn-trans}\<close> |
28762 | 1095 |
|
58618 | 1096 |
text \<open> |
48117 | 1097 |
\begin{tabular}{rcll} |
61493 | 1098 |
@{command_def "nonterminal"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
1099 |
@{command_def "syntax"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1100 |
@{command_def "no_syntax"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1101 |
@{command_def "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1102 |
@{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1103 |
@{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
1104 |
@{attribute_def syntax_ast_stats} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
48117 | 1105 |
\end{tabular} |
61421 | 1106 |
\<^medskip> |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
58842
diff
changeset
|
1107 |
|
46292 | 1108 |
Unlike mixfix notation for existing formal entities |
1109 |
(\secref{sec:notation}), raw syntax declarations provide full access |
|
48115 | 1110 |
to the priority grammar of the inner syntax, without any sanity |
1111 |
checks. This includes additional syntactic categories (via |
|
1112 |
@{command nonterminal}) and free-form grammar productions (via |
|
1113 |
@{command syntax}). Additional syntax translations (or macros, via |
|
1114 |
@{command translations}) are required to turn resulting parse trees |
|
1115 |
into proper representations of formal entities again. |
|
46292 | 1116 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55108
diff
changeset
|
1117 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1118 |
@@{command nonterminal} (@{syntax name} + @'and') |
28762 | 1119 |
; |
46494
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1120 |
(@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +) |
28762 | 1121 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1122 |
(@@{command translations} | @@{command no_translations}) |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1123 |
(transpat ('==' | '=>' | '<=' | '\<rightleftharpoons>' | '\<rightharpoonup>' | '\<leftharpoondown>') transpat +) |
28762 | 1124 |
; |
1125 |
||
46494
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1126 |
constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}? |
ea2ae63336f3
clarified outer syntax "constdecl", which is only local to some rail diagrams;
wenzelm
parents:
46483
diff
changeset
|
1127 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1128 |
mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')') |
28762 | 1129 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1130 |
transpat: ('(' @{syntax nameref} ')')? @{syntax string} |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55108
diff
changeset
|
1131 |
\<close>} |
28762 | 1132 |
|
61493 | 1133 |
\<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type |
1134 |
constructor \<open>c\<close> (without arguments) to act as purely syntactic |
|
28762 | 1135 |
type: a nonterminal symbol of the inner syntax. |
1136 |
||
61493 | 1137 |
\<^descr> @{command "syntax"}~\<open>(mode) c :: \<sigma> (mx)\<close> augments the |
46292 | 1138 |
priority grammar and the pretty printer table for the given print |
58724 | 1139 |
mode (default @{verbatim \<open>""\<close>}). An optional keyword @{keyword_ref |
46292 | 1140 |
"output"} means that only the pretty printer table is affected. |
1141 |
||
61493 | 1142 |
Following \secref{sec:mixfix}, the mixfix annotation \<open>mx = |
1143 |
template ps q\<close> together with type \<open>\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> and |
|
1144 |
specify a grammar production. The \<open>template\<close> contains |
|
1145 |
delimiter tokens that surround \<open>n\<close> argument positions |
|
46292 | 1146 |
(@{verbatim "_"}). The latter correspond to nonterminal symbols |
61493 | 1147 |
\<open>A\<^sub>i\<close> derived from the argument types \<open>\<tau>\<^sub>i\<close> as |
46292 | 1148 |
follows: |
1149 |
||
61493 | 1150 |
\<^item> \<open>prop\<close> if \<open>\<tau>\<^sub>i = prop\<close> |
46292 | 1151 |
|
61493 | 1152 |
\<^item> \<open>logic\<close> if \<open>\<tau>\<^sub>i = (\<dots>)\<kappa>\<close> for logical type |
1153 |
constructor \<open>\<kappa> \<noteq> prop\<close> |
|
46292 | 1154 |
|
61493 | 1155 |
\<^item> \<open>any\<close> if \<open>\<tau>\<^sub>i = \<alpha>\<close> for type variables |
46292 | 1156 |
|
61493 | 1157 |
\<^item> \<open>\<kappa>\<close> if \<open>\<tau>\<^sub>i = \<kappa>\<close> for nonterminal \<open>\<kappa>\<close> |
61458 | 1158 |
(syntactic type constructor) |
46292 | 1159 |
|
61493 | 1160 |
Each \<open>A\<^sub>i\<close> is decorated by priority \<open>p\<^sub>i\<close> from the |
1161 |
given list \<open>ps\<close>; missing priorities default to 0. |
|
46292 | 1162 |
|
1163 |
The resulting nonterminal of the production is determined similarly |
|
61493 | 1164 |
from type \<open>\<tau>\<close>, with priority \<open>q\<close> and default 1000. |
46292 | 1165 |
|
61421 | 1166 |
\<^medskip> |
61493 | 1167 |
Parsing via this production produces parse trees \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> for the argument slots. The resulting parse tree is |
1168 |
composed as \<open>c t\<^sub>1 \<dots> t\<^sub>n\<close>, by using the syntax constant \<open>c\<close> of the syntax declaration. |
|
46292 | 1169 |
|
1170 |
Such syntactic constants are invented on the spot, without formal |
|
1171 |
check wrt.\ existing declarations. It is conventional to use plain |
|
61493 | 1172 |
identifiers prefixed by a single underscore (e.g.\ \<open>_foobar\<close>). Names should be chosen with care, to avoid clashes |
48816 | 1173 |
with other syntax declarations. |
46292 | 1174 |
|
61421 | 1175 |
\<^medskip> |
61493 | 1176 |
The special case of copy production is specified by \<open>c = \<close>@{verbatim \<open>""\<close>} (empty string). It means that the |
1177 |
resulting parse tree \<open>t\<close> is copied directly, without any |
|
46292 | 1178 |
further decoration. |
46282 | 1179 |
|
61493 | 1180 |
\<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar |
1181 |
declarations (and translations) resulting from \<open>decls\<close>, which |
|
28762 | 1182 |
are interpreted in the same manner as for @{command "syntax"} above. |
46282 | 1183 |
|
61493 | 1184 |
\<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic |
48115 | 1185 |
translation rules (i.e.\ macros) as first-order rewrite rules on |
48816 | 1186 |
ASTs (\secref{sec:ast}). The theory context maintains two |
48115 | 1187 |
independent lists translation rules: parse rules (@{verbatim "=>"} |
61493 | 1188 |
or \<open>\<rightharpoonup>\<close>) and print rules (@{verbatim "<="} or \<open>\<leftharpoondown>\<close>). |
48115 | 1189 |
For convenience, both can be specified simultaneously as parse~/ |
61493 | 1190 |
print rules (@{verbatim "=="} or \<open>\<rightleftharpoons>\<close>). |
48115 | 1191 |
|
28762 | 1192 |
Translation patterns may be prefixed by the syntactic category to be |
61493 | 1193 |
used for parsing; the default is \<open>logic\<close> which means that |
48115 | 1194 |
regular term syntax is used. Both sides of the syntax translation |
1195 |
rule undergo parsing and parse AST translations |
|
1196 |
\secref{sec:tr-funs}, in order to perform some fundamental |
|
61493 | 1197 |
normalization like \<open>\<lambda>x y. b \<leadsto> \<lambda>x. \<lambda>y. b\<close>, but other AST |
61477 | 1198 |
translation rules are \<^emph>\<open>not\<close> applied recursively here. |
48115 | 1199 |
|
1200 |
When processing AST patterns, the inner syntax lexer runs in a |
|
1201 |
different mode that allows identifiers to start with underscore. |
|
1202 |
This accommodates the usual naming convention for auxiliary syntax |
|
1203 |
constants --- those that do not have a logical counter part --- by |
|
1204 |
allowing to specify arbitrary AST applications within the term |
|
1205 |
syntax, independently of the corresponding concrete syntax. |
|
1206 |
||
1207 |
Atomic ASTs are distinguished as @{ML Ast.Constant} versus @{ML |
|
1208 |
Ast.Variable} as follows: a qualified name or syntax constant |
|
1209 |
declared via @{command syntax}, or parse tree head of concrete |
|
1210 |
notation becomes @{ML Ast.Constant}, anything else @{ML |
|
61493 | 1211 |
Ast.Variable}. Note that \<open>CONST\<close> and \<open>XCONST\<close> within |
48115 | 1212 |
the term language (\secref{sec:pure-grammar}) allow to enforce |
1213 |
treatment as constants. |
|
1214 |
||
61493 | 1215 |
AST rewrite rules \<open>(lhs, rhs)\<close> need to obey the following |
48115 | 1216 |
side-conditions: |
1217 |
||
61493 | 1218 |
\<^item> Rules must be left linear: \<open>lhs\<close> must not contain |
61458 | 1219 |
repeated variables.\footnote{The deeper reason for this is that AST |
1220 |
equality is not well-defined: different occurrences of the ``same'' |
|
1221 |
AST could be decorated differently by accidental type-constraints or |
|
1222 |
source position information, for example.} |
|
48115 | 1223 |
|
61493 | 1224 |
\<^item> Every variable in \<open>rhs\<close> must also occur in \<open>lhs\<close>. |
48115 | 1225 |
|
61493 | 1226 |
\<^descr> @{command "no_translations"}~\<open>rules\<close> removes syntactic |
28762 | 1227 |
translation rules, which are interpreted in the same manner as for |
1228 |
@{command "translations"} above. |
|
1229 |
||
61439 | 1230 |
\<^descr> @{attribute syntax_ast_trace} and @{attribute |
48117 | 1231 |
syntax_ast_stats} control diagnostic output in the AST normalization |
1232 |
process, when translation rules are applied to concrete input or |
|
1233 |
output. |
|
1234 |
||
46293 | 1235 |
|
1236 |
Raw syntax and translations provides a slightly more low-level |
|
1237 |
access to the grammar and the form of resulting parse trees. It is |
|
1238 |
often possible to avoid this untyped macro mechanism, and use |
|
1239 |
type-safe @{command abbreviation} or @{command notation} instead. |
|
1240 |
Some important situations where @{command syntax} and @{command |
|
1241 |
translations} are really need are as follows: |
|
1242 |
||
61421 | 1243 |
\<^item> Iterated replacement via recursive @{command translations}. |
46293 | 1244 |
For example, consider list enumeration @{term "[a, b, c, d]"} as |
1245 |
defined in theory @{theory List} in Isabelle/HOL. |
|
1246 |
||
61421 | 1247 |
\<^item> Change of binding status of variables: anything beyond the |
46293 | 1248 |
built-in @{keyword "binder"} mixfix annotation requires explicit |
1249 |
syntax translations. For example, consider list filter |
|
1250 |
comprehension @{term "[x \<leftarrow> xs . P]"} as defined in theory @{theory |
|
1251 |
List} in Isabelle/HOL. |
|
61458 | 1252 |
\<close> |
46293 | 1253 |
|
28762 | 1254 |
|
58618 | 1255 |
subsubsection \<open>Applying translation rules\<close> |
48117 | 1256 |
|
58618 | 1257 |
text \<open>As a term is being parsed or printed, an AST is generated as |
48117 | 1258 |
an intermediate form according to \figref{fig:parse-print}. The AST |
1259 |
is normalized by applying translation rules in the manner of a |
|
1260 |
first-order term rewriting system. We first examine how a single |
|
1261 |
rule is applied. |
|
1262 |
||
61493 | 1263 |
Let \<open>t\<close> be the abstract syntax tree to be normalized and |
1264 |
\<open>(lhs, rhs)\<close> some translation rule. A subtree \<open>u\<close> |
|
1265 |
of \<open>t\<close> is called \<^emph>\<open>redex\<close> if it is an instance of \<open>lhs\<close>; in this case the pattern \<open>lhs\<close> is said to match the |
|
1266 |
object \<open>u\<close>. A redex matched by \<open>lhs\<close> may be |
|
1267 |
replaced by the corresponding instance of \<open>rhs\<close>, thus |
|
1268 |
\<^emph>\<open>rewriting\<close> the AST \<open>t\<close>. Matching requires some notion |
|
61477 | 1269 |
of \<^emph>\<open>place-holders\<close> in rule patterns: @{ML Ast.Variable} serves |
48117 | 1270 |
this purpose. |
1271 |
||
61493 | 1272 |
More precisely, the matching of the object \<open>u\<close> against the |
1273 |
pattern \<open>lhs\<close> is performed as follows: |
|
48117 | 1274 |
|
61493 | 1275 |
\<^item> Objects of the form @{ML Ast.Variable}~\<open>x\<close> or @{ML |
1276 |
Ast.Constant}~\<open>x\<close> are matched by pattern @{ML |
|
1277 |
Ast.Constant}~\<open>x\<close>. Thus all atomic ASTs in the object are |
|
48117 | 1278 |
treated as (potential) constants, and a successful match makes them |
1279 |
actual constants even before name space resolution (see also |
|
1280 |
\secref{sec:ast}). |
|
1281 |
||
61493 | 1282 |
\<^item> Object \<open>u\<close> is matched by pattern @{ML |
1283 |
Ast.Variable}~\<open>x\<close>, binding \<open>x\<close> to \<open>u\<close>. |
|
48117 | 1284 |
|
61493 | 1285 |
\<^item> Object @{ML Ast.Appl}~\<open>us\<close> is matched by @{ML |
1286 |
Ast.Appl}~\<open>ts\<close> if \<open>us\<close> and \<open>ts\<close> have the |
|
48117 | 1287 |
same length and each corresponding subtree matches. |
1288 |
||
61421 | 1289 |
\<^item> In every other case, matching fails. |
48117 | 1290 |
|
1291 |
||
61493 | 1292 |
A successful match yields a substitution that is applied to \<open>rhs\<close>, generating the instance that replaces \<open>u\<close>. |
48117 | 1293 |
|
1294 |
Normalizing an AST involves repeatedly applying translation rules |
|
1295 |
until none are applicable. This works yoyo-like: top-down, |
|
1296 |
bottom-up, top-down, etc. At each subtree position, rules are |
|
1297 |
chosen in order of appearance in the theory definitions. |
|
1298 |
||
1299 |
The configuration options @{attribute syntax_ast_trace} and |
|
48816 | 1300 |
@{attribute syntax_ast_stats} might help to understand this process |
48117 | 1301 |
and diagnose problems. |
1302 |
||
1303 |
\begin{warn} |
|
1304 |
If syntax translation rules work incorrectly, the output of |
|
61477 | 1305 |
@{command_ref print_syntax} with its \<^emph>\<open>rules\<close> sections reveals the |
48117 | 1306 |
actual internal forms of AST pattern, without potentially confusing |
1307 |
concrete syntax. Recall that AST constants appear as quoted strings |
|
1308 |
and variables without quotes. |
|
1309 |
\end{warn} |
|
1310 |
||
1311 |
\begin{warn} |
|
61493 | 1312 |
If @{attribute_ref eta_contract} is set to \<open>true\<close>, terms |
1313 |
will be \<open>\<eta>\<close>-contracted \<^emph>\<open>before\<close> the AST rewriter sees |
|
48117 | 1314 |
them. Thus some abstraction nodes needed for print rules to match |
61493 | 1315 |
may vanish. For example, \<open>Ball A (\<lambda>x. P x)\<close> would contract |
1316 |
to \<open>Ball A P\<close> and the standard print rule would fail to |
|
48117 | 1317 |
apply. This problem can be avoided by hand-written ML translation |
1318 |
functions (see also \secref{sec:tr-funs}), which is in fact the same |
|
1319 |
mechanism used in built-in @{keyword "binder"} declarations. |
|
1320 |
\end{warn} |
|
58618 | 1321 |
\<close> |
48117 | 1322 |
|
28762 | 1323 |
|
58618 | 1324 |
subsection \<open>Syntax translation functions \label{sec:tr-funs}\<close> |
28762 | 1325 |
|
58618 | 1326 |
text \<open> |
28762 | 1327 |
\begin{matharray}{rcl} |
61493 | 1328 |
@{command_def "parse_ast_translation"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
1329 |
@{command_def "parse_translation"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1330 |
@{command_def "print_translation"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1331 |
@{command_def "typed_print_translation"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1332 |
@{command_def "print_ast_translation"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1333 |
@{ML_antiquotation_def "class_syntax"} & : & \<open>ML antiquotation\<close> \\ |
|
1334 |
@{ML_antiquotation_def "type_syntax"} & : & \<open>ML antiquotation\<close> \\ |
|
1335 |
@{ML_antiquotation_def "const_syntax"} & : & \<open>ML antiquotation\<close> \\ |
|
1336 |
@{ML_antiquotation_def "syntax_const"} & : & \<open>ML antiquotation\<close> \\ |
|
28762 | 1337 |
\end{matharray} |
1338 |
||
48118 | 1339 |
Syntax translation functions written in ML admit almost arbitrary |
1340 |
manipulations of inner syntax, at the expense of some complexity and |
|
1341 |
obscurity in the implementation. |
|
1342 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55108
diff
changeset
|
1343 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1344 |
( @@{command parse_ast_translation} | @@{command parse_translation} | |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset
|
1345 |
@@{command print_translation} | @@{command typed_print_translation} | |
52143 | 1346 |
@@{command print_ast_translation}) @{syntax text} |
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
|
1347 |
; |
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
|
1348 |
(@@{ML_antiquotation class_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
|
1349 |
@@{ML_antiquotation type_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
|
1350 |
@@{ML_antiquotation const_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
|
1351 |
@@{ML_antiquotation syntax_const}) name |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55108
diff
changeset
|
1352 |
\<close>} |
28762 | 1353 |
|
61439 | 1354 |
\<^descr> @{command parse_translation} etc. declare syntax translation |
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
|
1355 |
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
|
1356 |
@{syntax text} argument that refers to an ML expression of |
52413 | 1357 |
appropriate type as follows: |
48118 | 1358 |
|
61421 | 1359 |
\<^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
|
1360 |
{\footnotesize |
52143 | 1361 |
\begin{tabular}{l} |
1362 |
@{command parse_ast_translation} : \\ |
|
1363 |
\quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\ |
|
1364 |
@{command parse_translation} : \\ |
|
1365 |
\quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\ |
|
1366 |
@{command print_translation} : \\ |
|
1367 |
\quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\ |
|
1368 |
@{command typed_print_translation} : \\ |
|
1369 |
\quad @{ML_type "(string * (Proof.context -> typ -> term list -> term)) list"} \\ |
|
1370 |
@{command print_ast_translation} : \\ |
|
1371 |
\quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\ |
|
48118 | 1372 |
\end{tabular}} |
61421 | 1373 |
\<^medskip> |
28762 | 1374 |
|
61493 | 1375 |
The argument list consists of \<open>(c, tr)\<close> pairs, where \<open>c\<close> is the syntax name of the formal entity involved, and \<open>tr\<close> a function that translates a syntax form \<open>c args\<close> into |
1376 |
\<open>tr ctxt args\<close> (depending on the context). The Isabelle/ML |
|
1377 |
naming convention for parse translations is \<open>c_tr\<close> and for |
|
1378 |
print translations \<open>c_tr'\<close>. |
|
48118 | 1379 |
|
1380 |
The @{command_ref print_syntax} command displays the sets of names |
|
61493 | 1381 |
associated with the translation functions of a theory under \<open>parse_ast_translation\<close> etc. |
48118 | 1382 |
|
61493 | 1383 |
\<^descr> \<open>@{class_syntax c}\<close>, \<open>@{type_syntax c}\<close>, |
1384 |
\<open>@{const_syntax c}\<close> inline the authentic syntax name of the |
|
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
|
1385 |
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
|
1386 |
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
|
1387 |
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
|
1388 |
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
|
1389 |
|
61493 | 1390 |
\<^descr> \<open>@{const_syntax c}\<close> inlines the name \<open>c\<close> of |
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
|
1391 |
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
|
1392 |
via some @{command 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
|
1393 |
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
|
1394 |
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
|
1395 |
names occurring in parse trees (unqualified constants etc.). |
58618 | 1396 |
\<close> |
48118 | 1397 |
|
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
|
1398 |
|
58618 | 1399 |
subsubsection \<open>The translation strategy\<close> |
28762 | 1400 |
|
58618 | 1401 |
text \<open>The different kinds of translation functions are invoked during |
48118 | 1402 |
the transformations between parse trees, ASTs and syntactic terms |
1403 |
(cf.\ \figref{fig:parse-print}). Whenever a combination of the form |
|
61493 | 1404 |
\<open>c x\<^sub>1 \<dots> x\<^sub>n\<close> is encountered, and a translation function |
1405 |
\<open>f\<close> of appropriate kind is declared for \<open>c\<close>, the |
|
1406 |
result is produced by evaluation of \<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> in ML. |
|
48118 | 1407 |
|
61493 | 1408 |
For AST translations, the arguments \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> are ASTs. A |
1409 |
combination has the form @{ML "Ast.Constant"}~\<open>c\<close> or @{ML |
|
1410 |
"Ast.Appl"}~\<open>[\<close>@{ML Ast.Constant}~\<open>c, x\<^sub>1, \<dots>, x\<^sub>n]\<close>. |
|
48118 | 1411 |
For term translations, the arguments are terms and a combination has |
61493 | 1412 |
the form @{ML Const}~\<open>(c, \<tau>)\<close> or @{ML Const}~\<open>(c, \<tau>) |
1413 |
$ x\<^sub>1 $ \<dots> $ x\<^sub>n\<close>. Terms allow more sophisticated transformations |
|
48118 | 1414 |
than ASTs do, typically involving abstractions and bound |
61477 | 1415 |
variables. \<^emph>\<open>Typed\<close> print translations may even peek at the type |
61493 | 1416 |
\<open>\<tau>\<close> of the constant they are invoked on, although some |
52413 | 1417 |
information might have been suppressed for term output already. |
48118 | 1418 |
|
1419 |
Regardless of whether they act on ASTs or terms, translation |
|
1420 |
functions called during the parsing process differ from those for |
|
1421 |
printing in their overall behaviour: |
|
1422 |
||
61439 | 1423 |
\<^descr>[Parse translations] are applied bottom-up. The arguments are |
48118 | 1424 |
already in translated form. The translations must not fail; |
1425 |
exceptions trigger an error message. There may be at most one |
|
1426 |
function associated with any syntactic name. |
|
46294 | 1427 |
|
61439 | 1428 |
\<^descr>[Print translations] are applied top-down. They are supplied |
48118 | 1429 |
with arguments that are partly still in internal form. The result |
1430 |
again undergoes translation; therefore a print translation should |
|
1431 |
not introduce as head the very constant that invoked it. The |
|
1432 |
function may raise exception @{ML Match} to indicate failure; in |
|
1433 |
this event it has no effect. Multiple functions associated with |
|
1434 |
some syntactic name are tried in the order of declaration in the |
|
1435 |
theory. |
|
1436 |
||
1437 |
||
1438 |
Only constant atoms --- constructor @{ML Ast.Constant} for ASTs and |
|
1439 |
@{ML Const} for terms --- can invoke translation functions. This |
|
1440 |
means that parse translations can only be associated with parse tree |
|
1441 |
heads of concrete syntax, or syntactic constants introduced via |
|
1442 |
other translations. For plain identifiers within the term language, |
|
1443 |
the status of constant versus variable is not yet know during |
|
1444 |
parsing. This is in contrast to print translations, where constants |
|
1445 |
are explicitly known from the given term in its fully internal form. |
|
58618 | 1446 |
\<close> |
28762 | 1447 |
|
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1448 |
|
58618 | 1449 |
subsection \<open>Built-in syntax transformations\<close> |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1450 |
|
58618 | 1451 |
text \<open> |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1452 |
Here are some further details of the main syntax transformation |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1453 |
phases of \figref{fig:parse-print}. |
58618 | 1454 |
\<close> |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1455 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1456 |
|
58618 | 1457 |
subsubsection \<open>Transforming parse trees to ASTs\<close> |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1458 |
|
58618 | 1459 |
text \<open>The parse tree is the raw output of the parser. It is |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1460 |
transformed into an AST according to some basic scheme that may be |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1461 |
augmented by AST translation functions as explained in |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1462 |
\secref{sec:tr-funs}. |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1463 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1464 |
The parse tree is constructed by nesting the right-hand sides of the |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1465 |
productions used to recognize the input. Such parse trees are |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1466 |
simply lists of tokens and constituent parse trees, the latter |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1467 |
representing the nonterminals of the productions. Ignoring AST |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1468 |
translation functions, parse trees are transformed to ASTs by |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1469 |
stripping out delimiters and copy productions, while retaining some |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1470 |
source position information from input tokens. |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1471 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1472 |
The Pure syntax provides predefined AST translations to make the |
61493 | 1473 |
basic \<open>\<lambda>\<close>-term structure more apparent within the |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1474 |
(first-order) AST representation, and thus facilitate the use of |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1475 |
@{command translations} (see also \secref{sec:syn-trans}). This |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1476 |
covers ordinary term application, type application, nested |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1477 |
abstraction, iterated meta implications and function types. The |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1478 |
effect is illustrated on some representative input strings is as |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1479 |
follows: |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1480 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1481 |
\begin{center} |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1482 |
\begin{tabular}{ll} |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1483 |
input source & AST \\ |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1484 |
\hline |
61493 | 1485 |
\<open>f x y z\<close> & @{verbatim "(f x y z)"} \\ |
1486 |
\<open>'a ty\<close> & @{verbatim "(ty 'a)"} \\ |
|
1487 |
\<open>('a, 'b)ty\<close> & @{verbatim "(ty 'a 'b)"} \\ |
|
1488 |
\<open>\<lambda>x y z. t\<close> & @{verbatim \<open>("_abs" x ("_abs" y ("_abs" z t)))\<close>} \\ |
|
1489 |
\<open>\<lambda>x :: 'a. t\<close> & @{verbatim \<open>("_abs" ("_constrain" x 'a) t)\<close>} \\ |
|
1490 |
\<open>\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S\<close> & @{verbatim \<open>("Pure.imp" P ("Pure.imp" Q ("Pure.imp" R S)))\<close>} \\ |
|
1491 |
\<open>['a, 'b, 'c] \<Rightarrow> 'd\<close> & @{verbatim \<open>("fun" 'a ("fun" 'b ("fun" 'c 'd)))\<close>} \\ |
|
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1492 |
\end{tabular} |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1493 |
\end{center} |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1494 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1495 |
Note that type and sort constraints may occur in further places --- |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1496 |
translations need to be ready to cope with them. The built-in |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1497 |
syntax transformation from parse trees to ASTs insert additional |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1498 |
constraints that represent source positions. |
58618 | 1499 |
\<close> |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1500 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1501 |
|
58618 | 1502 |
subsubsection \<open>Transforming ASTs to terms\<close> |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1503 |
|
58618 | 1504 |
text \<open>After application of macros (\secref{sec:syn-trans}), the AST |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1505 |
is transformed into a term. This term still lacks proper type |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1506 |
information, but it might contain some constraints consisting of |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1507 |
applications with head @{verbatim "_constrain"}, where the second |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1508 |
argument is a type encoded as a pre-term within the syntax. Type |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1509 |
inference later introduces correct types, or indicates type errors |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1510 |
in the input. |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1511 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1512 |
Ignoring parse translations, ASTs are transformed to terms by |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1513 |
mapping AST constants to term constants, AST variables to term |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1514 |
variables or constants (according to the name space), and AST |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1515 |
applications to iterated term applications. |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1516 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1517 |
The outcome is still a first-order term. Proper abstractions and |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1518 |
bound variables are introduced by parse translations associated with |
58724 | 1519 |
certain syntax constants. Thus @{verbatim \<open>("_abs" x x)\<close>} eventually |
1520 |
becomes a de-Bruijn term @{verbatim \<open>Abs ("x", _, Bound 0)\<close>}. |
|
58618 | 1521 |
\<close> |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1522 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1523 |
|
58618 | 1524 |
subsubsection \<open>Printing of terms\<close> |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1525 |
|
58618 | 1526 |
text \<open>The output phase is essentially the inverse of the input |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1527 |
phase. Terms are translated via abstract syntax trees into |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1528 |
pretty-printed text. |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1529 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1530 |
Ignoring print translations, the transformation maps term constants, |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1531 |
variables and applications to the corresponding constructs on ASTs. |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1532 |
Abstractions are mapped to applications of the special constant |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1533 |
@{verbatim "_abs"} as seen before. Type constraints are represented |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1534 |
via special @{verbatim "_constrain"} forms, according to various |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1535 |
policies of type annotation determined elsewhere. Sort constraints |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1536 |
of type variables are handled in a similar fashion. |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1537 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1538 |
After application of macros (\secref{sec:syn-trans}), the AST is |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1539 |
finally pretty-printed. The built-in print AST translations reverse |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1540 |
the corresponding parse AST translations. |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1541 |
|
61421 | 1542 |
\<^medskip> |
1543 |
For the actual printing process, the priority grammar |
|
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1544 |
(\secref{sec:priority-grammar}) plays a vital role: productions are |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1545 |
used as templates for pretty printing, with argument slots stemming |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1546 |
from nonterminals, and syntactic sugar stemming from literal tokens. |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1547 |
|
61493 | 1548 |
Each AST application with constant head \<open>c\<close> and arguments |
1549 |
\<open>t\<^sub>1\<close>, \dots, \<open>t\<^sub>n\<close> (for \<open>n = 0\<close> the AST is |
|
1550 |
just the constant \<open>c\<close> itself) is printed according to the |
|
1551 |
first grammar production of result name \<open>c\<close>. The required |
|
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1552 |
syntax priority of the argument slot is given by its nonterminal |
61493 | 1553 |
\<open>A\<^sup>(\<^sup>p\<^sup>)\<close>. The argument \<open>t\<^sub>i\<close> that corresponds to the |
1554 |
position of \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is printed recursively, and then put in |
|
1555 |
parentheses \<^emph>\<open>if\<close> its priority \<open>p\<close> requires this. The |
|
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1556 |
resulting output is concatenated with the syntactic sugar according |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1557 |
to the grammar production. |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1558 |
|
61493 | 1559 |
If an AST application \<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> has more arguments than |
1560 |
the corresponding production, it is first split into \<open>((c x\<^sub>1 |
|
1561 |
\<dots> x\<^sub>n) x\<^sub>n\<^sub>+\<^sub>1 \<dots> x\<^sub>m)\<close> and then printed recursively as above. |
|
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1562 |
|
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1563 |
Applications with too few arguments or with non-constant head or |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1564 |
without a corresponding production are printed in prefix-form like |
61493 | 1565 |
\<open>f t\<^sub>1 \<dots> t\<^sub>n\<close> for terms. |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1566 |
|
61493 | 1567 |
Multiple productions associated with some name \<open>c\<close> are tried |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1568 |
in order of appearance within the grammar. An occurrence of some |
61493 | 1569 |
AST variable \<open>x\<close> is printed as \<open>x\<close> outright. |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1570 |
|
61421 | 1571 |
\<^medskip> |
61477 | 1572 |
White space is \<^emph>\<open>not\<close> inserted automatically. If |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1573 |
blanks (or breaks) are required to separate tokens, they need to be |
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1574 |
specified in the mixfix declaration (\secref{sec:mixfix}). |
58618 | 1575 |
\<close> |
52414
8429123bc58a
more on built-in syntax transformations, based on reduced version of old material;
wenzelm
parents:
52413
diff
changeset
|
1576 |
|
28762 | 1577 |
end |