6 |
6 |
7 section {* Useful Document Antiquotations *} |
7 section {* Useful Document Antiquotations *} |
8 |
8 |
9 text {* |
9 text {* |
10 {\bf Problem:} |
10 {\bf Problem:} |
11 How to keep ML-code included in a document in sync with the actual code.\smallskip |
11 How to keep your ML-code inside a document synchronised with the actual code?\smallskip |
12 |
12 |
13 {\bf Solution:} This can be achieved using document antiquotations.\smallskip |
13 {\bf Solution:} This can be achieved using document antiquotations.\smallskip |
14 |
14 |
15 Document antiquotations are a convenient method for type-setting consitently |
15 Document antiquotations can be used for ensuring consistent type-setting of |
16 a group of items in a document. They can also be used for sophisticated |
16 various entities in a document. They can also be used for sophisticated |
17 \LaTeX hacking. |
17 \LaTeX-hacking. |
18 |
18 |
19 Below we give the code for two such |
19 Below we give the code for two antiquotations that can be used to typeset |
20 antiquotations that can be used to typeset ML-code and also to check whether |
20 ML-code and also to check whether the given code actually compiles. This |
21 the code is actually compiles. In this way one can relatively easily |
21 provides a sanity check for the code and also allows one to keep documents |
22 keep documents in sync with code. |
22 in sync with other code, for example Isabelle. |
23 |
23 |
24 We first describe the antiquotation @{text "@{ML_checked \"\<dots>\"}"} which |
24 We first describe the antiquotation @{text "@{ML_checked \"\<dots>\"}"}. This |
25 takes a piece of code as argument. This code is checked by sending |
25 antiquotation takes a piece of code as argument; this code is then checked |
26 the ML-expression @{text "val _ = \<dots>"} containing the given code to the |
26 by sending the ML-expression @{text [quotes] "val _ = \<dots>"} containing the |
27 ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"}). The code |
27 given code to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"} |
28 for this antiquotation is as follows: |
28 in the snippet below). The code for @{text "@{ML_checked \"\<dots>\"}"} is as |
|
29 follows: |
|
30 |
29 *} |
31 *} |
30 |
32 |
31 ML {* |
33 ML %linenumbers {*fun ml_val txt = "val _ = " ^ txt |
32 fun ml_val txt = "val _ = " ^ txt |
|
33 |
34 |
34 fun output_ml ml src ctxt txt = |
35 fun output_ml ml src ctxt txt = |
35 (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt); |
36 (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt); |
36 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
37 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
37 (space_explode "\n" txt)) |
38 (space_explode "\n" txt)) |
38 |
39 |
39 val _ = ThyOutput.add_commands |
40 val _ = ThyOutput.add_commands |
40 [("ML_checked", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val))] |
41 [("ML_checked", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val))] |
41 *} |
42 *} |
42 |
43 |
43 text {* |
44 text {* |
44 |
45 |
45 Note that the parser @{ML "(Scan.lift Args.name)"} parses a string. If the |
46 Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
46 code is approved by the compiler, the output function |
47 in this case the code. This code is send to the ML-compiler in the line 4. |
47 @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} |
48 If the code is ``approved'' by the compiler, then the output function @{ML |
48 pretty prints the code. This function expects that the code is a list of strings |
49 "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the |
49 according to the line breaks (therefore the |
50 code. This function expects that the code is a list of strings where each |
50 @{ML_open "(space_explode \"\\n\" txt)" for txt} which produces this list). |
51 string correspond to a line (therefore the @{ML_open "(space_explode \"\\n\" txt)" for txt} |
51 There are a number of options that are observed by @{ML ThyOutput.output_list} |
52 which produces this list). There are a number of options for antiquotations |
52 when printing the code (for example @{text "[display]"} and @{text "[source]"}; |
53 that are observed by @{ML ThyOutput.output_list} when printing the code (for |
53 for more information about these options see \rsccite{sec:antiq}). |
54 example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). |
|
55 |
|
56 \begin{readmore} |
|
57 For more information about options of antiquotations see \rsccite{sec:antiq}). |
|
58 \end{readmore} |
54 |
59 |
55 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
60 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
56 information about the line number where an error might have occurred. We |
61 information about the line number where an error might have occurred. We |
57 can improve this code slightly by writing |
62 can improve this code slightly by writing |
58 |
63 |
59 The second |
|
60 *} |
64 *} |
61 |
65 |
62 ML {* |
66 ML {* |
63 fun output_ml ml src ctxt (txt,pos) = |
67 fun output_ml ml src ctxt (txt,pos) = |
64 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
68 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
70 (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val))] |
74 (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val))] |
71 *} |
75 *} |
72 |
76 |
73 text {* |
77 text {* |
74 (FIXME: say something about OuterParse.position) |
78 (FIXME: say something about OuterParse.position) |
|
79 |
|
80 We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to |
|
81 obtain @{ML_checked "2 + 3"} and be sure that this code compiles until |
|
82 somebody changes the definition of @{ML "(op +)"}. |
|
83 |
|
84 |
|
85 The second antiquotation extends the first by allowing to also give |
|
86 hints what the result of the ML-code is and check consistency of these |
|
87 hints. For this we use the antiquotation @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"} |
|
88 whose first argument is the ML-code and the second is the result. |
|
89 |
|
90 In the antiquotation @{text "@{ML_checked \"\<dots>\"}"} we send the expresion |
|
91 @{text [quotes] "val _ = \<dots>"} to the compiler. Now we will use the hints |
|
92 to construct a pattern for the @{text "_"}. To add some convenince we allow |
|
93 the user to give partial hints using @{text "\<dots>"}, which however need to |
|
94 be replaced by @{text "_"} before sending the code to the compiler. The |
|
95 function |
|
96 |
75 *} |
97 *} |
76 |
98 |
77 ML {* |
99 ML {* |
78 fun ml_pat (rhs, pat) = |
100 fun ml_pat (rhs, pat) = |
79 let val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
101 let val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
80 in |
102 in "val " ^ pat' ^ " = " ^ rhs end; |
81 "val " ^ pat' ^ " = " ^ rhs |
103 *} |
82 end; |
|
83 |
104 |
|
105 text {* |
|
106 will do this. Next we like to add a response indicator to the result using: |
|
107 *} |
|
108 |
|
109 |
|
110 ML {* |
84 fun add_response_indicator txt = |
111 fun add_response_indicator txt = |
85 map (fn s => "> " ^ s) (space_explode "\n" txt) |
112 map (fn s => "> " ^ s) (space_explode "\n" txt) |
|
113 *} |
86 |
114 |
|
115 text {* |
|
116 The rest of the code of the antiquotation is |
|
117 *} |
|
118 |
|
119 ML {* |
87 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
120 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
88 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
121 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
89 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
122 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
90 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
123 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
|
124 |
|
125 val _ = ThyOutput.add_commands |
|
126 [("ML_response", |
|
127 ThyOutput.args |
|
128 (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
|
129 (output_ml_response ml_pat))] |
91 *} |
130 *} |
92 |
131 |
93 |
132 text {* |
94 (* |
133 This extended antiquotation allows us to write |
95 val _ = ThyOutput.add_commands |
134 @{text [display] "@{ML_response [display] \"true andalso false\" \"false\"}"} |
96 [("ML_response", |
135 to obtain |
97 ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
|
98 (output_ml_response ml_pat)] |
|
99 *) |
|
100 |
|
101 |
|
102 ML {* |
|
103 |
|
104 let |
|
105 val i = 1 + 2 |
|
106 in |
|
107 i * i |
|
108 end |
|
109 |
|
110 *} |
|
111 |
|
112 (* |
|
113 A test: |
|
114 |
136 |
115 @{ML_response [display] "true andalso false" "false"} |
137 @{ML_response [display] "true andalso false" "false"} |
116 |
138 |
117 @{ML_response [display] |
139 or |
118 "let |
140 |
119 val i = 1 + 2 |
141 @{text [display] "@{ML_response [display] \"let val i = 3 in (i * i,\"foo\") end\" \"(9,\<dots>)\"}"} |
120 in |
142 |
121 i * i |
143 to obtain |
122 end" "9"} |
144 |
123 *) |
145 @{ML_response [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"} |
|
146 |
|
147 In both cases, the check by the compiler ensures that code and result match. A limitation |
|
148 of this antiquotation is that the hints can only be given for results that can actually |
|
149 be constructed as a pattern. This excludes values that are abstract types, like |
|
150 theorems or cterms. |
|
151 |
|
152 *} |
124 |
153 |
125 |
154 |
126 |
155 |
127 end |
156 end |
128 |
157 |