95 \<^medskip> |
95 \<^medskip> |
96 The categories for named tokens are defined once and for all as follows. |
96 The categories for named tokens are defined once and for all as follows. |
97 |
97 |
98 \begin{center} |
98 \begin{center} |
99 \begin{supertabular}{rcl} |
99 \begin{supertabular}{rcl} |
100 @{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\ |
100 @{syntax_def short_ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\ |
101 @{syntax_def longident} & = & \<open>ident(\<close>\<^verbatim>\<open>.\<close>\<open>ident)\<^sup>+\<close> \\ |
101 @{syntax_def long_ident} & = & \<open>short_ident(\<close>\<^verbatim>\<open>.\<close>\<open>short_ident)\<^sup>+\<close> \\ |
102 @{syntax_def symident} & = & \<open>sym\<^sup>+ |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close> \\ |
102 @{syntax_def sym_ident} & = & \<open>sym\<^sup>+ |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>short_ident\<close>\<^verbatim>\<open>>\<close> \\ |
103 @{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\ |
103 @{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\ |
104 @{syntax_def float} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat}~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>@{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\ |
104 @{syntax_def float} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat}~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>@{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\ |
105 @{syntax_def var} & = & \<^verbatim>\<open>?\<close>\<open>ident |\<close>~~\<^verbatim>\<open>?\<close>\<open>ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\ |
105 @{syntax_def term_var} & = & \<^verbatim>\<open>?\<close>\<open>short_ident |\<close>~~\<^verbatim>\<open>?\<close>\<open>short_ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\ |
106 @{syntax_def typefree} & = & \<^verbatim>\<open>'\<close>\<open>ident\<close> \\ |
106 @{syntax_def type_ident} & = & \<^verbatim>\<open>'\<close>\<open>short_ident\<close> \\ |
107 @{syntax_def typevar} & = & \<^verbatim>\<open>?\<close>\<open>typefree |\<close>~~\<^verbatim>\<open>?\<close>\<open>typefree\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\ |
107 @{syntax_def type_var} & = & \<^verbatim>\<open>?\<close>\<open>type_ident |\<close>~~\<^verbatim>\<open>?\<close>\<open>type_ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\ |
108 @{syntax_def string} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\ |
108 @{syntax_def string} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\ |
109 @{syntax_def altstring} & = & \<^verbatim>\<open>`\<close> \<open>\<dots>\<close> \<^verbatim>\<open>`\<close> \\ |
109 @{syntax_def altstring} & = & \<^verbatim>\<open>`\<close> \<open>\<dots>\<close> \<^verbatim>\<open>`\<close> \\ |
110 @{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\ |
110 @{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\ |
111 @{syntax_def verbatim} & = & \<^verbatim>\<open>{*\<close> \<open>\<dots>\<close> \<^verbatim>\<open>*}\<close> \\[1ex] |
111 @{syntax_def verbatim} & = & \<^verbatim>\<open>{*\<close> \<open>\<dots>\<close> \<^verbatim>\<open>*}\<close> \\[1ex] |
112 |
112 |
126 & & \<^verbatim>\<open>\<Lambda>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Sigma>\<close>~~\<open>|\<close> \\ |
126 & & \<^verbatim>\<open>\<Lambda>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Sigma>\<close>~~\<open>|\<close> \\ |
127 & & \<^verbatim>\<open>\<Upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Psi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Omega>\<close> \\ |
127 & & \<^verbatim>\<open>\<Upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Psi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Omega>\<close> \\ |
128 \end{supertabular} |
128 \end{supertabular} |
129 \end{center} |
129 \end{center} |
130 |
130 |
131 A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown, which is |
131 A @{syntax_ref term_var} or @{syntax_ref type_var} describes an unknown, |
132 internally a pair of base name and index (ML type @{ML_type indexname}). |
132 which is internally a pair of base name and index (ML type @{ML_type |
133 These components are either separated by a dot as in \<open>?x.1\<close> or \<open>?x7.3\<close> or |
133 indexname}). These components are either separated by a dot as in \<open>?x.1\<close> or |
134 run together as in \<open>?x1\<close>. The latter form is possible if the base name does |
134 \<open>?x7.3\<close> or run together as in \<open>?x1\<close>. The latter form is possible if the base |
135 not end with digits. If the index is 0, it may be dropped altogether: \<open>?x\<close> |
135 name does not end with digits. If the index is 0, it may be dropped |
136 and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the same unknown, with basename \<open>x\<close> and |
136 altogether: \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the same unknown, with |
137 index 0. |
137 basename \<open>x\<close> and index 0. |
138 |
138 |
139 The syntax of @{syntax_ref string} admits any characters, including |
139 The syntax of @{syntax_ref string} admits any characters, including |
140 newlines; ``\<^verbatim>\<open>"\<close>'' (double-quote) and ``\<^verbatim>\<open>\\<close>'' (backslash) need to be |
140 newlines; ``\<^verbatim>\<open>"\<close>'' (double-quote) and ``\<^verbatim>\<open>\\<close>'' (backslash) need to be |
141 escaped by a backslash; arbitrary character codes may be specified as |
141 escaped by a backslash; arbitrary character codes may be specified as |
142 ``\<^verbatim>\<open>\\<close>\<open>ddd\<close>'', with three decimal digits. Alternative strings according to |
142 ``\<^verbatim>\<open>\\<close>\<open>ddd\<close>'', with three decimal digits. Alternative strings according to |
181 Entity @{syntax name} usually refers to any name of types, constants, |
181 Entity @{syntax name} usually refers to any name of types, constants, |
182 theorems etc.\ Quoted strings provide an escape for non-identifier names or |
182 theorems etc.\ Quoted strings provide an escape for non-identifier names or |
183 those ruled out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>). |
183 those ruled out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>). |
184 |
184 |
185 @{rail \<open> |
185 @{rail \<open> |
186 @{syntax_def name}: @{syntax ident} | @{syntax longident} | |
186 @{syntax_def name}: @{syntax short_ident} | @{syntax long_ident} | |
187 @{syntax symident} | @{syntax nat} | @{syntax string} |
187 @{syntax sym_ident} | @{syntax nat} | @{syntax string} |
188 ; |
188 ; |
189 @{syntax_def par_name}: '(' @{syntax name} ')' |
189 @{syntax_def par_name}: '(' @{syntax name} ')' |
190 \<close>} |
190 \<close>} |
191 \<close> |
191 \<close> |
192 |
192 |
219 plain identifiers in the outer language may be used as inner language |
219 plain identifiers in the outer language may be used as inner language |
220 content without delimiters. |
220 content without delimiters. |
221 |
221 |
222 @{rail \<open> |
222 @{rail \<open> |
223 @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} | |
223 @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} | |
224 @{syntax ident} | @{syntax longident} | @{syntax symident} | |
224 @{syntax short_ident} | @{syntax long_ident} | @{syntax sym_ident} | |
225 @{syntax var} | @{syntax typefree} | @{syntax typevar} | @{syntax nat} |
225 @{syntax term_var} | @{syntax type_ident} | @{syntax type_var} | @{syntax nat} |
226 \<close>} |
226 \<close>} |
227 \<close> |
227 \<close> |
228 |
228 |
229 |
229 |
230 subsection \<open>Comments \label{sec:comments}\<close> |
230 subsection \<open>Comments \label{sec:comments}\<close> |
302 @{rail \<open> |
302 @{rail \<open> |
303 @{syntax_def named_inst}: variable '=' (type | term) |
303 @{syntax_def named_inst}: variable '=' (type | term) |
304 ; |
304 ; |
305 @{syntax_def named_insts}: (named_inst @'and' +) |
305 @{syntax_def named_insts}: (named_inst @'and' +) |
306 ; |
306 ; |
307 variable: @{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar} |
307 variable: @{syntax name} | @{syntax term_var} | @{syntax type_ident} | @{syntax type_var} |
308 \<close>} |
308 \<close>} |
309 |
309 |
310 Type declarations and definitions usually refer to @{syntax typespec} on the |
310 Type declarations and definitions usually refer to @{syntax typespec} on the |
311 left-hand side. This models basic type constructor application at the outer |
311 left-hand side. This models basic type constructor application at the outer |
312 syntax level. Note that only plain postfix notation is available here, but |
312 syntax level. Note that only plain postfix notation is available here, but |
313 no infixes. |
313 no infixes. |
314 |
314 |
315 @{rail \<open> |
315 @{rail \<open> |
316 @{syntax_def typespec}: |
316 @{syntax_def typespec}: |
317 (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name} |
317 (() | @{syntax type_ident} | '(' ( @{syntax type_ident} + ',' ) ')') @{syntax name} |
318 ; |
318 ; |
319 @{syntax_def typespec_sorts}: |
319 @{syntax_def typespec_sorts}: |
320 (() | (@{syntax typefree} ('::' @{syntax sort})?) | |
320 (() | (@{syntax type_ident} ('::' @{syntax sort})?) | |
321 '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name} |
321 '(' ( (@{syntax type_ident} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name} |
322 \<close>} |
322 \<close>} |
323 \<close> |
323 \<close> |
324 |
324 |
325 |
325 |
326 subsection \<open>Term patterns and declarations \label{sec:term-decls}\<close> |
326 subsection \<open>Term patterns and declarations \label{sec:term-decls}\<close> |
384 Attributes have their own ``semi-inner'' syntax, in the sense that input |
384 Attributes have their own ``semi-inner'' syntax, in the sense that input |
385 conforming to @{syntax args} below is parsed by the attribute a second time. |
385 conforming to @{syntax args} below is parsed by the attribute a second time. |
386 The attribute argument specifications may be any sequence of atomic entities |
386 The attribute argument specifications may be any sequence of atomic entities |
387 (identifiers, strings etc.), or properly bracketed argument lists. Below |
387 (identifiers, strings etc.), or properly bracketed argument lists. Below |
388 @{syntax atom} refers to any atomic entity, including any @{syntax keyword} |
388 @{syntax atom} refers to any atomic entity, including any @{syntax keyword} |
389 conforming to @{syntax symident}. |
389 conforming to @{syntax sym_ident}. |
390 |
390 |
391 @{rail \<open> |
391 @{rail \<open> |
392 @{syntax_def atom}: @{syntax name} | @{syntax typefree} | |
392 @{syntax_def atom}: @{syntax name} | @{syntax type_ident} | |
393 @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} | |
393 @{syntax type_var} | @{syntax term_var} | @{syntax nat} | @{syntax float} | |
394 @{syntax keyword} | @{syntax cartouche} |
394 @{syntax keyword} | @{syntax cartouche} |
395 ; |
395 ; |
396 arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']' |
396 arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']' |
397 ; |
397 ; |
398 @{syntax_def args}: arg * |
398 @{syntax_def args}: arg * |