diff -r 2c392f61f400 -r a2e49e0771b3 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Thu Nov 19 17:48:44 2009 +0100 +++ b/ProgTutorial/Essential.thy Thu Nov 19 20:00:10 2009 +0100 @@ -1341,15 +1341,10 @@ Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *} text {* - The fourth argument of @{ML note in Local_Theory} is the list of theorems we + The third argument of @{ML note in Local_Theory} is the list of theorems we want to store under a name. We can store more than one under a single name. - The first argument @{ML_ind theoremK in Thm} is - a kind indicator, which classifies the theorem. There are several such kind - indicators: for a theorem arising from a definition you should use @{ML_ind - definitionK in Thm}, and for - ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK - in Thm}. The second argument of @{ML note in Local_Theory} is the name under - which we store the theorem or theorems. The third argument can contain a + The first argument of @{ML note in Local_Theory} is the name under + which we store the theorem or theorems. The second argument can contain a list of theorem attributes, which we will explain in detail in Section~\ref{sec:attributes}. Below we just use one such attribute for adding the theorem to the simpset: @@ -1900,13 +1895,16 @@ *} ML{*fun MY_THEN thms = - Thm.rule_attribute - (fn _ => fn thm => fold (curry ((op RS) o swap)) thms thm)*} +let + fun RS_rev thm1 thm2 = thm2 RS thm1 +in + Thm.rule_attribute (fn _ => fn thm => fold RS_rev thms thm) +end*} text {* - where @{ML swap} swaps the components of a pair. The setup of this theorem - attribute uses the parser @{ML thms in Attrib}, which parses a list of - theorems. + where for convenience we define the reverse and curried version of @{ML RS}. + The setup of this theorem attribute uses the parser @{ML thms in Attrib}, + which parses a list of theorems. *} attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *} @@ -2023,6 +2021,7 @@ have to change the parser for reading the arguments accordingly. \footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?} + \footnote{\bf FIXME readmore} \begin{readmore} FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in @@ -2220,42 +2219,20 @@ 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and 28"} - Next we like to pretty-print a term and its type. For this we use the - function @{text "tell_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 in places - where a space is. In Lines 4 and 5 we pretty-print the term and its type - using the functions @{ML_ind pretty_term in Syntax} and @{ML_ind - pretty_typ in Syntax}. We also use the function @{ML_ind quote in - Pretty} in order to enclose the term and type inside quotation marks. In - Line 9 we add a 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 + Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out + a list of items, but automatically inserts forced breaks between each item. + Compare @{ML_response_fake [display,gray] - "tell_type @{context} @{term \"min (Suc 0)\"}" - "The term \"min (Suc 0)\" has type \"nat \ nat\"."} - - To see the proper line breaking, you can try out the function on a bigger term - and type. For example: - - @{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\"."} + "let + val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"] +in + pprint (Pretty.blk (0, a_and_b)); + pprint (Pretty.chunks a_and_b) +end" +"ab +a +b"} The function @{ML_ind big_list in Pretty} helps with printing long lists. It is used for example in the command \isacommand{print\_theorems}. An @@ -2276,24 +2253,56 @@ 9 10"} - Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out - a list of items, but automatically inserts forced breaks between each item. - Compare + The point of the pretty-printing functions is to conveninetly obtain + a lay-out of terms and types that is pleasing to the eye. If we print + out the the terms produced by the the function @{ML de_bruijn} from + exercise~\ref{ex:debruijn} we obtain the following: @{ML_response_fake [display,gray] - "let - val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"] + "pprint (Syntax.pretty_term @{context} (de_bruijn 4))" + "(P 3 = P 4 \ P 4 \ P 3 \ P 2 \ P 1) \ +(P 2 = P 3 \ P 4 \ P 3 \ P 2 \ P 1) \ +(P 1 = P 2 \ P 4 \ P 3 \ P 2 \ P 1) \ +(P 1 = P 4 \ P 4 \ P 3 \ P 2 \ P 1) \ +P 4 \ P 3 \ P 2 \ P 1"} + + We use the function @{ML_ind pretty_term in Syntax} for pretty-printing + terms. Next we like to pretty-print a term and its type. For this we use the + function @{text "tell_type"}. +*} + +ML %linenosgray{*fun tell_type ctxt trm = +let + fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s)) + val ptrm = Pretty.quote (Syntax.pretty_term ctxt trm) + val pty = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of trm)) in - pprint (Pretty.blk (0, a_and_b)); - pprint (Pretty.chunks a_and_b) -end" -"ab -a -b"} + 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 in places + where a space is. In Lines 4 and 5 we pretty-print the term and its type + using the functions @{ML pretty_term in Syntax} and @{ML_ind + pretty_typ in Syntax}. We also use the function @{ML_ind quote in + Pretty} in order to enclose the term and type inside quotation marks. In + Line 9 we add a 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\"."} - \footnote{\bf FIXME: What happens with printing big formulae?} + To see the proper line breaking, you can try out the function on a bigger term + and type. For example: - + @{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\"."} \begin{readmore} The general infrastructure for pretty-printing is implemented in the file @@ -2304,47 +2313,6 @@ \end{readmore} *} -(* -text {* - printing into the goal buffer as part of the proof state -*} - -text {* writing into the goal buffer *} - -ML {* fun my_hook interactive state = - (interactive ? Proof.goal_message (fn () => Pretty.str -"foo")) state -*} - -setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *} - -lemma "False" -oops -*) - -(* -ML {* -fun setmp_show_all_types f = - setmp show_all_types - (! show_types orelse ! show_sorts orelse ! show_all_types) f; - -val ctxt = @{context}; -val t1 = @{term "undefined::nat"}; -val t2 = @{term "Suc y"}; -val pty = Pretty.block (Pretty.breaks - [(setmp show_question_marks false o setmp_show_all_types) - (Syntax.pretty_term ctxt) t1, - Pretty.str "=", Syntax.pretty_term ctxt t2]); -pty |> Pretty.string_of -*} - -text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely *} - - -ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of |> tracing *} -ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *} -*) - section {* Summary *} text {*