# HG changeset patch # User Christian Urban # Date 1250550356 -7200 # Node ID ee864694315ba54d46d4a22de31398bc9c87f074 # Parent 007922777ff1fbcff3b36945a8c82b632ea9ca6c polished diff -r 007922777ff1 -r ee864694315b ProgTutorial/Base.thy --- a/ProgTutorial/Base.thy Mon Aug 17 20:57:32 2009 +0200 +++ b/ProgTutorial/Base.thy Tue Aug 18 01:05:56 2009 +0200 @@ -21,7 +21,7 @@ val stream = TextIO.openAppend name in TextIO.output (stream, txt); - TextIO.flushOut stream; + TextIO.flushOut stream; (* needed ?*) TextIO.closeOut stream end) *} @@ -45,7 +45,6 @@ (open_file name; write_file (txt ^ "\n")) *} - ML {* fun propagate_env (context as Context.Proof lthy) = @@ -54,27 +53,21 @@ fun propagate_env_prf prf = Proof.map_contexts (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf -*} -ML {* val _ = OuterSyntax.command "ML" "eval ML text within theory" (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) (OuterParse.position OuterParse.text >> (fn (txt, pos) => Toplevel.generic_theory (ML_Context.exec (fn () => (write_file_blk txt; ML_Context.eval true pos txt)) #> propagate_env))) -*} -ML {* val _ = OuterSyntax.command "ML_prf" "ML text within proof" (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) (OuterParse.ML_source >> (fn (txt, pos) => Toplevel.proof (Proof.map_context (Context.proof_map (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) -*} -ML {* val _ = OuterSyntax.command "ML_val" "diagnostic ML text" (OuterKeyword.tag "TutorialML" OuterKeyword.diag) diff -r 007922777ff1 -r ee864694315b ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Mon Aug 17 20:57:32 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Tue Aug 18 01:05:56 2009 +0200 @@ -8,8 +8,8 @@ chapter {* First Steps *} text {* - Isabelle programming is done in ML. Just like lemmas and proofs, ML-code - for Isabelle must be part of a theory. If you want to follow the code given in + Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for + Isabelle must be part of a theory. If you want to follow the code given in this chapter, we assume you are working inside the theory starting with \begin{quote} @@ -28,22 +28,22 @@ section {* Including ML-Code *} text {* - The easiest and quickest way to include code in a theory is - by using the \isacommand{ML}-command. For example: - -\begin{isabelle} -\begin{graybox} -\isacommand{ML}~@{text "\"}\isanewline -\hspace{5mm}@{ML "3 + 4"}\isanewline -@{text "\"}\isanewline -@{text "> 7"}\smallskip -\end{graybox} -\end{isabelle} - - Like normal Isabelle scripts, \isacommand{ML}-commands can be - evaluated by using the advance and undo buttons of your Isabelle - environment. The code inside the \isacommand{ML}-command can also contain - value and function bindings, for example + The easiest and quickest way to include code in a theory is by using the + \isacommand{ML}-command. For example: + + \begin{isabelle} + \begin{graybox} + \isacommand{ML}~@{text "\"}\isanewline + \hspace{5mm}@{ML "3 + 4"}\isanewline + @{text "\"}\isanewline + @{text "> 7"}\smallskip + \end{graybox} + \end{isabelle} + + Like normal Isabelle scripts, \isacommand{ML}-commands can be evaluated by + using the advance and undo buttons of your Isabelle environment. The code + inside the \isacommand{ML}-command can also contain value and function + bindings, for example *} ML %gray {* @@ -52,16 +52,15 @@ *} text {* - and even those can be undone when the proof - script is retracted. As mentioned in the Introduction, we will drop the - \isacommand{ML}~@{text "\ \ \"} scaffolding whenever we - show code. The lines prefixed with @{text [quotes] ">"} are not part of the - code, rather they indicate what the response is when the code is evaluated. - There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for - including ML-code. The first evaluates the given code, but any effect on the - theory, in which the code is embedded, is suppressed. The second needs to - be used if ML-code is defined - inside a proof. For example + and even those can be undone when the proof script is retracted. As + mentioned in the Introduction, we will drop the \isacommand{ML}~@{text + "\ \ \"} scaffolding whenever we show code. The lines + prefixed with @{text [quotes] ">"} are not part of the code, rather they + indicate what the response is when the code is evaluated. There are also + the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including + ML-code. The first evaluates the given code, but any effect on the theory, + in which the code is embedded, is suppressed. The second needs to be used if + ML-code is defined inside a proof. For example \begin{quote} \begin{isabelle} @@ -72,8 +71,8 @@ \end{isabelle} \end{quote} - However, both commands will only play minor roles in this tutorial (we will always - arrange that the ML-code is defined outside of proofs, for example). + However, both commands will only play minor roles in this tutorial (we will + always arrange that the ML-code is defined outside of proofs, for example). Once a portion of code is relatively stable, you usually want to export it to a separate ML-file. Such files can then be included somewhere inside a @@ -105,44 +104,44 @@ \end{tabular} \end{quote} - Note that no parentheses are given this time. 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. + Note that no parentheses are given this time. 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. *} section {* Debugging and Printing\label{sec:printing} *} text {* - - During development you might find it necessary to inspect some data - in your code. This can be done in a ``quick-and-dirty'' fashion using - the function @{ML [index] "writeln"}. For example + During development you might find it necessary to inspect some data in your + code. This can be done in a ``quick-and-dirty'' fashion using the function + @{ML [index] "writeln"}. For example @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""} - will print out @{text [quotes] "any string"} inside the response buffer - of Isabelle. This function expects a string as argument. If you develop under PolyML, - then there is a convenient, though again ``quick-and-dirty'', method for - converting values into strings, namely the function @{ML PolyML.makestring}: + will print out @{text [quotes] "any string"} inside the response buffer of + Isabelle. This function expects a string as argument. If you develop under + PolyML, then there is a convenient, though again ``quick-and-dirty'', method + for converting values into strings, namely the function + @{ML [index] makestring in PolyML}: @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} - However, @{ML [index] makestring in PolyML} only works if the type of what is converted is monomorphic - and not a function. - - The function @{ML "writeln"} should only be used for testing purposes, because any - output this function generates will be overwritten as soon as an error is - raised. For printing anything more serious and elaborate, the - function @{ML [index] tracing} is more appropriate. This function writes all output into - a separate tracing buffer. For example: + However, @{ML makestring in PolyML} only works if the type of what + is converted is monomorphic and not a function. + + The function @{ML "writeln"} should only be used for testing purposes, + because any output this function generates will be overwritten as soon as an + error is raised. For printing anything more serious and elaborate, the + function @{ML [index] tracing} is more appropriate. This function writes all + output into a separate tracing buffer. For example: @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} - It is also possible to redirect the ``channel'' where the string @{text "foo"} is - printed to a separate file, e.g., to prevent ProofGeneral from choking on massive - amounts of trace output. This redirection can be achieved with the code: + It is also possible to redirect the ``channel'' where the string @{text + "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from + choking on massive amounts of trace output. This redirection can be achieved + with the code: *} ML{*val strip_specials = @@ -198,7 +197,7 @@ text {* Most often you want to inspect data of Isabelle's most basic data - structures, namely @{ML_type term}, @{ML_type cterm} or @{ML_type + structures, namely @{ML_type term}, @{ML_type cterm} 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 @@ -270,8 +269,8 @@ In order to improve the readability of theorems we convert these schematic variables into free variables using the function @{ML [index] import in - Variable}. This is similar to the theorem attribute @{text "[no_vars]"} from - Isabelle's user-level. + Variable}. This is similar to statements like @{text "conjI[no_vars]"} + from Isabelle's user-level. *} ML{*fun no_vars ctxt thm = @@ -524,9 +523,9 @@ These two functions can be used to avoid explicit @{text "lets"} for intermediate values in functions that return pairs. Suppose for example you want to separate a list of integers into two lists according to a - treshold. For example if the treshold is @{ML "5"}, the list @{ML - "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}. This - function can be implemented as + treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"} + should be separated to @{ML "([1,2,3,4], [6,5])"}. This function can be + implemented as *} ML{*fun separate i [] = ([], []) @@ -619,7 +618,7 @@ text {* When using combinators for writing function in waterfall fashion, it is - sometimes necessary to do some ``plumbing'' for fitting functions + sometimes necessary to do some ``plumbing'' in order to fit functions 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 diff -r 007922777ff1 -r ee864694315b ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Mon Aug 17 20:57:32 2009 +0200 +++ b/ProgTutorial/antiquote_setup.ML Tue Aug 18 01:05:56 2009 +0200 @@ -6,12 +6,12 @@ open OutputTutorial (* functions for generating appropriate expressions *) -fun ml_val_open ys istruc txt = +fun ml_val_open ys strct txt = let fun ml_val_open_aux ys txt = - "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")"; + implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]; in - (case istruc of + (case strct of NONE => ml_val_open_aux ys txt | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end")) end diff -r 007922777ff1 -r ee864694315b ProgTutorial/output_tutorial.ML --- a/ProgTutorial/output_tutorial.ML Mon Aug 17 20:57:32 2009 +0200 +++ b/ProgTutorial/output_tutorial.ML Tue Aug 18 01:05:56 2009 +0200 @@ -8,6 +8,7 @@ val gray = ref false val linenos = ref false + fun output txt = let val prts = map Pretty.str txt @@ -26,7 +27,6 @@ #> enclose "\\isa{" "}") end - datatype qstring = NoString | Plain of string diff -r 007922777ff1 -r ee864694315b progtutorial.pdf Binary file progtutorial.pdf has changed