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