diff -r e21b2f888fa2 -r 631d12c25bde CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Tue Oct 14 01:33:55 2008 -0400 +++ b/CookBook/FirstSteps.thy Fri Oct 17 05:02:04 2008 -0400 @@ -14,7 +14,7 @@ \begin{center} \begin{tabular}{@ {}l} - \isacommand{theory} CookBook\\ + \isacommand{theory} FirstSteps\\ \isacommand{imports} Main\\ \isacommand{begin}\\ \ldots @@ -26,29 +26,31 @@ text {* The easiest and quickest way to include code in a theory is - by using the \isacommand{ML} command. For example -*} + by using the \isacommand{ML} command. For example\smallskip -ML {* - 3 + 4 -*} +\isacommand{ML} +@{ML_text "{"}@{ML_text "*"}\isanewline +\hspace{5mm}@{ML "3 + 4"}\isanewline +@{ML_text "*"}@{ML_text "}"}\isanewline +@{ML_text "> 7"}\smallskip -text {* Expressions inside \isacommand{ML} commands are immediately evaluated, like ``normal'' Isabelle proof scripts, 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. However on such \isacommand{ML} commands the undo operation behaves slightly counter-intuitive, because - if you define -*} + if you define\smallskip + +\isacommand{ML} +@{ML_text "{"}@{ML_text "*"}\isanewline +@{ML_text "val foo = true"}\isanewline +@{ML_text "*"}@{ML_text "}"}\isanewline +@{ML_text "> true"}\smallskip -ML {* - val foo = true -*} - -text {* then Isabelle's undo operation has no effect on the definition of - @{ML "foo"}. + @{ML_text "foo"}. Note that from now on we will drop the + \isacommand{ML} @{ML_text "{"}@{ML_text "* \ *"}@{ML_text "}"} whenever + we show code. Once a portion of code is relatively stable, one usually wants to export it to a separate ML-file. Such files can then be included in a @@ -63,6 +65,9 @@ \ldots \end{tabular} \end{center} + + Note that from now on we are going to drop the the + *} section {* Debugging and Printing *} @@ -72,40 +77,30 @@ During developments you might find it necessary to quickly inspect some data in your code. This can be done in a ``quick-and-dirty'' fashion using the function @{ML "warning"}. For example -*} -ML {* warning "any string" *} + @{ML [display] "warning \"any string\""} -text {* - will print out @{ML "\"any string\""} inside the response buffer of Isabelle. + will print out @{ML_text "\"any string\""} inside the response buffer of Isabelle. If you develop under PolyML, then there is a convenient, though again ``quick-and-dirty'', method for converting values into strings, for example: -*} -ML {* warning (makestring 1) *} + @{ML [display] "warning (makestring 1)"} -text {* However this only works if the type of what is converted is monomorphic and not a function. -*} -text {* - The funtion warning should only be used for testing purposes, because - any output this funtion generates will be overwritten, as soon as an error - is raised. - Therefore for printing anything more serious and elaborate, the function @{ML tracing} - should be used. This function writes all output into a separate buffer. -*} + The funtion warning should only be used for testing purposes, because any + output this funtion generates will be overwritten, as soon as an error is + raised. Therefore for printing anything more serious and elaborate, the + function @{ML tracing} should be used. This function writes all output into + a separate buffer. -ML {* tracing "foo" *} - -text {* + @{ML [display] "tracing \"foo\""} It is also possible to redirect the channel where the @{ML_text "foo"} is printed to a separate file, e.g. to prevent Proof General from choking on massive amounts of trace output. This rediretion can be achieved using the code - *} ML {* @@ -124,7 +119,7 @@ *} text {* - Calling @{ML_text "redirect_tracing"} with @{ML_text "(TextIO.openOut \"foo.bar\")"} + Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} will cause that all tracing information is printed into the file @{ML_text "foo.bar"}. *} @@ -138,15 +133,13 @@ on the logical level of Isabelle. This is done using antiquotations. For example, one can print out the name of the current theory by typing -*} - -ML {* Context.theory_name @{theory} *} - -text {* + + @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps : string"} + where @{text "@{theory}"} is an antiquotation that is substituted with the current theory (remember that we assumed we are inside the theory CookBook). - The name of this theory can be extracted using the function @{ML "Context.theory_name"}. - So the code above returns the string @{ML "\"CookBook\""}. + The name of this theory can be extracted using the function + @{ML "Context.theory_name"}. Note, however, that antiquotations are statically scoped, that is the value is determined at ``compile-time'', not ``run-time''. For example the function @@ -160,19 +153,18 @@ text {* does \emph{not} return the name of the current theory, if it is run in a different theory. Instead, the code above defines the constant function - that always returns the string @{ML "\"CookBook\""}, no matter where the + that always returns the string @{ML_text "FirstSteps"}, no matter where the function is called. Operationally speaking, @{text "@{theory}"} is \emph{not} replaced with code that will look up the current theory in some data structure and return it. Instead, it is literally replaced with the value representing the theory name. In a similar way you can use antiquotations to refer to theorems or simpsets: -*} + -ML {* @{thm allI} *} -ML {* @{simpset} *} + @{ML [display] "@{thm allI}"} + @{ML [display] "@{simpset}"} -text {* In the course of this introduction, we will learn more about these antiquotations: they greatly simplify Isabelle programming since one can directly access all kinds of logical elements from ML. @@ -184,14 +176,13 @@ text {* One way to construct terms of Isabelle on the ML level is by using the antiquotation \mbox{@{text "@{term \}"}}: -*} -ML {* @{term "(a::nat) + b = c"} *} + @{ML_response [display] "@{term \"(a::nat) + b = c\"}" + "Const (\"op =\", \) $ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} -text {* This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal representation of this term. This internal representation corresponds to the - datatype @{ML_text "term"}. + datatype @{ML_type "term"}. The internal representation of terms uses the usual de Bruijn index mechanism where bound variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to @@ -225,34 +216,33 @@ can use the following ML funtion to set the limit to a value high enough: \end{exercise} -*} -ML {* print_depth 50 *} -text {* - + @{ML [display] "print_depth 50"} + The antiquotation @{text "@{prop \}"} constructs terms of propositional type, inserting the invisible @{text "Trueprop"} coercions whenever necessary. Consider for example -*} - -ML {* @{term "P x"} ; @{prop "P x"} *} + @{ML_response [display] "@{term \"P x\"}" "Free (\"P\", \) $ Free (\"x\", \)"} + @{ML_response [display] "@{prop \"P x\"}" + "Const (\"Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \))"} -text {* which inserts the coercion in the latter case and *} - + which inserts the coercion in the latter case and -ML {* @{term "P x \ Q x"} ; @{prop "P x \ Q x"} *} + @{ML_response [display] "@{term \"P x \ Q x\"}" "Const (\"==>\", \) $ \ $ \"} + @{ML_response [display] "@{prop \"P x \ Q x\"}" "Const (\"==>\", \) $ \ $ \"} -text {* which does not. Types can be constructed using the antiquotation @{text "@{typ \}"}. For example *} -ML {* @{typ "bool \ nat"} *} text {* + + @{ML_response [display] "@{typ \"bool \ nat\"}" "Type \"} + (FIXME: Unlike the term antiquotation, @{text "@{typ \}"} does not print the internal representation. Is there a reason for this, that needs to be explained here?) @@ -265,8 +255,6 @@ *} - - section {* Constructing Terms and Types Manually *} text {* @@ -369,25 +357,23 @@ Type checking is always relative to a theory context. For now we can use the @{ML "@{theory}"} antiquotation to get hold of the current theory. For example we can write: -*} + + (FIXME ML-response-unchecked needed) -ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *} + @{ML [display] "@{term \"(a::nat) + b = c\"}"} -text {* and *} + and -ML {* - let - val natT = @{typ "nat"} - val zero = @{term "0::nat"} - in - cterm_of @{theory} - (Const (@{const_name plus}, natT --> natT --> natT) - $ zero $ zero) - end -*} +@{ML [display] +"let + val natT = @{typ \"nat\"} + val zero = @{term \"0::nat\"} +in + cterm_of @{theory} + (Const (@{const_name plus}, natT --> natT --> natT) + $ zero $ zero) +end"} -text {* - \begin{exercise} Check that the function defined in Exercise~\ref{fun:revsum} returns a result that type checks. @@ -574,5 +560,61 @@ section {* Theorem Attributes *} +ML {* + val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; + +fun ml_val ys txt = "fn " ^ + (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ + " => (" ^ txt ^ ");"; + +fun ml_val_open (ys, []) txt = ml_val ys txt + | ml_val_open (ys, xs) txt = + ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end"); + +fun ml_pat (rhs, pat) = + let val pat' = implode (map (fn "\\" => "_" | s => s) + (Symbol.explode pat)) + in + "val " ^ pat' ^ " = " ^ rhs + end; + +(* modified from original *) +fun ml_val txt = "fn _ => (" ^ txt ^ ");"; +fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"; +fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;"; + +*} + +ML {* ml_pat *} +ML {* K ml_pat *} + +ML {* +fun output_verbatim ml src ctxt (txt, pos) = + let val txt = ml ctxt (txt, pos) + in + (if ! ThyOutput.source then str_of_source src else txt) + |> (if ! ThyOutput.quotes then quote else I) + |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt + end; +*} + +ML {* +fun output_ml ml = output_verbatim + (fn ctxt => fn ((txt, p), pos) => + (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); + txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> + Chunks.transform_cmts |> implode)); +*} + +ML {* +fun output_ml_checked ml src ctxt (txt, pos) = + (ML_Context.eval_in (SOME ctxt) false pos (ml txt); + (if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos))) + |> (if ! ThyOutput.quotes then quote else I) + |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt) + +*} + + end \ No newline at end of file