--- a/ProgTutorial/FirstSteps.thy Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Sat Oct 03 19:10:23 2009 +0200
@@ -120,7 +120,7 @@
to track down errors.
*}
-section {* Debugging and Printing\label{sec:printing} *}
+section {* Printing and Debugging\label{sec:printing} *}
text {*
During development you might find it necessary to inspect some data in your
@@ -211,7 +211,7 @@
thm}. Isabelle contains elaborate pretty-printing functions for printing
them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
are a bit unwieldy. One way to transform a term into a string is to use the
- function @{ML_ind string_of_term in Syntax} in structure @{ML_struct
+ function @{ML_ind string_of_term in Syntax} in the structure @{ML_struct
Syntax}, which we bind for more convenience to the toplevel.
*}
@@ -635,7 +635,7 @@
together. We have already seen such plumbing in the function @{ML
apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such
- plumbing is also needed in situations where a functions operate over lists,
+ plumbing is also needed in situations where a function operate over lists,
but one calculates only with a single element. An example is the function
@{ML_ind check_terms in Syntax}, whose purpose is to type-check a list
of terms.
@@ -653,8 +653,8 @@
*}
text {*
- In this example we obtain three terms in which @{text m} and @{text n} are of
- type @{typ "nat"}. If you have only a single term, then @{ML
+ In this example we obtain three terms whose variables @{text m} and @{text
+ n} are of type @{typ "nat"}. If you have only a single term, then @{ML
check_terms in Syntax} needs plumbing. This can be done with the function
@{ML singleton}.\footnote{There is already a function @{ML check_term in
Syntax} in the Isabelle sources that is defined in terms of @{ML singleton}
@@ -713,7 +713,7 @@
the function @{ML_ind theory_name in Context}.
Note, however, that antiquotations are statically linked, that is their value is
- determined at ``compile-time'', not ``run-time''. For example the function
+ determined at ``compile-time'', not at ``run-time''. For example the function
*}
ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
@@ -743,7 +743,7 @@
The point of these antiquotations is that referring to theorems in this way
makes your code independent from what theorems the user might have stored
under this name (this becomes especially important when you deal with
- theorem lists; see Section \ref{sec:attributes}).
+ theorem lists; see Section \ref{sec:storing}).
You can also refer to the current simpset via an antiquotation. To illustrate
this we implement the function that extracts the theorem names stored in a
@@ -784,7 +784,7 @@
@{ML_ind define in LocalTheory}. This function is used below to define
the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
*}
-
+
local_setup %gray {*
LocalTheory.define Thm.internalK
((@{binding "TrueConj"}, NoSyn),
@@ -798,9 +798,16 @@
@{text "> "}~@{thm TrueConj_def}
\end{isabelle}
+ \begin{readmore}
+ The basic operations on bindings are implemented in
+ @{ML_file "Pure/General/binding.ML"}.
+ \end{readmore}
+
\footnote{\bf FIXME give a better example why bindings are important; maybe
give a pointer to \isacommand{local\_setup}; if not, then explain
why @{ML snd} is needed.}
+ \footnote{\bf FIXME: There should probably a separate section on binding, long-names
+ and sign.}
It is also possible to define your own antiquotations. But you should
exercise care when introducing new ones, as they can also make your code
@@ -1016,13 +1023,14 @@
"WrongRefData.get @{theory}"
"ref []"}
- For updating the reference we use the following function.
+ For updating the reference we use the following function
*}
ML{*fun ref_update n = WrongRefData.map
(fn r => let val _ = r := n::(!r) in r end)*}
text {*
+ which takes an integer and adds it to the content of the reference.
As above we update the reference with the command
\isacommand{setup}.
*}
@@ -1051,7 +1059,7 @@
Now imagine how often you go backwards and forwards in your proof scripts.
By using references in Isabelle code, you are bound to cause all
- hell to break lose. Therefore observe the coding convention:
+ hell to break loose. Therefore observe the coding convention:
Do not use references for storing data!
\begin{readmore}
@@ -1062,46 +1070,6 @@
tables and symtables in @{ML_file "Pure/General/table.ML"}.
\end{readmore}
- A special instance of the data storage mechanism described above are
- configuration values. They are used to enable users to configure tools
- without having to resort to the ML-level (and also to avoid
- references). Assume you want the user to control three values, say @{text
- bval} containing a boolean, @{text ival} containing an integer and @{text
- sval} containing a string. These values can be declared by
-*}
-
-ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
-val (ival, setup_ival) = Attrib.config_int "ival" 0
-val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
-
-text {*
- where each value needs to be given a default. To enable these values, they need to
- be set up with
-*}
-
-setup %gray {*
- setup_bval #>
- setup_ival
-*}
-
-text {*
- The user can now manipulate the values from the user-level of Isabelle
- with the command
-*}
-
-declare [[bval = true, ival = 3]]
-
-text {*
- On the ML-level these values can be retrieved using the
- function @{ML Config.get}.
-
- @{ML_response [display,gray] "Config.get @{context} bval" "true"}
-
- \begin{readmore}
- For more information about configuration values see
- @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
- \end{readmore}
-
Storing data in a proof context is done in a similar fashion. The
corresponding functor is @{ML_funct_ind ProofDataFun}. With the
following code we can store a list of terms in a proof context.
@@ -1155,9 +1123,112 @@
theory. Once we throw away the contexts, we have no access to their
associated data. This is different to theories, where the command
\isacommand{setup} registers the data with the current and future
- theories, and therefore can access the data potentially indefinitely.
+ theories, and therefore can access the data potentially
+ indefinitely.\footnote{\bf FIXME: check this; it seems that is in
+ conflict with the statements below.}
+
+ \footnote{\bf FIXME: Say something about generic contexts.}
+
+ There are two special instances of the data storage mechanism described
+ above. The first instance are named theorem lists. Since storing theorems in a list
+ is such a common task, there is the special functor @{ML_funct_ind Named_Thms}.
+ To obtain a named theorem list, you just declare
+*}
+
+ML{*structure FooRules = Named_Thms
+ (val name = "foo"
+ val description = "Theorems for foo") *}
+
+text {*
+ and set up the @{ML_struct FooRules} with the command
+*}
+
+setup %gray {* FooRules.setup *}
+
+text {*
+ This code declares a data container where the theorems are stored,
+ an attribute @{text foo} (with the @{text add} and @{text del} options
+ for adding and deleting theorems) and an internal ML-interface to retrieve and
+ modify the theorems.
+
+ Furthermore, the facts are made available on the user-level under the dynamic
+ fact name @{text foo}. For example you can declare three lemmas to be of the kind
+ @{text foo} by:
*}
+lemma rule1[foo]: "A" sorry
+lemma rule2[foo]: "B" sorry
+lemma rule3[foo]: "C" sorry
+
+text {* and undeclare the first one by: *}
+
+declare rule1[foo del]
+
+text {* and query the remaining ones with:
+
+ \begin{isabelle}
+ \isacommand{thm}~@{text "foo"}\\
+ @{text "> ?C"}\\
+ @{text "> ?B"}
+ \end{isabelle}
+
+ On the ML-level, we can add theorems to the list with @{ML FooRules.add_thm}:
+*}
+
+setup %gray {*
+ Context.theory_map (FooRules.add_thm @{thm TrueI})
+*}
+
+text {*
+ The rules in the list can be retrieved using the function
+ @{ML FooRules.get}:
+
+ @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"True\", \"?C\",\"?B\"]"}
+
+ \begin{readmore}
+ For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
+ \end{readmore}
+
+ The second special instance of the data storage mechanism are configuration
+ values. They are used to enable users to configure tools without having to
+ resort to the ML-level (and also to avoid references). Assume you want the
+ user to control three values, say @{text bval} containing a boolean, @{text
+ ival} containing an integer and @{text sval} containing a string. These
+ values can be declared by
+*}
+
+ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
+val (ival, setup_ival) = Attrib.config_int "ival" 0
+val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
+
+text {*
+ where each value needs to be given a default. To enable these values, they need to
+ be set up with
+*}
+
+setup %gray {*
+ setup_bval #>
+ setup_ival
+*}
+
+text {*
+ The user can now manipulate the values from the user-level of Isabelle
+ with the command
+*}
+
+declare [[bval = true, ival = 3]]
+
+text {*
+ On the ML-level these values can be retrieved using the
+ function @{ML Config.get}.
+
+ @{ML_response [display,gray] "Config.get @{context} bval" "true"}
+
+ \begin{readmore}
+ For more information about configuration values see
+ @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
+ \end{readmore}
+*}
(**************************************************)