46
|
1 |
|
|
2 |
theory Antiquotes
|
346
|
3 |
imports "../Appendix"
|
46
|
4 |
begin
|
|
5 |
|
565
|
6 |
section \<open>Useful Document Antiquotations\label{rec:docantiquotations}\<close>
|
46
|
7 |
|
565
|
8 |
text \<open>
|
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
|
565
|
17 |
\<close>
|
191
|
18 |
|
|
19 |
print_antiquotations
|
153
|
20 |
|
565
|
21 |
text \<open>
|
191
|
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 |
|
565
|
32 |
We first describe the antiquotation \<open>ML_checked\<close> with the syntax:
|
74
|
33 |
|
569
|
34 |
@{text [display] \<open>@{ML_checked "a_piece_of_code"}\<close>}
|
74
|
35 |
|
|
36 |
The code is checked by sending the ML-expression @{text [quotes] "val _ =
|
575
|
37 |
a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML \<open>ML_Context.eval_in\<close>} in Line 8 below). The complete code of the
|
175
|
38 |
document antiquotation is as follows:
|
51
|
39 |
|
565
|
40 |
\<close>
|
562
|
41 |
ML \<open>Input.pos_of\<close>
|
565
|
42 |
ML%linenosgray\<open>fun ml_enclose bg en source =
|
573
|
43 |
ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en;\<close>
|
46
|
44 |
|
565
|
45 |
ML%linenosgray\<open>fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt)
|
46
|
46 |
|
562
|
47 |
fun output_ml ctxt code_txt =
|
553
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
let
|
574
|
49 |
val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags
|
|
50 |
(Input.pos_of code_txt) (ml_val code_txt)
|
562
|
51 |
in
|
573
|
52 |
Pretty.str (fst (Input.source_content code_txt))
|
553
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
end
|
46
|
54 |
|
574
|
55 |
val ml_checked_setup = Thy_Output.antiquotation_pretty_source
|
|
56 |
@{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close>
|
471
|
57 |
|
565
|
58 |
setup \<open>ml_checked_setup\<close>
|
46
|
59 |
|
562
|
60 |
|
565
|
61 |
text \<open>
|
575
|
62 |
The parser @{ML \<open>(Scan.lift Args.text_input)\<close>} in Line 15 parses a string, in this
|
|
63 |
case the code, and then we call the function @{ML output_ml}. As mentioned
|
|
64 |
before, the parsed code is sent to the ML-compiler in Line 8 using the
|
191
|
65 |
function @{ML ml_val}, which constructs the appropriate ML-expression, and
|
569
|
66 |
using @{ML \<open>eval_in\<close> in ML_Context}, which calls the compiler. If the code is
|
575
|
67 |
``approved'' by the compiler, then the output given to @{ML \<open>antiquotation_pretty_source\<close> in
|
|
68 |
Thy_Output} in the Line 15 pretty prints the code. This function expects
|
|
69 |
that the code is (pretty) string. There are a
|
191
|
70 |
number of options for antiquotations that are observed by the function
|
569
|
71 |
@{ML \<open>output\<close> in Document_Antiquotation} when printing the code (including \<open>[display]\<close>
|
575
|
72 |
and \<open>[quotes]\<close>).
|
51
|
73 |
|
|
74 |
\begin{readmore}
|
175
|
75 |
For more information about options of document antiquotations see \rsccite{sec:antiq}).
|
51
|
76 |
\end{readmore}
|
46
|
77 |
|
565
|
78 |
\<close>
|
46
|
79 |
|
565
|
80 |
text \<open>
|
175
|
81 |
The second document antiquotation we describe extends the first by a pattern
|
191
|
82 |
that specifies what the result of the ML-code should be and checks the
|
175
|
83 |
consistency of the actual result with the given pattern. For this we are
|
191
|
84 |
going to implement the document antiquotation:
|
175
|
85 |
|
74
|
86 |
|
569
|
87 |
@{text [display] \<open>@{ML_resp "a_piece_of_code" "a_pattern"}\<close>}
|
74
|
88 |
|
168
|
89 |
To add some convenience and also to deal with large outputs, the user can
|
565
|
90 |
give a partial specification by using ellipses. For example \<open>(\<dots>, \<dots>)\<close>
|
191
|
91 |
for specifying a pair. In order to check consistency between the pattern
|
|
92 |
and the output of the code, we have to change the ML-expression that is sent
|
575
|
93 |
to the compiler:
|
565
|
94 |
\<close>
|
46
|
95 |
|
565
|
96 |
ML%linenosgray\<open>fun ml_pat pat code =
|
574
|
97 |
ML_Lex.read "val" @
|
|
98 |
ML_Lex.read_source pat @
|
|
99 |
ML_Lex.read " = " @
|
|
100 |
ML_Lex.read_source code\<close>
|
562
|
101 |
|
565
|
102 |
text \<open>
|
191
|
103 |
Next we add a response indicator to the result using:
|
565
|
104 |
\<close>
|
51
|
105 |
|
565
|
106 |
ML %grayML\<open>fun add_resp pat = map (fn s => "> " ^ s) pat\<close>
|
46
|
107 |
|
565
|
108 |
text \<open>
|
|
109 |
The rest of the code of \<open>ML_resp\<close> is:
|
|
110 |
\<close>
|
51
|
111 |
|
562
|
112 |
ML %linenosgray\<open>
|
|
113 |
fun output_ml_resp ctxt (code_txt, pat) =
|
|
114 |
let
|
574
|
115 |
val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags
|
|
116 |
(Input.pos_of code_txt) (ml_pat pat code_txt)
|
573
|
117 |
val code = space_explode "\n" (fst (Input.source_content code_txt))
|
|
118 |
val resp = add_resp (space_explode "\n" (fst (Input.source_content pat)))
|
562
|
119 |
in
|
|
120 |
Pretty.str (cat_lines (code @ resp))
|
|
121 |
end
|
|
122 |
|
574
|
123 |
val ml_response_setup = Thy_Output.antiquotation_pretty_source
|
|
124 |
@{binding "ML_resp"}
|
|
125 |
(Scan.lift (Args.text_input -- Args.text_input))
|
|
126 |
output_ml_resp
|
562
|
127 |
|
|
128 |
\<close>
|
|
129 |
|
565
|
130 |
setup \<open>ml_response_setup\<close>
|
46
|
131 |
|
562
|
132 |
(* FIXME *)
|
565
|
133 |
text \<open>
|
575
|
134 |
In comparison with \<open>ML_checked\<close>, we changed the line about
|
|
135 |
the compiler (Lines 4 to 5), the lines about
|
|
136 |
the output (Lines 6 to 7 and 9) and the parser setup (Line 14). Now
|
191
|
137 |
you can write
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
138 |
|
569
|
139 |
@{text [display] \<open>@{ML_resp [display] "true andalso false" "false"}\<close>}
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
140 |
|
51
|
141 |
to obtain
|
46
|
142 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
143 |
@{ML_resp [display] "true andalso false" "false"}
|
46
|
144 |
|
51
|
145 |
or
|
|
146 |
|
569
|
147 |
@{text [display] \<open>@{ML_resp [display] "let val i = 3 in (i * i, "foo") end" "(9, \<dots>)"}\<close>}
|
51
|
148 |
|
|
149 |
to obtain
|
|
150 |
|
562
|
151 |
@{ML_resp [display] "let val i = 3 in (i * i, \"foo\") end" "(9, _)"}
|
51
|
152 |
|
168
|
153 |
In both cases, the check by the compiler ensures that code and result
|
175
|
154 |
match. A limitation of this document antiquotation, however, is that the
|
|
155 |
pattern can only be given for values that can be constructed. This excludes
|
|
156 |
values that are abstract datatypes, like @{ML_type thm}s and @{ML_type cterm}s.
|
|
157 |
|
565
|
158 |
\<close>
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
159 |
end
|