author  wenzelm 
Thu, 13 Nov 2008 22:01:30 +0100  
changeset 28778  a25630deacaf 
parent 28777  2eeeced17228 
child 28779  698960f08652 
permissions  rwrr 
28762  1 
(* $Id$ *) 
2 

3 
theory Inner_Syntax 

4 
imports Main 

5 
begin 

6 

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

9 
section {* Printing logical entities *} 

10 

11 
subsection {* Diagnostic commands *} 

12 

13 
text {* 

14 
\begin{matharray}{rcl} 

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

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

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

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

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

24 
These diagnostic commands assist interactive development by printing 

25 
internal logical entities in a humanreadable fashion. 

26 

27 
\begin{rail} 

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

28 
'typ' modes? type 
28762  29 
; 
30 
'term' modes? term 

31 
; 

32 
'prop' modes? prop 

33 
; 

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

34 
'thm' modes? thmrefs 
28762  35 
; 
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

36 
( 'prf'  'full\_prf' ) modes? thmrefs? 
28762  37 
; 
28766
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

38 
'pr' modes? nat? (',' nat)? 
28762  39 
; 
40 

41 
modes: '(' (name + ) ')' 

42 
; 

43 
\end{rail} 

44 

45 
\begin{description} 

46 

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

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

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

49 

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

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

51 
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

52 
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

53 
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

54 
inspecting the current environment of term abbreviations. 
28762  55 

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

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

58 
attributes included in the theorem specifications are applied to a 

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

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

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

62 

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

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

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

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

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

68 

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

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

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

72 
there. 

73 

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

74 
\item @{command "pr"}~@{text "goals, prems"} prints the current 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

75 
proof state (if present), including the proof context, current facts 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

76 
and goals. The optional limit arguments affect the number of goals 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

77 
and premises to be displayed, which is initially 10 for both. 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

78 
Omitting limit values leaves the current setting unchanged. 
accab7594b8e
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28765
diff
changeset

79 

28762  80 
\end{description} 
81 

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

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

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

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

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

87 
with mathematical symbols and special characters represented in 

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

89 
\cite{isabellesys}. 

90 

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

92 
systematic way to include formal items into the printed text 

93 
document. 

94 
*} 

95 

96 

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

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

98 

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

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

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

101 
@{index_ML show_types: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

102 
@{index_ML show_sorts: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

103 
@{index_ML show_consts: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

104 
@{index_ML long_names: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

105 
@{index_ML short_names: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

106 
@{index_ML unique_names: "bool ref"} & default @{ML true} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

107 
@{index_ML show_brackets: "bool ref"} & default @{ML false} \\ 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

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

109 
@{index_ML goals_limit: "int ref"} & default @{ML 10} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

110 
@{index_ML Proof.show_main_goal: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

111 
@{index_ML show_hyps: "bool ref"} & default @{ML false} \\ 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

112 
@{index_ML show_tags: "bool ref"} & default @{ML false} \\ 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

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

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

115 

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

116 
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

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

118 

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

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

120 
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

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

122 
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

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

124 

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

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

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

127 

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

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

129 

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

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

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

132 
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

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

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

135 

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

136 
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

137 
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

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

139 

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

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

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

142 

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

143 
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

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

145 

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

146 
\item @{ML long_names}, @{ML short_names}, and @{ML unique_names} 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

147 
control the way of printing fully qualified internal names in 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

148 
external form. See also \secref{sec:antiq} for the document 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

149 
antiquotation options of the same names. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

150 

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

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

152 
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

153 
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

154 
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

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

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

157 

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

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

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

160 

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

161 
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

162 
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

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

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

165 
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

166 
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

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

168 

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

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

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

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

172 

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

173 
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

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

175 
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

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

177 

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

178 
\item @{ML goals_limit} controls the maximum number of subgoals to 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

179 
be shown in goal output. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

180 

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

181 
\item @{ML Proof.show_main_goal} controls whether the main result to 
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

182 
be proven should be displayed. This information might be relevant 
28765
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

183 
for schematic goals, to inspect the current claim that has been 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

184 
synthesized so far. 
28763
b5e6122ff575
added pretty printing options (from old ref manual);
wenzelm
parents:
28762
diff
changeset

185 

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

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

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

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

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

190 

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

191 
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

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

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

194 

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

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

196 
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

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

198 

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

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

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

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

202 

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

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

204 
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

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

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

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

208 

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

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

210 
*} 
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 
subsection {* Printing limits *} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

214 

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

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

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

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

218 
@{index_ML Pretty.setmargin: "int > unit"} \\ 
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 

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

226 
\item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

227 
limit the printing depth to @{text d}. This affects the display of 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

228 
types, terms, theorems etc. The default value is 0, which permits 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

229 
printing to an arbitrary depth. Other useful values for @{text d} 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

230 
are 10 and 20. 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

231 

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

232 
\item @{ML Pretty.setmargin}~@{text m} tells the pretty printer to 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

233 
assume a right margin (page width) of @{text m}. The initial margin 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

234 
is 76, but user interfaces might adapt the margin automatically when 
da8f6f4a74be
misc tuning and rearrangement of section "Printing logical entities";
wenzelm
parents:
28763
diff
changeset

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

236 

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

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

238 
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

239 
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

240 
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

241 

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

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

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

244 

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

245 

28762  246 
section {* Mixfix annotations *} 
247 

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

28767  249 
Isabelle types and terms. Some commands such as @{command 
250 
"typedecl"} admit infixes only, while @{command "definition"} etc.\ 

251 
support the full range of general mixfixes and binders. Fixed 

252 
parameters in toplevel theorem statements, locale specifications 

253 
also admit mixfix annotations. 

28762  254 

255 
\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} 

256 
\begin{rail} 

257 
infix: '(' ('infix'  'infixl'  'infixr') string nat ')' 

258 
; 

259 
mixfix: infix  '(' string prios? nat? ')'  '(' 'binder' string prios? nat ')' 

260 
; 

261 
structmixfix: mixfix  '(' 'structure' ')' 

262 
; 

263 

264 
prios: '[' (nat + ',') ']' 

265 
; 

266 
\end{rail} 

267 

268 
Here the \railtok{string} specifications refer to the actual mixfix 

269 
template, which may include literal text, spacing, blocks, and 

270 
arguments (denoted by ``@{text _}''); the special symbol 

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

272 
argument that specifies an implicit structure reference (see also 

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

274 
abbreviations for particular mixfix declarations. So in practice, 

275 
mixfix templates mostly degenerate to literal text for concrete 

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

277 

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

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

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

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

282 
delimiters that surround argument positions as indicated by 

283 
underscores. 

284 

285 
Altogether this determines a production for a contextfree priority 

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

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

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

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

290 
default 0 for arguments and 1000 for the result. 

291 

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

293 
type scheme may have more argument positions than the mixfix 

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

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

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

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

298 
template, the concrete syntax is ignored. 

299 

300 
\medskip A mixfix template may also contain additional directives 

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

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

303 
entities. 

304 

28778  305 
\begin{description} 
28762  306 

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

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

308 
characters other than the following special characters: 
28762  309 

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

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

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

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

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

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

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

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

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

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

319 
\medskip 
28762  320 

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

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

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

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

324 

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

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

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

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

328 

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

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

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

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

333 
where implicit structure arguments can be attached. 
28762  334 

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

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

336 
This and the following specifications do not affect parsing at all. 
28762  337 

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

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

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

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

342 
@{verbatim "(00"} is unbreakable. 
28762  343 

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

344 
\item @{verbatim ")"} closes a pretty printing block. 
28762  345 

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

346 
\item @{verbatim "//"} forces a line break. 
28762  347 

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

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

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

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

28778  352 
\end{description} 
28762  353 

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

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

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

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

357 
line break; the entire phrase is a pretty printing block. 
28762  358 

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

360 
described in \cite{paulsonml2}. 

361 
*} 

362 

363 

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

364 
section {* Explicit term notation *} 
28762  365 

366 
text {* 

367 
\begin{matharray}{rcll} 

368 
@{command_def "notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 

369 
@{command_def "no_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 

370 
\end{matharray} 

371 

372 
\begin{rail} 

373 
('notation'  'no\_notation') target? mode? (nameref structmixfix + 'and') 

374 
; 

375 
\end{rail} 

376 

377 
\begin{description} 

378 

379 
\item @{command "notation"}~@{text "c (mx)"} associates mixfix 

380 
syntax with an existing constant or fixed variable. This is a 

381 
robust interface to the underlying @{command "syntax"} primitive 

382 
(\secref{sec:syntrans}). Type declaration and internal syntactic 

383 
representation of the given entity is retrieved from the context. 

384 

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

386 
but removes the specified syntax annotation from the present 

387 
context. 

388 

389 
\end{description} 

390 
*} 

391 

28778  392 

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

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

394 

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

396 

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

397 
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

398 
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

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

400 
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

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

402 
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

403 
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

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

405 

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

406 
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

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

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

409 
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

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

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

412 

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

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

414 
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

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

418 

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

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

420 
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

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

422 

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

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

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

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

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

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

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

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

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

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

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

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

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

436 

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

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

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

439 

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

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

441 

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

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

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

444 

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

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

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

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

448 

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

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

450 

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

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

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

453 

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

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

455 

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

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

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

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

459 
\begin{tabular}{rclc} 
28774  460 
@{text A} & @{text "="} & @{verbatim "("} @{text A} @{verbatim ")"} \\ 
461 
& @{text ""} & @{verbatim 0} & \qquad\qquad \\ 

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

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

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

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

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

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

467 
*} 
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 

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

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

471 

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

472 
text {* 
28773  473 
The priority grammar of the @{text "Pure"} theory is defined as follows: 
474 

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

477 

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

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

480 

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

28778  483 
@{syntax_def (inner) prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\ 
28772  484 
& @{text ""} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ 
28773  485 
& @{text ""} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ 
28772  486 
& @{text ""} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ 
28773  487 
& @{text ""} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\ 
28772  488 
& @{text ""} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28773  489 
& @{text ""} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28772  490 
& @{text ""} & @{verbatim "["} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28773  491 
& @{text ""} & @{text "\<lbrakk>"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{text "\<rbrakk>"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ 
28772  492 
& @{text ""} & @{verbatim "!!"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ 
28773  493 
& @{text ""} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\ 
494 
& @{text ""} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\ 

495 
& @{text ""} & @{verbatim SORT_CONSTRAINT} @{verbatim "("} @{text type} @{verbatim ")"} \\ 

496 
& @{text ""} & @{verbatim PROP} @{text aprop} \\\\ 

28772  497 

28778  498 
@{syntax_def (inner) aprop} & = & @{text "id  longid  var  "}@{verbatim "_"}@{text "  "}@{verbatim "..."} \\ 
28773  499 
& @{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

500 

28778  501 
@{syntax_def (inner) logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\ 
28772  502 
& @{text ""} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\ 
28773  503 
& @{text ""} & @{text "id  longid  var  "}@{verbatim "_"}@{text "  "}@{verbatim "..."} \\ 
504 
& @{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  505 
& @{text ""} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ 
28773  506 
& @{text ""} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\ 
507 
& @{text ""} & @{verbatim CONST} @{text "id  "}@{verbatim CONST} @{text "longid"} \\ 

28772  508 
& @{text ""} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\ 
509 

28778  510 
@{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text "  id  "}@{verbatim "_"} \\ 
28773  511 
& @{text ""} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\ 
512 
& @{text ""} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\ 

28772  513 

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

28778  516 
@{syntax_def (inner) pttrn} & = & @{text idt} \\\\ 
28772  517 

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

28778  520 
@{syntax_def (inner) type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\ 
28773  521 
& @{text ""} & @{text "tid  tvar  "}@{verbatim "_"} \\ 
522 
& @{text ""} & @{text "tid"} @{verbatim "::"} @{text "sort  tvar "}@{verbatim "::"} @{text "sort  "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\ 

28772  523 
& @{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} \\ 
524 
& @{text ""} & @{text "longid  type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) longid  "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text longid} \\ 

525 
& @{text ""} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\ 

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

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

28772  529 

28778  530 
@{syntax_def (inner) sort} & = & @{text "id  longid  "}@{verbatim "{}"}@{text "  "}@{verbatim "{"} @{text "(id  longid)"} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text "(id  longid)"} @{verbatim "}"} \\ 
28773  531 
\end{supertabular} 
28770
93a372e2dc7a
added section "The Pure grammar" (incomplete version, based on old ref manual);
wenzelm
parents:
28769
diff
changeset

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

533 

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

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

537 
grammar is as follows: 

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

538 

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

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

540 

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

542 

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

545 
the metalogic is carefully distinguished from usual conventions for 

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

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

548 

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

551 
explicit @{verbatim PROP} token. 

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

552 

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

553 
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

554 
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

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

558 

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

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

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

563 
anything defined by the user. 

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

564 

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

565 
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

566 
(excluding @{typ prop}) are \emph{collapsed} to this single category 
28778  567 
of @{syntax (inner) logic}. 
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) idt} denotes identifiers, possibly 
570 
constrained by types. 

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

571 

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

574 
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

575 

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

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

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

580 
additional productions for binding forms. 

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

581 

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

583 

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

585 

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

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

587 

28774  588 
Here are some further explanations of certain syntax features. 
28773  589 

590 
\begin{itemize} 

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

591 

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

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

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

28773  596 

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

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

599 
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

600 
sequence of identifiers. 
28773  601 

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

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

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

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

606 
:: nat)"}. 

607 

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

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

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

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

28773  614 

615 
\begin{description} 

616 

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

619 
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

620 

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

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

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

28773  625 

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

628 
= x"}. 

28773  629 

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

632 
implicitly abstracted over its context of locally bound variables. 

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

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

635 
using both bound and schematic dummies. 

28773  636 

637 
\end{description} 

638 

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

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

642 
context. This special term abbreviation works nicely with 

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

644 

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

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

647 

28777  648 

28774  649 
section {* Lexical matters \label{sec:innerlex} *} 
650 

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

653 
two main categories of inner syntax tokens: 

654 

655 
\begin{enumerate} 

656 

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

658 
productions of the given priority grammar (cf.\ 

659 
\secref{sec:prioritygrammar}); 

660 

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

662 

663 
\end{enumerate} 

664 

665 
Delimiters override named tokens and may thus render certain 

666 
identifiers inaccessible. Sometimes the logical context admits 

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

668 
qualified names. 

669 

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

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

672 
(\secref{sec:outerlex}). 

673 

674 
\begin{center} 

675 
\begin{supertabular}{rcl} 

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

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

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

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

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

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

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

683 

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

685 
\end{supertabular} 

686 
\end{center} 

687 

688 
The token categories @{syntax_ref (inner) num}, @{syntax_ref (inner) 

689 
xnum}, and @{syntax_ref (inner) xstr} are not used in Pure. 

690 
Objectlogics may implement numerals and string constants by adding 

691 
appropriate syntax declarations, together with some translation 

692 
functions (e.g.\ see Isabelle/HOL). 

693 
*} 

28774  694 

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

695 

28762  696 
section {* Syntax and translations \label{sec:syntrans} *} 
697 

698 
text {* 

699 
\begin{matharray}{rcl} 

700 
@{command_def "nonterminals"} & : & @{text "theory \<rightarrow> theory"} \\ 

701 
@{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\ 

702 
@{command_def "no_syntax"} & : & @{text "theory \<rightarrow> theory"} \\ 

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

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

705 
\end{matharray} 

706 

707 
\begin{rail} 

708 
'nonterminals' (name +) 

709 
; 

710 
('syntax'  'no\_syntax') mode? (constdecl +) 

711 
; 

712 
('translations'  'no\_translations') (transpat ('=='  '=>'  '<='  rightleftharpoons  rightharpoonup  leftharpoondown) transpat +) 

713 
; 

714 

715 
mode: ('(' ( name  'output'  name 'output' ) ')') 

716 
; 

717 
transpat: ('(' nameref ')')? string 

718 
; 

719 
\end{rail} 

720 

721 
\begin{description} 

722 

723 
\item @{command "nonterminals"}~@{text c} declares a type 

724 
constructor @{text c} (without arguments) to act as purely syntactic 

725 
type: a nonterminal symbol of the inner syntax. 

726 

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

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

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

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

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

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

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

734 
input and output grammar. 

735 

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

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

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

739 

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

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

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

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

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

745 

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

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

748 
@{command "translations"} above. 

749 

750 
\end{description} 

751 
*} 

752 

753 

754 
section {* Syntax translation functions *} 

755 

756 
text {* 

757 
\begin{matharray}{rcl} 

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

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

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

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

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

763 
\end{matharray} 

764 

765 
\begin{rail} 

766 
( 'parse\_ast\_translation'  'parse\_translation'  'print\_translation'  

767 
'typed\_print\_translation'  'print\_ast\_translation' ) ('(advanced)')? text 

768 
; 

769 
\end{rail} 

770 

771 
Syntax translation functions written in ML admit almost arbitrary 

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

773 
have a single \railqtok{text} argument that refers to an ML 

774 
expression of appropriate type, which are as follows by default: 

775 

776 
%FIXME proper antiquotations 

777 
\begin{ttbox} 

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

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

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

781 
val typed_print_translation : 

782 
(string * (bool > typ > term list > term)) list 

783 
val print_ast_translation : (string * (ast list > ast)) list 

784 
\end{ttbox} 

785 

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

787 
translation functions may depend on the current theory or proof 

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

789 
translations functions may refer to specific theory declarations or 

790 
auxiliary proof data. 

791 

792 
See also \cite[\S8]{isabelleref} for more information on the 

793 
general concept of syntax transformations in Isabelle. 

794 

795 
%FIXME proper antiquotations 

796 
\begin{ttbox} 

797 
val parse_ast_translation: 

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

799 
val parse_translation: 

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

801 
val print_translation: 

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

803 
val typed_print_translation: 

804 
(string * (Proof.context > bool > typ > term list > term)) list 

805 
val print_ast_translation: 

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

807 
\end{ttbox} 

808 
*} 

809 

810 
end 