author  wenzelm 
Sat, 04 Feb 2012 15:56:49 +0100  
changeset 46288  8a2c5dc0b00e 
parent 46287  0bb3d8ee5d25 
child 46289  d0199d9f9c5b 
permissions  rwrr 
28762  1 
theory Inner_Syntax 
42651  2 
imports Base Main 
28762  3 
begin 
4 

28778  5 
chapter {* Inner syntax  the term language \label{ch:innersyntax} *} 
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 sublanguages 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 
userdefined 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 contextfree grammar (see 

26 
\secref{sec:puresyntax}), and various mechanisms for \emph{syntax 

27 
translations}  either as rewrite systems on firstorder ASTs 

28 
(\secref{sec:syntrans}) or ML functions on ASTs or @{text 

29 
"\<lambda>"}terms that represent parse trees (\secref{sec:trfuns}). 

30 
*} 

31 

32 

28762  33 
section {* Printing logical entities *} 
34 

46284  35 
subsection {* Diagnostic commands \label{sec:printdiag} *} 
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 humanreadable 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 
metalogic 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, typecheck 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:printmodes}. 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{isabellesys}. 
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 subexpressions 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}. Higherorder 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 higherorder 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 lowlevel 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:printmodes} *} 
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:printdiag}) 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 threadsafe 

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 
userinterfaces 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 ``XSymbol'' 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 builtin pretty printer, with initial value 

320 
76. Note that userinterfaces 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 runtime 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 1001000 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 contextfree 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 nonempty 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 
metacharacters, 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 nonempty 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{paulsonml2}; 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 

46288  460 
Commands that introduce new logical entities (terms or types) 
461 
usually allow to provide mixfix annotations on the spot, which is 

462 
convenient for default notation. Nonetheless, the syntax may be 

463 
modified later on by declarations for explicit notation. This 

464 
allows to add or delete mixfix annotations for of existing logical 

465 
entities within the current context. 

466 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

467 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

468 
(@@{command type_notation}  @@{command no_type_notation}) @{syntax target}? 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

469 
@{syntax mode}? \\ (@{syntax nameref} @{syntax mixfix} + @'and') 
35413  470 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

471 
(@@{command notation}  @@{command no_notation}) @{syntax target}? @{syntax mode}? \\ 
42705  472 
(@{syntax nameref} @{syntax struct_mixfix} + @'and') 
28762  473 
; 
42705  474 
@@{command write} @{syntax mode}? (@{syntax nameref} @{syntax struct_mixfix} + @'and') 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

475 
"} 
28762  476 

477 
\begin{description} 

478 

35413  479 
\item @{command "type_notation"}~@{text "c (mx)"} associates mixfix 
480 
syntax with an existing type constructor. The arity of the 

481 
constructor is retrieved from the context. 

46282  482 

35413  483 
\item @{command "no_type_notation"} is similar to @{command 
484 
"type_notation"}, but removes the specified syntax annotation from 

485 
the present context. 

486 

28762  487 
\item @{command "notation"}~@{text "c (mx)"} associates mixfix 
35413  488 
syntax with an existing constant or fixed variable. The type 
489 
declaration of the given entity is retrieved from the context. 

46282  490 

28762  491 
\item @{command "no_notation"} is similar to @{command "notation"}, 
492 
but removes the specified syntax annotation from the present 

493 
context. 

494 

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

495 
\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

496 
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

497 

28762  498 
\end{description} 
35413  499 

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

500 
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

501 
@{command "no_syntax"} (\secref{sec:syntrans}) 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

502 
to the syntax tables of a global theory. 
28762  503 
*} 
504 

28778  505 

506 
section {* The Pure syntax \label{sec:puresyntax} *} 

28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

507 

46282  508 
subsection {* Lexical matters \label{sec:innerlex} *} 
509 

510 
text {* The inner lexical syntax vaguely resembles the outer one 

511 
(\secref{sec:outerlex}), but some details are different. There are 

512 
two main categories of inner syntax tokens: 

513 

514 
\begin{enumerate} 

515 

516 
\item \emph{delimiters}  the literal tokens occurring in 

517 
productions of the given priority grammar (cf.\ 

518 
\secref{sec:prioritygrammar}); 

519 

520 
\item \emph{named tokens}  various categories of identifiers etc. 

521 

522 
\end{enumerate} 

523 

524 
Delimiters override named tokens and may thus render certain 

525 
identifiers inaccessible. Sometimes the logical context admits 

526 
alternative ways to refer to the same entity, potentially via 

527 
qualified names. 

528 

529 
\medskip The categories for named tokens are defined once and for 

530 
all as follows, reusing some categories of the outer token syntax 

531 
(\secref{sec:outerlex}). 

532 

533 
\begin{center} 

534 
\begin{supertabular}{rcl} 

535 
@{syntax_def (inner) id} & = & @{syntax_ref ident} \\ 

536 
@{syntax_def (inner) longid} & = & @{syntax_ref longident} \\ 

537 
@{syntax_def (inner) var} & = & @{syntax_ref var} \\ 

538 
@{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\ 

539 
@{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\ 

540 
@{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text "  "}@{verbatim ""}@{syntax_ref nat} \\ 

541 
@{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  "}@{verbatim ""}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ 

542 
@{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  "}@{verbatim "#"}@{syntax_ref nat} \\ 

543 

544 
@{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\ 

545 
\end{supertabular} 

546 
\end{center} 

547 

548 
The token categories @{syntax (inner) num_token}, @{syntax (inner) 

549 
float_token}, @{syntax (inner) xnum_token}, and @{syntax (inner) 

550 
xstr} are not used in Pure. Objectlogics may implement numerals 

551 
and string constants by adding appropriate syntax declarations, 

552 
together with some translation functions (e.g.\ see Isabelle/HOL). 

553 

554 
The derived categories @{syntax_def (inner) num_const}, @{syntax_def 

555 
(inner) float_const}, and @{syntax_def (inner) num_const} provide 

556 
robust access to the respective tokens: the syntax tree holds a 

557 
syntactic constant instead of a free variable. 

558 
*} 

559 

560 

28777  561 
subsection {* Priority grammars \label{sec:prioritygrammar} *} 
28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

562 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

563 
text {* A contextfree grammar consists of a set of \emph{terminal 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

564 
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

565 
\emph{productions}. Productions have the form @{text "A = \<gamma>"}, 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

566 
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

567 
terminals and nonterminals. One designated nonterminal is called 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

568 
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

569 
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

570 
root symbol by applying productions as rewrite rules. 
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 
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

573 
grammar}. Each nonterminal is decorated by an integer priority: 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

574 
@{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

575 
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

576 
priority grammar can be translated into a normal contextfree 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

577 
grammar by introducing new nonterminals and productions. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

578 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

579 
\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

580 
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

581 
\<alpha>} and @{text \<beta>} denote strings of terminal or nonterminal symbols. 
28774  582 
Then @{text "\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>"} holds if and only if @{text G} 
583 
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

584 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

585 
\medskip The following grammar for arithmetic expressions 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

586 
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

587 
enforced by priorities. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

588 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

589 
\begin{center} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

590 
\begin{tabular}{rclr} 
28774  591 
@{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

592 
@{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

593 
@{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

594 
@{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

595 
@{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

596 
\end{tabular} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

597 
\end{center} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

598 
The choice of priorities determines that @{verbatim ""} binds 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

599 
tighter than @{verbatim "*"}, which binds tighter than @{verbatim 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

600 
"+"}. Furthermore @{verbatim "+"} associates to the left and 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

601 
@{verbatim "*"} to the right. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

602 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

603 
\medskip For clarity, grammars obey these conventions: 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

604 
\begin{itemize} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

605 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

606 
\item All priorities must lie between 0 and 1000. 
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 Priority 0 on the righthand side and priority 1000 on the 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

609 
lefthand side may be omitted. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

610 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

611 
\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

612 
(p)"}, i.e.\ the priority of the lefthand side actually appears in 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

613 
a column on the far right. 
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 
\item Alternatives are separated by @{text ""}. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

616 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

617 
\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

618 
but obvious way. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

619 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

620 
\end{itemize} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

621 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

622 
Using these conventions, the example grammar specification above 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

623 
takes the form: 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

624 
\begin{center} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

625 
\begin{tabular}{rclc} 
28774  626 
@{text A} & @{text "="} & @{verbatim "("} @{text A} @{verbatim ")"} \\ 
627 
& @{text ""} & @{verbatim 0} & \qquad\qquad \\ 

28769
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

628 
& @{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

629 
& @{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

630 
& @{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

631 
\end{tabular} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

632 
\end{center} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

633 
*} 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

634 

8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

635 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

636 
subsection {* The Pure grammar *} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

637 

46287  638 
text {* The priority grammar of the @{text "Pure"} theory is defined 
639 
approximately like this: 

28774  640 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

641 
\begin{center} 
28773  642 
\begin{supertabular}{rclr} 
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

643 

28778  644 
@{syntax_def (inner) any} & = & @{text "prop  logic"} \\\\ 
28772  645 

28778  646 
@{syntax_def (inner) prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\ 
28772  647 
& @{text ""} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ 
648 
& @{text ""} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ 

28773  649 
& @{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

650 
& @{text ""} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ 
28772  651 
& @{text ""} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28773  652 
& @{text ""} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28772  653 
& @{text ""} & @{verbatim "["} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28773  654 
& @{text ""} & @{text "\<lbrakk>"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{text "\<rbrakk>"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28772  655 
& @{text ""} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ 
28773  656 
& @{text ""} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ 
657 
& @{text ""} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\ 

658 
& @{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

659 
& @{text ""} & @{verbatim TERM} @{text logic} \\ 
28773  660 
& @{text ""} & @{verbatim PROP} @{text aprop} \\\\ 
28772  661 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28779
diff
changeset

662 
@{syntax_def (inner) aprop} & = & @{verbatim "("} @{text aprop} @{verbatim ")"} \\ 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28779
diff
changeset

663 
& @{text ""} & @{text "id  longid  var  "}@{verbatim "_"}@{text "  "}@{verbatim "..."} \\ 
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)"} \\\\ 
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

667 

28778  668 
@{syntax_def (inner) logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\ 
28772  669 
& @{text ""} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ 
28773  670 
& @{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

671 
& @{text ""} & @{verbatim CONST} @{text "id  "}@{verbatim CONST} @{text "longid"} \\ 
46287  672 
& @{text ""} & @{verbatim XCONST} @{text "id  "}@{verbatim XCONST} @{text "longid"} \\ 
28773  673 
& @{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  674 
& @{text ""} & @{text "\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} \\ 
28772  675 
& @{text ""} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ 
28773  676 
& @{text ""} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ 
46287  677 
& @{text ""} & @{verbatim op} @{verbatim "=="}@{text "  "}@{verbatim op} @{text "\<equiv>"}@{text "  "}@{verbatim op} @{verbatim "&&&"} \\ 
678 
& @{text ""} & @{verbatim op} @{verbatim "==>"}@{text "  "}@{verbatim op} @{text "\<Longrightarrow>"} \\ 

28772  679 
& @{text ""} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\ 
680 

28778  681 
@{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text "  id  "}@{verbatim "_"} \\ 
28773  682 
& @{text ""} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\ 
683 
& @{text ""} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\ 

28772  684 

46287  685 
@{syntax_def (inner) index} & = & @{verbatim "\<^bsub>"} @{text "logic\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "\<^esub>"}@{text "   \<index>"} \\\\ 
686 

28778  687 
@{syntax_def (inner) idts} & = & @{text "idt  idt\<^sup>(\<^sup>1\<^sup>) idts"} & @{text "(0)"} \\\\ 
28772  688 

28778  689 
@{syntax_def (inner) pttrn} & = & @{text idt} \\\\ 
28772  690 

28778  691 
@{syntax_def (inner) pttrns} & = & @{text "pttrn  pttrn\<^sup>(\<^sup>1\<^sup>) pttrns"} & @{text "(0)"} \\\\ 
28774  692 

28778  693 
@{syntax_def (inner) type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\ 
28773  694 
& @{text ""} & @{text "tid  tvar  "}@{verbatim "_"} \\ 
695 
& @{text ""} & @{text "tid"} @{verbatim "::"} @{text "sort  tvar "}@{verbatim "::"} @{text "sort  "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\ 

46287  696 
& @{text ""} & @{text "type_name  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) type_name"} \\ 
697 
& @{text ""} & @{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text type_name} \\ 

28772  698 
& @{text ""} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\ 
28773  699 
& @{text ""} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\ 
700 
& @{text ""} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\ 

46287  701 
& @{text ""} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\ 
702 
@{syntax_def (inner) type_name} & = & @{text "id  longid"} \\\\ 

28772  703 

46287  704 
@{syntax_def (inner) sort} & = & @{syntax class_name}~@{text "  "}@{verbatim "{}"} \\ 
705 
& @{text ""} & @{verbatim "{"} @{syntax class_name} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{syntax class_name} @{verbatim "}"} \\ 

706 
@{syntax_def (inner) class_name} & = & @{text "id  longid"} \\ 

28773  707 
\end{supertabular} 
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

708 
\end{center} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

709 

28774  710 
\medskip Here literal terminals are printed @{verbatim "verbatim"}; 
711 
see also \secref{sec:innerlex} for further token categories of the 

712 
inner syntax. The meaning of the nonterminals defined by the above 

713 
grammar is as follows: 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

714 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

715 
\begin{description} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

716 

28778  717 
\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

718 

28778  719 
\item @{syntax_ref (inner) prop} denotes metalevel propositions, 
720 
which are terms of type @{typ prop}. The syntax of such formulae of 

721 
the metalogic is carefully distinguished from usual conventions for 

722 
objectlogics. In particular, plain @{text "\<lambda>"}term notation is 

723 
\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

724 

28778  725 
\item @{syntax_ref (inner) aprop} denotes atomic propositions, which 
726 
are embedded into regular @{syntax (inner) prop} by means of an 

727 
explicit @{verbatim PROP} token. 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

728 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

729 
Terms of type @{typ prop} with nonconstant head, e.g.\ a plain 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

730 
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

731 
prop} are expected to provide their own concrete syntax; otherwise 
28778  732 
the printed version will appear like @{syntax (inner) logic} and 
733 
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

734 

28778  735 
\item @{syntax_ref (inner) logic} denotes arbitrary terms of a 
736 
logical type, excluding type @{typ prop}. This is the main 

737 
syntactic category of objectlogic entities, covering plain @{text 

738 
\<lambda>}term notation (variables, abstraction, application), plus 

739 
anything defined by the user. 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

740 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

741 
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

742 
(excluding @{typ prop}) are \emph{collapsed} to this single category 
28778  743 
of @{syntax (inner) logic}. 
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

744 

46287  745 
\item @{syntax_ref (inner) index} denotes an optional index term for 
746 
indexed syntax. If omitted, it refers to the first @{keyword 

747 
"structure"} variable in the context. The special dummy ``@{text 

748 
"\<index>"}'' serves as pattern variable in mixfix annotations that 

749 
introduce indexed notation. 

750 

28778  751 
\item @{syntax_ref (inner) idt} denotes identifiers, possibly 
752 
constrained by types. 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

753 

28778  754 
\item @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref 
755 
(inner) idt}. This is the most basic category for variables in 

756 
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

757 

28778  758 
\item @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns} 
759 
denote patterns for abstraction, cases bindings etc. In Pure, these 

760 
categories start as a merely copy of @{syntax (inner) idt} and 

761 
@{syntax (inner) idts}, respectively. Objectlogics may add 

762 
additional productions for binding forms. 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

763 

28778  764 
\item @{syntax_ref (inner) type} denotes types of the metalogic. 
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

765 

28778  766 
\item @{syntax_ref (inner) sort} denotes metalevel sorts. 
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

767 

93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

768 
\end{description} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

769 

28774  770 
Here are some further explanations of certain syntax features. 
28773  771 

772 
\begin{itemize} 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

773 

28778  774 
\item In @{syntax (inner) idts}, note that @{text "x :: nat y"} is 
775 
parsed as @{text "x :: (nat y)"}, treating @{text y} like a type 

776 
constructor applied to @{text nat}. To avoid this interpretation, 

777 
write @{text "(x :: nat) y"} with explicit parentheses. 

28773  778 

779 
\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

780 
(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

781 
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

782 
sequence of identifiers. 
28773  783 

784 
\item Type constraints for terms bind very weakly. For example, 

785 
@{text "x < y :: nat"} is normally parsed as @{text "(x < y) :: 

786 
nat"}, unless @{text "<"} has a very low priority, in which case the 

787 
input is likely to be ambiguous. The correct form is @{text "x < (y 

788 
:: nat)"}. 

789 

790 
\item Constraints may be either written with two literal colons 

791 
``@{verbatim "::"}'' or the doublecolon symbol @{verbatim "\<Colon>"}, 

28774  792 
which actually looks exactly the same in some {\LaTeX} styles. 
28773  793 

28774  794 
\item Dummy variables (written as underscore) may occur in different 
795 
roles. 

28773  796 

797 
\begin{description} 

798 

28774  799 
\item A type ``@{text "_"}'' or ``@{text "_ :: sort"}'' acts like an 
800 
anonymous inference parameter, which is filledin according to the 

801 
most general type produced by the typechecking phase. 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

802 

28774  803 
\item A bound ``@{text "_"}'' refers to a vacuous abstraction, where 
804 
the body does not refer to the binding introduced here. As in the 

805 
term @{term "\<lambda>x _. x"}, which is @{text "\<alpha>"}equivalent to @{text 

806 
"\<lambda>x y. x"}. 

28773  807 

28774  808 
\item A free ``@{text "_"}'' refers to an implicit outer binding. 
809 
Higher definitional packages usually allow forms like @{text "f x _ 

810 
= x"}. 

28773  811 

28774  812 
\item A schematic ``@{text "_"}'' (within a term pattern, see 
813 
\secref{sec:termdecls}) refers to an anonymous variable that is 

814 
implicitly abstracted over its context of locally bound variables. 

815 
For example, this allows pattern matching of @{text "{x. f x = g 

816 
x}"} against @{text "{x. _ = _}"}, or even @{text "{_. _ = _}"} by 

817 
using both bound and schematic dummies. 

28773  818 

819 
\end{description} 

820 

28774  821 
\item The three literal dots ``@{verbatim "..."}'' may be also 
822 
written as ellipsis symbol @{verbatim "\<dots>"}. In both cases this 

823 
refers to a special schematic variable, which is bound in the 

824 
context. This special term abbreviation works nicely with 

825 
calculational reasoning (\secref{sec:calculation}). 

826 

46287  827 
\item @{verbatim CONST} ensures that the given identifier is treated 
828 
as constant term, and passed through the parse tree in fully 

829 
internalized form. This is particularly relevant for translation 

830 
rules (\secref{sec:syntrans}), notably on the RHS. 

831 

832 
\item @{verbatim XCONST} is similar to @{verbatim CONST}, but 

833 
retains the constant name as given. This is only relevant to 

834 
translation rules (\secref{sec:syntrans}), notably on the LHS. 

835 

28773  836 
\end{itemize} 
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

837 
*} 
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

838 

28777  839 

46282  840 
subsection {* Inspecting the syntax *} 
28777  841 

46282  842 
text {* 
843 
\begin{matharray}{rcl} 

844 
@{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 

845 
\end{matharray} 

28777  846 

46282  847 
\begin{description} 
848 

849 
\item @{command "print_syntax"} prints the inner syntax of the 

850 
current context. The output can be quite large; the most important 

851 
sections are explained below. 

28777  852 

46282  853 
\begin{description} 
28777  854 

46282  855 
\item @{text "lexicon"} lists the delimiters of the inner token 
856 
language; see \secref{sec:innerlex}. 

28777  857 

46282  858 
\item @{text "prods"} lists the productions of the underlying 
859 
priority grammar; see \secref{sec:prioritygrammar}. 

28777  860 

46282  861 
The nonterminal @{text "A\<^sup>(\<^sup>p\<^sup>)"} is rendered in plain text as @{text 
862 
"A[p]"}; delimiters are quoted. Many productions have an extra 

863 
@{text "\<dots> => name"}. These names later become the heads of parse 

864 
trees; they also guide the pretty printer. 

28777  865 

46282  866 
Productions without such parse tree names are called \emph{copy 
867 
productions}. Their righthand side must have exactly one 

868 
nonterminal symbol (or named token). The parser does not create a 

869 
new parse tree node for copy productions, but simply returns the 

870 
parse tree of the righthand symbol. 

871 

872 
If the righthand side of a copy production consists of a single 

873 
nonterminal without any delimiters, then it is called a \emph{chain 

874 
production}. Chain productions act as abbreviations: conceptually, 

875 
they are removed from the grammar by adding new productions. 

876 
Priority information attached to chain productions is ignored; only 

877 
the dummy value @{text "1"} is displayed. 

878 

879 
\item @{text "print modes"} lists the alternative print modes 

880 
provided by this grammar; see \secref{sec:printmodes}. 

28777  881 

46282  882 
\item @{text "parse_rules"} and @{text "print_rules"} relate to 
883 
syntax translations (macros); see \secref{sec:syntrans}. 

884 

885 
\item @{text "parse_ast_translation"} and @{text 

886 
"print_ast_translation"} list sets of constants that invoke 

887 
translation functions for abstract syntax trees, which are only 

888 
required in very special situations; see \secref{sec:trfuns}. 

28777  889 

46282  890 
\item @{text "parse_translation"} and @{text "print_translation"} 
891 
list the sets of constants that invoke regular translation 

892 
functions; see \secref{sec:trfuns}. 

29157  893 

46282  894 
\end{description} 
895 

896 
\end{description} 

28777  897 
*} 
28774  898 

28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

899 

46282  900 
section {* Raw syntax and translations \label{sec:syntrans} *} 
28762  901 

902 
text {* 

903 
\begin{matharray}{rcl} 

41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
40879
diff
changeset

904 
@{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\ 
28762  905 
@{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\ 
906 
@{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\ 

907 
@{command_def "translations"} & : & @{text "theory \<rightarrow> theory"} \\ 

908 
@{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\ 

909 
\end{matharray} 

910 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

911 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

912 
@@{command nonterminal} (@{syntax name} + @'and') 
28762  913 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

914 
(@@{command syntax}  @@{command no_syntax}) @{syntax mode}? (@{syntax constdecl} +) 
28762  915 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

916 
(@@{command translations}  @@{command no_translations}) 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

917 
(transpat ('=='  '=>'  '<='  '\<rightleftharpoons>'  '\<rightharpoonup>'  '\<leftharpoondown>') transpat +) 
28762  918 
; 
919 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

920 
mode: ('(' ( @{syntax name}  @'output'  @{syntax name} @'output' ) ')') 
28762  921 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

922 
transpat: ('(' @{syntax nameref} ')')? @{syntax string} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

923 
"} 
28762  924 

925 
\begin{description} 

46282  926 

41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
40879
diff
changeset

927 
\item @{command "nonterminal"}~@{text c} declares a type 
28762  928 
constructor @{text c} (without arguments) to act as purely syntactic 
929 
type: a nonterminal symbol of the inner syntax. 

930 

931 
\item @{command "syntax"}~@{text "(mode) decls"} is similar to 

932 
@{command "consts"}~@{text decls}, except that the actual logical 

933 
signature extension is omitted. Thus the context free grammar of 

934 
Isabelle's inner syntax may be augmented in arbitrary ways, 

935 
independently of the logic. The @{text mode} argument refers to the 

936 
print mode that the grammar rules belong; unless the @{keyword_ref 

937 
"output"} indicator is given, all productions are added both to the 

938 
input and output grammar. 

46282  939 

28762  940 
\item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar 
941 
declarations (and translations) resulting from @{text decls}, which 

942 
are interpreted in the same manner as for @{command "syntax"} above. 

46282  943 

28762  944 
\item @{command "translations"}~@{text rules} specifies syntactic 
945 
translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}), 

946 
parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}). 

947 
Translation patterns may be prefixed by the syntactic category to be 

948 
used for parsing; the default is @{text logic}. 

46282  949 

28762  950 
\item @{command "no_translations"}~@{text rules} removes syntactic 
951 
translation rules, which are interpreted in the same manner as for 

952 
@{command "translations"} above. 

953 

954 
\end{description} 

955 
*} 

956 

957 

28779
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

958 
section {* Syntax translation functions \label{sec:trfuns} *} 
28762  959 

960 
text {* 

961 
\begin{matharray}{rcl} 

962 
@{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\ 

963 
@{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\ 

964 
@{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\ 

965 
@{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\ 

966 
@{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\ 

967 
\end{matharray} 

968 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

969 
@{rail " 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

970 
( @@{command parse_ast_translation}  @@{command parse_translation}  
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

971 
@@{command print_translation}  @@{command typed_print_translation}  
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

972 
@@{command print_ast_translation}) ('(' @'advanced' ')')? @{syntax text} 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

973 
"} 
28762  974 

975 
Syntax translation functions written in ML admit almost arbitrary 

976 
manipulations of Isabelle's inner syntax. Any of the above commands 

42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

977 
have a single @{syntax text} argument that refers to an ML 
28762  978 
expression of appropriate type, which are as follows by default: 
979 

980 
%FIXME proper antiquotations 

981 
\begin{ttbox} 

982 
val parse_ast_translation : (string * (ast list > ast)) list 

983 
val parse_translation : (string * (term list > term)) list 

984 
val print_translation : (string * (term list > term)) list 

42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
41229
diff
changeset

985 
val typed_print_translation : (string * (typ > term list > term)) list 
28762  986 
val print_ast_translation : (string * (ast list > ast)) list 
987 
\end{ttbox} 

988 

989 
If the @{text "(advanced)"} option is given, the corresponding 

990 
translation functions may depend on the current theory or proof 

991 
context. This allows to implement advanced syntax mechanisms, as 

992 
translations functions may refer to specific theory declarations or 

993 
auxiliary proof data. 

994 

30397  995 
See also \cite{isabelleref} for more information on the general 
996 
concept of syntax transformations in Isabelle. 

28762  997 

998 
%FIXME proper antiquotations 

999 
\begin{ttbox} 

1000 
val parse_ast_translation: 

1001 
(string * (Proof.context > ast list > ast)) list 

1002 
val parse_translation: 

1003 
(string * (Proof.context > term list > term)) list 

1004 
val print_translation: 

1005 
(string * (Proof.context > term list > term)) list 

1006 
val typed_print_translation: 

42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
41229
diff
changeset

1007 
(string * (Proof.context > typ > term list > term)) list 
28762  1008 
val print_ast_translation: 
1009 
(string * (Proof.context > ast list > ast)) list 

1010 
\end{ttbox} 

1011 
*} 

1012 

1013 
end 