--- 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.
--- 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}
--- 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 "\<CODEGEN>"} 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 \<Rightarrow> '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 \<Rightarrow> 1 | Suc m \<Rightarrow> 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 "\<PRINTCLASSES>"}
+ 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 \<in> set xs \<longleftrightarrow> 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 \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
+
+text {*
+ \item eliminating superfluous constants:
*}
-lemma [code inline]:
- "xs = [] \<longleftrightarrow> 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 = [] \<longleftrightarrow> 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 "\<PRINTCODESETUP>"} 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 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> 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 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
"(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
unfolding less_prod_def less_eq_prod_def by simp_all
@@ -653,7 +656,7 @@
*}
code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> 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>" 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 \<and>"
(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]: "\<Union>set xs = foldr (op \<union>) xs {}" by (induct xs) simp_all
-code_gen "{}" insert "op \<in>" "op \<union>" "Union" (*<*)(SML #)(*>*)(SML "examples/set_list.ML")
+code_gen "{}" insert "op \<in>" "op \<union>" "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}
--- 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}
--- 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}
--- 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 =" \<equiv> "(==)")
@@ -114,16 +114,10 @@
instance bool :: eq ..
lemma [code func]:
- "True = P \<longleftrightarrow> P" by simp
-
-lemma [code func]:
- "False = P \<longleftrightarrow> \<not> P" by simp
-
-lemma [code func]:
- "P = True \<longleftrightarrow> P" by simp
-
-lemma [code func]:
- "P = False \<longleftrightarrow> \<not> P" by simp
+ shows "True = P \<longleftrightarrow> P"
+ and "False = P \<longleftrightarrow> \<not> P"
+ and "P = True \<longleftrightarrow> P"
+ and "P = False \<longleftrightarrow> \<not> P" by simp_all
code_type bool
(SML "bool")
@@ -211,7 +205,7 @@
definition
if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> '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"
--- 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\<Colon>nat) n = (m div n, m mod n)"
lemma divmod_zero [code]: "divmod m 0 = (0, m)"
--- 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 \<equiv> arbitrary_LT'
arbitrary_TT \<equiv> arbitrary_TT'
-code_gen higman_idx (SML #)
+code_gen higman_idx in SML
ML {*
local
--- 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)"
--- 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
--- 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 \<Rightarrow> 'a"
- assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
- assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
+ fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90)
+ assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
+ assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
definition
- Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a" where
+ Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a"
+where
"Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
-theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x <= Sup A"
+theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x \<le> Sup A"
by (auto simp: Sup_def intro: Inf_greatest)
-theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
+theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> 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 = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
apply (rule order_antisym)
@@ -221,7 +222,7 @@
Inf_set_def: "Inf S \<equiv> \<Inter>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 = \<Union>S"
apply (rule subset_antisym)
--- 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 \<le> g \<equiv> \<forall>x. f x \<le> g x"
less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> 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: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> 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 \<circ>"
@@ -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
--- 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 \<Rightarrow> 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 \<equiv> int 0" ..
@@ -53,7 +53,7 @@
"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"
less_int_def: "z < w \<equiv> z \<le> w \<and> z \<noteq> 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 \<Rightarrow> nat"
where
- [code nofunc]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
+ [code func del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
proof -
--- 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 \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
- [code nofunc]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+ [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
class number = type + -- {* for numeric types: nat, int, real, \dots *}
fixes number_of :: "int \<Rightarrow> 'a"
@@ -70,11 +70,11 @@
definition
succ :: "int \<Rightarrow> int" where
- [code nofunc]: "succ k = k + 1"
+ [code func del]: "succ k = k + 1"
definition
pred :: "int \<Rightarrow> 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 \<equiv> 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"
--- 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;
--- 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 \<or> n1 = n2 \<and> 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 \<equiv> min"
--- 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 \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
+lemma [code unfold, code inline del]:
+ "nat_case \<equiv> (\<lambda>f g n. if n = 0 then f else g (n - 1))"
proof -
have rewrite: "\<And>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 = (\<lambda>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 =
--- 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 *}
--- 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 \<le> H \<equiv> dest_graph G \<subseteq> 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}" ..
--- 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) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> 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]: "\<not> (x < [])"
by (unfold list_less_def) simp
--- 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))"
--- 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 \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> 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\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
--- 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\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
+lemmas [code func del] = term.recs term.cases term.size
+lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
code_type "typ" and "term"
(SML "Term.typ" and "Term.term")
--- 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
--- 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 \<le> (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
--- 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 \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
-lemmas [code nofunc] = subset_def psubset_def
+lemmas [code func del] = subset_def psubset_def
abbreviation
subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> 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 \<equiv> A \<union> 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 *}
--- 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)"
--- 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 \<otimes>" \<one> 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
--- 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
--- 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
--- 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 \<longrightarrow> 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
--- 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
--- 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 =
--- 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;
--- 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*)