46
|
1 |
|
|
2 |
theory Antiquotes
|
346
|
3 |
imports "../Appendix"
|
46
|
4 |
begin
|
|
5 |
|
292
|
6 |
section {* Useful Document Antiquotations\label{rec:docantiquotations} *}
|
46
|
7 |
|
|
8 |
text {*
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
9 |
{\bf Problem:}
|
51
|
10 |
How to keep your ML-code inside a document synchronised with the actual code?\smallskip
|
46
|
11 |
|
191
|
12 |
{\bf Solution:} This can be achieved with document antiquotations.\smallskip
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
|
51
|
14 |
Document antiquotations can be used for ensuring consistent type-setting of
|
|
15 |
various entities in a document. They can also be used for sophisticated
|
191
|
16 |
\LaTeX-hacking. If you type on the Isabelle level
|
|
17 |
*}
|
|
18 |
|
|
19 |
print_antiquotations
|
153
|
20 |
|
191
|
21 |
text {*
|
|
22 |
you obtain a list of all currently available document antiquotations and
|
|
23 |
their options.
|
46
|
24 |
|
191
|
25 |
Below we will give the code for two additional document
|
|
26 |
antiquotations both of which are intended to typeset ML-code. The crucial point
|
|
27 |
of these document antiquotations is that they not just print the ML-code, but also
|
|
28 |
check whether it compiles. This will provide a sanity check for the code
|
|
29 |
and also allows you to keep documents in sync with other code, for example
|
|
30 |
Isabelle.
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
|
74
|
32 |
We first describe the antiquotation @{text "ML_checked"} with the syntax:
|
|
33 |
|
|
34 |
@{text [display] "@{ML_checked \"a_piece_of_code\"}"}
|
|
35 |
|
|
36 |
The code is checked by sending the ML-expression @{text [quotes] "val _ =
|
|
37 |
a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML
|
438
|
38 |
"ML_Context.eval_text_in"} in Line 4 below). The complete code of the
|
175
|
39 |
document antiquotation is as follows:
|
51
|
40 |
|
46
|
41 |
*}
|
|
42 |
|
114
|
43 |
ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
|
46
|
44 |
|
168
|
45 |
fun output_ml {context = ctxt, ...} code_txt =
|
438
|
46 |
(ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt);
|
449
|
47 |
Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
|
46
|
48 |
|
471
|
49 |
val ml_checked_setup = Thy_Output.antiquotation @{binding "ML_checked"} (Scan.lift Args.name) output_ml*}
|
|
50 |
|
|
51 |
setup {* ml_checked_setup *}
|
46
|
52 |
|
|
53 |
text {*
|
191
|
54 |
The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this
|
|
55 |
case the code, and then calls the function @{ML output_ml}. As mentioned
|
|
56 |
before, the parsed code is sent to the ML-compiler in Line 4 using the
|
|
57 |
function @{ML ml_val}, which constructs the appropriate ML-expression, and
|
|
58 |
using @{ML "eval_in" in ML_Context}, which calls the compiler. If the code is
|
|
59 |
``approved'' by the compiler, then the output function @{ML "output" in
|
438
|
60 |
Thy_Output} in the next line pretty prints the code. This function expects
|
191
|
61 |
that the code is a list of (pretty)strings where each string correspond to a
|
|
62 |
line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)"
|
|
63 |
for txt} which produces such a list according to linebreaks. There are a
|
|
64 |
number of options for antiquotations that are observed by the function
|
438
|
65 |
@{ML "output" in Thy_Output} when printing the code (including @{text "[display]"}
|
|
66 |
and @{text "[quotes]"}). The function @{ML "antiquotation" in Thy_Output} in
|
191
|
67 |
Line 7 sets up the new document antiquotation.
|
51
|
68 |
|
|
69 |
\begin{readmore}
|
175
|
70 |
For more information about options of document antiquotations see \rsccite{sec:antiq}).
|
51
|
71 |
\end{readmore}
|
46
|
72 |
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
Since we used the argument @{ML "Position.none"}, the compiler cannot give specific
|
59
|
74 |
information about the line number, in case an error is detected. We
|
|
75 |
can improve the code above slightly by writing
|
46
|
76 |
*}
|
|
77 |
|
171
|
78 |
ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) =
|
438
|
79 |
(ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt);
|
449
|
80 |
Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
|
46
|
81 |
|
471
|
82 |
val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"}
|
426
|
83 |
(Scan.lift (Parse.position Args.name)) output_ml *}
|
46
|
84 |
|
471
|
85 |
setup {* ml_checked_setup2 *}
|
|
86 |
|
46
|
87 |
text {*
|
171
|
88 |
where in Lines 1 and 2 the positional information is properly treated. The
|
426
|
89 |
parser @{ML Parse.position} encodes the positional information in the
|
171
|
90 |
result.
|
58
|
91 |
|
471
|
92 |
We can now write @{text "@{ML_checked2 \"2 + 3\"}"} in a document in order to
|
|
93 |
obtain @{ML_checked2 "2 + 3"} and be sure that this code compiles until
|
191
|
94 |
somebody changes the definition of addition.
|
51
|
95 |
|
|
96 |
|
175
|
97 |
The second document antiquotation we describe extends the first by a pattern
|
191
|
98 |
that specifies what the result of the ML-code should be and checks the
|
175
|
99 |
consistency of the actual result with the given pattern. For this we are
|
191
|
100 |
going to implement the document antiquotation:
|
175
|
101 |
|
74
|
102 |
|
168
|
103 |
@{text [display] "@{ML_resp \"a_piece_of_code\" \"a_pattern\"}"}
|
74
|
104 |
|
168
|
105 |
To add some convenience and also to deal with large outputs, the user can
|
191
|
106 |
give a partial specification by using ellipses. For example @{text "(\<dots>, \<dots>)"}
|
|
107 |
for specifying a pair. In order to check consistency between the pattern
|
|
108 |
and the output of the code, we have to change the ML-expression that is sent
|
471
|
109 |
to the compiler: in @{text "ML_checked2"} we sent the expression @{text [quotes]
|
191
|
110 |
"val _ = a_piece_of_code"} to the compiler; now the wildcard @{text "_"}
|
|
111 |
must be be replaced by the given pattern. However, we have to remove all
|
|
112 |
ellipses from it and replace them by @{text [quotes] "_"}. The following
|
|
113 |
function will do this:
|
46
|
114 |
*}
|
|
115 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
116 |
ML %grayML{*fun ml_pat (code_txt, pat) =
|
168
|
117 |
let val pat' =
|
59
|
118 |
implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
|
168
|
119 |
in
|
|
120 |
"val " ^ pat' ^ " = " ^ code_txt
|
|
121 |
end*}
|
46
|
122 |
|
51
|
123 |
text {*
|
191
|
124 |
Next we add a response indicator to the result using:
|
51
|
125 |
*}
|
|
126 |
|
|
127 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
128 |
ML %grayML{*fun add_resp pat = map (fn s => "> " ^ s) pat*}
|
46
|
129 |
|
51
|
130 |
text {*
|
191
|
131 |
The rest of the code of @{text "ML_resp"} is:
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
132 |
*}
|
51
|
133 |
|
191
|
134 |
ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) =
|
438
|
135 |
(ML_Context.eval_text_in (SOME ctxt) false pos (ml_pat (code_txt, pat));
|
59
|
136 |
let
|
191
|
137 |
val code_output = space_explode "\n" code_txt
|
|
138 |
val resp_output = add_resp (space_explode "\n" pat)
|
59
|
139 |
in
|
449
|
140 |
Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output))
|
59
|
141 |
end)
|
46
|
142 |
|
471
|
143 |
val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"}
|
426
|
144 |
(Scan.lift (Parse.position (Args.name -- Args.name)))
|
191
|
145 |
output_ml_resp*}
|
46
|
146 |
|
471
|
147 |
setup {* ml_resp_setup *}
|
|
148 |
|
51
|
149 |
text {*
|
471
|
150 |
In comparison with @{text "ML_checked2"}, we only changed the line about
|
191
|
151 |
the compiler (Line~2), the lines about
|
|
152 |
the output (Lines 4 to 7) and the parser in the setup (Line 11). Now
|
|
153 |
you can write
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
154 |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
155 |
@{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"}
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
156 |
|
51
|
157 |
to obtain
|
46
|
158 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
159 |
@{ML_resp [display] "true andalso false" "false"}
|
46
|
160 |
|
51
|
161 |
or
|
|
162 |
|
168
|
163 |
@{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i, \"foo\") end\" \"(9, \<dots>)\"}"}
|
51
|
164 |
|
|
165 |
to obtain
|
|
166 |
|
168
|
167 |
@{ML_resp [display] "let val i = 3 in (i * i, \"foo\") end" "(9, \<dots>)"}
|
51
|
168 |
|
168
|
169 |
In both cases, the check by the compiler ensures that code and result
|
175
|
170 |
match. A limitation of this document antiquotation, however, is that the
|
|
171 |
pattern can only be given for values that can be constructed. This excludes
|
|
172 |
values that are abstract datatypes, like @{ML_type thm}s and @{ML_type cterm}s.
|
|
173 |
|
51
|
174 |
*}
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
175 |
end
|