106 *} |
106 *} |
107 |
107 |
108 text {* |
108 text {* |
109 The syntax of the \simpleinductive{} command can be described by the |
109 The syntax of the \simpleinductive{} command can be described by the |
110 railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less |
110 railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less |
111 translates directly into the parser |
111 translates directly into the parser: |
112 |
112 |
113 @{ML_chunk [display,gray,linenos] parser} |
113 @{ML_chunk [display,gray] parser} |
114 |
114 |
115 which we also described in Section~\ref{sec:parsingspecs} |
115 which we also described in Section~\ref{sec:parsingspecs}. Its return value |
|
116 of this parser is a locale, the predicates, parameters and specifications of |
|
117 the introduction rules. This is all the information we need to call the package. |
|
118 |
|
119 @{ML_chunk [display,gray,linenos] syntax} |
|
120 |
|
121 The locale is passed as argument to the function |
|
122 @{ML Toplevel.local_theory}.\footnote{FIXME Is this already described?} The |
|
123 other arguments, i.e.~the predicates, parameters and specifications, are passed |
|
124 to the function @{ML add_inductive in SimpleInductivePackage} (Line 4). The |
|
125 actual command is defined in Lines 6 and 7. We called @{ML OuterSyntax.command} |
|
126 with the kind-indicator @{ML OuterKeyword.thy_decl} since the package does |
|
127 not need to open up any goal state (see Section~\ref{sec:newcommand}). |
116 |
128 |
117 In order to add a new inductive predicate to a theory with the help of our |
129 In order to add a new inductive predicate to a theory with the help of our |
118 package, the user must \emph{invoke} it. For every package, there are |
130 package, the user must \emph{invoke} it. For every package, there are |
119 essentially two different ways of invoking it, which we will refer to as |
131 essentially two different ways of invoking it, which we will refer to as |
120 \emph{external} and \emph{internal}. By external invocation we mean that the |
132 \emph{external} and \emph{internal}. By external invocation we mean that the |
303 |
315 |
304 We now have all the necessary tools to write the parser for our |
316 We now have all the necessary tools to write the parser for our |
305 \isa{\isacommand{simple{\isacharunderscore}inductive}} command: |
317 \isa{\isacommand{simple{\isacharunderscore}inductive}} command: |
306 |
318 |
307 |
319 |
308 |
|
309 The definition of the parser \verb!ind_decl! closely follows the railroad |
|
310 diagram shown above. In order to make the code more readable, the structures |
|
311 @{ML_struct OuterParse} and @{ML_struct OuterKeyword} are abbreviated by |
|
312 \texttt{P} and \texttt{K}, respectively. Note how the parser combinator |
|
313 @{ML "!!!" in OuterParse} is used: once the keyword \texttt{where} |
|
314 has been parsed, a non-empty list of introduction rules must follow. |
|
315 Had we not used the combinator @{ML "!!!" in OuterParse}, a |
|
316 \texttt{where} not followed by a list of rules would have caused the parser |
|
317 to respond with the somewhat misleading error message |
|
318 |
|
319 \begin{verbatim} |
|
320 Outer syntax error: end of input expected, but keyword where was found |
|
321 \end{verbatim} |
|
322 |
|
323 rather than with the more instructive message |
|
324 |
|
325 \begin{verbatim} |
|
326 Outer syntax error: proposition expected, but terminator was found |
|
327 \end{verbatim} |
|
328 |
|
329 Once all arguments of the command have been parsed, we apply the function |
320 Once all arguments of the command have been parsed, we apply the function |
330 @{ML add_inductive in SimpleInductivePackage}, which yields a local theory |
321 @{ML add_inductive in SimpleInductivePackage}, which yields a local theory |
331 transformer of type @{ML_type "local_theory -> local_theory"}. Commands in |
322 transformer of type @{ML_type "local_theory -> local_theory"}. Commands in |
332 Isabelle/Isar are realized by transition transformers of type |
323 Isabelle/Isar are realized by transition transformers of type |
333 @{ML_type [display] "Toplevel.transition -> Toplevel.transition"} |
324 @{ML_type [display] "Toplevel.transition -> Toplevel.transition"} |