author  wenzelm 
Mon, 02 May 2011 01:05:50 +0200  
changeset 42596  6c621a9d612a 
parent 42358  b47d41d9f4b5 
child 42651  e3fdb7c96be5 
permissions  rwrr 
28762  1 
theory Inner_Syntax 
2 
imports Main 

3 
begin 

4 

28778  5 
chapter {* Inner syntax  the term language \label{ch:innersyntax} *} 
28762  6 

7 
section {* Printing logical entities *} 

8 

9 
subsection {* Diagnostic commands *} 

10 

11 
text {* 

12 
\begin{matharray}{rcl} 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

13 
@{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
28762  14 
@{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
15 
@{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

16 
@{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
28762  17 
@{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
18 
@{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

19 
@{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ 
28762  20 
\end{matharray} 
21 

22 
These diagnostic commands assist interactive development by printing 

23 
internal logical entities in a humanreadable fashion. 

24 

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

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

26 
@@{command typ} @{syntax modes}? @{syntax type} 
28762  27 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

28 
@@{command term} @{syntax modes}? @{syntax term} 
28762  29 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

30 
@@{command prop} @{syntax modes}? @{syntax prop} 
28762  31 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

32 
@@{command thm} @{syntax modes}? @{syntax thmrefs} 
28762  33 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

34 
( @@{command prf}  @@{command full_prf} ) @{syntax modes}? @{syntax thmrefs}? 
28762  35 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

36 
@@{command pr} @{syntax modes}? @{syntax nat}? 
28762  37 
; 
38 

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

39 
@{syntax_def modes}: '(' (@{syntax name} + ) ')' 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

40 
"} 
28762  41 

42 
\begin{description} 

43 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

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

45 
metalogic according to the current theory or proof context. 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

46 

accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

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

48 
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

49 
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

50 
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

51 
inspecting the current environment of term abbreviations. 
28762  52 

53 
\item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves 

54 
theorems from the current theory or proof context. Note that any 

55 
attributes included in the theorem specifications are applied to a 

56 
temporary context derived from the current theory or proof; the 

57 
result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1, 

58 
\<dots>, a\<^sub>n"} do not have any permanent effect. 

59 

60 
\item @{command "prf"} displays the (compact) proof term of the 

61 
current proof state (if present), or of the given theorems. Note 

62 
that this requires proof terms to be switched on for the current 

63 
object logic (see the ``Proof terms'' section of the Isabelle 

64 
reference manual for information on how to do this). 

65 

66 
\item @{command "full_prf"} is like @{command "prf"}, but displays 

67 
the full proof term, i.e.\ also displays information omitted in the 

68 
compact proof term, which is denoted by ``@{text _}'' placeholders 

69 
there. 

70 

39165  71 
\item @{command "pr"}~@{text "goals"} prints the current proof state 
72 
(if present), including current facts and goals. The optional limit 

73 
arguments affect the number of goals to be displayed, which is 

74 
initially 10. Omitting limit value leaves the current setting 

75 
unchanged. 

28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

76 

28762  77 
\end{description} 
78 

79 
All of the diagnostic commands above admit a list of @{text modes} 

80 
to be specified, which is appended to the current print mode (see 

81 
also \cite{isabelleref}). Thus the output behavior may be modified 

82 
according particular print mode features. For example, @{command 

83 
"pr"}~@{text "(latex xsymbols)"} would print the current proof state 

84 
with mathematical symbols and special characters represented in 

85 
{\LaTeX} source, according to the Isabelle style 

86 
\cite{isabellesys}. 

87 

88 
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more 

89 
systematic way to include formal items into the printed text 

90 
document. 

91 
*} 

92 

93 

28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

94 
subsection {* Details of printed content *} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

95 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

96 
text {* 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

97 
\begin{mldecls} 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39130
diff
changeset

98 
@{index_ML show_types: "bool Config.T"} & default @{ML false} \\ 
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39130
diff
changeset

99 
@{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\ 
39050
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
38980
diff
changeset

100 
@{index_ML show_consts: "bool Config.T"} & default @{ML false} \\ 
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40255
diff
changeset

101 
@{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\ 
39137
ccb53edd59f0
turned show_brackets into proper configuration option;
wenzelm
parents:
39134
diff
changeset

102 
@{index_ML show_brackets: "bool Config.T"} & default @{ML false} \\ 
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42279
diff
changeset

103 
@{index_ML Name_Space.long_names: "bool Config.T"} & default @{ML false} \\ 
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42279
diff
changeset

104 
@{index_ML Name_Space.short_names: "bool Config.T"} & default @{ML false} \\ 
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42279
diff
changeset

105 
@{index_ML Name_Space.unique_names: "bool Config.T"} & default @{ML true} \\ 
39130  106 
@{index_ML eta_contract: "bool Config.T"} & default @{ML true} \\ 
107 
@{index_ML Goal_Display.goals_limit: "int Config.T"} & default @{ML 10} \\ 

108 
@{index_ML Goal_Display.show_main_goal: "bool Config.T"} & default @{ML false} \\ 

39279  109 
@{index_ML show_hyps: "bool Config.T"} & default @{ML false} \\ 
110 
@{index_ML show_tags: "bool Config.T"} & default @{ML false} \\ 

38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
36747
diff
changeset

111 
@{index_ML show_question_marks: "bool Config.T"} & default @{ML true} \\ 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

112 
\end{mldecls} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

113 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

114 
These global ML variables control the detail of information that is 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

115 
displayed for types, terms, theorems, goals etc. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

116 

28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

117 
In interactive sessions, the user interface usually manages these 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

118 
global parameters of the Isabelle process, even with some concept of 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

119 
persistence. Nonetheless it is occasionally useful to manipulate ML 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

120 
variables directly, e.g.\ using @{command "ML_val"} or @{command 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

121 
"ML_command"}. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

122 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

123 
Batchmode logic sessions may be configured by putting appropriate 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

124 
ML text directly into the @{verbatim ROOT.ML} file. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

125 

28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

126 
\begin{description} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

127 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

128 
\item @{ML show_types} and @{ML show_sorts} control printing of type 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

129 
constraints for term variables, and sort constraints for type 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

130 
variables. By default, neither of these are shown in output. If 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

131 
@{ML show_sorts} is set to @{ML true}, types are always shown as 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

132 
well. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

133 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

134 
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

135 
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

136 
rule does not apply as expected. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

137 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

138 
\item @{ML show_consts} controls printing of types of constants when 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

139 
displaying a goal state. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

140 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

141 
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

142 
often occur at several different type instances. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

143 

40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40255
diff
changeset

144 
\item @{ML show_abbrevs} controls folding of constant abbreviations. 
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40255
diff
changeset

145 

28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

146 
\item @{ML show_brackets} controls bracketing in pretty printed 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

147 
output. If set to @{ML true}, all subexpressions of the pretty 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

148 
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

149 
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

150 
pretty printed entities may occasionally help to diagnose problems 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

151 
with operator priorities, for example. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

152 

42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42279
diff
changeset

153 
\item @{ML Name_Space.long_names}, @{ML Name_Space.short_names}, and 
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42279
diff
changeset

154 
@{ML Name_Space.unique_names} control the way of printing fully 
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42279
diff
changeset

155 
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

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

157 
same names. 
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42279
diff
changeset

158 

28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

159 
\item @{ML eta_contract} controls @{text "\<eta>"}contracted printing of 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

160 
terms. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

161 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

162 
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

163 
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

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

165 
g x"} for all @{text x}. Higherorder unification frequently puts 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

166 
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

167 
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

168 
"\<lambda>h. F (\<lambda>x. h x)"}. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

169 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

170 
Setting @{ML eta_contract} makes Isabelle perform @{text 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

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

172 
appears simply as @{text F}. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

173 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

174 
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

175 
form occasionally matters. While higherorder resolution and 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

176 
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

177 
might look at terms more discretely. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

178 

39130  179 
\item @{ML Goal_Display.goals_limit} controls the maximum number of 
180 
subgoals to be shown in goal output. 

28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

181 

39130  182 
\item @{ML Goal_Display.show_main_goal} controls whether the main 
183 
result to be proven should be displayed. This information might be 

184 
relevant for schematic goals, to inspect the current claim that has 

185 
been synthesized so far. 

28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

186 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

187 
\item @{ML show_hyps} controls printing of implicit hypotheses of 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

188 
local facts. Normally, only those hypotheses are displayed that are 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

189 
\emph{not} covered by the assumptions of the current context: this 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

190 
situation indicates a fault in some tool being used. 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

191 

28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

192 
By setting @{ML show_hyps} to @{ML true}, output of \emph{all} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

193 
hypotheses can be enforced, which is occasionally useful for 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

194 
diagnostic purposes. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

195 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

196 
\item @{ML show_tags} controls printing of extra annotations within 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

197 
theorems, such as internal position information, or the case names 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

198 
being attached by the attribute @{attribute case_names}. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

199 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

200 
Note that the @{attribute tagged} and @{attribute untagged} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

201 
attributes provide lowlevel access to the collection of tags 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

202 
associated with a theorem. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

203 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

204 
\item @{ML show_question_marks} controls printing of question marks 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

205 
for schematic variables, such as @{text ?x}. Only the leading 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

206 
question mark is affected, the remaining text is unchanged 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

207 
(including proper markup for schematic variables that might be 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

208 
relevant for user interfaces). 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

209 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

210 
\end{description} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

211 
*} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

212 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

213 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

214 
subsection {* Printing limits *} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

215 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

216 
text {* 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

217 
\begin{mldecls} 
36745  218 
@{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\ 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

219 
@{index_ML print_depth: "int > unit"} \\ 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

220 
\end{mldecls} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

221 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

222 
These ML functions set limits for pretty printed text. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

223 

da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

224 
\begin{description} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

225 

36745  226 
\item @{ML Pretty.margin_default} indicates the global default for 
227 
the right margin of the builtin pretty printer, with initial value 

228 
76. Note that userinterfaces typically control margins 

229 
automatically when resizing windows, or even bypass the formatting 

230 
engine of Isabelle/ML altogether and do it within the front end via 

231 
Isabelle/Scala. 

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

234 
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

235 
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

236 
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

237 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

238 
\end{description} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

239 
*} 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

240 

b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

241 

28762  242 
section {* Mixfix annotations *} 
243 

244 
text {* Mixfix annotations specify concrete \emph{inner syntax} of 

35351
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
32833
diff
changeset

245 
Isabelle types and terms. Locally fixed parameters in toplevel 
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
32833
diff
changeset

246 
theorem statements, locale specifications etc.\ also admit mixfix 
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
32833
diff
changeset

247 
annotations. 
28762  248 

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

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

250 
@{syntax_def \"infix\"}: '(' (@'infix'  @'infixl'  @'infixr') 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

251 
@{syntax string} @{syntax nat} ')' 
28762  252 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

253 
@{syntax_def mixfix}: @{syntax \"infix\"}  '(' @{syntax string} prios? @{syntax nat}? ')'  
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

254 
'(' @'binder' @{syntax string} prios? @{syntax nat} ')' 
28762  255 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

256 
@{syntax_def structmixfix}: @{syntax mixfix}  '(' @'structure' ')' 
28762  257 
; 
258 

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

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

260 
"} 
28762  261 

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

262 
Here the @{syntax string} specifications refer to the actual mixfix 
28762  263 
template, which may include literal text, spacing, blocks, and 
264 
arguments (denoted by ``@{text _}''); the special symbol 

265 
``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index 

266 
argument that specifies an implicit structure reference (see also 

267 
\secref{sec:locale}). Infix and binder declarations provide common 

268 
abbreviations for particular mixfix declarations. So in practice, 

269 
mixfix templates mostly degenerate to literal text for concrete 

270 
syntax, such as ``@{verbatim "++"}'' for an infix symbol. 

271 

272 
\medskip In full generality, mixfix declarations work as follows. 

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

274 
annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text 

275 
"mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of 

276 
delimiters that surround argument positions as indicated by 

277 
underscores. 

278 

279 
Altogether this determines a production for a contextfree priority 

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

281 
is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and 

282 
the result category is determined from @{text "\<tau>"} (with 

283 
priority @{text "p"}). Priority specifications are optional, with 

284 
default 0 for arguments and 1000 for the result. 

285 

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

287 
type scheme may have more argument positions than the mixfix 

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

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

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

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

292 
template, the concrete syntax is ignored. 

293 

294 
\medskip A mixfix template may also contain additional directives 

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

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

297 
entities. 

298 

28778  299 
\begin{description} 
28762  300 

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

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

302 
characters other than the following special characters: 
28762  303 

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

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

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

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

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

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

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

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

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

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

313 
\medskip 
28762  314 

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

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

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

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

318 

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

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

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

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

322 

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

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

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

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

327 
where implicit structure arguments can be attached. 
28762  328 

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

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

330 
This and the following specifications do not affect parsing at all. 
28762  331 

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

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

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

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

336 
@{verbatim "(00"} is unbreakable. 
28762  337 

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

338 
\item @{verbatim ")"} closes a pretty printing block. 
28762  339 

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

340 
\item @{verbatim "//"} forces a line break. 
28762  341 

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

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

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

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

28778  346 
\end{description} 
28762  347 

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

348 
For example, the template @{verbatim "(_ +/ _)"} specifies an infix 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

349 
operator. There are two argument positions; the delimiter 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

350 
@{verbatim "+"} is preceded by a space and followed by a space or 
4510201c6aaf
mixfix annotations: verbatim for special symbols;
wenzelm
parents:
28770
diff
changeset

351 
line break; the entire phrase is a pretty printing block. 
28762  352 

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

354 
described in \cite{paulsonml2}. 

355 
*} 

356 

357 

35413  358 
section {* Explicit notation *} 
28762  359 

360 
text {* 

361 
\begin{matharray}{rcll} 

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

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

366 
@{command_def "write"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\ 
28762  367 
\end{matharray} 
368 

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

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

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

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

373 
(@@{command notation}  @@{command no_notation}) @{syntax target}? @{syntax mode}? \\ 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

374 
(@{syntax nameref} @{syntax structmixfix} + @'and') 
28762  375 
; 
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

376 
@@{command write} @{syntax mode}? (@{syntax nameref} @{syntax structmixfix} + @'and') 
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
42358
diff
changeset

377 
"} 
28762  378 

379 
\begin{description} 

380 

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

383 
constructor is retrieved from the context. 

384 

385 
\item @{command "no_type_notation"} is similar to @{command 

386 
"type_notation"}, but removes the specified syntax annotation from 

387 
the present context. 

388 

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

28762  392 

393 
\item @{command "no_notation"} is similar to @{command "notation"}, 

394 
but removes the specified syntax annotation from the present 

395 
context. 

396 

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

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

398 
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

399 

28762  400 
\end{description} 
35413  401 

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

402 
Note that the more primitive commands @{command "syntax"} and 
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35413
diff
changeset

403 
@{command "no_syntax"} (\secref{sec:syntrans}) provide raw access 
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35413
diff
changeset

404 
to the syntax tables of a global theory. 
28762  405 
*} 
406 

28778  407 

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

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

409 

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

411 

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

412 
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

413 
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

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

415 
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

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

417 
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

418 
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

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

420 

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

421 
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

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

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

424 
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

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

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

427 

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

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

429 
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

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

433 

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

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

435 
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

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

437 

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

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

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

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

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

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

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

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

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

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

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

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

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

451 

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

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

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

454 

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

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

456 

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

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

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

459 

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

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

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

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

463 

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

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

465 

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

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

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

468 

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

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

470 

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

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

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

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

474 
\begin{tabular}{rclc} 
28774  475 
@{text A} & @{text "="} & @{verbatim "("} @{text A} @{verbatim ")"} \\ 
476 
& @{text ""} & @{verbatim 0} & \qquad\qquad \\ 

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

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

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

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

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

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

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

483 

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

484 

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

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

486 

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

487 
text {* 
28773  488 
The priority grammar of the @{text "Pure"} theory is defined as follows: 
489 

28774  490 
%FIXME syntax for "index" (?) 
491 
%FIXME "op" versions of ==> etc. (?) 

492 

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

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

495 

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

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

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

502 
& @{text ""} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ 
28772  503 
& @{text ""} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28773  504 
& @{text ""} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28772  505 
& @{text ""} & @{verbatim "["} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28773  506 
& @{text ""} & @{text "\<lbrakk>"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{text "\<rbrakk>"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28772  507 
& @{text ""} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ 
28773  508 
& @{text ""} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ 
509 
& @{text ""} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\ 

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

511 
& @{text ""} & @{verbatim TERM} @{text logic} \\ 
28773  512 
& @{text ""} & @{verbatim PROP} @{text aprop} \\\\ 
28772  513 

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

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

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

516 
& @{text ""} & @{verbatim CONST} @{text "id  "}@{verbatim CONST} @{text "longid"} \\ 
28773  517 
& @{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

518 

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

522 
& @{text ""} & @{verbatim CONST} @{text "id  "}@{verbatim CONST} @{text "longid"} \\ 
28773  523 
& @{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)"} \\ 
28772  524 
& @{text ""} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ 
28773  525 
& @{text ""} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ 
28772  526 
& @{text ""} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\ 
527 

28778  528 
@{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text "  id  "}@{verbatim "_"} \\ 
28773  529 
& @{text ""} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\ 
530 
& @{text ""} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\ 

28772  531 

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

28778  534 
@{syntax_def (inner) pttrn} & = & @{text idt} \\\\ 
28772  535 

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

28778  538 
@{syntax_def (inner) type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\ 
28773  539 
& @{text ""} & @{text "tid  tvar  "}@{verbatim "_"} \\ 
540 
& @{text ""} & @{text "tid"} @{verbatim "::"} @{text "sort  tvar "}@{verbatim "::"} @{text "sort  "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\ 

28772  541 
& @{text ""} & @{text "id  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) id  "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text id} \\ 
29741  542 
& @{text ""} & @{text "longid  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) longid"} \\ 
543 
& @{text ""} & @{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text longid} \\ 

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

547 
& @{text ""} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\\\ 

28772  548 

29741  549 
@{syntax_def (inner) sort} & = & @{text "id  longid  "}@{verbatim "{}"} \\ 
550 
& @{text ""} & @{verbatim "{"} @{text "(id  longid)"} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text "(id  longid)"} @{verbatim "}"} \\ 

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

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

553 

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

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

557 
grammar is as follows: 

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

558 

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

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

560 

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

562 

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

565 
the metalogic is carefully distinguished from usual conventions for 

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

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

568 

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

571 
explicit @{verbatim PROP} token. 

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

572 

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

573 
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

574 
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

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

578 

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

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

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

583 
anything defined by the user. 

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

584 

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

585 
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

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

588 

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

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

591 

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

594 
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

595 

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

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

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

600 
additional productions for binding forms. 

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

601 

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

603 

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

605 

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

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

607 

28774  608 
Here are some further explanations of certain syntax features. 
28773  609 

610 
\begin{itemize} 

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

611 

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

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

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

28773  616 

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

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

619 
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

620 
sequence of identifiers. 
28773  621 

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

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

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

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

626 
:: nat)"}. 

627 

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

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

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

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

28773  634 

635 
\begin{description} 

636 

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

639 
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

640 

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

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

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

28773  645 

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

648 
= x"}. 

28773  649 

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

652 
implicitly abstracted over its context of locally bound variables. 

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

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

655 
using both bound and schematic dummies. 

28773  656 

657 
\end{description} 

658 

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

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

662 
context. This special term abbreviation works nicely with 

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

664 

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

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

667 

28777  668 

28774  669 
section {* Lexical matters \label{sec:innerlex} *} 
670 

28777  671 
text {* The inner lexical syntax vaguely resembles the outer one 
672 
(\secref{sec:outerlex}), but some details are different. There are 

673 
two main categories of inner syntax tokens: 

674 

675 
\begin{enumerate} 

676 

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

678 
productions of the given priority grammar (cf.\ 

679 
\secref{sec:prioritygrammar}); 

680 

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

682 

683 
\end{enumerate} 

684 

685 
Delimiters override named tokens and may thus render certain 

686 
identifiers inaccessible. Sometimes the logical context admits 

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

688 
qualified names. 

689 

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

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

692 
(\secref{sec:outerlex}). 

693 

694 
\begin{center} 

695 
\begin{supertabular}{rcl} 

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

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

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

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

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

701 
@{syntax_def (inner) num} & = & @{syntax_ref nat}@{text "  "}@{verbatim ""}@{syntax_ref nat} \\ 

29157  702 
@{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  "}@{verbatim ""}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ 
28777  703 
@{syntax_def (inner) xnum} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  "}@{verbatim "#"}@{syntax_ref nat} \\ 
704 

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

706 
\end{supertabular} 

707 
\end{center} 

708 

29157  709 
The token categories @{syntax (inner) num}, @{syntax (inner) 
710 
float_token}, @{syntax (inner) xnum}, and @{syntax (inner) xstr} are 

711 
not used in Pure. Objectlogics may implement numerals and string 

712 
constants by adding appropriate syntax declarations, together with 

713 
some translation functions (e.g.\ see Isabelle/HOL). 

714 

715 
The derived categories @{syntax_def (inner) num_const} and 

716 
@{syntax_def (inner) float_const} provide robust access to @{syntax 

717 
(inner) num}, and @{syntax (inner) float_token}, respectively: the 

718 
syntax tree holds a syntactic constant instead of a free variable. 

28777  719 
*} 
28774  720 

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

721 

28762  722 
section {* Syntax and translations \label{sec:syntrans} *} 
723 

724 
text {* 

725 
\begin{matharray}{rcl} 

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

726 
@{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\ 
28762  727 
@{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\ 
728 
@{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\ 

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

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

731 
\end{matharray} 

732 

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

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

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

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

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

739 
(transpat ('=='  '=>'  '<='  '\<rightleftharpoons>'  '\<rightharpoonup>'  '\<leftharpoondown>') transpat +) 
28762  740 
; 
741 

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

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

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

745 
"} 
28762  746 

747 
\begin{description} 

748 

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

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

752 

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

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

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

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

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

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

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

760 
input and output grammar. 

761 

762 
\item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar 

763 
declarations (and translations) resulting from @{text decls}, which 

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

765 

766 
\item @{command "translations"}~@{text rules} specifies syntactic 

767 
translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}), 

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

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

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

771 

772 
\item @{command "no_translations"}~@{text rules} removes syntactic 

773 
translation rules, which are interpreted in the same manner as for 

774 
@{command "translations"} above. 

775 

776 
\end{description} 

777 
*} 

778 

779 

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

780 
section {* Syntax translation functions \label{sec:trfuns} *} 
28762  781 

782 
text {* 

783 
\begin{matharray}{rcl} 

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

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

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

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

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

789 
\end{matharray} 

790 

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

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

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

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

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

795 
"} 
28762  796 

797 
Syntax translation functions written in ML admit almost arbitrary 

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

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

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

802 
%FIXME proper antiquotations 

803 
\begin{ttbox} 

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

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

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

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

807 
val typed_print_translation : (string * (typ > term list > term)) list 
28762  808 
val print_ast_translation : (string * (ast list > ast)) list 
809 
\end{ttbox} 

810 

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

812 
translation functions may depend on the current theory or proof 

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

814 
translations functions may refer to specific theory declarations or 

815 
auxiliary proof data. 

816 

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

28762  819 

820 
%FIXME proper antiquotations 

821 
\begin{ttbox} 

822 
val parse_ast_translation: 

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

824 
val parse_translation: 

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

826 
val print_translation: 

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

828 
val typed_print_translation: 

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

829 
(string * (Proof.context > typ > term list > term)) list 
28762  830 
val print_ast_translation: 
831 
(string * (Proof.context > ast list > ast)) list 

832 
\end{ttbox} 

833 
*} 

834 

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

835 

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

836 
section {* Inspecting the syntax *} 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

837 

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

838 
text {* 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

839 
\begin{matharray}{rcl} 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

840 
@{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

841 
\end{matharray} 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

842 

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

843 
\begin{description} 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

844 

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

845 
\item @{command "print_syntax"} prints the inner syntax of the 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

846 
current context. The output can be quite large; the most important 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

847 
sections are explained below. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

848 

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

849 
\begin{description} 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

850 

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

851 
\item @{text "lexicon"} lists the delimiters of the inner token 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

852 
language; see \secref{sec:innerlex}. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

853 

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

854 
\item @{text "prods"} lists the productions of the underlying 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

855 
priority grammar; see \secref{sec:prioritygrammar}. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

856 

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

857 
The nonterminal @{text "A\<^sup>(\<^sup>p\<^sup>)"} is rendered in plain text as @{text 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

858 
"A[p]"}; delimiters are quoted. Many productions have an extra 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

859 
@{text "\<dots> => name"}. These names later become the heads of parse 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

860 
trees; they also guide the pretty printer. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

861 

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

862 
Productions without such parse tree names are called \emph{copy 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

863 
productions}. Their righthand side must have exactly one 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

864 
nonterminal symbol (or named token). The parser does not create a 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

865 
new parse tree node for copy productions, but simply returns the 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

866 
parse tree of the righthand symbol. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

867 

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

868 
If the righthand side of a copy production consists of a single 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

869 
nonterminal without any delimiters, then it is called a \emph{chain 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

870 
production}. Chain productions act as abbreviations: conceptually, 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

871 
they are removed from the grammar by adding new productions. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

872 
Priority information attached to chain productions is ignored; only 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

873 
the dummy value @{text "1"} is displayed. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

874 

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

875 
\item @{text "print modes"} lists the alternative print modes 
28779
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

876 
provided by this grammar; see \secref{sec:printmodes}. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

877 

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

878 
\item @{text "parse_rules"} and @{text "print_rules"} relate to 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

879 
syntax translations (macros); see \secref{sec:syntrans}. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

880 

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

881 
\item @{text "parse_ast_translation"} and @{text 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

882 
"print_ast_translation"} list sets of constants that invoke 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

883 
translation functions for abstract syntax trees, which are only 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

884 
required in very special situations; see \secref{sec:trfuns}. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

885 

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

886 
\item @{text "parse_translation"} and @{text "print_translation"} 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

887 
list the sets of constants that invoke regular translation 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

888 
functions; see \secref{sec:trfuns}. 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

889 

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

890 
\end{description} 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

891 

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

892 
\end{description} 
698960f08652
separate section "Inspecting the syntax" for print_syntax;
wenzelm
parents:
28778
diff
changeset

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

894 

28762  895 
end 