--- a/CookBook/Package/Ind_Interface.thy Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy Sun Feb 15 18:58:21 2009 +0000
@@ -1,5 +1,5 @@
theory Ind_Interface
-imports "../Base" Simple_Inductive_Package
+imports "../Base" "../Parsing" Simple_Inductive_Package
begin
section {* The Interface \label{sec:ind-interface} *}
@@ -7,10 +7,10 @@
text {*
The purpose of the package we show next is that the user just specifies the
inductive predicate by stating some introduction rules and then the packages
- makes the equivalent definition and derives from it useful properties.
+ makes the equivalent definition and derives from it the needed properties.
To be able to write down the specification in Isabelle, we have to introduce
a new command (see Section~\ref{sec:newcommand}). As the keyword for the new
- command we use \simpleinductive{}. The specifications corresponding to our
+ command we chose \simpleinductive{}. The specifications corresponding to our
examples described earlier are:
*}
@@ -33,7 +33,8 @@
accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
text {*
- We expect a constant (or constants) with possible typing annotations and a
+ After the keyword we expect a constant (or constants) with possible typing
+ annotations and a
list of introduction rules. While these specifications are all
straightforward, there is a technicality we like to deal with to do with
fixed parameters and locales. Remember we pointed out that the parameter
@@ -46,8 +47,8 @@
*}
text_raw {*
-\begin{figure}[p]
-\begin{isabelle}
+ \begin{figure}[p]
+ \begin{isabelle}
*}
simple_inductive
trcl' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -72,18 +73,34 @@
where
accpartI: "(\<forall>y. R y x \<longrightarrow> accpart'' y) \<Longrightarrow> accpart'' x"
text_raw {*
-\end{isabelle}
-\caption{The first definition is for the transitive closure where the
-relation @{text R} is explicitly fixed. Simiraly the second definition
-of the accessible part of the relation @{text R}. The last two definitions
-specify the same inductive predicates, but this time defined inside
-a locale.\label{fig:inddefsfixed}}
-\end{figure}
+ \end{isabelle}
+ \caption{The first definition is for the transitive closure where the
+ relation @{text R} is explicitly fixed. Simiraly the second definition
+ of the accessible part of the relation @{text R}. The last two definitions
+ specify the same inductive predicates, but this time defined inside
+ a locale.\label{fig:inddefsfixed}}
+ \end{figure}
*}
text {*
-\begin{figure}[p]
-\begin{isabelle}
+ From a high-level perspective the package consists of 6 subtasks:
+
+ \begin{itemize}
+ \item reading the various parts of specification (i.e.~parser),
+ \item transforming the parser outut into an internal
+ (typed) datastructure,
+ \item making the definitions,
+ \item deriving the induction principles,
+ \item deriving the introduction rules, and
+ \item storing the results in the given theory to be visible
+ to the user.
+ \end{itemize}
+
+*}
+
+text {*
+ \begin{figure}[p]
+ \begin{isabelle}
\railnontermfont{\rmfamily\itshape}
\railterm{simpleinductive,where,for}
\railalias{simpleinductive}{\simpleinductive{}}
@@ -94,37 +111,102 @@
(where (thmdecl? prop + '|'))?
;
\end{rail}
-\end{isabelle}
-\caption{A railroad diagram describing the syntax of \simpleinductive{}.
-The \emph{target} indicates an optional locale; the \emph{fixes} are an
-\isacommand{and}-separated list of names for the inductive predicates (they
-can also contain typing- and syntax anotations); similarly the \emph{fixes}
-after \isacommand{for} to indicate fixed parameters; \emph{prop} stands for a
-introduction rule with an optional theorem declaration (\emph{thmdecl}).
-\label{fig:railroad}}
-\end{figure}
+ \end{isabelle}
+ \caption{A railroad diagram describing the syntax of \simpleinductive{}.
+ The \emph{target} indicates an optional locale; the \emph{fixes} are an
+ \isacommand{and}-separated list of names for the inductive predicates (they
+ can also contain typing- and syntax anotations); similarly the \emph{fixes}
+ after \isacommand{for} to indicate fixed parameters; \emph{prop} stands for a
+ introduction rule with an optional theorem declaration (\emph{thmdecl}).
+ \label{fig:railroad}}
+ \end{figure}
*}
text {*
- The syntax of the \simpleinductive{} command can be described by the
- railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less
- translates directly into the parser:
+ For the first subtask, the syntax of the \simpleinductive{} command can be
+ described by the railroad diagram in Figure~\ref{fig:railroad}. This diagram
+ more or less translates directly into the parser:
+
@{ML_chunk [display,gray] parser}
- which we also described in Section~\ref{sec:parsingspecs}. Its return value
- of this parser is a locale, the predicates, parameters and specifications of
- the introduction rules. This is all the information we need to call the package.
+ which we described in Section~\ref{sec:parsingspecs}. If we feed into the
+ parser the string (which corresponds to our definition of @{term even} and
+ @{term odd}):
+
+ @{ML_response [display,gray]
+"let
+ val input = filtered_input
+ (\"even and odd \" ^
+ \"where \" ^
+ \" even0[intro]: \\\"even 0\\\" \" ^
+ \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^
+ \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
+in
+ parse spec_parser input
+end"
+"((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),
+ [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
+ ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
+ ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
+*}
+
+
+text {*
+ then we get back a locale (in this case @{ML NONE}), the predicates (with type
+ and syntax annotations), the parameters (similar as the predicates) and
+ the specifications of the introduction rules.
+
+
+
+ This is all the information we
+ need for calling the package and setting up the keyword. The latter is
+ done in Lines 6 and 7 in the code below.
@{ML_chunk [display,gray,linenos] syntax}
+
+ We call @{ML OuterSyntax.command} with the kind-indicator @{ML
+ OuterKeyword.thy_decl} since the package does not need to open up any goal
+ state (see Section~\ref{sec:newcommand}). Note that the predicates and
+ parameters are at the moment only some ``naked'' variables: they have no
+ type yet (even if we annotate them with types) and they are also no defined
+ constants yet (which the predicates will eventually be). In Lines 1 to 4 we
+ gather the information from the parser to be processed further. The locale
+ is passed as argument to the function @{ML
+ Toplevel.local_theory}.\footnote{FIXME Is this already described?} The other
+ arguments, i.e.~the predicates, parameters and intro rule specifications,
+ are passed to the function @{ML add_inductive in SimpleInductivePackage}
+ (Line 4).
- The locale is passed as argument to the function
- @{ML Toplevel.local_theory}.\footnote{FIXME Is this already described?} The
- other arguments, i.e.~the predicates, parameters and specifications, are passed
- to the function @{ML add_inductive in SimpleInductivePackage} (Line 4). The
- actual command is defined in Lines 6 and 7. We called @{ML OuterSyntax.command}
- with the kind-indicator @{ML OuterKeyword.thy_decl} since the package does
- not need to open up any goal state (see Section~\ref{sec:newcommand}).
+ We now come to the second subtask of the package, namely transforming the
+ parser output into some internal datastructures that can be processed further.
+ Remember that at the moment the introduction rules are just strings, and even
+ if the predicates and parameters can contain some typing annotations, they
+ are not yet in any way reflected in the introduction rules. So the task of
+ @{ML add_inductive in SimpleInductivePackage} is to transform the strings
+ into properly typed terms. For this it can use the function
+ @{ML read_specification in Specification}. This function takes some constants
+ with possible typing annotations and some rule specifications and attempts to
+ find a type according to the given type constraints and the type constraints
+ by the surrounding (local theory). However this function is a bit
+ too general for our purposes: we want that each introduction rule has only
+ name (for example @{text even0} or @{text evenS}), if a name is given at all.
+ The function @{ML read_specification in Specification} however allows more
+ than one rule. Since it is quite convenient to rely on this function (instead of
+ building your own) we just quick ly write a wrapper function that translates
+ between our specific format and the general format expected by
+ @{ML read_specification in Specification}. The code of this wrapper is as follows:
+
+ @{ML_chunk [display,gray,linenos] read_specification}
+
+ It takes a list of constants, a list of rule specifications and a local theory
+ as input. Does the transformation of the rule specifications in Line 3; calls
+ the function and transforms the now typed rule specifications back into our
+ format and returns the type parameter and typed rule specifications.
+
+
+ @{ML_chunk [display,gray,linenos] add_inductive}
+
In order to add a new inductive predicate to a theory with the help of our
package, the user must \emph{invoke} it. For every package, there are
@@ -136,7 +218,7 @@
actually make the definition, the type and introduction rules have to be
parsed. In contrast, internal invocation means that the package is called by
some other package. For example, the function definition package
- \cite{Krauss-IJCAR06} calls the inductive definition package to define the
+ calls the inductive definition package to define the
graph of the function. However, it is not a good idea for the function
definition package to pass the introduction rules for the function graph to
the inductive definition package as strings. In this case, it is better to