--- a/ProgTutorial/Essential.thy Mon Jul 19 15:44:13 2010 +0100
+++ b/ProgTutorial/Essential.thy Tue Jul 20 13:34:44 2010 +0100
@@ -1548,7 +1548,7 @@
final statement of the theorem.
@{ML_response_fake [display, gray]
- "tracing (string_of_thm @{context} my_thm)"
+ "pwriteln (pretty_thm @{context} my_thm)"
"\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
However, internally the code-snippet constructs the following
@@ -1769,8 +1769,8 @@
@{ML_response_fake [display,gray,linenos]
"Thm.reflexive @{cterm \"True\"}
|> Simplifier.rewrite_rule [@{thm True_def}]
- |> string_of_thm @{context}
- |> tracing"
+ |> pretty_thm @{context}
+ |> pwriteln"
"(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
Often it is necessary to transform theorems to and from the object
--- 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
--- a/ProgTutorial/Intro.thy Mon Jul 19 15:44:13 2010 +0100
+++ b/ProgTutorial/Intro.thy Tue Jul 20 13:34:44 2010 +0100
@@ -25,11 +25,11 @@
\medskip
If your next project requires you to program on the ML-level of Isabelle,
then this tutorial is for you. It will guide you through the first steps of
- Isabelle programming, and also explain tricks of the trade. We also hope
- the tutorial will encourage researchers to play with Isabelle and implement
- new ideas. The source code of Isabelle can look intimidating, but beginners
- can get by with knowledge of only a small number functions and a few basic
- coding conventions.
+ Isabelle programming, and also explain ``tricks of the trade''. We also hope
+ the tutorial will encourage students and researchers to play with Isabelle
+ and implement new ideas. The source code of Isabelle can look intimidating,
+ but beginners can get by with knowledge of only a small number functions and
+ a few basic coding conventions.
The best way to get to know the ML-level of Isabelle is by experimenting
@@ -39,7 +39,7 @@
please let us know. It is impossible for us to know every environment,
operating system or editor in which Isabelle is used. If you have comments,
criticism or like to add to the tutorial, please feel free---you are most
- welcome! The tutorial is meant to be gentle and comprehensive. To achieve
+ welcome!! The tutorial is meant to be gentle and comprehensive. To achieve
this we need your help and feedback.
*}
@@ -85,7 +85,7 @@
learn from it. This tutorial contains frequently pointers to the
Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is
often your best friend while programming with Isabelle.\footnote{Or
- hypersearch if you program using jEdit under MacOSX.} To understand the sources,
+ hypersearch if you work with jEdit under MacOSX.} To understand the sources,
it is often also necessary to track the change history of a file or
files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}}
for Isabelle provides convenient interfaces to query the history of
@@ -109,7 +109,7 @@
These boxes correspond to how code can be processed inside the interactive
environment of Isabelle. It is therefore easy to experiment with the code
- that is given in this tutorial. However, for better readability we will drop
+ that is shown in this tutorial. However, for better readability we will drop
the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just
write:
@@ -135,9 +135,9 @@
Further information or pointers to files.
\end{readmore}
- The pointers to Isabelle files are hyperlinked to the tip of the Mercurial
+ Note that pointers to Isabelle files are hyperlinked to the tip of the Mercurial
repository at \href{http://isabelle.in.tum.de/repos/isabelle/}
- {http://isabelle.in.tum.de/repos/isabelle/}, not the latest release
+ {http://isabelle.in.tum.de/repos/isabelle/}, not the latest stable release
of Isabelle.
A few exercises are scattered around the text. Their solutions are given
@@ -145,25 +145,25 @@
to solve the exercises on your own, and then look at the solutions.
*}
-section {* How To Understand Code in Isabelle *}
+section {* How To Understand Isabelle Code *}
text {*
- One of the more difficult aspects of programming is to understand somebody
- else's code. This is aggravated in Isabelle by the fact that many parts of
- the code contain only few comments. There is one strategy that might be
+ One of the more difficult aspects of any kind of programming is to understand code
+ written by somebody else. This is aggravated in Isabelle by the fact that many parts of
+ the code contain none or only few comments. There is one strategy that might be
helpful to navigate your way: ML is an interactive programming environment,
which means you can evaluate code on the fly (for example inside an
\isacommand{ML}~@{text "\<verbopen>\<dots>\<verbclose>"} section). So you can copy
- self-contained chunks of existing code into a separate theory file and then
- study it alongside with examples. You can also install probes inside the
+ (self-contained) chunks of existing code into a separate theory file and then
+ study it alongside with examples. You can also install ``probes'' inside the
copied code without having to recompile the whole Isabelle distributions. Such
probes might be messages or printouts of variables (see chapter
\ref{chp:firststeps}). Although PolyML also contains a debugger, it seems
- probing the code with explicit print statements is the most efficient method
- for understanding what some code is doing. However do not expect quick
+ probing the code with explicit print statements is the most effective method
+ for understanding what some piece of code is doing. However do not expect quick
results with this! Depending on the size of the code you are looking at,
- you will spend the better part of a quiet afternoon with it. But there
- seems to be no better way around it.
+ you will spend the better part of a quiet afternoon with it. And there
+ seems to be no better way for understanding code in Isabelle.
*}
@@ -171,7 +171,7 @@
text {*
One unpleasant aspect of any code development inside a larger system is that
- one has to aim at a ``moving target''. Isabelle is no exception. Every
+ one has to aim at a ``moving target''. Isabelle is no exception of this. Every
update lets potentially all hell break loose, because other developers have
changed code you are relying on. Cursing is somewhat helpful in such situations,
but taking the view that incompatible code changes are a fact of life
--- a/ProgTutorial/Package/Ind_Code.thy Mon Jul 19 15:44:13 2010 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy Tue Jul 20 13:34:44 2010 +0100
@@ -162,7 +162,7 @@
val (defs, lthy') =
defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy
in
- tracing (string_of_thms_no_vars lthy' defs); lthy
+ pwriteln (pretty_thms_no_vars lthy' defs); lthy
end *}
text {*
@@ -381,7 +381,7 @@
val intro =
prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
in
- tracing (string_of_thm lthy intro); lthy
+ pwriteln (pretty_thm lthy intro); lthy
end *}
text {*
@@ -440,7 +440,7 @@
let
val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy
in
- tracing (string_of_thms lthy ind_thms); lthy
+ pwriteln (pretty_thms lthy ind_thms); lthy
end *}
@@ -506,7 +506,7 @@
val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
val new_thm = all_elims ctrms @{thm all_elims_test}
in
- tracing (string_of_thm_no_vars @{context} new_thm)
+ pwriteln (pretty_thm_no_vars @{context} new_thm)
end"
"P a b c"}
@@ -522,7 +522,7 @@
"let
val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
in
- tracing (string_of_thm_no_vars @{context} res)
+ pwriteln (pretty_thm_no_vars @{context} res)
end"
"C"}
@@ -590,13 +590,13 @@
*}
ML{*fun chop_print params1 params2 prems1 prems2 ctxt =
let
- val s = ["Params1 from the rule:", string_of_cterms ctxt params1]
- @ ["Params2 from the predicate:", string_of_cterms ctxt params2]
- @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1)
- @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2)
+ val pps = [Pretty.big_list "Params1 from the rule:" (map (pretty_cterm ctxt) params1),
+ Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2),
+ Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1),
+ Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)]
in
- s |> cat_lines
- |> tracing
+ pps |> Pretty.chunks
+ |> tracing o Pretty.string_of
end*}
text_raw{*
\end{isabelle}
--- a/ProgTutorial/Solutions.thy Mon Jul 19 15:44:13 2010 +0100
+++ b/ProgTutorial/Solutions.thy Tue Jul 20 13:34:44 2010 +0100
@@ -305,7 +305,7 @@
This function generates for example:
@{ML_response_fake [display,gray]
- "writeln (string_of_term @{context} (term_tree 2))"
+ "pwriteln (pretty_term @{context} (term_tree 2))"
"(1 + 2) + (3 + 4)"}
The next function constructs a goal of the form @{text "P \<dots>"} with a term
--- a/ProgTutorial/Tactical.thy Mon Jul 19 15:44:13 2010 +0100
+++ b/ProgTutorial/Tactical.thy Tue Jul 20 13:34:44 2010 +0100
@@ -252,7 +252,7 @@
ML{*fun my_print_tac ctxt thm =
let
- val _ = tracing (string_of_thm_no_vars ctxt thm)
+ val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))
in
Seq.single thm
end*}
@@ -544,24 +544,19 @@
ML{*fun foc_tac {prems, params, asms, concl, context, schematics} =
let
- fun pairs1 f1 f2 xs =
- commas (map (fn (x, y) => f1 x ^ ":=" ^ f2 y) xs)
-
- fun pairs2 f xs = pairs1 f f xs
-
- val string_of_params = pairs1 I (string_of_cterm context) params
- val string_of_asms = string_of_cterms context asms
- val string_of_concl = string_of_cterm context concl
- val string_of_prems = string_of_thms_no_vars context prems
- val string_of_schms = pairs2 (string_of_cterm context) (snd schematics)
-
- val strs = ["params: " ^ string_of_params,
- "schematics: " ^ string_of_schms,
- "assumptions: " ^ string_of_asms,
- "conclusion: " ^ string_of_concl,
- "premises: " ^ string_of_prems]
+ fun assgn1 f1 f2 xs =
+ Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs)
+
+ fun assgn2 f xs = assgn1 f f xs
+
+ val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp])
+ [("params: ", assgn1 Pretty.str (pretty_cterm context) params),
+ ("assumptions: ", pretty_cterms context asms),
+ ("conclusion: ", pretty_cterm context concl),
+ ("premises: ", pretty_thms_no_vars context prems),
+ ("schematics: ", assgn2 (pretty_cterm context) (snd schematics))]
in
- tracing (cat_lines strs); all_tac
+ tracing (Pretty.string_of (Pretty.chunks pps)); all_tac
end*}
text_raw{*
@@ -583,7 +578,7 @@
\begin{quote}\small
\begin{tabular}{ll}
- params: & @{text "x:=x"}, @{text "y:=y"}\\
+ params: & @{text "x:= x"}, @{text "y:= y"}\\
schematics: & @{text "?z:=z"}\\
assumptions: & @{term "A x y"}\\
conclusion: & @{term "B y x \<longrightarrow> C (z y) x"}\\
@@ -611,7 +606,7 @@
\begin{quote}\small
\begin{tabular}{ll}
- params: & @{text "x:=x"}, @{text "y:=y"}\\
+ params: & @{text "x:= x"}, @{text "y:= y"}\\
schematics: & @{text "?z:=z"}\\
assumptions: & @{term "A x y"}, @{term "B y x"}\\
conclusion: & @{term "C (z y) x"}\\
@@ -1493,16 +1488,16 @@
val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
fun name_thm (nm, thm) =
- " " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm)
+ Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
fun name_ctrm (nm, ctrm) =
- " " ^ nm ^ ": " ^ (string_of_cterms ctxt ctrm)
-
- val s = ["Simplification rules:"] @ map name_thm simps @
- ["Congruences rules:"] @ map name_thm congs @
- ["Simproc patterns:"] @ map name_ctrm procs
+ Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm]
+
+ val pps = [Pretty.big_list "Simplification rules:" (map name_thm simps),
+ Pretty.big_list "Congruences rules:" (map name_thm congs),
+ Pretty.big_list "Simproc patterns:" (map name_ctrm procs)]
in
- s |> cat_lines
- |> tracing
+ pps |> Pretty.chunks
+ |> pwriteln
end*}
text_raw {*
\end{isabelle}
Binary file progtutorial.pdf has changed