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