changed code generator invocation syntax
authorhaftmann
Sun May 06 21:50:17 2007 +0200 (2007-05-06)
changeset 228455f9138bcb3d7
parent 22844 91c05f4b509e
child 22846 fb79144af9a3
changed code generator invocation syntax
NEWS
doc-src/IsarAdvanced/Classes/Thy/Classes.thy
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
doc-src/IsarRef/logics.tex
src/HOL/Code_Generator.thy
src/HOL/Divides.thy
src/HOL/Extraction/Higman.thy
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Extraction/QuotRem.thy
src/HOL/FixedPoint.thy
src/HOL/Fun.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/Numeral.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/Eval.thy
src/HOL/Library/Graphs.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Pretty_Char_chr.thy
src/HOL/Library/Product_ord.thy
src/HOL/Library/Pure_term.thy
src/HOL/Library/SCT_Implementation.thy
src/HOL/Nat.thy
src/HOL/Set.thy
src/HOL/Wellfounded_Recursion.thy
src/HOL/ex/Classpackage.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/Codegenerator_Rat.thy
src/HOL/ex/NormalForm.thy
src/HOL/ex/Random.thy
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/codegen.ML
     1.1 --- a/NEWS	Sun May 06 21:49:44 2007 +0200
     1.2 +++ b/NEWS	Sun May 06 21:50:17 2007 +0200
     1.3 @@ -95,10 +95,10 @@
     1.4  
     1.5  Theorem attributs for selecting and transforming function equations theorems:
     1.6  
     1.7 -    [code fun]:       select a theorem as function equation for a specific constant
     1.8 -    [code nofun]:     deselect a theorem as function equation for a specific constant
     1.9 -    [code inline]:    select an equation theorem for unfolding (inlining) in place
    1.10 -    [code noinline]:  deselect an equation theorem for unfolding (inlining) in place
    1.11 +    [code fun]:        select a theorem as function equation for a specific constant
    1.12 +    [code fun del]:    deselect a theorem as function equation for a specific constant
    1.13 +    [code inline]:     select an equation theorem for unfolding (inlining) in place
    1.14 +    [code inline del]: deselect an equation theorem for unfolding (inlining) in place
    1.15  
    1.16  User-defined serializations (target in {SML, OCaml, Haskell}):
    1.17  
    1.18 @@ -519,6 +519,13 @@
    1.19  
    1.20  *** HOL ***
    1.21  
    1.22 +* case expressions and primrec: missing cases now mapped to "undefined"
    1.23 +instead of "arbitrary"
    1.24 +
    1.25 +* new constant "undefined" with axiom "undefined x = undefined"
    1.26 +
    1.27 +* new class "default" with associated constant "default"
    1.28 +
    1.29  * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
    1.30      when generating code.
    1.31  
    1.32 @@ -639,11 +646,11 @@
    1.33      meet_min                ~> inf_min
    1.34      join_max                ~> sup_max
    1.35  
    1.36 -* Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
    1.37 +* Classes "order" and "linorder": facts "refl", "trans" and
    1.38  "cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
    1.39  avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.
    1.40  
    1.41 -* Addes class (axclass + locale) "preorder" as superclass of "order";
    1.42 +* Classes "order" and "linorder": 
    1.43  potential INCOMPATIBILITY: order of proof goals in order/linorder instance
    1.44  proofs changed.
    1.45  
     2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Sun May 06 21:49:44 2007 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Sun May 06 21:50:17 2007 +0200
     2.3 @@ -459,7 +459,7 @@
     2.4    \noindent This maps to Haskell as:
     2.5  *}
     2.6  
     2.7 -code_gen example (Haskell "code_examples/")
     2.8 +code_gen example in Haskell file "code_examples/"
     2.9    (* NOTE: you may use Haskell only once in this document, otherwise
    2.10    you have to work in distinct subdirectories *)
    2.11  
    2.12 @@ -471,7 +471,7 @@
    2.13    \noindent The whole code in SML with explicit dictionary passing:
    2.14  *}
    2.15  
    2.16 -code_gen example (*<*)(SML #)(*>*)(SML "code_examples/classes.ML")
    2.17 +code_gen example (*<*)in SML(*>*)in SML file "code_examples/classes.ML"
    2.18  
    2.19  text {*
    2.20    \lstsml{Thy/code_examples/classes.ML}
     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Sun May 06 21:49:44 2007 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Sun May 06 21:50:17 2007 +0200
     3.3 @@ -143,7 +143,7 @@
     3.4    \noindent Then we generate code
     3.5  *}
     3.6  
     3.7 -code_gen example (*<*)(SML #)(*>*)(SML "examples/tree.ML")
     3.8 +code_gen example (*<*)in SML(*>*)in SML file "examples/tree.ML"
     3.9  
    3.10  text {*
    3.11    \noindent which looks like:
    3.12 @@ -221,15 +221,14 @@
    3.13    \noindent This executable specification is now turned to SML code:
    3.14  *}
    3.15  
    3.16 -code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac.ML")
    3.17 +code_gen fac (*<*)in SML(*>*)in SML file "examples/fac.ML"
    3.18  
    3.19  text {*
    3.20    \noindent  The @{text "\<CODEGEN>"} command takes a space-separated list of
    3.21    constants together with \qn{serialization directives}
    3.22 -  in parentheses. These start with a \qn{target language}
    3.23 -  identifier, followed by arguments, their semantics
    3.24 -  depending on the target. In the SML case, a filename
    3.25 -  is given where to write the generated code to.
    3.26 +  These start with a \qn{target language}
    3.27 +  identifier, followed by a file specification
    3.28 +  where to write the generated code to.
    3.29  
    3.30    Internally, the defining equations for all selected
    3.31    constants are taken, including any transitively required
    3.32 @@ -260,7 +259,7 @@
    3.33    pick_some :: "'a list \<Rightarrow> 'a" where
    3.34    "pick_some = hd"
    3.35  (*>*)
    3.36 -code_gen pick_some (SML "examples/fail_const.ML")
    3.37 +code_gen pick_some in SML file "examples/fail_const.ML"
    3.38  
    3.39  text {* \noindent will fail. *}
    3.40  
    3.41 @@ -304,7 +303,7 @@
    3.42    "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
    3.43    by simp
    3.44  
    3.45 -code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML")
    3.46 +code_gen pick (*<*)in SML(*>*) in SML file "examples/pick1.ML"
    3.47  
    3.48  text {*
    3.49    \noindent This theorem now is used for generating code:
    3.50 @@ -312,12 +311,12 @@
    3.51    \lstsml{Thy/examples/pick1.ML}
    3.52  
    3.53    \noindent It might be convenient to remove the pointless original
    3.54 -  equation, using the \emph{nofunc} attribute:
    3.55 +  equation, using the \emph{func del} attribute:
    3.56  *}
    3.57  
    3.58 -lemmas [code nofunc] = pick.simps 
    3.59 +lemmas [code func del] = pick.simps 
    3.60  
    3.61 -code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick2.ML")
    3.62 +code_gen pick (*<*)in SML(*>*) in SML file "examples/pick2.ML"
    3.63  
    3.64  text {*
    3.65    \lstsml{Thy/examples/pick2.ML}
    3.66 @@ -333,7 +332,7 @@
    3.67    "fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)"
    3.68    by (cases n) simp_all
    3.69  
    3.70 -code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac_case.ML")
    3.71 +code_gen fac (*<*)in SML(*>*)in SML file "examples/fac_case.ML"
    3.72  
    3.73  text {*
    3.74    \lstsml{Thy/examples/fac_case.ML}
    3.75 @@ -342,7 +341,7 @@
    3.76      The attributes \emph{code} and \emph{code del}
    3.77      associated with the existing code generator also apply to
    3.78      the new one: \emph{code} implies \emph{code func},
    3.79 -    and \emph{code del} implies \emph{code nofunc}.
    3.80 +    and \emph{code del} implies \emph{code func del}.
    3.81    \end{warn}
    3.82  *}
    3.83  
    3.84 @@ -392,10 +391,10 @@
    3.85    as SML, but, in accordance with conventions
    3.86    some Haskell systems enforce, each module ends
    3.87    up in a single file. The module hierarchy is reflected in
    3.88 -  the file system, with root given by the user.
    3.89 +  the file system, with root directory given as file specification.
    3.90  *}
    3.91  
    3.92 -code_gen dummy (Haskell "examples/")
    3.93 +code_gen dummy in Haskell file "examples/"
    3.94    (* NOTE: you may use Haskell only once in this document, otherwise
    3.95    you have to work in distinct subdirectories *)
    3.96  
    3.97 @@ -408,7 +407,7 @@
    3.98    The whole code in SML with explicit dictionary passing:
    3.99  *}
   3.100  
   3.101 -code_gen dummy (*<*)(SML #)(*>*)(SML "examples/class.ML")
   3.102 +code_gen dummy (*<*)in SML(*>*)in SML file "examples/class.ML"
   3.103  
   3.104  text {*
   3.105    \lstsml{Thy/examples/class.ML}
   3.106 @@ -418,13 +417,14 @@
   3.107    \noindent or in OCaml:
   3.108  *}
   3.109  
   3.110 -code_gen dummy (OCaml "examples/class.ocaml")
   3.111 +code_gen dummy in OCaml file "examples/class.ocaml"
   3.112  
   3.113  text {*
   3.114    \lstsml{Thy/examples/class.ocaml}
   3.115  
   3.116    \medskip The explicit association of constants
   3.117    to classes can be inspected using the @{text "\<PRINTCLASSES>"}
   3.118 +  command.
   3.119  *}
   3.120  
   3.121  
   3.122 @@ -496,38 +496,41 @@
   3.123    hand side and the arguments of the left hand side of an
   3.124    equation, but never to the constant heading the left hand side.
   3.125    Inline theorems may be declared an undeclared using the
   3.126 -  \emph{code inline} or \emph{code noinline} attribute respectively.
   3.127 +  \emph{code inline} or \emph{code inline del} attribute respectively.
   3.128    Some common applications:
   3.129  *}
   3.130  
   3.131  text_raw {*
   3.132    \begin{itemize}
   3.133 -     \item replacing non-executable constructs by executable ones: \\
   3.134 -*}     
   3.135 -
   3.136 -lemma [code inline]:
   3.137 -  "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
   3.138 -
   3.139 -text_raw {*
   3.140 -     \item eliminating superfluous constants: \\
   3.141  *}
   3.142  
   3.143 -lemma [code inline]:
   3.144 -  "1 = Suc 0" by simp
   3.145 +text {*
   3.146 +     \item replacing non-executable constructs by executable ones:
   3.147 +*}     
   3.148  
   3.149 -text_raw {*
   3.150 -     \item replacing executable but inconvenient constructs: \\
   3.151 +  lemma [code inline]:
   3.152 +    "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
   3.153 +
   3.154 +text {*
   3.155 +     \item eliminating superfluous constants:
   3.156  *}
   3.157  
   3.158 -lemma [code inline]:
   3.159 -  "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
   3.160 +  lemma [code inline]:
   3.161 +    "1 = Suc 0" by simp
   3.162 +
   3.163 +text {*
   3.164 +     \item replacing executable but inconvenient constructs:
   3.165 +*}
   3.166 +
   3.167 +  lemma [code inline]:
   3.168 +    "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
   3.169  
   3.170  text_raw {*
   3.171    \end{itemize}
   3.172  *}
   3.173  
   3.174  text {*
   3.175 -  The current set of inline theorems may be inspected using
   3.176 +  \noindent The current set of inline theorems may be inspected using
   3.177    the @{text "\<PRINTCODESETUP>"} command.
   3.178  
   3.179    \emph{Inline procedures} are a generalized version of inline
   3.180 @@ -580,7 +583,7 @@
   3.181    performs an explicit equality check.
   3.182  *}
   3.183  
   3.184 -code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML")
   3.185 +code_gen collect_duplicates (*<*)in SML(*>*)in SML file "examples/collect_duplicates.ML"
   3.186  
   3.187  text {*
   3.188    \lstsml{Thy/examples/collect_duplicates.ML}
   3.189 @@ -623,9 +626,9 @@
   3.190      "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
   3.191      x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" ..
   3.192  
   3.193 -lemmas [code nofunc] = less_prod_def less_eq_prod_def
   3.194 +lemmas [code func del] = less_prod_def less_eq_prod_def
   3.195  
   3.196 -lemma ord_prod [code func(*<*), code nofunc(*>*)]:
   3.197 +lemma ord_prod [code func(*<*), code func del(*>*)]:
   3.198    "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   3.199    "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
   3.200    unfolding less_prod_def less_eq_prod_def by simp_all
   3.201 @@ -653,7 +656,7 @@
   3.202  *}
   3.203  
   3.204  code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   3.205 -  (*<*)(SML #)(*>*)(SML "examples/lexicographic.ML")
   3.206 +  (*<*)in SML(*>*)in SML file "examples/lexicographic.ML"
   3.207  
   3.208  text {*
   3.209    \lstsml{Thy/examples/lexicographic.ML}
   3.210 @@ -713,7 +716,7 @@
   3.211  code_const %tt True and False and "op \<and>" and Not
   3.212    (SML and and and)
   3.213  (*>*)
   3.214 -code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_literal.ML")
   3.215 +code_gen in_interval (*<*)in SML(*>*)in SML file "examples/bool_literal.ML"
   3.216  
   3.217  text {*
   3.218    \lstsml{Thy/examples/bool_literal.ML}
   3.219 @@ -756,7 +759,7 @@
   3.220    After this setup, code looks quite more readable:
   3.221  *}
   3.222  
   3.223 -code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_mlbool.ML")
   3.224 +code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_mlbool.ML"
   3.225  
   3.226  text {*
   3.227    \lstsml{Thy/examples/bool_mlbool.ML}
   3.228 @@ -772,7 +775,7 @@
   3.229  code_const %tt "op \<and>"
   3.230    (SML infixl 1 "andalso")
   3.231  
   3.232 -code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_infix.ML")
   3.233 +code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_infix.ML"
   3.234  
   3.235  text {*
   3.236    \lstsml{Thy/examples/bool_infix.ML}
   3.237 @@ -901,7 +904,7 @@
   3.238  
   3.239  lemma [code func]: "\<Union>set xs = foldr (op \<union>) xs {}" by (induct xs) simp_all
   3.240  
   3.241 -code_gen "{}" insert "op \<in>" "op \<union>" "Union" (*<*)(SML #)(*>*)(SML "examples/set_list.ML")
   3.242 +code_gen "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML"
   3.243  
   3.244  text {*
   3.245    \lstsml{Thy/examples/set_list.ML}
   3.246 @@ -1025,7 +1028,7 @@
   3.247      "dummy_option (x#xs) = Some x"
   3.248    | "dummy_option [] = arbitrary"
   3.249  
   3.250 -code_gen dummy_option (*<*)(SML #)(*>*)(SML "examples/arbitrary.ML")
   3.251 +code_gen dummy_option (*<*)in SML(*>*)in SML file "examples/arbitrary.ML"
   3.252  
   3.253  text {*
   3.254    \lstsml{Thy/examples/arbitrary.ML}
     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Sun May 06 21:49:44 2007 +0200
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Sun May 06 21:50:17 2007 +0200
     4.3 @@ -172,7 +172,7 @@
     4.4  \end{isamarkuptext}%
     4.5  \isamarkuptrue%
     4.6  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
     4.7 -\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
     4.8 +\ example\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}%
     4.9  \begin{isamarkuptext}%
    4.10  \noindent which looks like:
    4.11    \lstsml{Thy/examples/tree.ML}%
    4.12 @@ -255,14 +255,13 @@
    4.13  \end{isamarkuptext}%
    4.14  \isamarkuptrue%
    4.15  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    4.16 -\ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
    4.17 +\ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}%
    4.18  \begin{isamarkuptext}%
    4.19  \noindent  The \isa{{\isasymCODEGEN}} command takes a space-separated list of
    4.20    constants together with \qn{serialization directives}
    4.21 -  in parentheses. These start with a \qn{target language}
    4.22 -  identifier, followed by arguments, their semantics
    4.23 -  depending on the target. In the SML case, a filename
    4.24 -  is given where to write the generated code to.
    4.25 +  These start with a \qn{target language}
    4.26 +  identifier, followed by a file specification
    4.27 +  where to write the generated code to.
    4.28  
    4.29    Internally, the defining equations for all selected
    4.30    constants are taken, including any transitively required
    4.31 @@ -309,7 +308,7 @@
    4.32  %
    4.33  \endisadelimML
    4.34  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    4.35 -\ pick{\isacharunderscore}some\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
    4.36 +\ pick{\isacharunderscore}some\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}%
    4.37  \begin{isamarkuptext}%
    4.38  \noindent will fail.%
    4.39  \end{isamarkuptext}%
    4.40 @@ -374,21 +373,21 @@
    4.41  \endisadelimproof
    4.42  \isanewline
    4.43  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    4.44 -\ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
    4.45 +\ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}%
    4.46  \begin{isamarkuptext}%
    4.47  \noindent This theorem now is used for generating code:
    4.48  
    4.49    \lstsml{Thy/examples/pick1.ML}
    4.50  
    4.51    \noindent It might be convenient to remove the pointless original
    4.52 -  equation, using the \emph{nofunc} attribute:%
    4.53 +  equation, using the \emph{func del} attribute:%
    4.54  \end{isamarkuptext}%
    4.55  \isamarkuptrue%
    4.56  \isacommand{lemmas}\isamarkupfalse%
    4.57 -\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline
    4.58 +\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline
    4.59  \isanewline
    4.60  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    4.61 -\ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
    4.62 +\ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}%
    4.63  \begin{isamarkuptext}%
    4.64  \lstsml{Thy/examples/pick2.ML}
    4.65  
    4.66 @@ -419,7 +418,7 @@
    4.67  \endisadelimproof
    4.68  \isanewline
    4.69  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    4.70 -\ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isacharunderscore}case{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
    4.71 +\ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isacharunderscore}case{\isachardot}ML{\isachardoublequoteclose}%
    4.72  \begin{isamarkuptext}%
    4.73  \lstsml{Thy/examples/fac_case.ML}
    4.74  
    4.75 @@ -427,7 +426,7 @@
    4.76      The attributes \emph{code} and \emph{code del}
    4.77      associated with the existing code generator also apply to
    4.78      the new one: \emph{code} implies \emph{code func},
    4.79 -    and \emph{code del} implies \emph{code nofunc}.
    4.80 +    and \emph{code del} implies \emph{code func del}.
    4.81    \end{warn}%
    4.82  \end{isamarkuptext}%
    4.83  \isamarkuptrue%
    4.84 @@ -510,11 +509,11 @@
    4.85    as SML, but, in accordance with conventions
    4.86    some Haskell systems enforce, each module ends
    4.87    up in a single file. The module hierarchy is reflected in
    4.88 -  the file system, with root given by the user.%
    4.89 +  the file system, with root directory given as file specification.%
    4.90  \end{isamarkuptext}%
    4.91  \isamarkuptrue%
    4.92  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
    4.93 -\ dummy\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
    4.94 +\ dummy\ \isakeyword{in}\ Haskell\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}%
    4.95  \begin{isamarkuptext}%
    4.96  \lsthaskell{Thy/examples/Codegen.hs}
    4.97    \noindent (we have left out all other modules).
    4.98 @@ -525,7 +524,7 @@
    4.99  \end{isamarkuptext}%
   4.100  \isamarkuptrue%
   4.101  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   4.102 -\ dummy\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   4.103 +\ dummy\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}%
   4.104  \begin{isamarkuptext}%
   4.105  \lstsml{Thy/examples/class.ML}
   4.106  
   4.107 @@ -535,12 +534,13 @@
   4.108  \end{isamarkuptext}%
   4.109  \isamarkuptrue%
   4.110  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   4.111 -\ dummy\ {\isacharparenleft}OCaml\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}{\isacharparenright}%
   4.112 +\ dummy\ \isakeyword{in}\ OCaml\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}%
   4.113  \begin{isamarkuptext}%
   4.114  \lstsml{Thy/examples/class.ocaml}
   4.115  
   4.116    \medskip The explicit association of constants
   4.117 -  to classes can be inspected using the \isa{{\isasymPRINTCLASSES}}%
   4.118 +  to classes can be inspected using the \isa{{\isasymPRINTCLASSES}}
   4.119 +  command.%
   4.120  \end{isamarkuptext}%
   4.121  \isamarkuptrue%
   4.122  %
   4.123 @@ -620,16 +620,20 @@
   4.124    hand side and the arguments of the left hand side of an
   4.125    equation, but never to the constant heading the left hand side.
   4.126    Inline theorems may be declared an undeclared using the
   4.127 -  \emph{code inline} or \emph{code noinline} attribute respectively.
   4.128 +  \emph{code inline} or \emph{code inline del} attribute respectively.
   4.129    Some common applications:%
   4.130  \end{isamarkuptext}%
   4.131  \isamarkuptrue%
   4.132  %
   4.133  \begin{itemize}
   4.134 -     \item replacing non-executable constructs by executable ones: \\
   4.135 -\isacommand{lemma}\isamarkupfalse%
   4.136 +%
   4.137 +\begin{isamarkuptext}%
   4.138 +\item replacing non-executable constructs by executable ones:%
   4.139 +\end{isamarkuptext}%
   4.140 +\isamarkuptrue%
   4.141 +\ \ \isacommand{lemma}\isamarkupfalse%
   4.142  \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
   4.143 -\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
   4.144 +\ \ \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
   4.145  \isadelimproof
   4.146  \ %
   4.147  \endisadelimproof
   4.148 @@ -644,10 +648,13 @@
   4.149  %
   4.150  \endisadelimproof
   4.151  %
   4.152 -\item eliminating superfluous constants: \\
   4.153 -\isacommand{lemma}\isamarkupfalse%
   4.154 +\begin{isamarkuptext}%
   4.155 +\item eliminating superfluous constants:%
   4.156 +\end{isamarkuptext}%
   4.157 +\isamarkuptrue%
   4.158 +\ \ \isacommand{lemma}\isamarkupfalse%
   4.159  \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
   4.160 -\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}%
   4.161 +\ \ \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}%
   4.162  \isadelimproof
   4.163  \ %
   4.164  \endisadelimproof
   4.165 @@ -662,10 +669,13 @@
   4.166  %
   4.167  \endisadelimproof
   4.168  %
   4.169 -\item replacing executable but inconvenient constructs: \\
   4.170 -\isacommand{lemma}\isamarkupfalse%
   4.171 +\begin{isamarkuptext}%
   4.172 +\item replacing executable but inconvenient constructs:%
   4.173 +\end{isamarkuptext}%
   4.174 +\isamarkuptrue%
   4.175 +\ \ \isacommand{lemma}\isamarkupfalse%
   4.176  \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
   4.177 -\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}%
   4.178 +\ \ \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}%
   4.179  \isadelimproof
   4.180  \ %
   4.181  \endisadelimproof
   4.182 @@ -683,7 +693,7 @@
   4.183  \end{itemize}
   4.184  %
   4.185  \begin{isamarkuptext}%
   4.186 -The current set of inline theorems may be inspected using
   4.187 +\noindent The current set of inline theorems may be inspected using
   4.188    the \isa{{\isasymPRINTCODESETUP}} command.
   4.189  
   4.190    \emph{Inline procedures} are a generalized version of inline
   4.191 @@ -739,7 +749,7 @@
   4.192  \end{isamarkuptext}%
   4.193  \isamarkuptrue%
   4.194  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   4.195 -\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   4.196 +\ collect{\isacharunderscore}duplicates\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}%
   4.197  \begin{isamarkuptext}%
   4.198  \lstsml{Thy/examples/collect_duplicates.ML}%
   4.199  \end{isamarkuptext}%
   4.200 @@ -817,7 +827,7 @@
   4.201  \isanewline
   4.202  \isanewline
   4.203  \isacommand{lemmas}\isamarkupfalse%
   4.204 -\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
   4.205 +\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
   4.206  \isanewline
   4.207  \isacommand{lemma}\isamarkupfalse%
   4.208  \ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
   4.209 @@ -878,7 +888,7 @@
   4.210  \isamarkuptrue%
   4.211  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   4.212  \ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
   4.213 -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   4.214 +\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}%
   4.215  \begin{isamarkuptext}%
   4.216  \lstsml{Thy/examples/lexicographic.ML}%
   4.217  \end{isamarkuptext}%
   4.218 @@ -952,7 +962,7 @@
   4.219  %
   4.220  \endisadelimtt
   4.221  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   4.222 -\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}literal{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   4.223 +\ in{\isacharunderscore}interval\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}literal{\isachardot}ML{\isachardoublequoteclose}%
   4.224  \begin{isamarkuptext}%
   4.225  \lstsml{Thy/examples/bool_literal.ML}
   4.226  
   4.227 @@ -1009,7 +1019,7 @@
   4.228  \end{isamarkuptext}%
   4.229  \isamarkuptrue%
   4.230  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   4.231 -\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   4.232 +\ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}%
   4.233  \begin{isamarkuptext}%
   4.234  \lstsml{Thy/examples/bool_mlbool.ML}
   4.235  
   4.236 @@ -1039,7 +1049,7 @@
   4.237  \isanewline
   4.238  \isanewline
   4.239  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   4.240 -\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}infix{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   4.241 +\ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}infix{\isachardot}ML{\isachardoublequoteclose}%
   4.242  \begin{isamarkuptext}%
   4.243  \lstsml{Thy/examples/bool_infix.ML}
   4.244  
   4.245 @@ -1315,7 +1325,7 @@
   4.246  \isanewline
   4.247  \isanewline
   4.248  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   4.249 -\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ insert\ {\isachardoublequoteopen}op\ {\isasymin}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymunion}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Union{\isachardoublequoteclose}\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}set{\isacharunderscore}list{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   4.250 +\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ insert\ {\isachardoublequoteopen}op\ {\isasymin}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymunion}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Union{\isachardoublequoteclose}\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}set{\isacharunderscore}list{\isachardot}ML{\isachardoublequoteclose}%
   4.251  \begin{isamarkuptext}%
   4.252  \lstsml{Thy/examples/set_list.ML}
   4.253  
   4.254 @@ -1449,7 +1459,7 @@
   4.255  \ \ {\isacharbar}\ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline
   4.256  \isanewline
   4.257  \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
   4.258 -\ dummy{\isacharunderscore}option\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
   4.259 +\ dummy{\isacharunderscore}option\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}%
   4.260  \begin{isamarkuptext}%
   4.261  \lstsml{Thy/examples/arbitrary.ML}
   4.262  
     5.1 --- a/doc-src/IsarRef/logics.tex	Sun May 06 21:49:44 2007 +0200
     5.2 +++ b/doc-src/IsarRef/logics.tex	Sun May 06 21:50:17 2007 +0200
     5.3 @@ -772,9 +772,7 @@
     5.4  \indexisarcmd{code-abstype}
     5.5  \indexisarcmd{print-codesetup}
     5.6  \indexisaratt{code func}
     5.7 -\indexisaratt{code nofunc}
     5.8  \indexisaratt{code inline}
     5.9 -\indexisaratt{code noinline}
    5.10  
    5.11  \begin{matharray}{rcl}
    5.12    \isarcmd{code_gen}^* & : & \isarkeep{theory~|~proof} \\
    5.13 @@ -793,13 +791,12 @@
    5.14    \isarcmd{code_abstype} & : & \isartrans{theory}{theory} \\
    5.15    \isarcmd{print_codesetup}^* & : & \isarkeep{theory~|~proof} \\
    5.16    code\ func & : & \isaratt \\
    5.17 -  code\ nofunc & : & \isaratt \\
    5.18    code\ inline & : & \isaratt \\
    5.19 -  code\ noinline & : & \isaratt \\
    5.20  \end{matharray}
    5.21  
    5.22  \begin{rail}
    5.23 -'code\_gen' ( constexpr + ) ? ( seri + ) ?;
    5.24 +'code\_gen' ( constexpr + ) ? \\
    5.25 +  ( ( 'in' target ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
    5.26  
    5.27  'code\_thms' ( constexpr + ) ?;
    5.28  
    5.29 @@ -813,24 +810,23 @@
    5.30  
    5.31  class : nameref;
    5.32  
    5.33 -seri : target | 'SML' ( string | '-' ) | 'OCaml' ( string | '-' ) | 'Haskell' ( 'root:' string ) ? 'string\_classes' ? string;
    5.34 -
    5.35  target : 'OCaml' | 'SML' | 'Haskell';
    5.36  
    5.37  'code\_datatype' const +;
    5.38  
    5.39  'code\_const' (const + 'and') \\
    5.40 -  ( ( '(' target ( syntax + 'and' ) ')' ) + );
    5.41 +  ( ( '(' target ( syntax ? + 'and' ) ')' ) + );
    5.42  
    5.43  'code\_type' (typeconstructor + 'and') \\
    5.44 -  ( ( '(' target ( syntax + 'and' ) ')' ) + );
    5.45 +  ( ( '(' target ( syntax ? + 'and' ) ')' ) + );
    5.46  
    5.47  'code\_class' (class + 'and') \\
    5.48    ( ( '(' target \\
    5.49 -    ( ( string ('where' ( const ( '==' | equiv ) string ) + ) ? ) + 'and' ) ')' ) + );
    5.50 +    ( ( string ('where' \\
    5.51 +      ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + );
    5.52  
    5.53  'code\_instance' (( typeconstructor '::' class ) + 'and') \\
    5.54 -  ( ( '(' target ( '-' + 'and' ) ')' ) + );
    5.55 +  ( ( '(' target ( '-' ? + 'and' ) ')' ) + );
    5.56  
    5.57  'code\_monad' term term term;
    5.58  
    5.59 @@ -848,7 +844,9 @@
    5.60  
    5.61  'print\_codesetup';
    5.62  
    5.63 -('code\ func' | 'code\ nofunc' | 'code\ inline' | 'code\ noinline');
    5.64 +'code\ func' ( 'del' ) ?;
    5.65 +
    5.66 +'code\ inline' ( 'del' ) ?;
    5.67  \end{rail}
    5.68  
    5.69  \begin{descr}
    5.70 @@ -856,7 +854,7 @@
    5.71  \item [$\isarcmd{code_gen}$] is the canonical interface for generating and
    5.72    serializing code: for a given list of constants, code is generated for the specified
    5.73    target language(s).  Abstract code is cached incrementally.  If no constant is given,
    5.74 -  the whole current cache is serialized.  If no serialization instruction
    5.75 +  the currently cached code is serialized.  If no serialization instruction
    5.76    is given, only abstract code is cached.
    5.77  
    5.78    Constants may be specified by giving them literally, referring
    5.79 @@ -864,45 +862,45 @@
    5.80    by giving (``name.*''), or referring to \emph{all} executable
    5.81    constants currently available (``*'').
    5.82  
    5.83 -  The \emph{SML} serializer takes either a filename or an ``-'' or ``*''
    5.84 -  as argument.  In the first case, code is written to the specified file,
    5.85 -  in the second to standard output and in the last case
    5.86 -  it is compiled internally in the context of the current ML session.
    5.87 -
    5.88 -  The \emph{OCaml} serializer is like the \emph{SML} serializer
    5.89 -  but it produces code for OCaml and does not support internal compilation.
    5.90 +  For \emph{SML} and \emph{OCaml}, the file specification refers to
    5.91 +  a single file;  for \emph{Haskell}, it refers to a whole directory,
    5.92 +  where code is generated in multiple files reflecting the module hierarchy.
    5.93 +  The file specification ``-'' denotes standard output.  For \emph{SML},
    5.94 +  omitting the file specification compiles code internally
    5.95 +  in the context of the current ML session.
    5.96  
    5.97 -  For \emph{Haskell}, a directory name is specified; different modules
    5.98 -  are serialized to different files in this directory or
    5.99 -  subdirectories, reflecting the module hierarchy. Additionally
   5.100 -  a module name prefix may be given using the ``root:'' argument;
   5.101 -  ``string\_classes'' adds a ``deriving (Read, Show)'' clause
   5.102 +  Serializers take an optional list of arguments in parentheses. 
   5.103 +  For \emph{Haskell} a module name prefix may be given using the ``root:''
   5.104 +  argument;  ``string\_classes'' adds a ``deriving (Read, Show)'' clause
   5.105    to each appropriate datatype declaration.
   5.106 -  A ``-'' instead of a directory name prints code to standard output.
   5.107  
   5.108  \item [$\isarcmd{code_thms}$] prints a list of theorems representing the
   5.109    corresponding program containing all given constants; if no constants are
   5.110 -  given, the current cache of code theorems in printed.
   5.111 +  given, the currently cached code theorems in printed.
   5.112  
   5.113  \item [$\isarcmd{code_deps}$] visualizes dependencies of theorems representing the
   5.114    corresponding program containing all given constants; if no constants are
   5.115 -  given, the current cache os visualized.
   5.116 +  given, the currently cached code theorems are visualized.
   5.117  
   5.118  \item [$\isarcmd{code_datatype}$] specifies a constructor set for a logical type.
   5.119  
   5.120  \item [$\isarcmd{code_const}$] associates a list of constants
   5.121 -  with target-specific serializations.
   5.122 +  with target-specific serializations; omitting a serialization
   5.123 +  deletes an existing serialization.
   5.124  
   5.125  \item [$\isarcmd{code_type}$] associates a list of type constructors
   5.126 -  with target-specific serializations.
   5.127 +  with target-specific serializations; omitting a serialization
   5.128 +  deletes an existing serialization.
   5.129  
   5.130  \item [$\isarcmd{code_class}$] associates a list of classes
   5.131    with target-specific class names; in addition, constants associated
   5.132    with this class may be given target-specific names used for instance
   5.133 -  declarations.  Applies only to \emph{Haskell}.
   5.134 +  declarations; omitting a serialization
   5.135 +  deletes an existing serialization.  Applies only to \emph{Haskell}.
   5.136  
   5.137  \item [$\isarcmd{code_instance}$] declares a list of type constructor / class
   5.138    instance relations as ``already present'' for a given target.
   5.139 +  Omitting a ``-'' deletes an existing ``already present'' declaration.
   5.140    Applies only to \emph{Haskell}.
   5.141  
   5.142  \item [$\isarcmd{code_monad}$] provides an auxiliary mechanism
   5.143 @@ -925,15 +923,16 @@
   5.144  \item [$\isarcmd{code_abstype}$] offers an interface for implementing
   5.145    an abstract type plus operations by executable counterparts.
   5.146  
   5.147 -\item [$code\ func$ and $code\ nofunc$] select or deselect explicitly
   5.148 +\item [$code\ func$] selects (or with option ''del``, deselects) explicitly
   5.149    a defining equation for code generation.  Usually packages introducing
   5.150    defining equations provide a resonable default setup for selection.
   5.151  
   5.152 -\item [$code\ inline$ and $code\ noinline$] select or deselect
   5.153 -  inlining theorems which are applied as rewrite rules to any defining equation.
   5.154 +\item [$code\ inline$] declares (or with option ''del``, removes)
   5.155 +  inlining theorems which are applied as rewrite rules to any defining equation
   5.156 +  during preprocessing.
   5.157  
   5.158  \item [$\isarcmd{print_codesetup}$] gives an overview on selected
   5.159 -  defining equations, code generator datatypes and inlining theorems.
   5.160 +  defining equations, code generator datatypes and preprocessor setup.
   5.161  
   5.162  \end{descr}
   5.163  
     6.1 --- a/src/HOL/Code_Generator.thy	Sun May 06 21:49:44 2007 +0200
     6.2 +++ b/src/HOL/Code_Generator.thy	Sun May 06 21:50:17 2007 +0200
     6.3 @@ -78,7 +78,7 @@
     6.4  class eq (attach "op =") = type
     6.5  
     6.6  
     6.7 -text {* equality for Haskell *}
     6.8 +text {* using built-in Haskell equality *}
     6.9  
    6.10  code_class eq
    6.11    (Haskell "Eq" where "op =" \<equiv> "(==)")
    6.12 @@ -114,16 +114,10 @@
    6.13  instance bool :: eq ..
    6.14  
    6.15  lemma [code func]:
    6.16 -  "True = P \<longleftrightarrow> P" by simp
    6.17 -
    6.18 -lemma [code func]:
    6.19 -  "False = P \<longleftrightarrow> \<not> P" by simp
    6.20 -
    6.21 -lemma [code func]:
    6.22 -  "P = True \<longleftrightarrow> P" by simp
    6.23 -
    6.24 -lemma [code func]:
    6.25 -  "P = False \<longleftrightarrow> \<not> P" by simp
    6.26 +  shows "True = P \<longleftrightarrow> P"
    6.27 +    and "False = P \<longleftrightarrow> \<not> P"
    6.28 +    and "P = True \<longleftrightarrow> P"
    6.29 +    and "P = False \<longleftrightarrow> \<not> P" by simp_all
    6.30  
    6.31  code_type bool
    6.32    (SML "bool")
    6.33 @@ -211,7 +205,7 @@
    6.34  
    6.35  definition
    6.36    if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
    6.37 -  [code nofunc]: "if_delayed b f g = (if b then f True else g False)"
    6.38 +  [code func del]: "if_delayed b f g = (if b then f True else g False)"
    6.39  
    6.40  lemma [code func]:
    6.41    shows "if_delayed True f g = f True"
     7.1 --- a/src/HOL/Divides.thy	Sun May 06 21:49:44 2007 +0200
     7.2 +++ b/src/HOL/Divides.thy	Sun May 06 21:50:17 2007 +0200
     7.3 @@ -898,7 +898,7 @@
     7.4  
     7.5  subsection {* Code generation for div, mod and dvd on nat *}
     7.6  
     7.7 -definition [code nofunc]:
     7.8 +definition [code func del]:
     7.9    "divmod (m\<Colon>nat) n = (m div n, m mod n)"
    7.10  
    7.11  lemma divmod_zero [code]: "divmod m 0 = (0, m)"
     8.1 --- a/src/HOL/Extraction/Higman.thy	Sun May 06 21:49:44 2007 +0200
     8.2 +++ b/src/HOL/Extraction/Higman.thy	Sun May 06 21:50:17 2007 +0200
     8.3 @@ -406,7 +406,7 @@
     8.4    arbitrary_LT \<equiv> arbitrary_LT'
     8.5    arbitrary_TT \<equiv> arbitrary_TT'
     8.6  
     8.7 -code_gen higman_idx (SML #)
     8.8 +code_gen higman_idx in SML
     8.9  
    8.10  ML {*
    8.11  local
     9.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Sun May 06 21:49:44 2007 +0200
     9.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Sun May 06 21:50:17 2007 +0200
     9.3 @@ -309,7 +309,7 @@
     9.4    test' = test'
     9.5    test'' = test''
     9.6  
     9.7 -code_gen test test' test'' (SML #)
     9.8 +code_gen test test' test'' in SML
     9.9  
    9.10  ML "timeit (fn () => PH.test 10)"
    9.11  ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
    10.1 --- a/src/HOL/Extraction/QuotRem.thy	Sun May 06 21:49:44 2007 +0200
    10.2 +++ b/src/HOL/Extraction/QuotRem.thy	Sun May 06 21:50:17 2007 +0200
    10.3 @@ -49,6 +49,6 @@
    10.4  contains
    10.5    test = "division 9 2"
    10.6  
    10.7 -code_gen division (SML #)
    10.8 +code_gen division in SML
    10.9  
   10.10  end
    11.1 --- a/src/HOL/FixedPoint.thy	Sun May 06 21:49:44 2007 +0200
    11.2 +++ b/src/HOL/FixedPoint.thy	Sun May 06 21:50:17 2007 +0200
    11.3 @@ -14,18 +14,19 @@
    11.4  subsection {* Complete lattices *}
    11.5  
    11.6  class complete_lattice = lattice +
    11.7 -  fixes Inf :: "'a set \<Rightarrow> 'a"
    11.8 -  assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
    11.9 -  assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
   11.10 +  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90)
   11.11 +  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
   11.12 +  assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
   11.13  
   11.14  definition
   11.15 -  Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a" where
   11.16 +  Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a"
   11.17 +where
   11.18    "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
   11.19  
   11.20 -theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x <= Sup A"
   11.21 +theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x \<le> Sup A"
   11.22    by (auto simp: Sup_def intro: Inf_greatest)
   11.23  
   11.24 -theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
   11.25 +theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z"
   11.26    by (auto simp: Sup_def intro: Inf_lower)
   11.27  
   11.28  definition
   11.29 @@ -198,7 +199,7 @@
   11.30    apply (iprover elim: le_funE)
   11.31    done
   11.32  
   11.33 -lemmas [code nofunc] = Inf_fun_def
   11.34 +lemmas [code func del] = Inf_fun_def
   11.35  
   11.36  theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
   11.37    apply (rule order_antisym)
   11.38 @@ -221,7 +222,7 @@
   11.39    Inf_set_def: "Inf S \<equiv> \<Inter>S"
   11.40    by intro_classes (auto simp add: Inf_set_def)
   11.41  
   11.42 -lemmas [code nofunc] = Inf_set_def
   11.43 +lemmas [code func del] = Inf_set_def
   11.44  
   11.45  theorem Sup_set_eq: "Sup S = \<Union>S"
   11.46    apply (rule subset_antisym)
    12.1 --- a/src/HOL/Fun.thy	Sun May 06 21:49:44 2007 +0200
    12.2 +++ b/src/HOL/Fun.thy	Sun May 06 21:50:17 2007 +0200
    12.3 @@ -466,13 +466,12 @@
    12.4    le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
    12.5    less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
    12.6  
    12.7 -lemmas [code nofunc] = le_fun_def less_fun_def
    12.8 -
    12.9 -instance "fun" :: (type, preorder) preorder
   12.10 -  by default (auto simp add: le_fun_def less_fun_def intro: order_trans)
   12.11 +lemmas [code func del] = le_fun_def less_fun_def
   12.12  
   12.13  instance "fun" :: (type, order) order
   12.14 -  by default (rule ext, auto simp add: le_fun_def less_fun_def intro: order_antisym)
   12.15 +  by default
   12.16 +    (auto simp add: le_fun_def less_fun_def expand_fun_eq
   12.17 +       intro: order_trans order_antisym)
   12.18  
   12.19  lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
   12.20    unfolding le_fun_def by simp
   12.21 @@ -536,12 +535,45 @@
   12.22  apply (auto dest: le_funD)
   12.23  done
   12.24  
   12.25 -lemmas [code nofunc] = inf_fun_eq sup_fun_eq
   12.26 +lemmas [code func del] = inf_fun_eq sup_fun_eq
   12.27  
   12.28  instance "fun" :: (type, distrib_lattice) distrib_lattice
   12.29    by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
   12.30  
   12.31  
   12.32 +subsection {* Proof tool setup *} 
   12.33 +
   12.34 +text {* simplifies terms of the form
   12.35 +  f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *}
   12.36 +
   12.37 +ML {*
   12.38 +let
   12.39 +  fun gen_fun_upd NONE T _ _ = NONE
   12.40 +    | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd},T) $ f $ x $ y)
   12.41 +  fun dest_fun_T1 (Type (_, T :: Ts)) = T
   12.42 +  fun find_double (t as Const (@{const_name fun_upd},T) $ f $ x $ y) =
   12.43 +    let
   12.44 +      fun find (Const (@{const_name fun_upd},T) $ g $ v $ w) =
   12.45 +            if v aconv x then SOME g else gen_fun_upd (find g) T v w
   12.46 +        | find t = NONE
   12.47 +    in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
   12.48 +  fun fun_upd_prover ss =
   12.49 +    rtac eq_reflection 1 THEN rtac ext 1 THEN
   12.50 +    simp_tac (Simplifier.inherit_context ss @{simpset}) 1
   12.51 +  val fun_upd2_simproc =
   12.52 +    Simplifier.simproc @{theory}
   12.53 +      "fun_upd2" ["f(v := w, x := y)"]
   12.54 +      (fn _ => fn ss => fn t =>
   12.55 +        case find_double t of (T, NONE) => NONE
   12.56 +        | (T, SOME rhs) =>
   12.57 +            SOME (Goal.prove (Simplifier.the_context ss) [] []
   12.58 +              (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
   12.59 +in
   12.60 +  Addsimprocs [fun_upd2_simproc]
   12.61 +end;
   12.62 +*}
   12.63 +
   12.64 +
   12.65  subsection {* Code generator setup *}
   12.66  
   12.67  code_const "op \<circ>"
   12.68 @@ -554,115 +586,20 @@
   12.69  
   12.70  subsection {* ML legacy bindings *} 
   12.71  
   12.72 -text{*The ML section includes some compatibility bindings and a simproc
   12.73 -for function updates, in addition to the usual ML-bindings of theorems.*}
   12.74 -ML
   12.75 -{*
   12.76 -val id_def = thm "id_def";
   12.77 -val inj_on_def = thm "inj_on_def";
   12.78 -val surj_def = thm "surj_def";
   12.79 -val bij_def = thm "bij_def";
   12.80 -val fun_upd_def = thm "fun_upd_def";
   12.81 -
   12.82 -val o_def = thm "comp_def";
   12.83 -val injI = thm "inj_onI";
   12.84 -val inj_inverseI = thm "inj_on_inverseI";
   12.85 -val set_cs = claset() delrules [equalityI];
   12.86 -
   12.87 -val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];
   12.88 -
   12.89 -(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
   12.90 -local
   12.91 -  fun gen_fun_upd NONE T _ _ = NONE
   12.92 -    | gen_fun_upd (SOME f) T x y = SOME (Const ("Fun.fun_upd",T) $ f $ x $ y)
   12.93 -  fun dest_fun_T1 (Type (_, T :: Ts)) = T
   12.94 -  fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) =
   12.95 -    let
   12.96 -      fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) =
   12.97 -            if v aconv x then SOME g else gen_fun_upd (find g) T v w
   12.98 -        | find t = NONE
   12.99 -    in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
  12.100 -
  12.101 -  val current_ss = simpset ()
  12.102 -  fun fun_upd_prover ss =
  12.103 -    rtac eq_reflection 1 THEN rtac ext 1 THEN
  12.104 -    simp_tac (Simplifier.inherit_context ss current_ss) 1
  12.105 -in
  12.106 -  val fun_upd2_simproc =
  12.107 -    Simplifier.simproc @{theory}
  12.108 -      "fun_upd2" ["f(v := w, x := y)"]
  12.109 -      (fn _ => fn ss => fn t =>
  12.110 -        case find_double t of (T, NONE) => NONE
  12.111 -        | (T, SOME rhs) =>
  12.112 -            SOME (Goal.prove (Simplifier.the_context ss) [] []
  12.113 -              (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
  12.114 -end;
  12.115 -Addsimprocs[fun_upd2_simproc];
  12.116 +ML {*
  12.117 +val set_cs = claset() delrules [equalityI]
  12.118 +*}
  12.119  
  12.120 -val expand_fun_eq = thm "expand_fun_eq";
  12.121 -val apply_inverse = thm "apply_inverse";
  12.122 -val id_apply = thm "id_apply";
  12.123 -val o_apply = thm "o_apply";
  12.124 -val o_assoc = thm "o_assoc";
  12.125 -val id_o = thm "id_o";
  12.126 -val o_id = thm "o_id";
  12.127 -val image_compose = thm "image_compose";
  12.128 -val image_eq_UN = thm "image_eq_UN";
  12.129 -val UN_o = thm "UN_o";
  12.130 -val datatype_injI = thm "datatype_injI";
  12.131 -val injD = thm "injD";
  12.132 -val inj_eq = thm "inj_eq";
  12.133 -val inj_onI = thm "inj_onI";
  12.134 -val inj_on_inverseI = thm "inj_on_inverseI";
  12.135 -val inj_onD = thm "inj_onD";
  12.136 -val inj_on_iff = thm "inj_on_iff";
  12.137 -val comp_inj_on = thm "comp_inj_on";
  12.138 -val inj_on_contraD = thm "inj_on_contraD";
  12.139 -val inj_singleton = thm "inj_singleton";
  12.140 -val subset_inj_on = thm "subset_inj_on";
  12.141 -val surjI = thm "surjI";
  12.142 -val surj_range = thm "surj_range";
  12.143 -val surjD = thm "surjD";
  12.144 -val surjE = thm "surjE";
  12.145 -val comp_surj = thm "comp_surj";
  12.146 -val bijI = thm "bijI";
  12.147 -val bij_is_inj = thm "bij_is_inj";
  12.148 -val bij_is_surj = thm "bij_is_surj";
  12.149 -val image_ident = thm "image_ident";
  12.150 -val image_id = thm "image_id";
  12.151 -val vimage_ident = thm "vimage_ident";
  12.152 -val vimage_id = thm "vimage_id";
  12.153 -val vimage_image_eq = thm "vimage_image_eq";
  12.154 -val image_vimage_subset = thm "image_vimage_subset";
  12.155 -val image_vimage_eq = thm "image_vimage_eq";
  12.156 -val surj_image_vimage_eq = thm "surj_image_vimage_eq";
  12.157 -val inj_vimage_image_eq = thm "inj_vimage_image_eq";
  12.158 -val vimage_subsetD = thm "vimage_subsetD";
  12.159 -val vimage_subsetI = thm "vimage_subsetI";
  12.160 -val vimage_subset_eq = thm "vimage_subset_eq";
  12.161 -val image_Int_subset = thm "image_Int_subset";
  12.162 -val image_diff_subset = thm "image_diff_subset";
  12.163 -val inj_on_image_Int = thm "inj_on_image_Int";
  12.164 -val inj_on_image_set_diff = thm "inj_on_image_set_diff";
  12.165 -val image_Int = thm "image_Int";
  12.166 -val image_set_diff = thm "image_set_diff";
  12.167 -val inj_image_mem_iff = thm "inj_image_mem_iff";
  12.168 -val inj_image_subset_iff = thm "inj_image_subset_iff";
  12.169 -val inj_image_eq_iff = thm "inj_image_eq_iff";
  12.170 -val image_UN = thm "image_UN";
  12.171 -val image_INT = thm "image_INT";
  12.172 -val bij_image_INT = thm "bij_image_INT";
  12.173 -val surj_Compl_image_subset = thm "surj_Compl_image_subset";
  12.174 -val inj_image_Compl_subset = thm "inj_image_Compl_subset";
  12.175 -val bij_image_Compl_eq = thm "bij_image_Compl_eq";
  12.176 -val fun_upd_idem_iff = thm "fun_upd_idem_iff";
  12.177 -val fun_upd_idem = thm "fun_upd_idem";
  12.178 -val fun_upd_apply = thm "fun_upd_apply";
  12.179 -val fun_upd_same = thm "fun_upd_same";
  12.180 -val fun_upd_other = thm "fun_upd_other";
  12.181 -val fun_upd_upd = thm "fun_upd_upd";
  12.182 -val fun_upd_twist = thm "fun_upd_twist";
  12.183 -val range_ex1_eq = thm "range_ex1_eq";
  12.184 +ML {*
  12.185 +val id_apply = @{thm id_apply}
  12.186 +val id_def = @{thm id_def}
  12.187 +val o_apply = @{thm o_apply}
  12.188 +val o_assoc = @{thm o_assoc}
  12.189 +val o_def = @{thm o_def}
  12.190 +val injD = @{thm injD}
  12.191 +val datatype_injI = @{thm datatype_injI}
  12.192 +val range_ex1_eq = @{thm range_ex1_eq}
  12.193 +val expand_fun_eq = @{thm expand_fun_eq}
  12.194  *}
  12.195  
  12.196  end
    13.1 --- a/src/HOL/Integ/IntDef.thy	Sun May 06 21:49:44 2007 +0200
    13.2 +++ b/src/HOL/Integ/IntDef.thy	Sun May 06 21:50:17 2007 +0200
    13.3 @@ -25,7 +25,7 @@
    13.4  definition
    13.5    int :: "nat \<Rightarrow> int"
    13.6  where
    13.7 -  [code nofunc]: "int m = Abs_Integ (intrel `` {(m, 0)})"
    13.8 +  [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})"
    13.9  
   13.10  instance int :: zero
   13.11    Zero_int_def: "0 \<equiv> int 0" ..
   13.12 @@ -53,7 +53,7 @@
   13.13     "z \<le> w \<equiv> \<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w"
   13.14    less_int_def: "z < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
   13.15  
   13.16 -lemmas [code nofunc] = Zero_int_def One_int_def add_int_def
   13.17 +lemmas [code func del] = Zero_int_def One_int_def add_int_def
   13.18    minus_int_def mult_int_def le_int_def less_int_def
   13.19  
   13.20  
   13.21 @@ -380,7 +380,7 @@
   13.22  definition
   13.23    nat :: "int \<Rightarrow> nat"
   13.24  where
   13.25 -  [code nofunc]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
   13.26 +  [code func del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
   13.27  
   13.28  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
   13.29  proof -
    14.1 --- a/src/HOL/Integ/Numeral.thy	Sun May 06 21:49:44 2007 +0200
    14.2 +++ b/src/HOL/Integ/Numeral.thy	Sun May 06 21:50:17 2007 +0200
    14.3 @@ -34,15 +34,15 @@
    14.4  
    14.5  definition
    14.6    Pls :: int where
    14.7 -  [code nofunc]:"Pls = 0"
    14.8 +  [code func del]:"Pls = 0"
    14.9  
   14.10  definition
   14.11    Min :: int where
   14.12 -  [code nofunc]:"Min = - 1"
   14.13 +  [code func del]:"Min = - 1"
   14.14  
   14.15  definition
   14.16    Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
   14.17 -  [code nofunc]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
   14.18 +  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
   14.19  
   14.20  class number = type + -- {* for numeric types: nat, int, real, \dots *}
   14.21    fixes number_of :: "int \<Rightarrow> 'a"
   14.22 @@ -70,11 +70,11 @@
   14.23  
   14.24  definition
   14.25    succ :: "int \<Rightarrow> int" where
   14.26 -  [code nofunc]: "succ k = k + 1"
   14.27 +  [code func del]: "succ k = k + 1"
   14.28  
   14.29  definition
   14.30    pred :: "int \<Rightarrow> int" where
   14.31 -  [code nofunc]: "pred k = k - 1"
   14.32 +  [code func del]: "pred k = k - 1"
   14.33  
   14.34  lemmas
   14.35    max_number_of [simp] = max_def
   14.36 @@ -211,7 +211,7 @@
   14.37    int_number_of_def: "number_of w \<equiv> of_int w"
   14.38    by intro_classes (simp only: int_number_of_def)
   14.39  
   14.40 -lemmas [code nofunc] = int_number_of_def
   14.41 +lemmas [code func del] = int_number_of_def
   14.42  
   14.43  lemma number_of_is_id:
   14.44    "number_of (k::int) = k"
    15.1 --- a/src/HOL/Lambda/WeakNorm.thy	Sun May 06 21:49:44 2007 +0200
    15.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Sun May 06 21:50:17 2007 +0200
    15.3 @@ -573,8 +573,7 @@
    15.4    CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
    15.5  *}
    15.6  
    15.7 -code_gen
    15.8 -  type_NF nat int (SML #)
    15.9 +code_gen type_NF nat int in SML
   15.10  
   15.11  ML {*
   15.12  structure Norm = ROOT.WeakNorm;
    16.1 --- a/src/HOL/Library/Char_ord.thy	Sun May 06 21:49:44 2007 +0200
    16.2 +++ b/src/HOL/Library/Char_ord.thy	Sun May 06 21:50:17 2007 +0200
    16.3 @@ -47,7 +47,7 @@
    16.4      n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    16.5    by default (auto simp: char_less_eq_def char_less_def split: char.splits)
    16.6  
    16.7 -lemmas [code nofunc] = char_less_eq_def char_less_def
    16.8 +lemmas [code func del] = char_less_eq_def char_less_def
    16.9  
   16.10  instance char :: distrib_lattice
   16.11    "inf \<equiv> min"
    17.1 --- a/src/HOL/Library/EfficientNat.thy	Sun May 06 21:49:44 2007 +0200
    17.2 +++ b/src/HOL/Library/EfficientNat.thy	Sun May 06 21:50:17 2007 +0200
    17.3 @@ -20,7 +20,7 @@
    17.4  subsection {* Logical rewrites *}
    17.5  
    17.6  text {*
    17.7 -  A int-to-nat conversion with domain
    17.8 +  An int-to-nat conversion
    17.9    restricted to non-negative ints (in contrast to @{const nat}).
   17.10    Note that this restriction has no logical relevance and
   17.11    is just a kind of proof hint -- nothing prevents you from 
   17.12 @@ -52,7 +52,8 @@
   17.13    expression:
   17.14  *}
   17.15  
   17.16 -lemma [code unfold, code noinline]: "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
   17.17 +lemma [code unfold, code inline del]:
   17.18 +  "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
   17.19  proof -
   17.20    have rewrite: "\<And>f g n. nat_case f g n = (if n = 0 then f else g (n - 1))"
   17.21    proof -
   17.22 @@ -66,7 +67,7 @@
   17.23  
   17.24  lemma [code inline]:
   17.25    "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int n - 1)))"
   17.26 -proof rule+
   17.27 +proof (rule ext)+
   17.28    fix f g n
   17.29    show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
   17.30    by (cases n) (simp_all add: nat_of_int_int)
   17.31 @@ -81,8 +82,8 @@
   17.32    by (simp add: nat_of_int_def)
   17.33  lemma [code func, code inline]:  "1 = nat_of_int 1"
   17.34    by (simp add: nat_of_int_def)
   17.35 -lemma [code func]: "Suc n = n + 1"
   17.36 -  by simp
   17.37 +lemma [code func]: "Suc n = nat_of_int (int n + 1)"
   17.38 +  by (simp add: nat_of_int_def)
   17.39  lemma [code]: "m + n = nat (int m + int n)"
   17.40    by arith
   17.41  lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
   17.42 @@ -154,11 +155,6 @@
   17.43  
   17.44  code_datatype nat_of_int
   17.45  
   17.46 -lemma [code func]: "0 = nat_of_int 0"
   17.47 -  by (auto simp add: nat_of_int_def)
   17.48 -lemma [code func]: "Suc n = nat_of_int (int n + 1)"
   17.49 -  by (auto simp add: nat_of_int_def)
   17.50 -
   17.51  code_type nat
   17.52    (SML "IntInf.int")
   17.53    (OCaml "Big'_int.big'_int")
   17.54 @@ -212,7 +208,7 @@
   17.55    Natural numerals should be expressed using @{const nat_of_int}.
   17.56  *}
   17.57  
   17.58 -lemmas [code noinline] = nat_number_of_def
   17.59 +lemmas [code inline del] = nat_number_of_def
   17.60  
   17.61  ML {*
   17.62  fun nat_of_int_of_number_of thy cts =
    18.1 --- a/src/HOL/Library/Eval.thy	Sun May 06 21:49:44 2007 +0200
    18.2 +++ b/src/HOL/Library/Eval.thy	Sun May 06 21:50:17 2007 +0200
    18.3 @@ -111,7 +111,7 @@
    18.4  
    18.5  text {* Adaption for @{typ ml_string}s *}
    18.6  
    18.7 -lemmas [code func, code nofunc] = term_of_ml_string_def
    18.8 +lemmas [code func, code func del] = term_of_ml_string_def
    18.9  
   18.10  
   18.11  subsection {* Evaluation infrastructure *}
    19.1 --- a/src/HOL/Library/Graphs.thy	Sun May 06 21:49:44 2007 +0200
    19.2 +++ b/src/HOL/Library/Graphs.thy	Sun May 06 21:50:17 2007 +0200
    19.3 @@ -73,7 +73,7 @@
    19.4    by auto
    19.5  qed
    19.6  
    19.7 -lemmas [code nofunc] = graph_plus_def
    19.8 +lemmas [code func del] = graph_plus_def
    19.9  
   19.10  instance graph :: (type, type) "{distrib_lattice, complete_lattice}"
   19.11    graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
   19.12 @@ -123,7 +123,7 @@
   19.13      unfolding Inf_graph_def graph_leq_def by auto }
   19.14  qed
   19.15  
   19.16 -lemmas [code nofunc] = graph_leq_def graph_less_def
   19.17 +lemmas [code func del] = graph_leq_def graph_less_def
   19.18    inf_graph_def sup_graph_def Inf_graph_def
   19.19  
   19.20  lemma in_grplus:
   19.21 @@ -150,7 +150,7 @@
   19.22      by (cases a) (simp add:grcomp.simps)
   19.23  qed
   19.24  
   19.25 -lemmas [code nofunc] = graph_mult_def
   19.26 +lemmas [code func del] = graph_mult_def
   19.27  
   19.28  instance graph :: (type, one) one 
   19.29    graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
    20.1 --- a/src/HOL/Library/List_lexord.thy	Sun May 06 21:49:44 2007 +0200
    20.2 +++ b/src/HOL/Library/List_lexord.thy	Sun May 06 21:50:17 2007 +0200
    20.3 @@ -13,7 +13,7 @@
    20.4    list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
    20.5    list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
    20.6  
    20.7 -lemmas list_ord_defs [code nofunc] = list_less_def list_le_def
    20.8 +lemmas list_ord_defs [code func del] = list_less_def list_le_def
    20.9  
   20.10  instance list :: (order) order
   20.11    apply (intro_classes, unfold list_ord_defs)
   20.12 @@ -40,7 +40,7 @@
   20.13    by intro_classes
   20.14      (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
   20.15  
   20.16 -lemmas [code nofunc] = inf_list_def sup_list_def
   20.17 +lemmas [code func del] = inf_list_def sup_list_def
   20.18  
   20.19  lemma not_less_Nil [simp]: "\<not> (x < [])"
   20.20    by (unfold list_less_def) simp
    21.1 --- a/src/HOL/Library/Pretty_Char_chr.thy	Sun May 06 21:49:44 2007 +0200
    21.2 +++ b/src/HOL/Library/Pretty_Char_chr.thy	Sun May 06 21:50:17 2007 +0200
    21.3 @@ -23,7 +23,7 @@
    21.4    "char_of_nat = char_of_int o int"
    21.5    unfolding char_of_int_def by (simp add: expand_fun_eq)
    21.6  
    21.7 -lemmas [code nofunc] = char.recs char.cases char.size
    21.8 +lemmas [code func del] = char.recs char.cases char.size
    21.9  
   21.10  lemma [code func, code inline]:
   21.11    "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
    22.1 --- a/src/HOL/Library/Product_ord.thy	Sun May 06 21:49:44 2007 +0200
    22.2 +++ b/src/HOL/Library/Product_ord.thy	Sun May 06 21:50:17 2007 +0200
    22.3 @@ -13,7 +13,7 @@
    22.4    prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
    22.5    prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
    22.6  
    22.7 -lemmas prod_ord_defs [code nofunc] = prod_less_def prod_le_def
    22.8 +lemmas prod_ord_defs [code func del] = prod_less_def prod_le_def
    22.9  
   22.10  lemma [code func]:
   22.11    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
    23.1 --- a/src/HOL/Library/Pure_term.thy	Sun May 06 21:49:44 2007 +0200
    23.2 +++ b/src/HOL/Library/Pure_term.thy	Sun May 06 21:50:17 2007 +0200
    23.3 @@ -92,8 +92,8 @@
    23.4  
    23.5  code_datatype Const App Fix Absp Bound
    23.6  lemmas [code func] = Bnd_Bound Abs_Absp
    23.7 -lemmas [code nofunc] = term.recs term.cases term.size
    23.8 -lemma [code func, code nofunc]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
    23.9 +lemmas [code func del] = term.recs term.cases term.size
   23.10 +lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
   23.11  
   23.12  code_type "typ" and "term"
   23.13    (SML "Term.typ" and "Term.term")
    24.1 --- a/src/HOL/Library/SCT_Implementation.thy	Sun May 06 21:49:44 2007 +0200
    24.2 +++ b/src/HOL/Library/SCT_Implementation.thy	Sun May 06 21:50:17 2007 +0200
    24.3 @@ -118,6 +118,6 @@
    24.4    Kleene_Algebras SCT
    24.5    SCT_Implementation SCT
    24.6  
    24.7 -code_gen test_SCT (SML #)
    24.8 +code_gen test_SCT in SML
    24.9  
   24.10  end
    25.1 --- a/src/HOL/Nat.thy	Sun May 06 21:49:44 2007 +0200
    25.2 +++ b/src/HOL/Nat.thy	Sun May 06 21:50:17 2007 +0200
    25.3 @@ -64,7 +64,7 @@
    25.4    less_def: "m < n == (m, n) : pred_nat^+"
    25.5    le_def:   "m \<le> (n::nat) == ~ (n < m)" ..
    25.6  
    25.7 -lemmas [code nofunc] = less_def le_def
    25.8 +lemmas [code func del] = less_def le_def
    25.9  
   25.10  text {* Induction *}
   25.11  
   25.12 @@ -1100,6 +1100,11 @@
   25.13  
   25.14  subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
   25.15  
   25.16 +lemma subst_equals:
   25.17 +  assumes 1: "t = s" and 2: "u = t"
   25.18 +  shows "u = s"
   25.19 +  using 2 1 by (rule trans)
   25.20 +
   25.21  use "arith_data.ML"
   25.22  setup arith_setup
   25.23  
    26.1 --- a/src/HOL/Set.thy	Sun May 06 21:49:44 2007 +0200
    26.2 +++ b/src/HOL/Set.thy	Sun May 06 21:50:17 2007 +0200
    26.3 @@ -24,8 +24,8 @@
    26.4    UNIV          :: "'a set"
    26.5    insert        :: "'a => 'a set => 'a set"
    26.6    Collect       :: "('a => bool) => 'a set"              -- "comprehension"
    26.7 -  Int           :: "'a set => 'a set => 'a set"          (infixl 70)
    26.8 -  Un            :: "'a set => 'a set => 'a set"          (infixl 65)
    26.9 +  "op Int"      :: "'a set => 'a set => 'a set"          (infixl "Int" 70)
   26.10 +  "op Un"       :: "'a set => 'a set => 'a set"          (infixl "Un" 65)
   26.11    UNION         :: "'a set => ('a => 'b set) => 'b set"  -- "general union"
   26.12    INTER         :: "'a set => ('a => 'b set) => 'b set"  -- "general intersection"
   26.13    Union         :: "'a set set => 'a set"                -- "union of a set"
   26.14 @@ -148,7 +148,7 @@
   26.15    subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
   26.16    psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
   26.17  
   26.18 -lemmas [code nofunc] = subset_def psubset_def
   26.19 +lemmas [code func del] = subset_def psubset_def
   26.20  
   26.21  abbreviation
   26.22    subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   26.23 @@ -346,7 +346,7 @@
   26.24    Compl_def:    "- A            == {x. ~x:A}"
   26.25    set_diff_def: "A - B          == {x. x:A & ~x:B}" ..
   26.26  
   26.27 -lemmas [code nofunc] = Compl_def set_diff_def
   26.28 +lemmas [code func del] = Compl_def set_diff_def
   26.29  
   26.30  defs
   26.31    Un_def:       "A Un B         == {x. x:A | x:B}"
   26.32 @@ -2130,7 +2130,7 @@
   26.33    sup_set_eq: "sup A B \<equiv> A \<union> B"
   26.34    by intro_classes (auto simp add: inf_set_eq sup_set_eq)
   26.35  
   26.36 -lemmas [code nofunc] = inf_set_eq sup_set_eq
   26.37 +lemmas [code func del] = inf_set_eq sup_set_eq
   26.38  
   26.39  
   26.40  subsection {* Basic ML bindings *}
    27.1 --- a/src/HOL/Wellfounded_Recursion.thy	Sun May 06 21:49:44 2007 +0200
    27.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Sun May 06 21:50:17 2007 +0200
    27.3 @@ -35,7 +35,7 @@
    27.4       (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
    27.5  
    27.6    wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
    27.7 -  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    27.8 +  [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    27.9  
   27.10  abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   27.11    "acyclicP r == acyclic (Collect2 r)"
    28.1 --- a/src/HOL/ex/Classpackage.thy	Sun May 06 21:49:44 2007 +0200
    28.2 +++ b/src/HOL/ex/Classpackage.thy	Sun May 06 21:50:17 2007 +0200
    28.3 @@ -338,7 +338,6 @@
    28.4  definition "x2 = X (1::int) 2 3"
    28.5  definition "y2 = Y (1::int) 2 3"
    28.6  
    28.7 -code_gen "op \<otimes>" \<one> inv X Y
    28.8 -code_gen x1 x2 y2 (SML #) (OCaml -) (Haskell -)
    28.9 +code_gen x1 x2 y2 in SML in OCaml file - in Haskell file -
   28.10  
   28.11  end
    29.1 --- a/src/HOL/ex/Codegenerator.thy	Sun May 06 21:49:44 2007 +0200
    29.2 +++ b/src/HOL/ex/Codegenerator.thy	Sun May 06 21:50:17 2007 +0200
    29.3 @@ -8,7 +8,7 @@
    29.4  imports ExecutableContent
    29.5  begin
    29.6  
    29.7 -code_gen "*" (SML) (Haskell) (OCaml)
    29.8 -code_gen (SML #) (Haskell -) (OCaml -)
    29.9 +code_gen "*" in SML in OCaml file - in OCaml file -
   29.10 +code_gen in SML in OCaml file - in OCaml file -
   29.11  
   29.12  end
   29.13 \ No newline at end of file
    30.1 --- a/src/HOL/ex/Codegenerator_Rat.thy	Sun May 06 21:49:44 2007 +0200
    30.2 +++ b/src/HOL/ex/Codegenerator_Rat.thy	Sun May 06 21:50:17 2007 +0200
    30.3 @@ -29,7 +29,7 @@
    30.4  definition
    30.5    "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
    30.6  
    30.7 -code_gen foobar (SML #) (OCaml -) (Haskell -)
    30.8 +code_gen foobar in SML in OCaml file - in Haskell file -
    30.9  ML {* ROOT.Codegenerator_Rat.foobar *}
   30.10  
   30.11  code_module Foo
    31.1 --- a/src/HOL/ex/NormalForm.thy	Sun May 06 21:49:44 2007 +0200
    31.2 +++ b/src/HOL/ex/NormalForm.thy	Sun May 06 21:50:17 2007 +0200
    31.3 @@ -13,7 +13,7 @@
    31.4  lemma "p \<longrightarrow> True" by normalization
    31.5  declare disj_assoc [code func]
    31.6  lemma "((P | Q) | R) = (P | (Q | R))" by normalization
    31.7 -declare disj_assoc [code nofunc]
    31.8 +declare disj_assoc [code func del]
    31.9  lemma "0 + (n::nat) = n" by normalization
   31.10  lemma "0 + Suc n = Suc n" by normalization
   31.11  lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
    32.1 --- a/src/HOL/ex/Random.thy	Sun May 06 21:49:44 2007 +0200
    32.2 +++ b/src/HOL/ex/Random.thy	Sun May 06 21:50:17 2007 +0200
    32.3 @@ -13,7 +13,7 @@
    32.4  where
    32.5    pick_undef: "pick [] n = undefined"
    32.6    | pick_simp: "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
    32.7 -lemmas [code nofunc] = pick_undef
    32.8 +lemmas [code func del] = pick_undef
    32.9  
   32.10  typedecl randseed
   32.11  
   32.12 @@ -180,7 +180,4 @@
   32.13  code_const run_random
   32.14    (SML "case _ (Random.seed ()) of (x, '_) => x")
   32.15  
   32.16 -code_gen select select_weight
   32.17 -  (SML #)
   32.18 -
   32.19  end
    33.1 --- a/src/Pure/Tools/codegen_package.ML	Sun May 06 21:49:44 2007 +0200
    33.2 +++ b/src/Pure/Tools/codegen_package.ML	Sun May 06 21:50:17 2007 +0200
    33.3 @@ -7,8 +7,6 @@
    33.4  
    33.5  signature CODEGEN_PACKAGE =
    33.6  sig
    33.7 -  include BASIC_CODEGEN_THINGOL;
    33.8 -  val codegen_term: theory -> term -> iterm;
    33.9    val eval_term: theory -> (string (*reference name!*) * 'a option ref) * term -> 'a;
   33.10    val satisfies_ref: bool option ref;
   33.11    val satisfies: theory -> term -> string list -> bool;
   33.12 @@ -605,9 +603,9 @@
   33.13  
   33.14  fun code raw_cs seris thy =
   33.15    let
   33.16 -    val seris' = map (fn (target, args as _ :: _) =>
   33.17 -          (target, SOME (CodegenSerializer.get_serializer thy target args CodegenNames.labelled_name))
   33.18 -      | (target, []) => (CodegenSerializer.assert_serializer thy target, NONE)) seris;
   33.19 +    val seris' = map (fn ((target, file), args) =>
   33.20 +      (target, SOME (CodegenSerializer.get_serializer thy target file args
   33.21 +        CodegenNames.labelled_name))) seris;
   33.22      val targets = case map fst seris' of [] => NONE | xs => SOME xs;
   33.23      val cs = CodegenConsts.read_const_exprs thy
   33.24        (filter_generatable thy targets) raw_cs;
   33.25 @@ -632,13 +630,12 @@
   33.26  fun code_deps_cmd thy =
   33.27    code_deps thy o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy);
   33.28  
   33.29 -val code_exprP = (
   33.30 -    (Scan.repeat P.term
   33.31 -    -- Scan.repeat (P.$$$ "(" |--
   33.32 -        P.name -- P.arguments
   33.33 -        --| P.$$$ ")"))
   33.34 -    >> (fn (raw_cs, seris) => code raw_cs seris)
   33.35 -  );
   33.36 +val code_exprP =
   33.37 +  (Scan.repeat P.term
   33.38 +  -- Scan.repeat (P.$$$ "in" |-- P.name
   33.39 +     -- Scan.option (P.$$$ "file" |-- P.name)
   33.40 +     -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
   33.41 +  ) >> (fn (raw_cs, seris) => code raw_cs seris));
   33.42  
   33.43  val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) =
   33.44    ("code_gen", "code_abstype", "code_axioms", "code_thms", "code_deps");
   33.45 @@ -646,7 +643,7 @@
   33.46  in
   33.47  
   33.48  val codeP =
   33.49 -  OuterSyntax.improper_command codeK "generate and serialize executable code for constants"
   33.50 +  OuterSyntax.improper_command codeK "generate executable code for constants"
   33.51      K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   33.52  
   33.53  fun codegen_command thy cmd =
    34.1 --- a/src/Pure/Tools/codegen_serializer.ML	Sun May 06 21:49:44 2007 +0200
    34.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Sun May 06 21:50:17 2007 +0200
    34.3 @@ -31,7 +31,7 @@
    34.4  
    34.5    type serializer;
    34.6    val add_serializer: string * serializer -> theory -> theory;
    34.7 -  val get_serializer: theory -> string -> Args.T list -> (theory -> string -> string)
    34.8 +  val get_serializer: theory -> string -> string option -> Args.T list -> (theory -> string -> string)
    34.9      -> string list option -> CodegenThingol.code -> unit;
   34.10    val assert_serializer: theory -> string -> string;
   34.11  
   34.12 @@ -1026,16 +1026,15 @@
   34.13        (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes))
   34.14    in output p end;
   34.15  
   34.16 -val isar_seri_sml =
   34.17 +fun isar_seri_sml file =
   34.18    let
   34.19 -    fun output_file file = File.write (Path.explode file) o code_output;
   34.20 -    val output_diag = writeln o code_output;
   34.21 -    val output_internal = use_text "generated code" Output.ml_output false o code_output;
   34.22 +    val output = case file
   34.23 +     of NONE => use_text "generated code" Output.ml_output false o code_output
   34.24 +      | SOME "-" => writeln o code_output
   34.25 +      | SOME file => File.write (Path.explode file) o code_output;
   34.26    in
   34.27 -    parse_args ((Args.$$$ "-" >> K output_diag
   34.28 -      || Args.$$$ "#" >> K output_internal
   34.29 -      || Args.name >> output_file)
   34.30 -    >> (fn output => seri_ml pr_sml pr_sml_modl ML_Syntax.reserved output))
   34.31 +    parse_args (Scan.succeed ())
   34.32 +    #> (fn () => seri_ml pr_sml pr_sml_modl ML_Syntax.reserved output)
   34.33    end;
   34.34  
   34.35  val reserved_ocaml = Name.make_context ["and", "as", "assert", "begin", "class",
   34.36 @@ -1046,14 +1045,17 @@
   34.37    "sig", "struct", "then", "to", "true", "try", "type", "val",
   34.38    "virtual", "when", "while", "with", "mod"];
   34.39  
   34.40 -val isar_seri_ocaml =
   34.41 +fun isar_seri_ocaml file =
   34.42    let
   34.43 +    val output = case file
   34.44 +     of NONE => error "OCaml: no internal compilation"
   34.45 +      | SOME "-" => writeln o code_output
   34.46 +      | SOME file => File.write (Path.explode file) o code_output;
   34.47      fun output_file file = File.write (Path.explode file) o code_output;
   34.48      val output_diag = writeln o code_output;
   34.49    in
   34.50 -    parse_args ((Args.$$$ "-" >> K output_diag
   34.51 -      || Args.name >> output_file)
   34.52 -    >> (fn output => seri_ml pr_ocaml pr_ocaml_modl reserved_ocaml output))
   34.53 +    parse_args (Scan.succeed ())
   34.54 +    #> (fn () => seri_ml pr_ocaml pr_ocaml_modl reserved_ocaml output)
   34.55    end;
   34.56  
   34.57  
   34.58 @@ -1425,12 +1427,18 @@
   34.59        end;
   34.60    in Symtab.fold (fn modl => fn () => seri_module modl) code' () end;
   34.61  
   34.62 -val isar_seri_haskell =
   34.63 -  parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
   34.64 -    -- Scan.optional (Args.$$$ "string_classes" >> K true) false
   34.65 -    -- (Args.$$$ "-" >> K NONE || Args.name >> SOME)
   34.66 -    >> (fn ((module_prefix, string_classes), destination) =>
   34.67 -      seri_haskell module_prefix (Option.map Path.explode destination) string_classes));
   34.68 +fun isar_seri_haskell file =
   34.69 +  let
   34.70 +    val destination = case file
   34.71 +     of NONE => error ("Haskell: no internal compilation")
   34.72 +      | SOME "-" => NONE
   34.73 +      | SOME file => SOME (Path.explode file)
   34.74 +  in
   34.75 +    parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
   34.76 +      -- Scan.optional (Args.$$$ "string_classes" >> K true) false
   34.77 +      >> (fn (module_prefix, string_classes) =>
   34.78 +        seri_haskell module_prefix destination string_classes))
   34.79 +  end;
   34.80  
   34.81  
   34.82  (** diagnosis serializer **)
   34.83 @@ -1494,7 +1502,9 @@
   34.84      Symtab.merge (op =) (prolog1, prolog2)
   34.85    );
   34.86  
   34.87 -type serializer = Args.T list
   34.88 +type serializer =
   34.89 +  string option
   34.90 +  -> Args.T list
   34.91    -> (string -> string)
   34.92    -> string list
   34.93    -> (string -> string option)
   34.94 @@ -1581,10 +1591,10 @@
   34.95    #> add_serializer (target_SML, isar_seri_sml)
   34.96    #> add_serializer (target_OCaml, isar_seri_ocaml)
   34.97    #> add_serializer (target_Haskell, isar_seri_haskell)
   34.98 -  #> add_serializer (target_diag, (fn _ => fn _ => seri_diagnosis))
   34.99 +  #> add_serializer (target_diag, (fn _ => fn _ => fn _ => seri_diagnosis))
  34.100  );
  34.101  
  34.102 -fun get_serializer thy target args labelled_name = fn cs =>
  34.103 +fun get_serializer thy target file args labelled_name = fn cs =>
  34.104    let
  34.105      val data = case Symtab.lookup (CodegenSerializerData.get thy) target
  34.106       of SOME data => data
  34.107 @@ -1597,7 +1607,7 @@
  34.108        else CodegenThingol.project_code
  34.109          (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs;
  34.110    in
  34.111 -    project #> seri args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
  34.112 +    project #> seri file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
  34.113        (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
  34.114    end;
  34.115  
    35.1 --- a/src/Pure/codegen.ML	Sun May 06 21:49:44 2007 +0200
    35.2 +++ b/src/Pure/codegen.ML	Sun May 06 21:50:17 2007 +0200
    35.3 @@ -366,17 +366,19 @@
    35.4    (Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]);
    35.5  
    35.6  local
    35.7 +  fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    35.8    fun add_simple_attribute (name, f) =
    35.9 -    (add_attribute name o (Scan.succeed o Thm.declaration_attribute))
   35.10 -      (fn th => Context.mapping (f th) I);
   35.11 +    add_attribute name (Scan.succeed (mk_attribute f));
   35.12 +  fun add_del_attribute (name, (add, del)) =
   35.13 +    add_attribute name (Args.del |-- Scan.succeed (mk_attribute del)
   35.14 +      || Scan.succeed (mk_attribute add))
   35.15  in
   35.16 -  val _ = map (Context.add_setup o add_simple_attribute) [
   35.17 -    ("func", CodeData.add_func true),
   35.18 -    ("nofunc", CodeData.del_func),
   35.19 -    ("unfold", (fn thm => add_unfold thm #> CodeData.add_inline thm)),
   35.20 -    ("inline", CodeData.add_inline),
   35.21 -    ("noinline", CodeData.del_inline)
   35.22 -  ]
   35.23 +  val _ = Context.add_setup (add_simple_attribute ("unfold",
   35.24 +    fn thm => add_unfold thm #> CodeData.add_inline thm));
   35.25 +  val _ = map (Context.add_setup o add_del_attribute) [
   35.26 +    ("func", (CodeData.add_func true, CodeData.del_func)),
   35.27 +    ("inline", (CodeData.add_inline, CodeData.del_inline))
   35.28 +  ];
   35.29  end; (*local*)
   35.30  
   35.31