diff -r 3d4b49921cdb -r c346c156a7cd CookBook/Recipes/Antiquotes.thy --- a/CookBook/Recipes/Antiquotes.thy Tue Nov 25 05:19:27 2008 +0000 +++ b/CookBook/Recipes/Antiquotes.thy Fri Nov 28 05:19:55 2008 +0100 @@ -8,31 +8,32 @@ text {* {\bf Problem:} - How to keep ML-code included in a document in sync with the actual code.\smallskip + How to keep your ML-code inside a document synchronised with the actual code?\smallskip {\bf Solution:} This can be achieved using document antiquotations.\smallskip - Document antiquotations are a convenient method for type-setting consitently - a group of items in a document. They can also be used for sophisticated - \LaTeX hacking. + 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. - Below we give the code for two such - antiquotations that can be used to typeset ML-code and also to check whether - the code is actually compiles. In this way one can relatively easily - keep documents in sync with code. + Below we give the code for two antiquotations that can be used to typeset + ML-code and also to check whether the given code actually compiles. This + provides a sanity check for the code and also allows one to keep documents + in sync with other code, for example Isabelle. - We first describe the antiquotation @{text "@{ML_checked \"\\"}"} which - takes a piece of code as argument. This code is checked by sending - the ML-expression @{text "val _ = \"} containing the given code to the - ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"}). The code - for this antiquotation is as follows: + We first describe the antiquotation @{text "@{ML_checked \"\\"}"}. This + antiquotation takes a piece of code as argument; this code is then checked + by sending the ML-expression @{text [quotes] "val _ = \"} containing the + given code to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"} + in the snippet below). The code for @{text "@{ML_checked \"\\"}"} is as + follows: + *} -ML {* -fun ml_val txt = "val _ = " ^ txt +ML %linenumbers {*fun ml_val txt = "val _ = " ^ txt fun output_ml ml src ctxt txt = - (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt); + (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt); ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) @@ -41,22 +42,25 @@ *} text {* - - Note that the parser @{ML "(Scan.lift Args.name)"} parses a string. If the - code is approved by the compiler, the output function - @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} - pretty prints the code. This function expects that the code is a list of strings - according to the line breaks (therefore the - @{ML_open "(space_explode \"\\n\" txt)" for txt} which produces this list). - There are a number of options that are observed by @{ML ThyOutput.output_list} - when printing the code (for example @{text "[display]"} and @{text "[source]"}; - for more information about these options see \rsccite{sec:antiq}). + + Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, + in this case the code. This code is send to the ML-compiler in the line 4. + If the code is ``approved'' by the compiler, then the output function @{ML + "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the + code. This function expects that the code is a list of strings where each + string correspond to a line (therefore the @{ML_open "(space_explode \"\\n\" txt)" for txt} + which produces this list). There are a number of options for antiquotations + that are observed by @{ML ThyOutput.output_list} when printing the code (for + example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). + + \begin{readmore} + For more information about options of 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 where an error might have occurred. We can improve this code slightly by writing - The second *} ML {* @@ -72,55 +76,80 @@ text {* (FIXME: say something about OuterParse.position) + + We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to + obtain @{ML_checked "2 + 3"} and be sure that this code compiles until + somebody changes the definition of @{ML "(op +)"}. + + + The second antiquotation extends the first by allowing to also give + hints what the result of the ML-code is and check consistency of these + hints. For this we use the antiquotation @{text "@{ML_response \"\\" \"\\"}"} + whose first argument is the ML-code and the second is the result. + + In the antiquotation @{text "@{ML_checked \"\\"}"} we send the expresion + @{text [quotes] "val _ = \"} to the compiler. Now we will use the hints + to construct a pattern for the @{text "_"}. To add some convenince we allow + the user to give partial hints using @{text "\"}, which however need to + be replaced by @{text "_"} before sending the code to the compiler. The + function + *} ML {* fun ml_pat (rhs, pat) = - let val pat' = implode (map (fn "\" => "_" | s => s) (Symbol.explode pat)) - in - "val " ^ pat' ^ " = " ^ rhs - end; +let val pat' = implode (map (fn "\" => "_" | s => s) (Symbol.explode pat)) +in "val " ^ pat' ^ " = " ^ rhs end; +*} +text {* + will do this. Next we like to add a response indicator to the result using: +*} + + +ML {* fun add_response_indicator txt = map (fn s => "> " ^ s) (space_explode "\n" txt) +*} +text {* + The rest of the code of the antiquotation is + *} + +ML {* fun output_ml_response ml src ctxt ((lhs,pat),pos) = (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) -*} - -(* val _ = ThyOutput.add_commands [("ML_response", - ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) - (output_ml_response ml_pat)] -*) - - -ML {* - -let - val i = 1 + 2 -in - i * i -end - + ThyOutput.args + (Scan.lift (OuterParse.position (Args.name -- Args.name))) + (output_ml_response ml_pat))] *} -(* -A test: +text {* + This extended antiquotation allows us to write + @{text [display] "@{ML_response [display] \"true andalso false\" \"false\"}"} + to obtain @{ML_response [display] "true andalso false" "false"} -@{ML_response [display] -"let - val i = 1 + 2 -in - i * i -end" "9"} -*) + or + +@{text [display] "@{ML_response [display] \"let val i = 3 in (i * i,\"foo\") end\" \"(9,\)\"}"} + + to obtain + +@{ML_response [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\)"} + + In both cases, the check by the compiler ensures that code and result match. A limitation + of this antiquotation is that the hints can only be given for results that can actually + be constructed as a pattern. This excludes values that are abstract types, like + theorems or cterms. + +*}