--- 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 "* \<dots> *"}@{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 \<dots>}"}}:
-*}
-ML {* @{term "(a::nat) + b = c"} *}
+ @{ML_response [display] "@{term \"(a::nat) + b = c\"}"
+ "Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
-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 \<dots>}"} 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\", \<dots>) $ Free (\"x\", \<dots>)"}
+ @{ML_response [display] "@{prop \"P x\"}"
+ "Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>))"}
-text {* which inserts the coercion in the latter case and *}
-
+ which inserts the coercion in the latter case and
-ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
+ @{ML_response [display] "@{term \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
+ @{ML_response [display] "@{prop \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
-text {*
which does not.
Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
*}
-ML {* @{typ "bool \<Rightarrow> nat"} *}
text {*
+
+ @{ML_response [display] "@{typ \"bool \<Rightarrow> nat\"}" "Type \<dots>"}
+
(FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} 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 "\\<dots>" => "_" | 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