author  wenzelm 
Tue, 07 Feb 2012 18:56:40 +0100  
changeset 46294  f9a1cd2599dd 
parent 46293  f248b5f2783a 
child 46483  10a9c31a22b4 
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 
46290  338 
theorem statements, locale and class specifications also admit 
339 
mixfix annotations in a fairly uniform manner. A mixfix annotation 

340 
describes describes the concrete syntax, the translation to abstract 

341 
syntax, and the pretty printing. Special case annotations provide a 

342 
simple means of specifying infix operators and binders. 

343 

344 
Isabelle mixfix syntax is inspired by {\OBJ} \cite{OBJ}. It allows 

345 
to specify any contextfree priority grammar, which is more general 

346 
than the fixity declarations of ML and Prolog. 

28762  347 

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

348 
@{rail " 
46289  349 
@{syntax_def mixfix}: '(' mfix ')' 
28762  350 
; 
46289  351 
@{syntax_def struct_mixfix}: '(' ( mfix  @'structure' ) ')' 
28762  352 
; 
353 

46290  354 
mfix: @{syntax template} prios? @{syntax nat}?  
355 
(@'infix'  @'infixl'  @'infixr') @{syntax template} @{syntax nat}  

356 
@'binder' @{syntax template} prios? @{syntax nat} 

357 
; 

358 
template: string 

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

360 
prios: '[' (@{syntax nat} + ',') ']' 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

361 
"} 
28762  362 

46290  363 
The string given as @{text template} may include literal text, 
364 
spacing, blocks, and arguments (denoted by ``@{text _}''); the 

365 
special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') 

366 
represents an index argument that specifies an implicit structure 

367 
reference (see also \secref{sec:locale}). Infix and binder 

368 
declarations provide common abbreviations for particular mixfix 

369 
declarations. So in practice, mixfix templates mostly degenerate to 

370 
literal text for concrete syntax, such as ``@{verbatim "++"}'' for 

371 
an infix symbol. 

372 
*} 

28762  373 

46290  374 

375 
subsection {* The general mixfix form *} 

376 

377 
text {* In full generality, mixfix declarations work as follows. 

378 
Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is annotated by 

379 
@{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text "mixfix"} is a string 

380 
@{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of delimiters that surround 

381 
argument positions as indicated by underscores. 

28762  382 

383 
Altogether this determines a production for a contextfree priority 

384 
grammar, where for each argument @{text "i"} the syntactic category 

46292  385 
is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and the 
386 
result category is determined from @{text "\<tau>"} (with priority @{text 

387 
"p"}). Priority specifications are optional, with default 0 for 

388 
arguments and 1000 for the result.\footnote{Omitting priorities is 

389 
prone to syntactic ambiguities unless the delimiter tokens determine 

390 
fully bracketed notation, as in @{text "if _ then _ else _ fi"}.} 

28762  391 

392 
Since @{text "\<tau>"} may be again a function type, the constant 

393 
type scheme may have more argument positions than the mixfix 

394 
pattern. Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for 

395 
@{text "m > n"} works by attaching concrete notation only to the 

396 
innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"} 

397 
instead. If a term has fewer arguments than specified in the mixfix 

398 
template, the concrete syntax is ignored. 

399 

400 
\medskip A mixfix template may also contain additional directives 

401 
for pretty printing, notably spaces, blocks, and breaks. The 

402 
general template format is a sequence over any of the following 

403 
entities. 

404 

28778  405 
\begin{description} 
28762  406 

28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

407 
\item @{text "d"} is a delimiter, namely a nonempty sequence of 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

408 
characters other than the following special characters: 
28762  409 

28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

410 
\smallskip 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

411 
\begin{tabular}{ll} 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

412 
@{verbatim "'"} & single quote \\ 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

413 
@{verbatim "_"} & underscore \\ 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

414 
@{text "\<index>"} & index symbol \\ 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

415 
@{verbatim "("} & open parenthesis \\ 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

416 
@{verbatim ")"} & close parenthesis \\ 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

417 
@{verbatim "/"} & slash \\ 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

418 
\end{tabular} 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

419 
\medskip 
28762  420 

28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

421 
\item @{verbatim "'"} escapes the special meaning of these 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

422 
metacharacters, producing a literal version of the following 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

423 
character, unless that is a blank. 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

424 

4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

425 
A single quote followed by a blank separates delimiters, without 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

426 
affecting printing, but input tokens may have additional white space 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

427 
here. 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

428 

4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

429 
\item @{verbatim "_"} is an argument position, which stands for a 
28762  430 
certain syntactic category in the underlying grammar. 
431 

28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

432 
\item @{text "\<index>"} is an indexed argument position; this is the place 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

433 
where implicit structure arguments can be attached. 
28762  434 

28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

435 
\item @{text "s"} is a nonempty sequence of spaces for printing. 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

436 
This and the following specifications do not affect parsing at all. 
28762  437 

28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

438 
\item @{verbatim "("}@{text n} opens a pretty printing block. The 
28762  439 
optional number specifies how much indentation to add when a line 
440 
break occurs within the block. If the parenthesis is not followed 

441 
by digits, the indentation defaults to 0. A block specified via 

28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

442 
@{verbatim "(00"} is unbreakable. 
28762  443 

28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

444 
\item @{verbatim ")"} closes a pretty printing block. 
28762  445 

28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

446 
\item @{verbatim "//"} forces a line break. 
28762  447 

28771
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

448 
\item @{verbatim "/"}@{text s} allows a line break. Here @{text s} 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

449 
stands for the string of spaces (zero or more) right after the 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

450 
slash. These spaces are printed if the break is \emph{not} taken. 
28762  451 

28778  452 
\end{description} 
28762  453 

454 
The general idea of pretty printing with blocks and breaks is also 

46286  455 
described in \cite{paulsonml2}; it goes back to \cite{Oppen:1980}. 
28762  456 
*} 
457 

458 

46290  459 
subsection {* Infixes *} 
460 

461 
text {* Infix operators are specified by convenient short forms that 

462 
abbreviate general mixfix annotations as follows: 

463 

464 
\begin{center} 

465 
\begin{tabular}{lll} 

466 

46292  467 
@{verbatim "("}@{keyword_def "infix"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"} 
46290  468 
& @{text "\<mapsto>"} & 
469 
@{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\ 

46292  470 
@{verbatim "("}@{keyword_def "infixl"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"} 
46290  471 
& @{text "\<mapsto>"} & 
472 
@{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\ 

46292  473 
@{verbatim "("}@{keyword_def "infixr"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"} 
46290  474 
& @{text "\<mapsto>"} & 
475 
@{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\ 

476 

477 
\end{tabular} 

478 
\end{center} 

479 

46292  480 
The mixfix template @{verbatim "\"(_ "}@{text sy}@{verbatim "/ _)\""} 
481 
specifies two argument positions; the delimiter is preceded by a 

482 
space and followed by a space or line break; the entire phrase is a 

483 
pretty printing block. 

46290  484 

485 
The alternative notation @{verbatim "op"}~@{text sy} is introduced 

486 
in addition. Thus any infix operator may be written in prefix form 

487 
(as in ML), independently of the number of arguments in the term. 

488 
*} 

489 

490 

491 
subsection {* Binders *} 

492 

493 
text {* A \emph{binder} is a variablebinding construct such as a 

494 
quantifier. The idea to formalize @{text "\<forall>x. b"} as @{text "All 

495 
(\<lambda>x. b)"} for @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} already goes back 

496 
to \cite{church40}. Isabelle declarations of certain higherorder 

46292  497 
operators may be annotated with @{keyword_def "binder"} annotations 
498 
as follows: 

46290  499 

500 
\begin{center} 

501 
@{text "c :: "}@{verbatim "\""}@{text "(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\" ("}@{keyword "binder"}@{verbatim " \""}@{text "sy"}@{verbatim "\" ["}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"} 

502 
\end{center} 

503 

504 
This introduces concrete binder syntax @{text "sy x. b"}, where 

505 
@{text x} is a bound variable of type @{text "\<tau>\<^sub>1"}, the body @{text 

506 
b} has type @{text "\<tau>\<^sub>2"} and the whole term has type @{text "\<tau>\<^sub>3"}. 

507 
The optional integer @{text p} specifies the syntactic priority of 

508 
the body; the default is @{text "q"}, which is also the priority of 

509 
the whole construct. 

510 

511 
Internally, the binder syntax is expanded to something like this: 

512 
\begin{center} 

513 
@{text "c_binder :: "}@{verbatim "\""}@{text "idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\" (\"(3"}@{text sy}@{verbatim "_./ _)\" [0, "}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"} 

514 
\end{center} 

515 

516 
Here @{syntax (inner) idts} is the nonterminal symbol for a list of 

517 
identifiers with optional type constraints (see also 

518 
\secref{sec:puregrammar}). The mixfix template @{verbatim 

519 
"\"(3"}@{text sy}@{verbatim "_./ _)\""} defines argument positions 

520 
for the bound identifiers and the body, separated by a dot with 

521 
optional line break; the entire phrase is a pretty printing block of 

522 
indentation level 3. Note that there is no extra space after @{text 

523 
"sy"}, so it needs to be included user specification if the binder 

524 
syntax ends with a token that may be continued by an identifier 

525 
token at the start of @{syntax (inner) idts}. 

526 

527 
Furthermore, a syntax translation to transforms @{text "c_binder x\<^sub>1 

528 
\<dots> x\<^sub>n b"} into iterated application @{text "c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)"}. 

529 
This works in both directions, for parsing and printing. *} 

530 

531 

46282  532 
section {* Explicit notation \label{sec:notation} *} 
28762  533 

534 
text {* 

535 
\begin{matharray}{rcll} 

35413  536 
@{command_def "type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
537 
@{command_def "no_type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 

28762  538 
@{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
539 
@{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

540 
@{command_def "write"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\ 
28762  541 
\end{matharray} 
542 

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

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

546 
modified later on by declarations for explicit notation. This 

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

548 
entities within the current context. 

549 

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

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

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

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

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

558 
"} 
28762  559 

560 
\begin{description} 

561 

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

564 
constructor is retrieved from the context. 

46282  565 

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

568 
the present context. 

569 

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

46282  573 

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

576 
context. 

577 

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

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

579 
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

580 

28762  581 
\end{description} 
582 
*} 

583 

28778  584 

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

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

586 

46282  587 
subsection {* Lexical matters \label{sec:innerlex} *} 
588 

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

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

591 
two main categories of inner syntax tokens: 

592 

593 
\begin{enumerate} 

594 

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

596 
productions of the given priority grammar (cf.\ 

597 
\secref{sec:prioritygrammar}); 

598 

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

600 

601 
\end{enumerate} 

602 

603 
Delimiters override named tokens and may thus render certain 

604 
identifiers inaccessible. Sometimes the logical context admits 

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

606 
qualified names. 

607 

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

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

610 
(\secref{sec:outerlex}). 

611 

612 
\begin{center} 

613 
\begin{supertabular}{rcl} 

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

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

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

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

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

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

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

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

622 

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

624 
\end{supertabular} 

625 
\end{center} 

626 

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

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

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

630 
and string constants by adding appropriate syntax declarations, 

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

632 

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

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

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

636 
syntactic constant instead of a free variable. 

637 
*} 

638 

639 

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

641 

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

642 
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

643 
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

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

645 
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

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

647 
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

648 
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

649 
root symbol by applying productions as rewrite rules. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

650 

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

651 
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

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

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

654 
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

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

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

657 

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

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

659 
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

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

663 

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

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

665 
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

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

667 

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

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

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

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

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

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

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

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

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

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

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

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

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

681 

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

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

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

684 

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

685 
\item All priorities must lie between 0 and 1000. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

686 

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

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

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

689 

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

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

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

692 
a column on the far right. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

693 

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

694 
\item Alternatives are separated by @{text ""}. 
8fc228f21861
added section "Priority grammars" (variant from old ref manual);
wenzelm
parents:
28767
diff
changeset

695 

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

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

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

698 

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

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

700 

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

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

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

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

704 
\begin{tabular}{rclc} 
28774  705 
@{text A} & @{text "="} & @{verbatim "("} @{text A} @{verbatim ")"} \\ 
706 
& @{text ""} & @{verbatim 0} & \qquad\qquad \\ 

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

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

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

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

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

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

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

713 

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

714 

46290  715 
subsection {* The Pure grammar \label{sec:puregrammar} *} 
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

716 

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

28774  719 

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

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

722 

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

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

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

729 
& @{text ""} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ 
28772  730 
& @{text ""} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28773  731 
& @{text ""} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28772  732 
& @{text ""} & @{verbatim "["} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28773  733 
& @{text ""} & @{text "\<lbrakk>"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{text "\<rbrakk>"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28772  734 
& @{text ""} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ 
28773  735 
& @{text ""} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ 
736 
& @{text ""} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\ 

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

738 
& @{text ""} & @{verbatim TERM} @{text logic} \\ 
28773  739 
& @{text ""} & @{verbatim PROP} @{text aprop} \\\\ 
28772  740 

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

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

742 
& @{text ""} & @{text "id  longid  var  "}@{verbatim "_"}@{text "  "}@{verbatim "..."} \\ 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28779
diff
changeset

743 
& @{text ""} & @{verbatim CONST} @{text "id  "}@{verbatim CONST} @{text "longid"} \\ 
46287  744 
& @{text ""} & @{verbatim XCONST} @{text "id  "}@{verbatim XCONST} @{text "longid"} \\ 
28773  745 
& @{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

746 

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

750 
& @{text ""} & @{verbatim CONST} @{text "id  "}@{verbatim CONST} @{text "longid"} \\ 
46287  751 
& @{text ""} & @{verbatim XCONST} @{text "id  "}@{verbatim XCONST} @{text "longid"} \\ 
28773  752 
& @{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  753 
& @{text ""} & @{text "\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} \\ 
28772  754 
& @{text ""} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ 
28773  755 
& @{text ""} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ 
46287  756 
& @{text ""} & @{verbatim op} @{verbatim "=="}@{text "  "}@{verbatim op} @{text "\<equiv>"}@{text "  "}@{verbatim op} @{verbatim "&&&"} \\ 
757 
& @{text ""} & @{verbatim op} @{verbatim "==>"}@{text "  "}@{verbatim op} @{text "\<Longrightarrow>"} \\ 

28772  758 
& @{text ""} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\ 
759 

28778  760 
@{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text "  id  "}@{verbatim "_"} \\ 
28773  761 
& @{text ""} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\ 
762 
& @{text ""} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\ 

28772  763 

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

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

28778  768 
@{syntax_def (inner) pttrn} & = & @{text idt} \\\\ 
28772  769 

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

28778  772 
@{syntax_def (inner) type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\ 
28773  773 
& @{text ""} & @{text "tid  tvar  "}@{verbatim "_"} \\ 
774 
& @{text ""} & @{text "tid"} @{verbatim "::"} @{text "sort  tvar "}@{verbatim "::"} @{text "sort  "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\ 

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

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

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

28772  782 

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

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

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

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

788 

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

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

792 
grammar is as follows: 

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

793 

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

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

795 

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

797 

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

800 
the metalogic is carefully distinguished from usual conventions for 

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

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

803 

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

806 
explicit @{verbatim PROP} token. 

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

807 

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

808 
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

809 
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

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

813 

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

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

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

818 
anything defined by the user. 

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

819 

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

820 
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

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

823 

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

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

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

828 
introduce indexed notation. 

829 

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

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

832 

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

835 
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

836 

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

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

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

841 
additional productions for binding forms. 

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

842 

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

844 

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

846 

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

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

848 

28774  849 
Here are some further explanations of certain syntax features. 
28773  850 

851 
\begin{itemize} 

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

852 

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

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

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

28773  857 

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

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

860 
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

861 
sequence of identifiers. 
28773  862 

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

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

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

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

867 
:: nat)"}. 

868 

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

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

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

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

28773  875 

876 
\begin{description} 

877 

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

880 
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

881 

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

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

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

28773  886 

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

889 
= x"}. 

28773  890 

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

893 
implicitly abstracted over its context of locally bound variables. 

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

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

896 
using both bound and schematic dummies. 

28773  897 

898 
\end{description} 

899 

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

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

903 
context. This special term abbreviation works nicely with 

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

905 

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

908 
internalized form. This is particularly relevant for translation 

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

910 

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

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

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

914 

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

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

917 

28777  918 

46282  919 
subsection {* Inspecting the syntax *} 
28777  920 

46282  921 
text {* 
922 
\begin{matharray}{rcl} 

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

924 
\end{matharray} 

28777  925 

46282  926 
\begin{description} 
927 

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

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

930 
sections are explained below. 

28777  931 

46282  932 
\begin{description} 
28777  933 

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

28777  936 

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

28777  939 

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

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

943 
trees; they also guide the pretty printer. 

28777  944 

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

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

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

949 
parse tree of the righthand symbol. 

950 

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

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

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

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

955 
Priority information attached to chain productions is ignored; only 

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

957 

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

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

28777  960 

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

963 

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

965 
"print_ast_translation"} list sets of constants that invoke 

966 
translation functions for abstract syntax trees, which are only 

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

28777  968 

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

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

29157  972 

46282  973 
\end{description} 
974 

975 
\end{description} 

28777  976 
*} 
28774  977 

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

978 

46291  979 
subsection {* Ambiguity of parsed expressions *} 
980 

981 
text {* 

982 
\begin{tabular}{rcll} 

983 
@{attribute_def syntax_ambiguity_level} & : & @{text attribute} & default @{text 1} \\ 

984 
\end{tabular} 

985 

986 
\begin{mldecls} 

987 
@{index_ML Syntax.ambiguity_limit: "int Config.T"} \\ %FIXME attribute 

988 
\end{mldecls} 

989 

990 
Depending on the grammar and the given input, parsing may be 

991 
ambiguous. Isabelle lets the Earley parser enumerate all possible 

992 
parse trees, and then tries to make the best out of the situation. 

993 
Terms that cannot be typechecked are filtered out, which often 

994 
leads to a unique result in the end. Unlike regular type 

995 
reconstruction, which is applied to the whole collection of input 

996 
terms simultaneously, the filtering stage only treats each given 

997 
term in isolation. Filtering is also not attempted for individual 

998 
types or raw ASTs (as required for @{command translations}). 

999 

1000 
Certain warning or error messages are printed, depending on the 

1001 
situation and the given configuration options. Parsing ultimately 

1002 
fails, if multiple results remain after the filtering phase. 

1003 

1004 
\begin{description} 

1005 

1006 
\item @{attribute syntax_ambiguity_level} determines the number of 

1007 
parser results that are tolerated without printing a detailed 

1008 
message. 

1009 

1010 
\item @{ML Syntax.ambiguity_limit} determines the number of 

1011 
resulting parse trees that are shown as part of the printed message 

1012 
in case of an ambiguity. 

1013 

1014 
\end{description} 

1015 
*} 

1016 

1017 

46282  1018 
section {* Raw syntax and translations \label{sec:syntrans} *} 
28762  1019 

1020 
text {* 

1021 
\begin{matharray}{rcl} 

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

1022 
@{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\ 
28762  1023 
@{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\ 
1024 
@{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\ 

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

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

1027 
\end{matharray} 

1028 

46292  1029 
Unlike mixfix notation for existing formal entities 
1030 
(\secref{sec:notation}), raw syntax declarations provide full access 

1031 
to the priority grammar of the inner syntax. This includes 

1032 
additional syntactic categories (via @{command nonterminal}) and 

1033 
freeform grammar productions (via @{command syntax}). Additional 

1034 
syntax translations (or macros, via @{command translations}) are 

1035 
required to turn resulting parse trees into proper representations 

1036 
of formal entities again. 

1037 

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

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

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

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

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

1044 
(transpat ('=='  '=>'  '<='  '\<rightleftharpoons>'  '\<rightharpoonup>'  '\<leftharpoondown>') transpat +) 
28762  1045 
; 
1046 

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

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

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

1050 
"} 
28762  1051 

1052 
\begin{description} 

46282  1053 

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

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

1057 

46292  1058 
\item @{command "syntax"}~@{text "(mode) c :: \<sigma> (mx)"} augments the 
1059 
priority grammar and the pretty printer table for the given print 

1060 
mode (default @{verbatim "\"\""}). An optional keyword @{keyword_ref 

1061 
"output"} means that only the pretty printer table is affected. 

1062 

1063 
Following \secref{sec:mixfix}, the mixfix annotation @{text "mx = 

1064 
template ps q"} together with type @{text "\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} and 

1065 
specify a grammar production. The @{text template} contains 

1066 
delimiter tokens that surround @{text "n"} argument positions 

1067 
(@{verbatim "_"}). The latter correspond to nonterminal symbols 

1068 
@{text "A\<^sub>i"} derived from the argument types @{text "\<tau>\<^sub>i"} as 

1069 
follows: 

1070 
\begin{itemize} 

1071 

1072 
\item @{text "prop"} if @{text "\<tau>\<^sub>i = prop"} 

1073 

1074 
\item @{text "logic"} if @{text "\<tau>\<^sub>i = (\<dots>)\<kappa>"} for logical type 

1075 
constructor @{text "\<kappa> \<noteq> prop"} 

1076 

1077 
\item @{text any} if @{text "\<tau>\<^sub>i = \<alpha>"} for type variables 

1078 

1079 
\item @{text "\<kappa>"} if @{text "\<tau>\<^sub>i = \<kappa>"} for nonterminal @{text "\<kappa>"} 

1080 
(syntactic type constructor) 

1081 

1082 
\end{itemize} 

1083 

1084 
Each @{text "A\<^sub>i"} is decorated by priority @{text "p\<^sub>i"} from the 

1085 
given list @{text "ps"}; misssing priorities default to 0. 

1086 

1087 
The resulting nonterminal of the production is determined similarly 

1088 
from type @{text "\<tau>"}, with priority @{text "q"} and default 1000. 

1089 

1090 
\medskip Parsing via this production produces parse trees @{text 

1091 
"t\<^sub>1, \<dots>, t\<^sub>n"} for the argument slots. The resulting parse tree is 

1092 
composed as @{text "c t\<^sub>1 \<dots> t\<^sub>n"}, by using the syntax constant @{text 

1093 
"c"} of the syntax declaration. 

1094 

1095 
Such syntactic constants are invented on the spot, without formal 

1096 
check wrt.\ existing declarations. It is conventional to use plain 

1097 
identifiers prefixed by a single underscore (e.g.\ @{text 

1098 
"_foobar"}). Names should be chosen with care, to avoid clashes 

1099 
with unrelated syntax declarations. 

1100 

1101 
\medskip The special case of copy production is specified by @{text 

1102 
"c = "}@{verbatim "\"\""} (empty string). It means that the 

1103 
resulting parse tree @{text "t"} is copied directly, without any 

1104 
further decoration. 

46282  1105 

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

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

46282  1109 

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

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

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

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

46282  1115 

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

1118 
@{command "translations"} above. 

1119 

1120 
\end{description} 

46293  1121 

1122 
Raw syntax and translations provides a slightly more lowlevel 

1123 
access to the grammar and the form of resulting parse trees. It is 

1124 
often possible to avoid this untyped macro mechanism, and use 

1125 
typesafe @{command abbreviation} or @{command notation} instead. 

1126 
Some important situations where @{command syntax} and @{command 

1127 
translations} are really need are as follows: 

1128 

1129 
\begin{itemize} 

1130 

1131 
\item Iterated replacement via recursive @{command translations}. 

1132 
For example, consider list enumeration @{term "[a, b, c, d]"} as 

1133 
defined in theory @{theory List} in Isabelle/HOL. 

1134 

1135 
\item Change of binding status of variables: anything beyond the 

1136 
builtin @{keyword "binder"} mixfix annotation requires explicit 

1137 
syntax translations. For example, consider list filter 

1138 
comprehension @{term "[x \<leftarrow> xs . P]"} as defined in theory @{theory 

1139 
List} in Isabelle/HOL. 

1140 

1141 
\end{itemize} 

28762  1142 
*} 
1143 

1144 

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

1145 
section {* Syntax translation functions \label{sec:trfuns} *} 
28762  1146 

1147 
text {* 

1148 
\begin{matharray}{rcl} 

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

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

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

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

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

1154 
\end{matharray} 

1155 

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

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

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

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

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

1160 
"} 
28762  1161 

1162 
Syntax translation functions written in ML admit almost arbitrary 

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

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

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

1167 
%FIXME proper antiquotations 

1168 
\begin{ttbox} 

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

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

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

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

1172 
val typed_print_translation : (string * (typ > term list > term)) list 
28762  1173 
val print_ast_translation : (string * (ast list > ast)) list 
1174 
\end{ttbox} 

1175 

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

1177 
translation functions may depend on the current theory or proof 

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

1179 
translations functions may refer to specific theory declarations or 

1180 
auxiliary proof data. 

1181 

1182 
%FIXME proper antiquotations 

1183 
\begin{ttbox} 

1184 
val parse_ast_translation: 

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

1186 
val parse_translation: 

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

1188 
val print_translation: 

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

1190 
val typed_print_translation: 

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

1191 
(string * (Proof.context > typ > term list > term)) list 
28762  1192 
val print_ast_translation: 
1193 
(string * (Proof.context > ast list > ast)) list 

1194 
\end{ttbox} 

46294  1195 

1196 
\medskip See also the chapter on ``Syntax Transformations'' in old 

1197 
\cite{isabelleref} for further details on translations on parse 

1198 
trees. 

28762  1199 
*} 
1200 

1201 
end 