19 Below we give the code for two antiquotations that can be used to typeset |
19 Below we give the code for two antiquotations that can be used to typeset |
20 ML-code and also to check whether the given code actually compiles. This |
20 ML-code and also to check whether the given code actually compiles. This |
21 provides a sanity check for the code and also allows one to keep documents |
21 provides a sanity check for the code and also allows one to keep documents |
22 in sync with other code, for example Isabelle. |
22 in sync with other code, for example Isabelle. |
23 |
23 |
24 We first describe the antiquotation @{text "@{ML_checked \"\<dots>\"}"}. This |
24 We first describe the antiquotation @{text "@{ML_checked \"expr\"}"}. This |
25 antiquotation takes a piece of code as argument; this code is then checked |
25 antiquotation takes a piece of code as argument. The argument is checked |
26 by sending the ML-expression @{text [quotes] "val _ = \<dots>"} containing the |
26 by sending the ML-expression @{text [quotes] "val _ = \<dots>"} containing the |
27 given code to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"} |
27 given argument to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"} |
28 in the snippet below). The code for @{text "@{ML_checked \"\<dots>\"}"} is as |
28 in Line 4 in the code below). The code of @{text "@{ML_checked \"expr\"}"} |
29 follows: |
29 is as follows: |
30 |
30 |
31 *} |
31 *} |
32 |
32 |
33 ML %linenumbers {*fun ml_val txt = "val _ = " ^ txt |
33 ML %linenumbers {*fun ml_val txt = "val _ = " ^ txt |
34 |
34 |
42 *} |
42 *} |
43 |
43 |
44 text {* |
44 text {* |
45 |
45 |
46 Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
46 Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
47 in this case the code. This code is send to the ML-compiler in the line 4. |
47 in this case the code given as argument. This argument is send to the ML-compiler in the line 4. |
48 If the code is ``approved'' by the compiler, then the output function @{ML |
48 If the code is ``approved'' by the compiler, then the output function @{ML |
49 "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the |
49 "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the |
50 code. This function expects that the code is a list of strings where each |
50 code. This function expects that the code is a list of strings where each |
51 string correspond to a line (therefore the @{ML "(space_explode \"\\n\" txt)" for txt} |
51 string correspond to a line. Therefore the @{ML "(space_explode \"\\n\" txt)" for txt} |
52 which produces this list). There are a number of options for antiquotations |
52 which produces this list. There are a number of options for antiquotations |
53 that are observed by @{ML ThyOutput.output_list} when printing the code (for |
53 that are observed by @{ML ThyOutput.output_list} when printing the code (for |
54 example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). |
54 example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). |
55 |
55 |
56 \begin{readmore} |
56 \begin{readmore} |
57 For more information about options of antiquotations see \rsccite{sec:antiq}). |
57 For more information about options of antiquotations see \rsccite{sec:antiq}). |
61 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 |
62 can improve this code slightly by writing |
62 can improve this code slightly by writing |
63 |
63 |
64 *} |
64 *} |
65 |
65 |
66 ML {* |
66 ML %linenumbers {* fun output_ml ml src ctxt (txt,pos) = |
67 fun output_ml ml src ctxt (txt,pos) = |
|
68 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
67 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
69 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
68 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
70 (space_explode "\n" txt)) |
69 (space_explode "\n" txt)) |
71 |
70 |
72 val _ = ThyOutput.add_commands |
71 val _ = ThyOutput.add_commands |
73 [("ML_checked", ThyOutput.args |
72 [("ML_checked", ThyOutput.args |
74 (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val))] |
73 (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val))] |
75 *} |
74 *} |
76 |
75 |
77 text {* |
76 text {* |
|
77 where in Lines 1 and 2 the positional information is properly treated. |
|
78 |
78 (FIXME: say something about OuterParse.position) |
79 (FIXME: say something about OuterParse.position) |
79 |
80 |
80 We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to |
81 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 obtain @{ML_checked "2 + 3"} and be sure that this code compiles until |
82 somebody changes the definition of @{ML "(op +)"}. |
83 somebody changes the definition of \mbox{@{ML "(op +)"}}. |
83 |
84 |
84 |
85 |
85 The second antiquotation extends the first by allowing to also give |
86 The second antiquotation extends the first by allowing also to give |
86 hints what the result of the ML-code is and check consistency of these |
87 hints what the result of the ML-code is and check the consistency of |
87 hints. For this we use the antiquotation @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"} |
88 the actual result with these hints. For this we use the antiquotation |
88 whose first argument is the ML-code and the second is the result. |
89 @{text "@{ML_response \"expr\" \"pat\"}"} |
|
90 whose first argument is the ML-code and the second is a pattern specifying |
|
91 the result. To add some convenience we allow the user to give a partial |
|
92 specification using @{text "\<dots>"}. |
89 |
93 |
90 In the antiquotation @{text "@{ML_checked \"\<dots>\"}"} we send the expresion |
94 In the antiquotation @{text "@{ML_checked \"expr\"}"} we send the expression |
91 @{text [quotes] "val _ = \<dots>"} to the compiler. Now we will use the hints |
95 @{text [quotes] "val _ = expr"} to the compiler. Instead of the wildcard |
92 to construct a pattern for the @{text "_"}. To add some convenince we allow |
96 @{text "_"}, we will here use the hints to construct a proper pattern. To |
93 the user to give partial hints using @{text "\<dots>"}, which however need to |
97 do this we need to replace the @{text "\<dots>"} by @{text "_"} before sending the |
94 be replaced by @{text "_"} before sending the code to the compiler. The |
98 code to the compiler. The function |
95 function |
|
96 |
99 |
97 *} |
100 *} |
98 |
101 |
99 ML {* |
102 ML {* |
100 fun ml_pat (rhs, pat) = |
103 fun ml_pat (rhs, pat) = |
101 let val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
104 let val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
102 in "val " ^ pat' ^ " = " ^ rhs end; |
105 in "val " ^ pat' ^ " = " ^ rhs end; |
103 *} |
106 *} |
104 |
107 |
105 text {* |
108 text {* |
106 will do this. Next we like to add a response indicator to the result using: |
109 will construct the pattern that the compiler can use. Next we like to add |
|
110 a response indicator to the result using: |
107 *} |
111 *} |
108 |
112 |
109 |
113 |
110 ML {* |
114 ML {* |
111 fun add_response_indicator txt = |
115 fun add_response_indicator txt = |