# HG changeset patch # User Christian Urban # Date 1241870125 -7200 # Node ID 11851b20fb786e930e23b308d5b59e347029b461 # Parent afa2d9c6b3b7b6bf7b587bd7e54fab2dcb26ba4c added more to the pretty section and updated the acknowledgements diff -r afa2d9c6b3b7 -r 11851b20fb78 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Sat May 09 03:11:36 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Sat May 09 13:55:25 2009 +0200 @@ -1693,38 +1693,43 @@ *) (*>*) -section {* Pretty-Printing *} +section {* Pretty-Printing\label{sec:pretty} *} text {* - Isabelle has a sophisticated infrastructure for pretty-printing text - involving for example long formulae. This infrastructure is loosely based - on a paper by Oppen~\cite{Oppen80}. Most of its functions do not operate - directly on @{ML_type string}s, but on instances of the type: + So far we printed out only plain strings without any formatting except for + occasional explicit line breaks using @{text [quotes] "\\n"}. This is + sufficient for ``quick-and-dirty'' printouts. For something more + sophisticated, Isabelle includes an infrastructure for formatting text. + This infrastructure is quite useful for printing for example large formulae. + It is loosely based on a paper by Oppen~\cite{Oppen80}. Most of + its functions do not operate on @{ML_type string}s, but on instances of the + type: @{ML_type [display, gray] "Pretty.T"} - The function @{ML "Pretty.str"} transforms a string into such a pretty + The function @{ML "Pretty.str"} transforms a (plain) string into such a pretty type. For example @{ML_response_fake [display,gray] "Pretty.str \"test\"" "String (\"test\", 4)"} - where the result indicates that we transformed a string with length 4. - Once you have a pretty type, you can, for example, control where line breaks - can occur and with how much indentation a text should be printed. - However, if you want to actually output the formatted text, you have to - transform the pretty type back into a @{ML_type string}. This can be done - with the function @{ML Pretty.string_of}. In what follows we will use - the following wrapper function for printing a pretty type: + where the result indicates that we transformed a string with length 4. Once + you have a pretty type, you can, for example, control where line breaks can + occur in case the text wraps over a line, or with how much indentation a + text should be printed. However, if you want to actually output the + formatted text, you have to transform the pretty type back into a @{ML_type + string}. This can be done with the function @{ML Pretty.string_of}. In what + follows we will use the following wrapper function for printing a pretty + type: *} ML{*fun pprint prt = writeln (Pretty.string_of prt)*} text {* - The point of the pretty-printing infrastructure is to aid the layout - of text. Let us first explain how you can insert places where a - line break can occur. For this assume the following function that - replicates a string n times: + The point of the pretty-printing infrastructure is to give hints how to + layout text and let the system do the actual layout. Let us first explain + how you can insert places where a line break can occur. For this assume the + following function that replicates a string n times: *} ML{*fun rep n str = implode (replicate n str) *} @@ -1736,7 +1741,8 @@ ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*} text {* - If we use for printing the usial ``quick-and-dirty'' method + Since @{ML test_str} is a string spanning over more than one line, we + obtain the ugly @{ML_response_fake [display,gray] "writeln test_str" @@ -1745,7 +1751,8 @@ aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo oooooooooooooobaaaaaaaaaaaar"} - we obtain an ugly layout. Similarly if we just use + if we print the string by the usual ``quick-and-dirty'' method. + We obtain the same if we just use @{ML_response_fake [display,gray] "pprint (Pretty.str test_str)" @@ -1754,15 +1761,13 @@ aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo oooooooooooooobaaaaaaaaaaaar"} -*} + However by using pretty types you have the ability to indicate a possible + line break for example at each space. You can achieve this with the function + @{ML Pretty.breaks}, which expects a list of pretty types and inserts a + possible line break in between every two elements in this list. To print + this this list of pretty types as a single string, we concatenate them + with the function @{ML Pretty.blk} as follows -text {* - We obtain better results if we indicate a possible line break at every - spece. You can achieve this with the function @{ML Pretty.breaks}, which - expects a list of pretty types and inserts a possible place for a - line break in between every two elements in this list. To print this - this list of pretty types we concatenate them with the function @{ML - Pretty.blk} as follows @{ML_response_fake [display,gray] "let @@ -1775,9 +1780,9 @@ fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"} - Here the layout of @{ML test_str} is much more pleaseing to the - eye. The @{ML "0"} in @{ML Pretty.blk} stands for a zero-intendation - of the printed string. If we increase the intentation we obtain + Here the layout of @{ML test_str} is much more pleasing to the + eye. The @{ML "0"} in @{ML Pretty.blk} stands for a zero-indentation + of the printed string. If you increase the indentation, you obtain @{ML_response_fake [display,gray] "let @@ -1805,56 +1810,131 @@ fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"} -*} + If you want to print out a list of items separated by commas and + have the line breaks handled properly, you can use the function + @{ML Pretty.commas}. For example +@{ML_response_fake [display,gray] +"let + val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020) +in + pprint (Pretty.blk (0, Pretty.commas ptrs)) +end" +"99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, +100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, +100016, 100017, 100018, 100019, 100020"} + + where @{ML upto} generates a list of integers. You can print this + list out as an ``set'' enclosed inside @{text [quotes] "{"} and + @{text [quotes] "}"}, and separated by commas by using the function + @{ML Pretty.enum}. For example +*} -ML{*fun p_strs str = Pretty.breaks (map Pretty.str (space_explode " " str)) *} +text {* + +@{ML_response_fake [display,gray] +"let + val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020) +in + pprint (Pretty.enum \",\" \"{\" \"}\" ptrs) +end" +"{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, + 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, + 100016, 100017, 100018, 100019, 100020}"} -ML{*pprint (Pretty.blk (0, Pretty.commas (map (Pretty.str o string_of_int) (1 upto 20))))*} + As can be seen, this function prints out the ``set'' so that starting + from the second each new line as an indentation of 2. + + If you print something out which goes beyond the capabilities of the + standard function, you can do the formating yourself. Assume you want + to print out a list of items where like in English the last two items + are separated by @{text [quotes] "and"}. For this you can write the + function +*} -ML{*fun and_list [] = [] +ML %linenosgray{*fun and_list [] = [] | and_list [x] = [x] | and_list xs = let val (front, last) = split_last xs in - (Pretty.commas front) @ [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last] + (Pretty.commas front) @ + [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last] end *} -ML{* pprint (Pretty.block (and_list (map (Pretty.str o string_of_int) (1 upto 20)))) *} - -ML{* Pretty.enum "l" "r" "sep" *} - -text {* chunks = one ptr above the other*} - -ML{* pprint (Pretty.chunks ([(Pretty.str (rep 3 "foo "))] @ [(Pretty.str (rep 4 "bar "))])) *} - -ML {* pprint (Pretty.str "foo"); pprint (Pretty.str "bar") *} - +text {* + where in Line 7 we print the beginning of the list and in Line + 8 the last item. We have to use @{ML "Pretty.brk 1"} in order + to insert a space (of length 1) before the @{text [quotes] "and"} + where we also want that a line break can occur. We do the + same ater the @{text [quotes] "and"}. This gives you -text {* types, terms and text *} +@{ML_response_fake [display,gray] +"let + val ptrs = map (Pretty.str o string_of_int) (1 upto 22) +in + pprint (Pretty.blk (0, and_list ptrs)) +end" +"1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 +and 22"} -ML {*fun tell_type ctxt t = - pprint (Pretty.blk (0, (p_strs "The term ") - @ [Pretty.quote (Syntax.pretty_term ctxt t)] - @ p_strs " has type " - @ [Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t)), Pretty.str "."]))*} - -ML{*tell_type @{context} @{term "min (Suc 0)"} *} - - -ML {* -tell_type @{context} @{term "(op =) ((op =) ((op =) ((op =) ((op =) (op =)))))"} + Next we like to pretty print a term and its type. For this we use the + function @{text "tell_type"}: *} -text {* does not break inside the term or type *} +ML %linenosgray{*fun tell_type ctxt t = +let + fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s)) + val ptrm = Pretty.quote (Syntax.pretty_term ctxt t) + val pty = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t)) +in + pprint (Pretty.blk (0, + (pstr "The term " @ [ptrm] @ pstr " has type " + @ [pty, Pretty.str "."]))) +end*} text {* + In Line 3 we define a function that inserts possible linebreaks into + an (English) text according to spaces. In Lines 4 and 5 we pretty print + the term and its type using the functions @{ML Syntax.pretty_term} and + @{ML Syntax.pretty_typ}. We also use the function @{ML Pretty.quote} + in order to enclose the term and type with quotes. In Line 9 we add the + period right after the type without the possibility of a line break, + because we do not want that a line break occurs there. + + Now you can write + + @{ML_response_fake [display,gray] + "tell_type @{context} @{term \"min (Suc 0)\"}" + "The term \"min (Suc 0)\" has type \"nat \ nat\"."} + + You can see the proper line breaking with the term + + @{ML_response_fake [display,gray] + "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}" + "The term \"op = (op = (op = (op = (op = op =))))\" has type +\"((((('a \ 'a \ bool) \ bool) \ bool) \ bool) \ bool) \ bool\"."} + +*} + +text {* + Still to be done: + @{ML Pretty.big_list}, + @{ML Pretty.chunks} + equations colours + + What happens with big formulae? + + \begin{readmore} + The general infrastructure for pretty printing is implemented in + @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"} + contains pretty printing functions for terms, types, theorems and so on. + \end{readmore} *} section {* Misc (TBD) *} diff -r afa2d9c6b3b7 -r 11851b20fb78 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Sat May 09 03:11:36 2009 +0200 +++ b/ProgTutorial/Intro.thy Sat May 09 13:55:25 2009 +0200 @@ -10,7 +10,7 @@ Isabelle programming, and also explain tricks of the trade. The best way to get to know the ML-level of Isabelle is by experimenting with the many code examples included in the tutorial. The code is as far as possible checked - against \input{version}. If something does not work, + against the Isabelle code.\footnote{\input{version}} If something does not work, then 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 @@ -137,6 +137,7 @@ \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} \item @{text context} for generic contexts; ML-type @{ML_type Context.generic} \item @{text mx} for mixfix syntax annotations; ML-type @{ML_type mixfix} + \item @{text prt} for pretty printing; ML-type @{ML_type Pretty.T} \end{itemize} *} @@ -154,6 +155,8 @@ describing the package and has been helpful \emph{beyond measure} with answering questions about Isabelle. + \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}. + \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, \ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}. diff -r afa2d9c6b3b7 -r 11851b20fb78 ProgTutorial/document/root.tex --- a/ProgTutorial/document/root.tex Sat May 09 03:11:36 2009 +0200 +++ b/ProgTutorial/document/root.tex Sat May 09 13:55:25 2009 +0200 @@ -142,6 +142,7 @@ \author{by Christian Urban with contributions from:\\[2ex] \begin{tabular}{r@{\hspace{1.8mm}}l} Stefan & Berghofer\\ + Jasmin & Blanchette\\ Sascha & Böhme\\ Jeremy & Dawson\\ Alexander & Krauss\\ diff -r afa2d9c6b3b7 -r 11851b20fb78 progtutorial.pdf Binary file progtutorial.pdf has changed