|
1 |
|
2 %FIXME |
|
3 % - examples (!?) |
|
4 |
1 |
5 |
2 \chapter{Isar document syntax} |
6 \chapter{Isar document syntax} |
3 |
7 |
4 \section{Inner versus outer syntax} |
8 FIXME important note: inner versus outer syntax |
5 |
9 |
6 \section{Lexical matters} |
10 \section{Lexical matters} |
7 |
11 |
8 \section{Common syntax entities} |
12 \section{Common syntax entities} |
9 |
13 |
10 \subsection{Atoms} |
14 The Isar proof and theory language syntax has been carefully designed with |
11 |
15 orthogonality in mind. Many common syntax entities such that those for names, |
|
16 terms, types etc.\ have been factored out. Some of these basic syntactic |
|
17 entities usually represent the level of abstraction for error messages: e.g.\ |
|
18 some higher syntax element such as $\CONSTS$ referring to \railtoken{name} or |
|
19 \railtoken{type}, would really report a missing \railtoken{name} or |
|
20 \railtoken{type} rather than any of its constituent primitive tokens (as |
|
21 defined below). These quasi-tokens are represented in the syntax diagrams |
|
22 below using the same font as actual tokens (such as \railtoken{string}). |
|
23 |
|
24 |
|
25 \subsection{Names} |
|
26 |
|
27 Entity \railtoken{name} usually refers to any name of types, constants, |
|
28 theorems, etc.\ to be \emph{declared} or \emph{defined} (so qualified |
|
29 identifiers are excluded). Already existing objects are typically referenced |
|
30 by \railtoken{nameref}. |
|
31 |
|
32 \indexoutertoken{name}\indexoutertoken{nameref} |
12 \begin{rail} |
33 \begin{rail} |
13 name : ident | symident | string |
34 name : ident | symident | string |
14 ; |
35 ; |
15 |
|
16 nameref : name | longident |
36 nameref : name | longident |
17 ; |
37 ; |
18 |
38 \end{rail} |
19 text : nameref | verbatim |
39 |
20 ; |
|
21 \end{rail} |
|
22 |
40 |
23 \subsection{Comments} |
41 \subsection{Comments} |
24 |
42 |
25 \begin{rail} |
43 Large chunks of verbatim \railtoken{text} are usually given |
|
44 \railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\verb|*}|; for convenience, |
|
45 any of the smaller text entities (\railtoken{ident}, \railtoken{string} etc.) |
|
46 are admitted as well. Almost any of the Isar commands may be annotated by a |
|
47 marginal comment: \texttt{--} \railtoken{text}. Note that this kind of |
|
48 comment is actually part of the language, while source level comments |
|
49 \verb|(*|~\verb|*)| are already stripped at the lexical level. A few commands |
|
50 such as $\PROOFNAME$ admit some parts to be mark with a ``level of interest'': |
|
51 currently only \texttt{\%} for ``boring, don't read this''. |
|
52 |
|
53 \indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest} |
|
54 \begin{rail} |
|
55 text : verbatim | nameref |
|
56 ; |
26 comment : (() | '--' text) |
57 comment : (() | '--' text) |
27 ; |
58 ; |
28 interest : (() | '\%') |
59 interest : (() | '\%') |
29 ; |
60 ; |
30 \end{rail} |
61 \end{rail} |
31 |
62 |
32 |
63 |
33 \subsection{Sorts and arities} |
64 \subsection{Sorts and arities} |
34 |
65 |
|
66 The syntax of sorts and arities is given directly at the outer level. Note |
|
67 that this in contrast to that types and terms (see below). Only few commands |
|
68 ever refer to sorts or arities explicitly. |
|
69 |
|
70 \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity} |
35 \begin{rail} |
71 \begin{rail} |
36 sort : nameref | lbrace (nameref * ',') rbrace |
72 sort : nameref | lbrace (nameref * ',') rbrace |
37 ; |
73 ; |
38 arity : ( () | '(' (sort + ',') ')' ) sort |
74 arity : ( () | '(' (sort + ',') ')' ) sort |
39 ; |
75 ; |
40 simple\-arity : ( () | '(' (sort + ',') ')' ) nameref |
76 simplearity : ( () | '(' (sort + ',') ')' ) nameref |
41 ; |
77 ; |
42 \end{rail} |
78 \end{rail} |
43 |
79 |
44 |
80 |
45 \subsection{Terms and Types} |
81 \subsection{Types and terms} |
46 |
82 |
47 \begin{rail} |
83 The actual inner Isabelle syntax, i.e.\ that of types and terms, is far too |
48 |
84 flexible in order to be modeled explicitly at the outer theory level. |
49 \end{rail} |
85 Basically, any such entity would have to be quoted at the outer level to turn |
|
86 it into a single token, with the actual parsing deferred to some functions |
|
87 that read and type-check terms etc.\ (note that \railtoken{prop}s will be |
|
88 handled differently from plain \railtoken{term}s here). For convenience, the |
|
89 quotes may be omitted for any \emph{atomic} term or type (e.g.\ a single |
|
90 variable). |
|
91 |
|
92 \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop} |
|
93 \begin{rail} |
|
94 type : ident | longident | symident | typefree | typevar | string |
|
95 ; |
|
96 term : ident | longident | symident | var | textvar | nat | string |
|
97 ; |
|
98 prop : term |
|
99 ; |
|
100 \end{rail} |
|
101 |
|
102 Type definitions etc.\ usually refer to \railnonterm{typespec} on the |
|
103 left-hand side. This models basic type constructor application at the outer |
|
104 syntax level. Note that only plain postfix notation is available here, but no |
|
105 infixes. |
|
106 |
|
107 \indexouternonterm{typespec} |
|
108 \begin{rail} |
|
109 typespec : (() | typefree | '(' ( typefree + ',' ) ')') name |
|
110 ; |
|
111 \end{rail} |
|
112 |
|
113 |
|
114 \subsection{Term patterns} |
|
115 |
|
116 Statements like $\SHOWNAME$ involve propositions, some others like $\DEFNAME$ |
|
117 plain terms. Any of these usually admit automatic binding of schematic text |
|
118 variables by giving (optional) patterns $\IS{p@1 \dots p@n}$. For |
|
119 \railtoken{prop}s the $\CONCLNAME$ part refers to the conclusion only, in case |
|
120 actual rules are involved, rather than atomic propositions. |
|
121 |
|
122 \indexouternonterm{termpat}\indexouternonterm{proppat} |
|
123 \begin{rail} |
|
124 termpat : '(' (term + 'is' ) ')' |
|
125 ; |
|
126 proppat : '(' (() | (prop + 'is' )) (() | 'concl' (prop + 'is' )) ')' |
|
127 ; |
|
128 \end{rail} |
|
129 |
50 |
130 |
51 \subsection{Mixfix annotations} |
131 \subsection{Mixfix annotations} |
52 |
132 |
53 |
133 Mixfix annotations specify concrete \emph{inner} syntax. Some commands such |
54 \subsection{} |
134 as $\TYPES$ admit infixes only, while $\CONSTS$ etc.\ support the full range |
55 |
135 of general mixfixes and binders. |
56 \subsection{} |
136 |
57 |
137 \indexouternonterm{infix}\indexouternonterm{mixfix} |
58 \subsection{} |
138 \begin{rail} |
|
139 infix : '(' ('infixl' | 'infixr') (() | string) nat ')' |
|
140 ; |
|
141 |
|
142 mixfix : infix | string (() | '[' (nat + ',') ']') (() | nat) | |
|
143 'binder' string (() | '[' (nat + ',') ']') nat |
|
144 ; |
|
145 \end{rail} |
|
146 |
|
147 |
|
148 \subsection{Attributes and theorem specifications}\label{sec:syn-att} |
|
149 |
|
150 Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own |
|
151 ``semi-inner'' syntax, which does not have to be atomic at the outer level |
|
152 unlike that of types and terms. Instead, the attribute argument |
|
153 specifications may be any sequence of atomic entities (identifiers, strings |
|
154 etc.), or properly bracketed argument lists. Below \railtoken{atom} refers to |
|
155 any atomic entity (\railtoken{ident}, \railtoken{longident}, |
|
156 \railtoken{symident} etc.), including keywords that conform to |
|
157 \railtoken{symident}, but do not coincide with actual command names. |
|
158 |
|
159 \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes} |
|
160 \begin{rail} |
|
161 args : (atom | '(' (args *) ')' | '[' (args *) ']' | lbrace (args *) rbrace) * |
|
162 ; |
|
163 attributes : '[' (name args + ',') ']' |
|
164 ; |
|
165 \end{rail} |
|
166 |
|
167 Theorem specifications come in three flavours: \railnonterm{thmdecl} usually |
|
168 refers to the result of a goal statement (such as $\SHOWNAME$), |
|
169 \railnonterm{thmdef} collects lists of existing theorems (as in $\NOTENAME$), |
|
170 \railnonterm{thmref} refers to any list of existing theorems (e.g.\ occurring |
|
171 as proof method arguments). Any of these may include lists of attributes, |
|
172 which are applied to the preceding theorem or list of theorems. |
|
173 |
|
174 \indexouternonterm{thmdecl}\indexouternonterm{thmdef}\indexouternonterm{thmref} |
|
175 \begin{rail} |
|
176 thmdecl : (() | name) (() | attributes) ':' |
|
177 ; |
|
178 thmdef : (() | name) (() | attributes) '=' |
|
179 ; |
|
180 thmref : (name (() | attributes) +) |
|
181 ; |
|
182 \end{rail} |
|
183 |
|
184 |
|
185 \subsection{Proof methods}\label{sec:syn-meth} |
|
186 |
|
187 Proof methods are either basic ones, or expressions composed of methods via |
|
188 ``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternatives), |
|
189 ``\texttt{?}'' (try), ``\texttt{*}'' (repeat, ${} \ge 0$ times), |
|
190 ``\texttt{+}'' (repeat, ${} > 0$ times). In practice, proof methods are |
|
191 typically just a comma separeted list of \railtoken{name}~\railtoken{args} |
|
192 specifications. Thus the syntax is similar to that of attributes, with plain |
|
193 parentheses instead of square brackets (see also \S\ref{sec:syn-att}). Note |
|
194 that parentheses may be dropped for methods without arguments. |
|
195 |
|
196 \indexouternonterm{method} |
|
197 \begin{rail} |
|
198 method : (name args | (name | '(' method ')') (() | '?' | '*' | '+')) + (',' | '|') |
|
199 ; |
|
200 \end{rail} |
59 |
201 |
60 |
202 |
61 %%% Local Variables: |
203 %%% Local Variables: |
62 %%% mode: latex |
204 %%% mode: latex |
63 %%% TeX-master: "isar-ref" |
205 %%% TeX-master: "isar-ref" |