Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CookBook/Recipes/Antiquotes.thy
changeset 168 009ca4807baa
parent 165 890fbfef6d6b
child 171 18f90044c777
equal deleted inserted replaced
167:3e30ea95c7aa 168:009ca4807baa 
    34   "ML_Context.eval_in"} in Line 4 below). The complete code of the
 
    34   "ML_Context.eval_in"} in Line 4 below). The complete code of the
 
    35   antiquotation is as follows:
 
    35   antiquotation is as follows:
 
    36 
    36 
    37 *}
 
    37 *}
 
    38 
    38 
    39 ML {* Pretty.str *}
 
       
    40 
       
    41 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
 
    39 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
 
    42 
    40 
    43 fun output_ml {source = src, context = ctxt, ...} code_txt =
 
    41 fun output_ml {context = ctxt, ...} code_txt =
 
    44   (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); 
    42   (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); 
    45   ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
 
    43    ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
 
    46 
    44 
    47 val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}
 
    45 val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}
 
    48 
    46 
    49 text {*
 
    47 text {*
 
    50 
    48 
    51   Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, 
    49   Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, 
    52   in this case the code given as argument. As mentioned before, this argument 
    50   in this case the code. As mentioned before, the code
 
    53   is sent to the ML-compiler in the line 4 using the function @{ML ml_val},
 
    51   is sent to the ML-compiler in the line 4 using the function @{ML ml_val},
 
    54   which constructs the appropriate ML-expression.
 
    52   which constructs the appropriate ML-expression.
 
    55   If the code is ``approved'' by the compiler, then the output function @{ML
 
    53   If the code is ``approved'' by the compiler, then the output function @{ML
 
    56   "ThyOutput.output"} in the next line pretty prints the
 
    54   "ThyOutput.output"} in the next line pretty prints the
 
    57   code. This function expects that the code is a list of strings where each
 
    55   code. This function expects that the code is a list of strings where each
 
    58   string correspond to a line in the output. Therefore the use of 
    56   string correspond to a line in the output. Therefore the use of 
    59   @{ML "(space_explode \"\\n\" txt)" for txt} 
    57   @{ML "(space_explode \"\\n\" txt)" for txt} 
    60   which produces this list according to linebreaks.  There are a number of options 
    58   which produces this list according to linebreaks.  There are a number of options 
    61   for antiquotations that are observed by @{ML ThyOutput.output} when printing the 
    59   for antiquotations that are observed by @{ML ThyOutput.output} when printing the 
    62   code (including @{text "[display]"} and @{text "[quotes]"}).
 
    60   code (including @{text "[display]"} and @{text "[quotes]"}). Line 7 sets 
       
    61   up the new antiquotation.
 
    63 
    62 
    64   \begin{readmore}
 
    63   \begin{readmore}
 
    65   For more information about options of antiquotations see \rsccite{sec:antiq}).
 
    64   For more information about options of antiquotations see \rsccite{sec:antiq}).
 
    66   \end{readmore}
 
    65   \end{readmore}
 
    67 
    66 
    68   Since we used the argument @{ML "Position.none"}, the compiler cannot give specific 
    67   Since we used the argument @{ML "Position.none"}, the compiler cannot give specific 
    69   information about the line number, in case an error is detected. We 
    68   information about the line number, in case an error is detected. We 
    70   can improve the code above slightly by writing 
    69   can improve the code above slightly by writing 
    71 *}
 
    70 *}
 
    72 
    71 
    73 ML%linenosgray{*fun output_ml {source = src, context = ctxt, ...} (code_txt,pos) =
 
    72 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt,pos) =
 
    74   (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
 
    73   (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
 
    75   ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
 
    74    ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
 
    76 
    75 
    77 val _ = ThyOutput.antiquotation "ML_checked"
 
    76 val _ = ThyOutput.antiquotation "ML_checked"
 
    78        (Scan.lift (OuterParse.position Args.name)) output_ml *}
 
    77          (Scan.lift (OuterParse.position Args.name)) output_ml *}
 
    79 
    78 
    80 text {*
 
    79 text {*
 
    81   where in Lines 1 and 2 the positional information is properly treated.
 
    80   where in Lines 1 and 2 the positional information is properly treated.
 
    82 
       
    83   (FIXME: say something about OuterParse.position)
 
       
    84 
    81 
    85   We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to
 
    82   We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to
 
    86   obtain @{ML_checked "2 + 3"} and be sure that this code compiles until
 
    83   obtain @{ML_checked "2 + 3"} and be sure that this code compiles until
 
    87   somebody changes the definition of \mbox{@{ML "(op +)"}}.
 
    84   somebody changes the definition of \mbox{@{ML "(op +)"}}.
 
    88 
    85 
    89 
    86 
    90   The second antiquotation we describe extends the first by allowing also to give
 
    87   The second antiquotation we describe extends the first by a pattern that 
    91   a pattern that specifies what the result of the ML-code should be and to check 
    88   specifies what the result of the ML-code should be and check 
    92   the consistency of the actual result with the given pattern. For this we are going 
    89   the consistency of the actual result with the given pattern. For this we are going 
    93   to implement the antiquotation  
    90   to implement the antiquotation  
    94   
    91   
    95   @{text [display] "@{ML_resp \"a_piece_of_code\" \"pattern\"}"}
 
    92   @{text [display] "@{ML_resp \"a_piece_of_code\" \"a_pattern\"}"}
 
    96   
    93   
    97   To add some convenience and also to deal with large outputs,
 
    94   To add some convenience and also to deal with large outputs, the user can
 
    98   the user can give a partial specification by giving the abbreviation 
    95   give a partial specification inside the pattern by giving abbreviations of
 
    99   @{text [quotes] "\<dots>"}. For example @{text "(\<dots>,\<dots>)"} for a pair.
 
    96   the form @{text [quotes] "\<dots>"}. For example @{text "(\<dots>, \<dots>)"} to specify a
 
       
    97   pair.
 
   100 
    98 
   101   Whereas in the antiquotation @{text "@{ML_checked \"piece_of_code\"}"} above, 
    99   Whereas in the antiquotation @{text "@{ML_checked \"piece_of_code\"}"}
 
   102   we have sent the expression 
   100   above, we have sent the expression @{text [quotes] "val _ = piece_of_code"}
 
   103   @{text [quotes] "val _ = piece_of_code"} to the compiler, in the second the 
   101   to the compiler, in the second the wildcard @{text "_"} we will be replaced
 
   104   wildcard @{text "_"} we will be replaced by a proper pattern. To do this we 
   102   by the given pattern. To do this we need to replace the @{text [quotes] "\<dots>"}
 
   105   need to replace the @{text [quotes] "\<dots>"} by 
   103   by @{text [quotes] "_"} before sending the code to the compiler. The
 
   106   @{text [quotes] "_"}  before sending the code to the compiler. The following 
   104   following function will do this:
 
   107   function will do this:
 
       
   108 
       
   109 *}
 
   105 *}
 
   110 
   106 
   111 ML{*fun ml_pat (code_txt, pat) =
 
   107 ML{*fun ml_pat (code_txt, pat) =
 
   112    let val pat' = 
   108 let val pat' = 
   113          implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
 
   109          implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
 
   114    in 
   110 in 
   115      "val " ^ pat' ^ " = " ^ code_txt 
   111   "val " ^ pat' ^ " = " ^ code_txt 
   116    end*}
 
   112 end*}
 
   117 
   113 
   118 text {* 
   114 text {* 
   119   Next we like to add a response indicator to the result using:
 
   115   Next we like to add a response indicator to the result using:
 
   120 *}
 
   116 *}
 
   121 
   117 
   125 
   121 
   126 text {* 
   122 text {* 
   127   The rest of the code of the antiquotation is
 
   123   The rest of the code of the antiquotation is
 
   128 *}
 
   124 *}
 
   129 
   125 
   130 ML{*fun output_ml_resp {source = src, context = ctxt, ...} ((code_txt,pat),pos) = 
   126 ML{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = 
   131   (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat));
 
   127   (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt, pat));
 
   132    let 
   128    let 
   133      val output = (space_explode "\n" code_txt) @ (add_resp_indicator pat)
 
   129      val output = (space_explode "\n" code_txt) @ (add_resp_indicator pat)
 
   134    in 
   130    in 
   135      ThyOutput.output (map Pretty.str output) 
   131      ThyOutput.output (map Pretty.str output) 
   136    end)
 
   132    end)
 
   137 
   133 
   138 val _ = ThyOutput.antiquotation "ML_resp" 
   134 val _ = ThyOutput.antiquotation "ML_resp" 
   139      (Scan.lift (OuterParse.position (Args.name -- Args.name))) output_ml_resp*}
 
   135          (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
       
   136            output_ml_resp*}
 
   140 
   137 
   141 text {*
 
   138 text {*
 
   142   This extended antiquotation allows us to write
 
   139   This extended antiquotation allows us to write
 
   143  
   140  
   144   @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"}
 
   141   @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"}
 
   147 
   144 
   148   @{ML_resp [display] "true andalso false" "false"} 
   145   @{ML_resp [display] "true andalso false" "false"} 
   149 
   146 
   150   or 
   147   or 
   151 
   148 
   152   @{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i,\"foo\") end\" \"(9,\<dots>)\"}"}
 
   149   @{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i, \"foo\") end\" \"(9, \<dots>)\"}"}
 
   153   
   150   
   154   to obtain
 
   151   to obtain
 
   155 
   152 
   156   @{ML_resp [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"} 
   153   @{ML_resp [display] "let val i = 3 in (i * i, \"foo\") end" "(9, \<dots>)"} 
   157 
   154 
   158   In both cases, the check by the compiler ensures that code and result match. A limitation
 
   155   In both cases, the check by the compiler ensures that code and result
 
   159   of this antiquotation, however, is that the hints can only be given in case
 
   156   match. A limitation of this antiquotation, however, is that the pattern can
 
   160   they can be constructed as a pattern. This excludes values that are abstract datatypes, like 
   157   only be given for values that can be constructed. This excludes
 
   161   theorems or cterms.
 
   158   values that are abstract datatypes, like theorems or cterms.
 
   162 
       
   163 *}
 
   159 *}
 
   164 end
 
   160 end
 
   165   
       
   166 
       
   167 
       
   168
isabelle-cookbook