+ −
theory Antiquotes+ −
imports "../Appendix"+ −
begin+ −
+ −
section {* Useful Document Antiquotations\label{rec:docantiquotations} *}+ −
+ −
text {*+ −
{\bf Problem:} + −
How to keep your ML-code inside a document synchronised with the actual code?\smallskip+ −
+ −
{\bf Solution:} This can be achieved with document antiquotations.\smallskip+ −
+ −
Document antiquotations can be used for ensuring consistent type-setting of+ −
various entities in a document. They can also be used for sophisticated+ −
\LaTeX-hacking. If you type on the Isabelle level+ −
*}+ −
+ −
print_antiquotations+ −
+ −
text {*+ −
you obtain a list of all currently available document antiquotations and+ −
their options. + −
+ −
Below we will give the code for two additional document+ −
antiquotations both of which are intended to typeset ML-code. The crucial point+ −
of these document antiquotations is that they not just print the ML-code, but also + −
check whether it compiles. This will provide a sanity check for the code+ −
and also allows you to keep documents in sync with other code, for example+ −
Isabelle.+ −
+ −
We first describe the antiquotation @{text "ML_checked"} with the syntax:+ −
+ −
@{text [display] "@{ML_checked \"a_piece_of_code\"}"}+ −
+ −
The code is checked by sending the ML-expression @{text [quotes] "val _ =+ −
a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML+ −
"ML_Context.eval_text_in"} in Line 4 below). The complete code of the+ −
document antiquotation is as follows:+ −
+ −
*}+ −
+ −
ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt+ −
+ −
fun output_ml {context = ctxt, ...} code_txt =+ −
(ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); + −
Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))+ −
+ −
val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}+ −
+ −
text {*+ −
The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this+ −
case the code, and then calls the function @{ML output_ml}. As mentioned+ −
before, the parsed code is sent to the ML-compiler in Line 4 using the+ −
function @{ML ml_val}, which constructs the appropriate ML-expression, and+ −
using @{ML "eval_in" in ML_Context}, which calls the compiler. If the code is+ −
``approved'' by the compiler, then the output function @{ML "output" in+ −
Thy_Output} in the next line pretty prints the code. This function expects+ −
that the code is a list of (pretty)strings where each string correspond to a+ −
line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)"+ −
for txt} which produces such a list according to linebreaks. There are a+ −
number of options for antiquotations that are observed by the function + −
@{ML "output" in Thy_Output} when printing the code (including @{text "[display]"} + −
and @{text "[quotes]"}). The function @{ML "antiquotation" in Thy_Output} in + −
Line 7 sets up the new document antiquotation.+ −
+ −
\begin{readmore}+ −
For more information about options of document antiquotations see \rsccite{sec:antiq}).+ −
\end{readmore}+ −
+ −
Since we used the argument @{ML "Position.none"}, the compiler cannot give specific + −
information about the line number, in case an error is detected. We + −
can improve the code above slightly by writing + −
*}+ −
+ −
ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) =+ −
(ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt);+ −
Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))+ −
+ −
val _ = Thy_Output.antiquotation "ML_checked"+ −
(Scan.lift (Parse.position Args.name)) output_ml *}+ −
+ −
text {*+ −
where in Lines 1 and 2 the positional information is properly treated. The+ −
parser @{ML Parse.position} encodes the positional information in the + −
result.+ −
+ −
We can now write @{text "@{ML_checked \"2 + 3\"}"} in a document in order to+ −
obtain @{ML_checked "2 + 3"} and be sure that this code compiles until+ −
somebody changes the definition of addition.+ −
+ −
+ −
The second document antiquotation we describe extends the first by a pattern+ −
that specifies what the result of the ML-code should be and checks the+ −
consistency of the actual result with the given pattern. For this we are+ −
going to implement the document antiquotation:+ −
+ −
+ −
@{text [display] "@{ML_resp \"a_piece_of_code\" \"a_pattern\"}"}+ −
+ −
To add some convenience and also to deal with large outputs, the user can+ −
give a partial specification by using ellipses. For example @{text "(\<dots>, \<dots>)"}+ −
for specifying a pair. In order to check consistency between the pattern+ −
and the output of the code, we have to change the ML-expression that is sent + −
to the compiler: in @{text "ML_checked"} we sent the expression @{text [quotes]+ −
"val _ = a_piece_of_code"} to the compiler; now the wildcard @{text "_"}+ −
must be be replaced by the given pattern. However, we have to remove all+ −
ellipses from it and replace them by @{text [quotes] "_"}. The following + −
function will do this:+ −
*}+ −
+ −
ML{*fun ml_pat (code_txt, pat) =+ −
let val pat' = + −
implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))+ −
in + −
"val " ^ pat' ^ " = " ^ code_txt + −
end*}+ −
+ −
text {* + −
Next we add a response indicator to the result using:+ −
*}+ −
+ −
+ −
ML{*fun add_resp pat = map (fn s => "> " ^ s) pat*}+ −
+ −
text {* + −
The rest of the code of @{text "ML_resp"} is: + −
*}+ −
+ −
ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = + −
(ML_Context.eval_text_in (SOME ctxt) false pos (ml_pat (code_txt, pat));+ −
let + −
val code_output = space_explode "\n" code_txt + −
val resp_output = add_resp (space_explode "\n" pat)+ −
in + −
Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) + −
end)+ −
+ −
val _ = Thy_Output.antiquotation "ML_resp" + −
(Scan.lift (Parse.position (Args.name -- Args.name))) + −
output_ml_resp*}+ −
+ −
text {*+ −
In comparison with @{text "ML_checked"}, we only changed the line about + −
the compiler (Line~2), the lines about+ −
the output (Lines 4 to 7) and the parser in the setup (Line 11). Now + −
you can write+ −
+ −
@{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"}+ −
+ −
to obtain+ −
+ −
@{ML_resp [display] "true andalso false" "false"} + −
+ −
or + −
+ −
@{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i, \"foo\") end\" \"(9, \<dots>)\"}"}+ −
+ −
to obtain+ −
+ −
@{ML_resp [display] "let val i = 3 in (i * i, \"foo\") end" "(9, \<dots>)"} + −
+ −
In both cases, the check by the compiler ensures that code and result+ −
match. A limitation of this document antiquotation, however, is that the+ −
pattern can only be given for values that can be constructed. This excludes+ −
values that are abstract datatypes, like @{ML_type thm}s and @{ML_type cterm}s.+ −
+ −
*}+ −
end+ −