--- a/ProgTutorial/FirstSteps.thy Mon Jul 19 15:44:13 2010 +0100
+++ b/ProgTutorial/FirstSteps.thy Tue Jul 20 13:34:44 2010 +0100
@@ -124,7 +124,7 @@
\end{tabular}
\end{quote}
- Note that no parentheses are given this time. Note also that the included
+ Note that no parentheses are given in this case. Note also that the included
ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle
is unable to record all file dependencies, which is a nuisance if you have
to track down errors.
@@ -232,46 +232,35 @@
Most often you want to inspect data of Isabelle's basic data structures,
namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
- and @{ML_type 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} from the structure
- @{ML_struct Syntax}. For more convenience, we bind this function to the
- toplevel.
+ and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions,
+ which we will explain in more detail in Section \ref{sec:pretty}. For now
+ we just use the functions @{ML_ind writeln in Pretty} from the structure
+ @{ML_struct Pretty} and @{ML_ind pretty_term in Syntax} from the structure
+ @{ML_struct Syntax}. For more convenience, we bind them to the toplevel.
*}
ML{*val string_of_term = Syntax.string_of_term*}
+ML{*val pretty_term = Syntax.pretty_term*}
+ML{*val pwriteln = Pretty.writeln*}
text {*
- It can now be used as follows
+ They can now be used as follows
@{ML_response_fake [display,gray]
- "string_of_term @{context} @{term \"1::nat\"}"
- "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
-
- We obtain a string corrsponding to the term @{term [show_types] "1::nat"} with some
- additional information encoded in it. The string can be properly printed by
- using either the function @{ML writeln} or @{ML tracing}:
-
- @{ML_response_fake [display,gray]
- "writeln (string_of_term @{context} @{term \"1::nat\"})"
+ "pwriteln (pretty_term @{context} @{term \"1::nat\"})"
"\"1\""}
- or
-
- @{ML_response_fake [display,gray]
- "tracing (string_of_term @{context} @{term \"1::nat\"})"
- "\"1\""}
-
- If there are more than one term to be printed, you can use the
- function @{ML_ind commas in Library} to separate them.
+ If there is more than one term to be printed, you can use the
+ function @{ML_ind enum in Pretty} to separate them.
*}
ML{*fun string_of_terms ctxt ts =
commas (map (string_of_term ctxt) ts)*}
+ML{*fun pretty_terms ctxt ts =
+ Pretty.enum "," "" "" (map (pretty_term ctxt) ts)*}
text {*
- You can also print out terms together with typing information.
+ You can also print out terms together with their typing information.
For this you need to set the reference @{ML_ind show_types in Syntax}
to @{ML true}.
*}
@@ -279,10 +268,10 @@
ML{*show_types := true*}
text {*
- Now @{ML string_of_term} prints out
+ Now @{ML pretty_term} prints out
@{ML_response_fake [display, gray]
- "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
+ "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})"
"(1::nat, x::'a)"}
where @{text 1} and @{text x} are displayed with their inferred type.
@@ -294,7 +283,7 @@
(*>*)
text {*
@{ML_response_fake [display, gray]
- "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
+ "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})"
"(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
where @{term Pair} is the term-constructor for products.
@@ -304,28 +293,32 @@
(*<*)ML %linenos {*show_types := false; show_all_types := false*}
(*>*)
text {*
- A @{ML_type cterm} can be transformed into a string by the following function.
+ A @{ML_type cterm} can be printed with the following function.
*}
ML{*fun string_of_cterm ctxt ct =
string_of_term ctxt (term_of ct)*}
+ML{*fun pretty_cterm ctxt ct =
+ pretty_term ctxt (term_of ct)*}
text {*
- In this example the function @{ML_ind term_of in Thm} extracts the @{ML_type
- term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can again be
- printed with @{ML commas}.
+ Here the function @{ML_ind term_of in Thm} extracts the @{ML_type
+ term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can be
+ printed again with @{ML enum in Pretty}.
*}
ML{*fun string_of_cterms ctxt cts =
commas (map (string_of_cterm ctxt) cts)*}
+ML{*fun pretty_cterms ctxt cts =
+ Pretty.enum "," "" "" (map (pretty_cterm ctxt) cts)*}
text {*
The easiest way to get the string of a theorem is to transform it
into a @{ML_type term} using the function @{ML_ind prop_of in Thm}.
*}
-ML{*fun string_of_thm ctxt thm =
- string_of_term ctxt (prop_of thm)*}
+ML{*fun pretty_thm ctxt thm =
+ pretty_term ctxt (prop_of thm)*}
text {*
Theorems include schematic variables, such as @{text "?P"},
@@ -335,7 +328,7 @@
instantiation of @{text "?P"} and @{text "?Q"}.
@{ML_response_fake [display, gray]
- "tracing (string_of_thm @{context} @{thm conjI})"
+ "pwriteln (pretty_thm @{context} @{thm conjI})"
"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
However, in order to improve the readability when printing theorems, we
@@ -351,38 +344,39 @@
thm'
end
-fun string_of_thm_no_vars ctxt thm =
- string_of_term ctxt (prop_of (no_vars ctxt thm))*}
+fun pretty_thm_no_vars ctxt thm =
+ pretty_term ctxt (prop_of (no_vars ctxt thm))*}
+
text {*
With this function, theorem @{thm [source] conjI} is now printed as follows:
@{ML_response_fake [display, gray]
- "tracing (string_of_thm_no_vars @{context} @{thm conjI})"
+ "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"
"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
Again the function @{ML commas} helps with printing more than one theorem.
*}
-ML{*fun string_of_thms ctxt thms =
- commas (map (string_of_thm ctxt) thms)
+ML{*fun pretty_thms ctxt thms =
+ Pretty.enum "," "" "" (map (pretty_thm ctxt) thms)
-fun string_of_thms_no_vars ctxt thms =
- commas (map (string_of_thm_no_vars ctxt) thms) *}
+fun pretty_thms_no_vars ctxt thms =
+ Pretty.enum "," "" "" (map (pretty_thm_no_vars ctxt) thms)*}
text {*
The printing functions for types are
*}
-ML{*fun string_of_typ ctxt ty = Syntax.string_of_typ ctxt ty
-fun string_of_typs ctxt tys = commas (map (string_of_typ ctxt) tys)*}
+ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
+fun pretty_typs ctxt tys = Pretty.commas (map (pretty_typ ctxt) tys)*}
text {*
respectively ctypes
*}
-ML{*fun string_of_ctyp ctxt cty = string_of_typ ctxt (typ_of cty)
-fun string_of_ctyps ctxt ctys = commas (map (string_of_ctyp ctxt) ctys)*}
+ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
+fun pretty_ctyps ctxt ctys = Pretty.commas (map (pretty_ctyp ctxt) ctys)*}
text {*
\begin{readmore}
@@ -398,15 +392,15 @@
\emph{not} print out information as
@{ML_response_fake [display,gray]
-"tracing \"First half,\";
-tracing \"and second half.\""
+"writeln \"First half,\";
+writeln \"and second half.\""
"First half,
and second half."}
but as a single string with appropriate formatting. For example
@{ML_response_fake [display,gray]
-"tracing (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
+"writeln (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
"First half,
and second half."}
@@ -416,7 +410,7 @@
and inserts newlines in between each element.
@{ML_response_fake [display, gray]
- "tracing (cat_lines [\"foo\", \"bar\"])"
+ "writeln (cat_lines [\"foo\", \"bar\"])"
"foo
bar"}
@@ -427,7 +421,6 @@
Most of the basic string functions of Isabelle are defined in
@{ML_file "Pure/library.ML"}.
\end{readmore}
-
*}
@@ -897,12 +890,16 @@
ML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
+ML {*
+pretty_thms_no_vars
+*}
+
text {*
The result can be printed out as follows.
@{ML_response_fake [gray,display]
-"foo_thm |> string_of_thms_no_vars @{context}
- |> tracing"
+"foo_thm |> pretty_thms_no_vars @{context}
+ |> pwriteln"
"True, False \<Longrightarrow> P"}
You can also refer to the current simpset via an antiquotation. To illustrate