# HG changeset patch # User haftmann # Date 1178481017 -7200 # Node ID 5f9138bcb3d75b731a5851e2c01134251ae80831 # Parent 91c05f4b509ec50744244900fb374be574664dc6 changed code generator invocation syntax diff -r 91c05f4b509e -r 5f9138bcb3d7 NEWS --- a/NEWS Sun May 06 21:49:44 2007 +0200 +++ b/NEWS Sun May 06 21:50:17 2007 +0200 @@ -95,10 +95,10 @@ Theorem attributs for selecting and transforming function equations theorems: - [code fun]: select a theorem as function equation for a specific constant - [code nofun]: deselect a theorem as function equation for a specific constant - [code inline]: select an equation theorem for unfolding (inlining) in place - [code noinline]: deselect an equation theorem for unfolding (inlining) in place + [code fun]: select a theorem as function equation for a specific constant + [code fun del]: deselect a theorem as function equation for a specific constant + [code inline]: select an equation theorem for unfolding (inlining) in place + [code inline del]: deselect an equation theorem for unfolding (inlining) in place User-defined serializations (target in {SML, OCaml, Haskell}): @@ -519,6 +519,13 @@ *** HOL *** +* case expressions and primrec: missing cases now mapped to "undefined" +instead of "arbitrary" + +* new constant "undefined" with axiom "undefined x = undefined" + +* new class "default" with associated constant "default" + * Library/Pretty_Int.thy: maps HOL numerals on target language integer literals when generating code. @@ -639,11 +646,11 @@ meet_min ~> inf_min join_max ~> sup_max -* Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and +* Classes "order" and "linorder": facts "refl", "trans" and "cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY. -* Addes class (axclass + locale) "preorder" as superclass of "order"; +* Classes "order" and "linorder": potential INCOMPATIBILITY: order of proof goals in order/linorder instance proofs changed. diff -r 91c05f4b509e -r 5f9138bcb3d7 doc-src/IsarAdvanced/Classes/Thy/Classes.thy --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Sun May 06 21:49:44 2007 +0200 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Sun May 06 21:50:17 2007 +0200 @@ -459,7 +459,7 @@ \noindent This maps to Haskell as: *} -code_gen example (Haskell "code_examples/") +code_gen example in Haskell file "code_examples/" (* NOTE: you may use Haskell only once in this document, otherwise you have to work in distinct subdirectories *) @@ -471,7 +471,7 @@ \noindent The whole code in SML with explicit dictionary passing: *} -code_gen example (*<*)(SML #)(*>*)(SML "code_examples/classes.ML") +code_gen example (*<*)in SML(*>*)in SML file "code_examples/classes.ML" text {* \lstsml{Thy/code_examples/classes.ML} diff -r 91c05f4b509e -r 5f9138bcb3d7 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Sun May 06 21:49:44 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Sun May 06 21:50:17 2007 +0200 @@ -143,7 +143,7 @@ \noindent Then we generate code *} -code_gen example (*<*)(SML #)(*>*)(SML "examples/tree.ML") +code_gen example (*<*)in SML(*>*)in SML file "examples/tree.ML" text {* \noindent which looks like: @@ -221,15 +221,14 @@ \noindent This executable specification is now turned to SML code: *} -code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac.ML") +code_gen fac (*<*)in SML(*>*)in SML file "examples/fac.ML" text {* \noindent The @{text "\"} command takes a space-separated list of constants together with \qn{serialization directives} - in parentheses. These start with a \qn{target language} - identifier, followed by arguments, their semantics - depending on the target. In the SML case, a filename - is given where to write the generated code to. + These start with a \qn{target language} + identifier, followed by a file specification + where to write the generated code to. Internally, the defining equations for all selected constants are taken, including any transitively required @@ -260,7 +259,7 @@ pick_some :: "'a list \ 'a" where "pick_some = hd" (*>*) -code_gen pick_some (SML "examples/fail_const.ML") +code_gen pick_some in SML file "examples/fail_const.ML" text {* \noindent will fail. *} @@ -304,7 +303,7 @@ "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" by simp -code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML") +code_gen pick (*<*)in SML(*>*) in SML file "examples/pick1.ML" text {* \noindent This theorem now is used for generating code: @@ -312,12 +311,12 @@ \lstsml{Thy/examples/pick1.ML} \noindent It might be convenient to remove the pointless original - equation, using the \emph{nofunc} attribute: + equation, using the \emph{func del} attribute: *} -lemmas [code nofunc] = pick.simps +lemmas [code func del] = pick.simps -code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick2.ML") +code_gen pick (*<*)in SML(*>*) in SML file "examples/pick2.ML" text {* \lstsml{Thy/examples/pick2.ML} @@ -333,7 +332,7 @@ "fac n = (case n of 0 \ 1 | Suc m \ n * fac m)" by (cases n) simp_all -code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac_case.ML") +code_gen fac (*<*)in SML(*>*)in SML file "examples/fac_case.ML" text {* \lstsml{Thy/examples/fac_case.ML} @@ -342,7 +341,7 @@ The attributes \emph{code} and \emph{code del} associated with the existing code generator also apply to the new one: \emph{code} implies \emph{code func}, - and \emph{code del} implies \emph{code nofunc}. + and \emph{code del} implies \emph{code func del}. \end{warn} *} @@ -392,10 +391,10 @@ as SML, but, in accordance with conventions some Haskell systems enforce, each module ends up in a single file. The module hierarchy is reflected in - the file system, with root given by the user. + the file system, with root directory given as file specification. *} -code_gen dummy (Haskell "examples/") +code_gen dummy in Haskell file "examples/" (* NOTE: you may use Haskell only once in this document, otherwise you have to work in distinct subdirectories *) @@ -408,7 +407,7 @@ The whole code in SML with explicit dictionary passing: *} -code_gen dummy (*<*)(SML #)(*>*)(SML "examples/class.ML") +code_gen dummy (*<*)in SML(*>*)in SML file "examples/class.ML" text {* \lstsml{Thy/examples/class.ML} @@ -418,13 +417,14 @@ \noindent or in OCaml: *} -code_gen dummy (OCaml "examples/class.ocaml") +code_gen dummy in OCaml file "examples/class.ocaml" text {* \lstsml{Thy/examples/class.ocaml} \medskip The explicit association of constants to classes can be inspected using the @{text "\"} + command. *} @@ -496,38 +496,41 @@ hand side and the arguments of the left hand side of an equation, but never to the constant heading the left hand side. Inline theorems may be declared an undeclared using the - \emph{code inline} or \emph{code noinline} attribute respectively. + \emph{code inline} or \emph{code inline del} attribute respectively. Some common applications: *} text_raw {* \begin{itemize} - \item replacing non-executable constructs by executable ones: \\ -*} - -lemma [code inline]: - "x \ set xs \ x mem xs" by (induct xs) simp_all - -text_raw {* - \item eliminating superfluous constants: \\ *} -lemma [code inline]: - "1 = Suc 0" by simp +text {* + \item replacing non-executable constructs by executable ones: +*} -text_raw {* - \item replacing executable but inconvenient constructs: \\ + lemma [code inline]: + "x \ set xs \ x mem xs" by (induct xs) simp_all + +text {* + \item eliminating superfluous constants: *} -lemma [code inline]: - "xs = [] \ List.null xs" by (induct xs) simp_all + lemma [code inline]: + "1 = Suc 0" by simp + +text {* + \item replacing executable but inconvenient constructs: +*} + + lemma [code inline]: + "xs = [] \ List.null xs" by (induct xs) simp_all text_raw {* \end{itemize} *} text {* - The current set of inline theorems may be inspected using + \noindent The current set of inline theorems may be inspected using the @{text "\"} command. \emph{Inline procedures} are a generalized version of inline @@ -580,7 +583,7 @@ performs an explicit equality check. *} -code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML") +code_gen collect_duplicates (*<*)in SML(*>*)in SML file "examples/collect_duplicates.ML" text {* \lstsml{Thy/examples/collect_duplicates.ML} @@ -623,9 +626,9 @@ "p1 \ p2 \ let (x1 \ 'a\ord, y1 \ 'b\ord) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 \ y2)" .. -lemmas [code nofunc] = less_prod_def less_eq_prod_def +lemmas [code func del] = less_prod_def less_eq_prod_def -lemma ord_prod [code func(*<*), code nofunc(*>*)]: +lemma ord_prod [code func(*<*), code func del(*>*)]: "(x1 \ 'a\ord, y1 \ 'b\ord) < (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 < y2)" "(x1 \ 'a\ord, y1 \ 'b\ord) \ (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 \ y2)" unfolding less_prod_def less_eq_prod_def by simp_all @@ -653,7 +656,7 @@ *} code_gen "op \ \ 'a\{eq, ord} \ 'b\ord \ 'a \ 'b \ bool" - (*<*)(SML #)(*>*)(SML "examples/lexicographic.ML") + (*<*)in SML(*>*)in SML file "examples/lexicographic.ML" text {* \lstsml{Thy/examples/lexicographic.ML} @@ -713,7 +716,7 @@ code_const %tt True and False and "op \" and Not (SML and and and) (*>*) -code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_literal.ML") +code_gen in_interval (*<*)in SML(*>*)in SML file "examples/bool_literal.ML" text {* \lstsml{Thy/examples/bool_literal.ML} @@ -756,7 +759,7 @@ After this setup, code looks quite more readable: *} -code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_mlbool.ML") +code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_mlbool.ML" text {* \lstsml{Thy/examples/bool_mlbool.ML} @@ -772,7 +775,7 @@ code_const %tt "op \" (SML infixl 1 "andalso") -code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_infix.ML") +code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_infix.ML" text {* \lstsml{Thy/examples/bool_infix.ML} @@ -901,7 +904,7 @@ lemma [code func]: "\set xs = foldr (op \) xs {}" by (induct xs) simp_all -code_gen "{}" insert "op \" "op \" "Union" (*<*)(SML #)(*>*)(SML "examples/set_list.ML") +code_gen "{}" insert "op \" "op \" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML" text {* \lstsml{Thy/examples/set_list.ML} @@ -1025,7 +1028,7 @@ "dummy_option (x#xs) = Some x" | "dummy_option [] = arbitrary" -code_gen dummy_option (*<*)(SML #)(*>*)(SML "examples/arbitrary.ML") +code_gen dummy_option (*<*)in SML(*>*)in SML file "examples/arbitrary.ML" text {* \lstsml{Thy/examples/arbitrary.ML} diff -r 91c05f4b509e -r 5f9138bcb3d7 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Sun May 06 21:49:44 2007 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Sun May 06 21:50:17 2007 +0200 @@ -172,7 +172,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ example\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}tree{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent which looks like: \lstsml{Thy/examples/tree.ML}% @@ -255,14 +255,13 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent The \isa{{\isasymCODEGEN}} command takes a space-separated list of constants together with \qn{serialization directives} - in parentheses. These start with a \qn{target language} - identifier, followed by arguments, their semantics - depending on the target. In the SML case, a filename - is given where to write the generated code to. + These start with a \qn{target language} + identifier, followed by a file specification + where to write the generated code to. Internally, the defining equations for all selected constants are taken, including any transitively required @@ -309,7 +308,7 @@ % \endisadelimML \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ pick{\isacharunderscore}some\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ pick{\isacharunderscore}some\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent will fail.% \end{isamarkuptext}% @@ -374,21 +373,21 @@ \endisadelimproof \isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent This theorem now is used for generating code: \lstsml{Thy/examples/pick1.ML} \noindent It might be convenient to remove the pointless original - equation, using the \emph{nofunc} attribute:% + equation, using the \emph{func del} attribute:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemmas}\isamarkupfalse% -\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline +\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline \isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/examples/pick2.ML} @@ -419,7 +418,7 @@ \endisadelimproof \isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ fac\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isacharunderscore}case{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isacharunderscore}case{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/examples/fac_case.ML} @@ -427,7 +426,7 @@ The attributes \emph{code} and \emph{code del} associated with the existing code generator also apply to the new one: \emph{code} implies \emph{code func}, - and \emph{code del} implies \emph{code nofunc}. + and \emph{code del} implies \emph{code func del}. \end{warn}% \end{isamarkuptext}% \isamarkuptrue% @@ -510,11 +509,11 @@ as SML, but, in accordance with conventions some Haskell systems enforce, each module ends up in a single file. The module hierarchy is reflected in - the file system, with root given by the user.% + the file system, with root directory given as file specification.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ dummy\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}% +\ dummy\ \isakeyword{in}\ Haskell\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}% \begin{isamarkuptext}% \lsthaskell{Thy/examples/Codegen.hs} \noindent (we have left out all other modules). @@ -525,7 +524,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ dummy\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ dummy\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/examples/class.ML} @@ -535,12 +534,13 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ dummy\ {\isacharparenleft}OCaml\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}{\isacharparenright}% +\ dummy\ \isakeyword{in}\ OCaml\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/examples/class.ocaml} \medskip The explicit association of constants - to classes can be inspected using the \isa{{\isasymPRINTCLASSES}}% + to classes can be inspected using the \isa{{\isasymPRINTCLASSES}} + command.% \end{isamarkuptext}% \isamarkuptrue% % @@ -620,16 +620,20 @@ hand side and the arguments of the left hand side of an equation, but never to the constant heading the left hand side. Inline theorems may be declared an undeclared using the - \emph{code inline} or \emph{code noinline} attribute respectively. + \emph{code inline} or \emph{code inline del} attribute respectively. Some common applications:% \end{isamarkuptext}% \isamarkuptrue% % \begin{itemize} - \item replacing non-executable constructs by executable ones: \\ -\isacommand{lemma}\isamarkupfalse% +% +\begin{isamarkuptext}% +\item replacing non-executable constructs by executable ones:% +\end{isamarkuptext}% +\isamarkuptrue% +\ \ \isacommand{lemma}\isamarkupfalse% \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}% +\ \ \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}% \isadelimproof \ % \endisadelimproof @@ -644,10 +648,13 @@ % \endisadelimproof % -\item eliminating superfluous constants: \\ -\isacommand{lemma}\isamarkupfalse% +\begin{isamarkuptext}% +\item eliminating superfluous constants:% +\end{isamarkuptext}% +\isamarkuptrue% +\ \ \isacommand{lemma}\isamarkupfalse% \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}% +\ \ \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}% \isadelimproof \ % \endisadelimproof @@ -662,10 +669,13 @@ % \endisadelimproof % -\item replacing executable but inconvenient constructs: \\ -\isacommand{lemma}\isamarkupfalse% +\begin{isamarkuptext}% +\item replacing executable but inconvenient constructs:% +\end{isamarkuptext}% +\isamarkuptrue% +\ \ \isacommand{lemma}\isamarkupfalse% \ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}% +\ \ \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}% \isadelimproof \ % \endisadelimproof @@ -683,7 +693,7 @@ \end{itemize} % \begin{isamarkuptext}% -The current set of inline theorems may be inspected using +\noindent The current set of inline theorems may be inspected using the \isa{{\isasymPRINTCODESETUP}} command. \emph{Inline procedures} are a generalized version of inline @@ -739,7 +749,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ collect{\isacharunderscore}duplicates\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/examples/collect_duplicates.ML}% \end{isamarkuptext}% @@ -817,7 +827,7 @@ \isanewline \isanewline \isacommand{lemmas}\isamarkupfalse% -\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline +\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline \isanewline \isacommand{lemma}\isamarkupfalse% \ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline @@ -878,7 +888,7 @@ \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% \ {\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 -\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/examples/lexicographic.ML}% \end{isamarkuptext}% @@ -952,7 +962,7 @@ % \endisadelimtt \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}literal{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ in{\isacharunderscore}interval\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}literal{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/examples/bool_literal.ML} @@ -1009,7 +1019,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}mlbool{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/examples/bool_mlbool.ML} @@ -1039,7 +1049,7 @@ \isanewline \isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ in{\isacharunderscore}interval\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}infix{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ in{\isacharunderscore}interval\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}bool{\isacharunderscore}infix{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/examples/bool_infix.ML} @@ -1315,7 +1325,7 @@ \isanewline \isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ {\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}% +\ {\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}% \begin{isamarkuptext}% \lstsml{Thy/examples/set_list.ML} @@ -1449,7 +1459,7 @@ \ \ {\isacharbar}\ {\isachardoublequoteopen}dummy{\isacharunderscore}option\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ arbitrary{\isachardoublequoteclose}\isanewline \isanewline \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% -\ dummy{\isacharunderscore}option\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% +\ dummy{\isacharunderscore}option\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}arbitrary{\isachardot}ML{\isachardoublequoteclose}% \begin{isamarkuptext}% \lstsml{Thy/examples/arbitrary.ML} diff -r 91c05f4b509e -r 5f9138bcb3d7 doc-src/IsarRef/logics.tex --- a/doc-src/IsarRef/logics.tex Sun May 06 21:49:44 2007 +0200 +++ b/doc-src/IsarRef/logics.tex Sun May 06 21:50:17 2007 +0200 @@ -772,9 +772,7 @@ \indexisarcmd{code-abstype} \indexisarcmd{print-codesetup} \indexisaratt{code func} -\indexisaratt{code nofunc} \indexisaratt{code inline} -\indexisaratt{code noinline} \begin{matharray}{rcl} \isarcmd{code_gen}^* & : & \isarkeep{theory~|~proof} \\ @@ -793,13 +791,12 @@ \isarcmd{code_abstype} & : & \isartrans{theory}{theory} \\ \isarcmd{print_codesetup}^* & : & \isarkeep{theory~|~proof} \\ code\ func & : & \isaratt \\ - code\ nofunc & : & \isaratt \\ code\ inline & : & \isaratt \\ - code\ noinline & : & \isaratt \\ \end{matharray} \begin{rail} -'code\_gen' ( constexpr + ) ? ( seri + ) ?; +'code\_gen' ( constexpr + ) ? \\ + ( ( 'in' target ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?; 'code\_thms' ( constexpr + ) ?; @@ -813,24 +810,23 @@ class : nameref; -seri : target | 'SML' ( string | '-' ) | 'OCaml' ( string | '-' ) | 'Haskell' ( 'root:' string ) ? 'string\_classes' ? string; - target : 'OCaml' | 'SML' | 'Haskell'; 'code\_datatype' const +; 'code\_const' (const + 'and') \\ - ( ( '(' target ( syntax + 'and' ) ')' ) + ); + ( ( '(' target ( syntax ? + 'and' ) ')' ) + ); 'code\_type' (typeconstructor + 'and') \\ - ( ( '(' target ( syntax + 'and' ) ')' ) + ); + ( ( '(' target ( syntax ? + 'and' ) ')' ) + ); 'code\_class' (class + 'and') \\ ( ( '(' target \\ - ( ( string ('where' ( const ( '==' | equiv ) string ) + ) ? ) + 'and' ) ')' ) + ); + ( ( string ('where' \\ + ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + ); 'code\_instance' (( typeconstructor '::' class ) + 'and') \\ - ( ( '(' target ( '-' + 'and' ) ')' ) + ); + ( ( '(' target ( '-' ? + 'and' ) ')' ) + ); 'code\_monad' term term term; @@ -848,7 +844,9 @@ 'print\_codesetup'; -('code\ func' | 'code\ nofunc' | 'code\ inline' | 'code\ noinline'); +'code\ func' ( 'del' ) ?; + +'code\ inline' ( 'del' ) ?; \end{rail} \begin{descr} @@ -856,7 +854,7 @@ \item [$\isarcmd{code_gen}$] is the canonical interface for generating and serializing code: for a given list of constants, code is generated for the specified target language(s). Abstract code is cached incrementally. If no constant is given, - the whole current cache is serialized. If no serialization instruction + the currently cached code is serialized. If no serialization instruction is given, only abstract code is cached. Constants may be specified by giving them literally, referring @@ -864,45 +862,45 @@ by giving (``name.*''), or referring to \emph{all} executable constants currently available (``*''). - The \emph{SML} serializer takes either a filename or an ``-'' or ``*'' - as argument. In the first case, code is written to the specified file, - in the second to standard output and in the last case - it is compiled internally in the context of the current ML session. - - The \emph{OCaml} serializer is like the \emph{SML} serializer - but it produces code for OCaml and does not support internal compilation. + For \emph{SML} and \emph{OCaml}, the file specification refers to + a single file; for \emph{Haskell}, it refers to a whole directory, + where code is generated in multiple files reflecting the module hierarchy. + The file specification ``-'' denotes standard output. For \emph{SML}, + omitting the file specification compiles code internally + in the context of the current ML session. - For \emph{Haskell}, a directory name is specified; different modules - are serialized to different files in this directory or - subdirectories, reflecting the module hierarchy. Additionally - a module name prefix may be given using the ``root:'' argument; - ``string\_classes'' adds a ``deriving (Read, Show)'' clause + Serializers take an optional list of arguments in parentheses. + For \emph{Haskell} a module name prefix may be given using the ``root:'' + argument; ``string\_classes'' adds a ``deriving (Read, Show)'' clause to each appropriate datatype declaration. - A ``-'' instead of a directory name prints code to standard output. \item [$\isarcmd{code_thms}$] prints a list of theorems representing the corresponding program containing all given constants; if no constants are - given, the current cache of code theorems in printed. + given, the currently cached code theorems in printed. \item [$\isarcmd{code_deps}$] visualizes dependencies of theorems representing the corresponding program containing all given constants; if no constants are - given, the current cache os visualized. + given, the currently cached code theorems are visualized. \item [$\isarcmd{code_datatype}$] specifies a constructor set for a logical type. \item [$\isarcmd{code_const}$] associates a list of constants - with target-specific serializations. + with target-specific serializations; omitting a serialization + deletes an existing serialization. \item [$\isarcmd{code_type}$] associates a list of type constructors - with target-specific serializations. + with target-specific serializations; omitting a serialization + deletes an existing serialization. \item [$\isarcmd{code_class}$] associates a list of classes with target-specific class names; in addition, constants associated with this class may be given target-specific names used for instance - declarations. Applies only to \emph{Haskell}. + declarations; omitting a serialization + deletes an existing serialization. Applies only to \emph{Haskell}. \item [$\isarcmd{code_instance}$] declares a list of type constructor / class instance relations as ``already present'' for a given target. + Omitting a ``-'' deletes an existing ``already present'' declaration. Applies only to \emph{Haskell}. \item [$\isarcmd{code_monad}$] provides an auxiliary mechanism @@ -925,15 +923,16 @@ \item [$\isarcmd{code_abstype}$] offers an interface for implementing an abstract type plus operations by executable counterparts. -\item [$code\ func$ and $code\ nofunc$] select or deselect explicitly +\item [$code\ func$] selects (or with option ''del``, deselects) explicitly a defining equation for code generation. Usually packages introducing defining equations provide a resonable default setup for selection. -\item [$code\ inline$ and $code\ noinline$] select or deselect - inlining theorems which are applied as rewrite rules to any defining equation. +\item [$code\ inline$] declares (or with option ''del``, removes) + inlining theorems which are applied as rewrite rules to any defining equation + during preprocessing. \item [$\isarcmd{print_codesetup}$] gives an overview on selected - defining equations, code generator datatypes and inlining theorems. + defining equations, code generator datatypes and preprocessor setup. \end{descr} diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Code_Generator.thy --- a/src/HOL/Code_Generator.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Code_Generator.thy Sun May 06 21:50:17 2007 +0200 @@ -78,7 +78,7 @@ class eq (attach "op =") = type -text {* equality for Haskell *} +text {* using built-in Haskell equality *} code_class eq (Haskell "Eq" where "op =" \ "(==)") @@ -114,16 +114,10 @@ instance bool :: eq .. lemma [code func]: - "True = P \ P" by simp - -lemma [code func]: - "False = P \ \ P" by simp - -lemma [code func]: - "P = True \ P" by simp - -lemma [code func]: - "P = False \ \ P" by simp + shows "True = P \ P" + and "False = P \ \ P" + and "P = True \ P" + and "P = False \ \ P" by simp_all code_type bool (SML "bool") @@ -211,7 +205,7 @@ definition if_delayed :: "bool \ (bool \ 'a) \ (bool \ 'a) \ 'a" where - [code nofunc]: "if_delayed b f g = (if b then f True else g False)" + [code func del]: "if_delayed b f g = (if b then f True else g False)" lemma [code func]: shows "if_delayed True f g = f True" diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Divides.thy Sun May 06 21:50:17 2007 +0200 @@ -898,7 +898,7 @@ subsection {* Code generation for div, mod and dvd on nat *} -definition [code nofunc]: +definition [code func del]: "divmod (m\nat) n = (m div n, m mod n)" lemma divmod_zero [code]: "divmod m 0 = (0, m)" diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Extraction/Higman.thy --- a/src/HOL/Extraction/Higman.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Extraction/Higman.thy Sun May 06 21:50:17 2007 +0200 @@ -406,7 +406,7 @@ arbitrary_LT \ arbitrary_LT' arbitrary_TT \ arbitrary_TT' -code_gen higman_idx (SML #) +code_gen higman_idx in SML ML {* local diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Extraction/Pigeonhole.thy --- a/src/HOL/Extraction/Pigeonhole.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Extraction/Pigeonhole.thy Sun May 06 21:50:17 2007 +0200 @@ -309,7 +309,7 @@ test' = test' test'' = test'' -code_gen test test' test'' (SML #) +code_gen test test' test'' in SML ML "timeit (fn () => PH.test 10)" ML "timeit (fn () => ROOT.Pigeonhole.test 10)" diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Extraction/QuotRem.thy --- a/src/HOL/Extraction/QuotRem.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Extraction/QuotRem.thy Sun May 06 21:50:17 2007 +0200 @@ -49,6 +49,6 @@ contains test = "division 9 2" -code_gen division (SML #) +code_gen division in SML end diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/FixedPoint.thy --- a/src/HOL/FixedPoint.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/FixedPoint.thy Sun May 06 21:50:17 2007 +0200 @@ -14,18 +14,19 @@ subsection {* Complete lattices *} class complete_lattice = lattice + - fixes Inf :: "'a set \ 'a" - assumes Inf_lower: "x \ A \ Inf A \ x" - assumes Inf_greatest: "(\x. x \ A \ z \ x) \ z \ Inf A" + fixes Inf :: "'a set \ 'a" ("\_" [90] 90) + assumes Inf_lower: "x \ A \ \A \ x" + assumes Inf_greatest: "(\x. x \ A \ z \ x) \ z \ \A" definition - Sup :: "'a\complete_lattice set \ 'a" where + Sup :: "'a\complete_lattice set \ 'a" +where "Sup A = Inf {b. \a \ A. a \ b}" -theorem Sup_upper: "(x::'a::complete_lattice) \ A \ x <= Sup A" +theorem Sup_upper: "(x::'a::complete_lattice) \ A \ x \ Sup A" by (auto simp: Sup_def intro: Inf_greatest) -theorem Sup_least: "(\x::'a::complete_lattice. x \ A \ x <= z) \ Sup A <= z" +theorem Sup_least: "(\x::'a::complete_lattice. x \ A \ x \ z) \ Sup A \ z" by (auto simp: Sup_def intro: Inf_lower) definition @@ -198,7 +199,7 @@ apply (iprover elim: le_funE) done -lemmas [code nofunc] = Inf_fun_def +lemmas [code func del] = Inf_fun_def theorem Sup_fun_eq: "Sup A = (\x. Sup {y. \f\A. y = f x})" apply (rule order_antisym) @@ -221,7 +222,7 @@ Inf_set_def: "Inf S \ \S" by intro_classes (auto simp add: Inf_set_def) -lemmas [code nofunc] = Inf_set_def +lemmas [code func del] = Inf_set_def theorem Sup_set_eq: "Sup S = \S" apply (rule subset_antisym) diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Fun.thy Sun May 06 21:50:17 2007 +0200 @@ -466,13 +466,12 @@ le_fun_def: "f \ g \ \x. f x \ g x" less_fun_def: "f < g \ f \ g \ f \ g" .. -lemmas [code nofunc] = le_fun_def less_fun_def - -instance "fun" :: (type, preorder) preorder - by default (auto simp add: le_fun_def less_fun_def intro: order_trans) +lemmas [code func del] = le_fun_def less_fun_def instance "fun" :: (type, order) order - by default (rule ext, auto simp add: le_fun_def less_fun_def intro: order_antisym) + by default + (auto simp add: le_fun_def less_fun_def expand_fun_eq + intro: order_trans order_antisym) lemma le_funI: "(\x. f x \ g x) \ f \ g" unfolding le_fun_def by simp @@ -536,12 +535,45 @@ apply (auto dest: le_funD) done -lemmas [code nofunc] = inf_fun_eq sup_fun_eq +lemmas [code func del] = inf_fun_eq sup_fun_eq instance "fun" :: (type, distrib_lattice) distrib_lattice by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) +subsection {* Proof tool setup *} + +text {* simplifies terms of the form + f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *} + +ML {* +let + fun gen_fun_upd NONE T _ _ = NONE + | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd},T) $ f $ x $ y) + fun dest_fun_T1 (Type (_, T :: Ts)) = T + fun find_double (t as Const (@{const_name fun_upd},T) $ f $ x $ y) = + let + fun find (Const (@{const_name fun_upd},T) $ g $ v $ w) = + if v aconv x then SOME g else gen_fun_upd (find g) T v w + | find t = NONE + in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end + fun fun_upd_prover ss = + rtac eq_reflection 1 THEN rtac ext 1 THEN + simp_tac (Simplifier.inherit_context ss @{simpset}) 1 + val fun_upd2_simproc = + Simplifier.simproc @{theory} + "fun_upd2" ["f(v := w, x := y)"] + (fn _ => fn ss => fn t => + case find_double t of (T, NONE) => NONE + | (T, SOME rhs) => + SOME (Goal.prove (Simplifier.the_context ss) [] [] + (Term.equals T $ t $ rhs) (K (fun_upd_prover ss)))) +in + Addsimprocs [fun_upd2_simproc] +end; +*} + + subsection {* Code generator setup *} code_const "op \" @@ -554,115 +586,20 @@ subsection {* ML legacy bindings *} -text{*The ML section includes some compatibility bindings and a simproc -for function updates, in addition to the usual ML-bindings of theorems.*} -ML -{* -val id_def = thm "id_def"; -val inj_on_def = thm "inj_on_def"; -val surj_def = thm "surj_def"; -val bij_def = thm "bij_def"; -val fun_upd_def = thm "fun_upd_def"; - -val o_def = thm "comp_def"; -val injI = thm "inj_onI"; -val inj_inverseI = thm "inj_on_inverseI"; -val set_cs = claset() delrules [equalityI]; - -val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))]; - -(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *) -local - fun gen_fun_upd NONE T _ _ = NONE - | gen_fun_upd (SOME f) T x y = SOME (Const ("Fun.fun_upd",T) $ f $ x $ y) - fun dest_fun_T1 (Type (_, T :: Ts)) = T - fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) = - let - fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) = - if v aconv x then SOME g else gen_fun_upd (find g) T v w - | find t = NONE - in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end - - val current_ss = simpset () - fun fun_upd_prover ss = - rtac eq_reflection 1 THEN rtac ext 1 THEN - simp_tac (Simplifier.inherit_context ss current_ss) 1 -in - val fun_upd2_simproc = - Simplifier.simproc @{theory} - "fun_upd2" ["f(v := w, x := y)"] - (fn _ => fn ss => fn t => - case find_double t of (T, NONE) => NONE - | (T, SOME rhs) => - SOME (Goal.prove (Simplifier.the_context ss) [] [] - (Term.equals T $ t $ rhs) (K (fun_upd_prover ss)))) -end; -Addsimprocs[fun_upd2_simproc]; +ML {* +val set_cs = claset() delrules [equalityI] +*} -val expand_fun_eq = thm "expand_fun_eq"; -val apply_inverse = thm "apply_inverse"; -val id_apply = thm "id_apply"; -val o_apply = thm "o_apply"; -val o_assoc = thm "o_assoc"; -val id_o = thm "id_o"; -val o_id = thm "o_id"; -val image_compose = thm "image_compose"; -val image_eq_UN = thm "image_eq_UN"; -val UN_o = thm "UN_o"; -val datatype_injI = thm "datatype_injI"; -val injD = thm "injD"; -val inj_eq = thm "inj_eq"; -val inj_onI = thm "inj_onI"; -val inj_on_inverseI = thm "inj_on_inverseI"; -val inj_onD = thm "inj_onD"; -val inj_on_iff = thm "inj_on_iff"; -val comp_inj_on = thm "comp_inj_on"; -val inj_on_contraD = thm "inj_on_contraD"; -val inj_singleton = thm "inj_singleton"; -val subset_inj_on = thm "subset_inj_on"; -val surjI = thm "surjI"; -val surj_range = thm "surj_range"; -val surjD = thm "surjD"; -val surjE = thm "surjE"; -val comp_surj = thm "comp_surj"; -val bijI = thm "bijI"; -val bij_is_inj = thm "bij_is_inj"; -val bij_is_surj = thm "bij_is_surj"; -val image_ident = thm "image_ident"; -val image_id = thm "image_id"; -val vimage_ident = thm "vimage_ident"; -val vimage_id = thm "vimage_id"; -val vimage_image_eq = thm "vimage_image_eq"; -val image_vimage_subset = thm "image_vimage_subset"; -val image_vimage_eq = thm "image_vimage_eq"; -val surj_image_vimage_eq = thm "surj_image_vimage_eq"; -val inj_vimage_image_eq = thm "inj_vimage_image_eq"; -val vimage_subsetD = thm "vimage_subsetD"; -val vimage_subsetI = thm "vimage_subsetI"; -val vimage_subset_eq = thm "vimage_subset_eq"; -val image_Int_subset = thm "image_Int_subset"; -val image_diff_subset = thm "image_diff_subset"; -val inj_on_image_Int = thm "inj_on_image_Int"; -val inj_on_image_set_diff = thm "inj_on_image_set_diff"; -val image_Int = thm "image_Int"; -val image_set_diff = thm "image_set_diff"; -val inj_image_mem_iff = thm "inj_image_mem_iff"; -val inj_image_subset_iff = thm "inj_image_subset_iff"; -val inj_image_eq_iff = thm "inj_image_eq_iff"; -val image_UN = thm "image_UN"; -val image_INT = thm "image_INT"; -val bij_image_INT = thm "bij_image_INT"; -val surj_Compl_image_subset = thm "surj_Compl_image_subset"; -val inj_image_Compl_subset = thm "inj_image_Compl_subset"; -val bij_image_Compl_eq = thm "bij_image_Compl_eq"; -val fun_upd_idem_iff = thm "fun_upd_idem_iff"; -val fun_upd_idem = thm "fun_upd_idem"; -val fun_upd_apply = thm "fun_upd_apply"; -val fun_upd_same = thm "fun_upd_same"; -val fun_upd_other = thm "fun_upd_other"; -val fun_upd_upd = thm "fun_upd_upd"; -val fun_upd_twist = thm "fun_upd_twist"; -val range_ex1_eq = thm "range_ex1_eq"; +ML {* +val id_apply = @{thm id_apply} +val id_def = @{thm id_def} +val o_apply = @{thm o_apply} +val o_assoc = @{thm o_assoc} +val o_def = @{thm o_def} +val injD = @{thm injD} +val datatype_injI = @{thm datatype_injI} +val range_ex1_eq = @{thm range_ex1_eq} +val expand_fun_eq = @{thm expand_fun_eq} *} end diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Integ/IntDef.thy Sun May 06 21:50:17 2007 +0200 @@ -25,7 +25,7 @@ definition int :: "nat \ int" where - [code nofunc]: "int m = Abs_Integ (intrel `` {(m, 0)})" + [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})" instance int :: zero Zero_int_def: "0 \ int 0" .. @@ -53,7 +53,7 @@ "z \ w \ \x y u v. x+v \ u+y \ (x, y) \ Rep_Integ z \ (u, v) \ Rep_Integ w" less_int_def: "z < w \ z \ w \ z \ w" .. -lemmas [code nofunc] = Zero_int_def One_int_def add_int_def +lemmas [code func del] = Zero_int_def One_int_def add_int_def minus_int_def mult_int_def le_int_def less_int_def @@ -380,7 +380,7 @@ definition nat :: "int \ nat" where - [code nofunc]: "nat z = contents (\(x, y) \ Rep_Integ z. {x-y})" + [code func del]: "nat z = contents (\(x, y) \ Rep_Integ z. {x-y})" lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y" proof - diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Integ/Numeral.thy --- a/src/HOL/Integ/Numeral.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Integ/Numeral.thy Sun May 06 21:50:17 2007 +0200 @@ -34,15 +34,15 @@ definition Pls :: int where - [code nofunc]:"Pls = 0" + [code func del]:"Pls = 0" definition Min :: int where - [code nofunc]:"Min = - 1" + [code func del]:"Min = - 1" definition Bit :: "int \ bit \ int" (infixl "BIT" 90) where - [code nofunc]: "k BIT b = (case b of B0 \ 0 | B1 \ 1) + k + k" + [code func del]: "k BIT b = (case b of B0 \ 0 | B1 \ 1) + k + k" class number = type + -- {* for numeric types: nat, int, real, \dots *} fixes number_of :: "int \ 'a" @@ -70,11 +70,11 @@ definition succ :: "int \ int" where - [code nofunc]: "succ k = k + 1" + [code func del]: "succ k = k + 1" definition pred :: "int \ int" where - [code nofunc]: "pred k = k - 1" + [code func del]: "pred k = k - 1" lemmas max_number_of [simp] = max_def @@ -211,7 +211,7 @@ int_number_of_def: "number_of w \ of_int w" by intro_classes (simp only: int_number_of_def) -lemmas [code nofunc] = int_number_of_def +lemmas [code func del] = int_number_of_def lemma number_of_is_id: "number_of (k::int) = k" diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Lambda/WeakNorm.thy --- a/src/HOL/Lambda/WeakNorm.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Lambda/WeakNorm.thy Sun May 06 21:50:17 2007 +0200 @@ -573,8 +573,7 @@ CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")" *} -code_gen - type_NF nat int (SML #) +code_gen type_NF nat int in SML ML {* structure Norm = ROOT.WeakNorm; diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Library/Char_ord.thy --- a/src/HOL/Library/Char_ord.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Library/Char_ord.thy Sun May 06 21:50:17 2007 +0200 @@ -47,7 +47,7 @@ n1 < n2 \ n1 = n2 \ m1 < m2" by default (auto simp: char_less_eq_def char_less_def split: char.splits) -lemmas [code nofunc] = char_less_eq_def char_less_def +lemmas [code func del] = char_less_eq_def char_less_def instance char :: distrib_lattice "inf \ min" diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Library/EfficientNat.thy --- a/src/HOL/Library/EfficientNat.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Library/EfficientNat.thy Sun May 06 21:50:17 2007 +0200 @@ -20,7 +20,7 @@ subsection {* Logical rewrites *} text {* - A int-to-nat conversion with domain + An int-to-nat conversion restricted to non-negative ints (in contrast to @{const nat}). Note that this restriction has no logical relevance and is just a kind of proof hint -- nothing prevents you from @@ -52,7 +52,8 @@ expression: *} -lemma [code unfold, code noinline]: "nat_case \ (\f g n. if n = 0 then f else g (n - 1))" +lemma [code unfold, code inline del]: + "nat_case \ (\f g n. if n = 0 then f else g (n - 1))" proof - have rewrite: "\f g n. nat_case f g n = (if n = 0 then f else g (n - 1))" proof - @@ -66,7 +67,7 @@ lemma [code inline]: "nat_case = (\f g n. if n = 0 then f else g (nat_of_int (int n - 1)))" -proof rule+ +proof (rule ext)+ fix f g n show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))" by (cases n) (simp_all add: nat_of_int_int) @@ -81,8 +82,8 @@ by (simp add: nat_of_int_def) lemma [code func, code inline]: "1 = nat_of_int 1" by (simp add: nat_of_int_def) -lemma [code func]: "Suc n = n + 1" - by simp +lemma [code func]: "Suc n = nat_of_int (int n + 1)" + by (simp add: nat_of_int_def) lemma [code]: "m + n = nat (int m + int n)" by arith lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)" @@ -154,11 +155,6 @@ code_datatype nat_of_int -lemma [code func]: "0 = nat_of_int 0" - by (auto simp add: nat_of_int_def) -lemma [code func]: "Suc n = nat_of_int (int n + 1)" - by (auto simp add: nat_of_int_def) - code_type nat (SML "IntInf.int") (OCaml "Big'_int.big'_int") @@ -212,7 +208,7 @@ Natural numerals should be expressed using @{const nat_of_int}. *} -lemmas [code noinline] = nat_number_of_def +lemmas [code inline del] = nat_number_of_def ML {* fun nat_of_int_of_number_of thy cts = diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Library/Eval.thy --- a/src/HOL/Library/Eval.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Library/Eval.thy Sun May 06 21:50:17 2007 +0200 @@ -111,7 +111,7 @@ text {* Adaption for @{typ ml_string}s *} -lemmas [code func, code nofunc] = term_of_ml_string_def +lemmas [code func, code func del] = term_of_ml_string_def subsection {* Evaluation infrastructure *} diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Library/Graphs.thy --- a/src/HOL/Library/Graphs.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Library/Graphs.thy Sun May 06 21:50:17 2007 +0200 @@ -73,7 +73,7 @@ by auto qed -lemmas [code nofunc] = graph_plus_def +lemmas [code func del] = graph_plus_def instance graph :: (type, type) "{distrib_lattice, complete_lattice}" graph_leq_def: "G \ H \ dest_graph G \ dest_graph H" @@ -123,7 +123,7 @@ unfolding Inf_graph_def graph_leq_def by auto } qed -lemmas [code nofunc] = graph_leq_def graph_less_def +lemmas [code func del] = graph_leq_def graph_less_def inf_graph_def sup_graph_def Inf_graph_def lemma in_grplus: @@ -150,7 +150,7 @@ by (cases a) (simp add:grcomp.simps) qed -lemmas [code nofunc] = graph_mult_def +lemmas [code func del] = graph_mult_def instance graph :: (type, one) one graph_one_def: "1 == Graph { (x, 1, x) |x. True}" .. diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Library/List_lexord.thy --- a/src/HOL/Library/List_lexord.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Library/List_lexord.thy Sun May 06 21:50:17 2007 +0200 @@ -13,7 +13,7 @@ list_le_def: "(xs::('a::ord) list) \ ys \ (xs < ys \ xs = ys)" list_less_def: "(xs::('a::ord) list) < ys \ (xs, ys) \ lexord {(u,v). u < v}" .. -lemmas list_ord_defs [code nofunc] = list_less_def list_le_def +lemmas list_ord_defs [code func del] = list_less_def list_le_def instance list :: (order) order apply (intro_classes, unfold list_ord_defs) @@ -40,7 +40,7 @@ by intro_classes (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1) -lemmas [code nofunc] = inf_list_def sup_list_def +lemmas [code func del] = inf_list_def sup_list_def lemma not_less_Nil [simp]: "\ (x < [])" by (unfold list_less_def) simp diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Library/Pretty_Char_chr.thy --- a/src/HOL/Library/Pretty_Char_chr.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Library/Pretty_Char_chr.thy Sun May 06 21:50:17 2007 +0200 @@ -23,7 +23,7 @@ "char_of_nat = char_of_int o int" unfolding char_of_int_def by (simp add: expand_fun_eq) -lemmas [code nofunc] = char.recs char.cases char.size +lemmas [code func del] = char.recs char.cases char.size lemma [code func, code inline]: "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))" diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Library/Product_ord.thy --- a/src/HOL/Library/Product_ord.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Library/Product_ord.thy Sun May 06 21:50:17 2007 +0200 @@ -13,7 +13,7 @@ prod_le_def: "(x \ y) \ (fst x < fst y) \ (fst x = fst y \ snd x \ snd y)" prod_less_def: "(x < y) \ (fst x < fst y) \ (fst x = fst y \ snd x < snd y)" .. -lemmas prod_ord_defs [code nofunc] = prod_less_def prod_le_def +lemmas prod_ord_defs [code func del] = prod_less_def prod_le_def lemma [code func]: "(x1\'a\{ord, eq}, y1) \ (x2, y2) \ x1 < x2 \ x1 = x2 \ y1 \ y2" diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Library/Pure_term.thy --- a/src/HOL/Library/Pure_term.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Library/Pure_term.thy Sun May 06 21:50:17 2007 +0200 @@ -92,8 +92,8 @@ code_datatype Const App Fix Absp Bound lemmas [code func] = Bnd_Bound Abs_Absp -lemmas [code nofunc] = term.recs term.cases term.size -lemma [code func, code nofunc]: "(t1\term) = t2 \ t1 = t2" .. +lemmas [code func del] = term.recs term.cases term.size +lemma [code func, code func del]: "(t1\term) = t2 \ t1 = t2" .. code_type "typ" and "term" (SML "Term.typ" and "Term.term") diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Library/SCT_Implementation.thy --- a/src/HOL/Library/SCT_Implementation.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Library/SCT_Implementation.thy Sun May 06 21:50:17 2007 +0200 @@ -118,6 +118,6 @@ Kleene_Algebras SCT SCT_Implementation SCT -code_gen test_SCT (SML #) +code_gen test_SCT in SML end diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Nat.thy Sun May 06 21:50:17 2007 +0200 @@ -64,7 +64,7 @@ less_def: "m < n == (m, n) : pred_nat^+" le_def: "m \ (n::nat) == ~ (n < m)" .. -lemmas [code nofunc] = less_def le_def +lemmas [code func del] = less_def le_def text {* Induction *} @@ -1100,6 +1100,11 @@ subsection {* Further Arithmetic Facts Concerning the Natural Numbers *} +lemma subst_equals: + assumes 1: "t = s" and 2: "u = t" + shows "u = s" + using 2 1 by (rule trans) + use "arith_data.ML" setup arith_setup diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Set.thy --- a/src/HOL/Set.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Set.thy Sun May 06 21:50:17 2007 +0200 @@ -24,8 +24,8 @@ UNIV :: "'a set" insert :: "'a => 'a set => 'a set" Collect :: "('a => bool) => 'a set" -- "comprehension" - Int :: "'a set => 'a set => 'a set" (infixl 70) - Un :: "'a set => 'a set => 'a set" (infixl 65) + "op Int" :: "'a set => 'a set => 'a set" (infixl "Int" 70) + "op Un" :: "'a set => 'a set => 'a set" (infixl "Un" 65) UNION :: "'a set => ('a => 'b set) => 'b set" -- "general union" INTER :: "'a set => ('a => 'b set) => 'b set" -- "general intersection" Union :: "'a set set => 'a set" -- "union of a set" @@ -148,7 +148,7 @@ subset_def: "A \ B \ \x\A. x \ B" psubset_def: "A < B \ A \ B \ A \ B" .. -lemmas [code nofunc] = subset_def psubset_def +lemmas [code func del] = subset_def psubset_def abbreviation subset :: "'a set \ 'a set \ bool" where @@ -346,7 +346,7 @@ Compl_def: "- A == {x. ~x:A}" set_diff_def: "A - B == {x. x:A & ~x:B}" .. -lemmas [code nofunc] = Compl_def set_diff_def +lemmas [code func del] = Compl_def set_diff_def defs Un_def: "A Un B == {x. x:A | x:B}" @@ -2130,7 +2130,7 @@ sup_set_eq: "sup A B \ A \ B" by intro_classes (auto simp add: inf_set_eq sup_set_eq) -lemmas [code nofunc] = inf_set_eq sup_set_eq +lemmas [code func del] = inf_set_eq sup_set_eq subsection {* Basic ML bindings *} diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Wellfounded_Recursion.thy --- a/src/HOL/Wellfounded_Recursion.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/Wellfounded_Recursion.thy Sun May 06 21:50:17 2007 +0200 @@ -35,7 +35,7 @@ (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x" wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" - "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" + [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" abbreviation acyclicP :: "('a => 'a => bool) => bool" where "acyclicP r == acyclic (Collect2 r)" diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/ex/Classpackage.thy --- a/src/HOL/ex/Classpackage.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/ex/Classpackage.thy Sun May 06 21:50:17 2007 +0200 @@ -338,7 +338,6 @@ definition "x2 = X (1::int) 2 3" definition "y2 = Y (1::int) 2 3" -code_gen "op \" \ inv X Y -code_gen x1 x2 y2 (SML #) (OCaml -) (Haskell -) +code_gen x1 x2 y2 in SML in OCaml file - in Haskell file - end diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/ex/Codegenerator.thy --- a/src/HOL/ex/Codegenerator.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/ex/Codegenerator.thy Sun May 06 21:50:17 2007 +0200 @@ -8,7 +8,7 @@ imports ExecutableContent begin -code_gen "*" (SML) (Haskell) (OCaml) -code_gen (SML #) (Haskell -) (OCaml -) +code_gen "*" in SML in OCaml file - in OCaml file - +code_gen in SML in OCaml file - in OCaml file - end \ No newline at end of file diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/ex/Codegenerator_Rat.thy --- a/src/HOL/ex/Codegenerator_Rat.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/ex/Codegenerator_Rat.thy Sun May 06 21:50:17 2007 +0200 @@ -29,7 +29,7 @@ definition "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)" -code_gen foobar (SML #) (OCaml -) (Haskell -) +code_gen foobar in SML in OCaml file - in Haskell file - ML {* ROOT.Codegenerator_Rat.foobar *} code_module Foo diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/ex/NormalForm.thy --- a/src/HOL/ex/NormalForm.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/ex/NormalForm.thy Sun May 06 21:50:17 2007 +0200 @@ -13,7 +13,7 @@ lemma "p \ True" by normalization declare disj_assoc [code func] lemma "((P | Q) | R) = (P | (Q | R))" by normalization -declare disj_assoc [code nofunc] +declare disj_assoc [code func del] lemma "0 + (n::nat) = n" by normalization lemma "0 + Suc n = Suc n" by normalization lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/ex/Random.thy --- a/src/HOL/ex/Random.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/ex/Random.thy Sun May 06 21:50:17 2007 +0200 @@ -13,7 +13,7 @@ where pick_undef: "pick [] n = undefined" | pick_simp: "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" -lemmas [code nofunc] = pick_undef +lemmas [code func del] = pick_undef typedecl randseed @@ -180,7 +180,4 @@ code_const run_random (SML "case _ (Random.seed ()) of (x, '_) => x") -code_gen select select_weight - (SML #) - end diff -r 91c05f4b509e -r 5f9138bcb3d7 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Sun May 06 21:49:44 2007 +0200 +++ b/src/Pure/Tools/codegen_package.ML Sun May 06 21:50:17 2007 +0200 @@ -7,8 +7,6 @@ signature CODEGEN_PACKAGE = sig - include BASIC_CODEGEN_THINGOL; - val codegen_term: theory -> term -> iterm; val eval_term: theory -> (string (*reference name!*) * 'a option ref) * term -> 'a; val satisfies_ref: bool option ref; val satisfies: theory -> term -> string list -> bool; @@ -605,9 +603,9 @@ fun code raw_cs seris thy = let - val seris' = map (fn (target, args as _ :: _) => - (target, SOME (CodegenSerializer.get_serializer thy target args CodegenNames.labelled_name)) - | (target, []) => (CodegenSerializer.assert_serializer thy target, NONE)) seris; + val seris' = map (fn ((target, file), args) => + (target, SOME (CodegenSerializer.get_serializer thy target file args + CodegenNames.labelled_name))) seris; val targets = case map fst seris' of [] => NONE | xs => SOME xs; val cs = CodegenConsts.read_const_exprs thy (filter_generatable thy targets) raw_cs; @@ -632,13 +630,12 @@ fun code_deps_cmd thy = code_deps thy o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy); -val code_exprP = ( - (Scan.repeat P.term - -- Scan.repeat (P.$$$ "(" |-- - P.name -- P.arguments - --| P.$$$ ")")) - >> (fn (raw_cs, seris) => code raw_cs seris) - ); +val code_exprP = + (Scan.repeat P.term + -- Scan.repeat (P.$$$ "in" |-- P.name + -- Scan.option (P.$$$ "file" |-- P.name) + -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") [] + ) >> (fn (raw_cs, seris) => code raw_cs seris)); val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) = ("code_gen", "code_abstype", "code_axioms", "code_thms", "code_deps"); @@ -646,7 +643,7 @@ in val codeP = - OuterSyntax.improper_command codeK "generate and serialize executable code for constants" + OuterSyntax.improper_command codeK "generate executable code for constants" K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); fun codegen_command thy cmd = diff -r 91c05f4b509e -r 5f9138bcb3d7 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Sun May 06 21:49:44 2007 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Sun May 06 21:50:17 2007 +0200 @@ -31,7 +31,7 @@ type serializer; val add_serializer: string * serializer -> theory -> theory; - val get_serializer: theory -> string -> Args.T list -> (theory -> string -> string) + val get_serializer: theory -> string -> string option -> Args.T list -> (theory -> string -> string) -> string list option -> CodegenThingol.code -> unit; val assert_serializer: theory -> string -> string; @@ -1026,16 +1026,15 @@ (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes)) in output p end; -val isar_seri_sml = +fun isar_seri_sml file = let - fun output_file file = File.write (Path.explode file) o code_output; - val output_diag = writeln o code_output; - val output_internal = use_text "generated code" Output.ml_output false o code_output; + val output = case file + of NONE => use_text "generated code" Output.ml_output false o code_output + | SOME "-" => writeln o code_output + | SOME file => File.write (Path.explode file) o code_output; in - parse_args ((Args.$$$ "-" >> K output_diag - || Args.$$$ "#" >> K output_internal - || Args.name >> output_file) - >> (fn output => seri_ml pr_sml pr_sml_modl ML_Syntax.reserved output)) + parse_args (Scan.succeed ()) + #> (fn () => seri_ml pr_sml pr_sml_modl ML_Syntax.reserved output) end; val reserved_ocaml = Name.make_context ["and", "as", "assert", "begin", "class", @@ -1046,14 +1045,17 @@ "sig", "struct", "then", "to", "true", "try", "type", "val", "virtual", "when", "while", "with", "mod"]; -val isar_seri_ocaml = +fun isar_seri_ocaml file = let + val output = case file + of NONE => error "OCaml: no internal compilation" + | SOME "-" => writeln o code_output + | SOME file => File.write (Path.explode file) o code_output; fun output_file file = File.write (Path.explode file) o code_output; val output_diag = writeln o code_output; in - parse_args ((Args.$$$ "-" >> K output_diag - || Args.name >> output_file) - >> (fn output => seri_ml pr_ocaml pr_ocaml_modl reserved_ocaml output)) + parse_args (Scan.succeed ()) + #> (fn () => seri_ml pr_ocaml pr_ocaml_modl reserved_ocaml output) end; @@ -1425,12 +1427,18 @@ end; in Symtab.fold (fn modl => fn () => seri_module modl) code' () end; -val isar_seri_haskell = - parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name) - -- Scan.optional (Args.$$$ "string_classes" >> K true) false - -- (Args.$$$ "-" >> K NONE || Args.name >> SOME) - >> (fn ((module_prefix, string_classes), destination) => - seri_haskell module_prefix (Option.map Path.explode destination) string_classes)); +fun isar_seri_haskell file = + let + val destination = case file + of NONE => error ("Haskell: no internal compilation") + | SOME "-" => NONE + | SOME file => SOME (Path.explode file) + in + parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name) + -- Scan.optional (Args.$$$ "string_classes" >> K true) false + >> (fn (module_prefix, string_classes) => + seri_haskell module_prefix destination string_classes)) + end; (** diagnosis serializer **) @@ -1494,7 +1502,9 @@ Symtab.merge (op =) (prolog1, prolog2) ); -type serializer = Args.T list +type serializer = + string option + -> Args.T list -> (string -> string) -> string list -> (string -> string option) @@ -1581,10 +1591,10 @@ #> add_serializer (target_SML, isar_seri_sml) #> add_serializer (target_OCaml, isar_seri_ocaml) #> add_serializer (target_Haskell, isar_seri_haskell) - #> add_serializer (target_diag, (fn _ => fn _ => seri_diagnosis)) + #> add_serializer (target_diag, (fn _ => fn _ => fn _ => seri_diagnosis)) ); -fun get_serializer thy target args labelled_name = fn cs => +fun get_serializer thy target file args labelled_name = fn cs => let val data = case Symtab.lookup (CodegenSerializerData.get thy) target of SOME data => data @@ -1597,7 +1607,7 @@ else CodegenThingol.project_code (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs; in - project #> seri args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog) + project #> seri file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog) (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const) end; diff -r 91c05f4b509e -r 5f9138bcb3d7 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Sun May 06 21:49:44 2007 +0200 +++ b/src/Pure/codegen.ML Sun May 06 21:50:17 2007 +0200 @@ -366,17 +366,19 @@ (Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]); local + fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); fun add_simple_attribute (name, f) = - (add_attribute name o (Scan.succeed o Thm.declaration_attribute)) - (fn th => Context.mapping (f th) I); + add_attribute name (Scan.succeed (mk_attribute f)); + fun add_del_attribute (name, (add, del)) = + add_attribute name (Args.del |-- Scan.succeed (mk_attribute del) + || Scan.succeed (mk_attribute add)) in - val _ = map (Context.add_setup o add_simple_attribute) [ - ("func", CodeData.add_func true), - ("nofunc", CodeData.del_func), - ("unfold", (fn thm => add_unfold thm #> CodeData.add_inline thm)), - ("inline", CodeData.add_inline), - ("noinline", CodeData.del_inline) - ] + val _ = Context.add_setup (add_simple_attribute ("unfold", + fn thm => add_unfold thm #> CodeData.add_inline thm)); + val _ = map (Context.add_setup o add_del_attribute) [ + ("func", (CodeData.add_func true, CodeData.del_func)), + ("inline", (CodeData.add_inline, CodeData.del_inline)) + ]; end; (*local*)