--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Mon Aug 20 18:07:49 2007 +0200
@@ -504,7 +504,7 @@
\noindent This maps to Haskell as:
*}
-code_gen example in Haskell to Classes file "code_examples/"
+export_code example in Haskell to Classes file "code_examples/"
(* NOTE: you may use Haskell only once in this document, otherwise
you have to work in distinct subdirectories *)
@@ -514,7 +514,7 @@
\noindent The whole code in SML with explicit dictionary passing:
*}
-code_gen example (*<*)in SML to Classes(*>*)in SML to Classes file "code_examples/classes.ML"
+export_code example (*<*)in SML to Classes(*>*)in SML to Classes file "code_examples/classes.ML"
text {*
\lstsml{Thy/code_examples/classes.ML}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Mon Aug 20 18:07:49 2007 +0200
@@ -146,7 +146,7 @@
\noindent Then we generate code
*}
-code_gen example (*<*)in SML(*>*)in SML file "examples/tree.ML"
+export_code example (*<*)in SML(*>*)in SML file "examples/tree.ML"
text {*
\noindent which looks like:
@@ -224,10 +224,10 @@
\noindent This executable specification is now turned to SML code:
*}
-code_gen fac (*<*)in SML(*>*)in SML file "examples/fac.ML"
+export_code fac (*<*)in SML(*>*)in SML file "examples/fac.ML"
text {*
- \noindent The @{text "\<CODEGEN>"} command takes a space-separated list of
+ \noindent The @{text "\<EXPORTCODE>"} command takes a space-separated list of
constants together with \qn{serialization directives}
These start with a \qn{target language}
identifier, followed by a file specification
@@ -262,7 +262,7 @@
pick_some :: "'a list \<Rightarrow> 'a" where
"pick_some = hd"
(*>*)
-code_gen pick_some in SML file "examples/fail_const.ML"
+export_code pick_some in SML file "examples/fail_const.ML"
text {* \noindent will fail. *}
@@ -306,7 +306,7 @@
"pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
by simp
-code_gen pick (*<*)in SML(*>*) in SML file "examples/pick1.ML"
+export_code pick (*<*)in SML(*>*) in SML file "examples/pick1.ML"
text {*
\noindent This theorem now is used for generating code:
@@ -319,7 +319,7 @@
lemmas [code func del] = pick.simps
-code_gen pick (*<*)in SML(*>*) in SML file "examples/pick2.ML"
+export_code pick (*<*)in SML(*>*) in SML file "examples/pick2.ML"
text {*
\lstsml{Thy/examples/pick2.ML}
@@ -335,7 +335,7 @@
"fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)"
by (cases n) simp_all
-code_gen fac (*<*)in SML(*>*)in SML file "examples/fac_case.ML"
+export_code fac (*<*)in SML(*>*)in SML file "examples/fac_case.ML"
text {*
\lstsml{Thy/examples/fac_case.ML}
@@ -397,7 +397,7 @@
the file system, with root directory given as file specification.
*}
-code_gen dummy in Haskell file "examples/"
+export_code dummy in Haskell file "examples/"
(* NOTE: you may use Haskell only once in this document, otherwise
you have to work in distinct subdirectories *)
@@ -410,7 +410,7 @@
The whole code in SML with explicit dictionary passing:
*}
-code_gen dummy (*<*)in SML(*>*)in SML file "examples/class.ML"
+export_code dummy (*<*)in SML(*>*)in SML file "examples/class.ML"
text {*
\lstsml{Thy/examples/class.ML}
@@ -420,7 +420,7 @@
\noindent or in OCaml:
*}
-code_gen dummy in OCaml file "examples/class.ocaml"
+export_code dummy in OCaml file "examples/class.ocaml"
text {*
\lstsml{Thy/examples/class.ocaml}
@@ -596,7 +596,7 @@
performs an explicit equality check.
*}
-code_gen collect_duplicates (*<*)in SML(*>*)in SML file "examples/collect_duplicates.ML"
+export_code collect_duplicates (*<*)in SML(*>*)in SML file "examples/collect_duplicates.ML"
text {*
\lstsml{Thy/examples/collect_duplicates.ML}
@@ -668,7 +668,7 @@
\noindent Then code generation succeeds:
*}
-code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+export_code "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
(*<*)in SML(*>*)in SML file "examples/lexicographic.ML"
text {*
@@ -722,7 +722,7 @@
does not depend on instance @{text "monotype \<Colon> eq"}:
*}
-code_gen "op = :: monotype \<Rightarrow> monotype \<Rightarrow> bool"
+export_code "op = :: monotype \<Rightarrow> monotype \<Rightarrow> bool"
(*<*)in SML(*>*)in SML file "examples/monotype.ML"
text {*
@@ -771,7 +771,7 @@
code_const %tt True and False and "op \<and>" and Not
(SML and and and)
(*>*)
-code_gen in_interval (*<*)in SML(*>*)in SML file "examples/bool_literal.ML"
+export_code in_interval (*<*)in SML(*>*)in SML file "examples/bool_literal.ML"
text {*
\lstsml{Thy/examples/bool_literal.ML}
@@ -804,7 +804,7 @@
for the type constructor's (the constant's) arguments.
*}
-code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_mlbool.ML"
+export_code in_interval (*<*)in SML(*>*) in SML file "examples/bool_mlbool.ML"
text {*
\lstsml{Thy/examples/bool_mlbool.ML}
@@ -820,7 +820,7 @@
code_const %tt "op \<and>"
(SML infixl 1 "andalso")
-code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_infix.ML"
+export_code in_interval (*<*)in SML(*>*) in SML file "examples/bool_infix.ML"
text {*
\lstsml{Thy/examples/bool_infix.ML}
@@ -949,7 +949,7 @@
lemma [code func]: "\<Union>set xs = foldr (op \<union>) xs {}" by (induct xs) simp_all
-code_gen "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML"
+export_code "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML"
text {*
\lstsml{Thy/examples/set_list.ML}
@@ -997,7 +997,7 @@
hid away the details from the user. Anyway, caching
reaches the surface by using a slightly more general form
of the @{text "\<CODETHMS>"}, @{text "\<CODEDEPS>"}
- and @{text "\<CODEGEN>"} commands: the list of constants
+ and @{text "\<EXPORTCODE>"} commands: the list of constants
may be omitted. Then, all constants with code theorems
in the current cache are referred to.
*}
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Mon Aug 20 18:07:31 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Mon Aug 20 18:07:49 2007 +0200
@@ -32,7 +32,7 @@
\newcommand{\isasymSHOW}{\cmd{show}}
\newcommand{\isasymNOTE}{\cmd{note}}
\newcommand{\isasymIN}{\cmd{in}}
-\newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
+\newcommand{\isasymEXPORTCODE}{\cmd{export\_code}}
\newcommand{\isasymCODEDATATYPE}{\cmd{code\_datatype}}
\newcommand{\isasymCODECONST}{\cmd{code\_const}}
\newcommand{\isasymCODETYPE}{\cmd{code\_type}}
--- a/doc-src/IsarRef/logics.tex Mon Aug 20 18:07:31 2007 +0200
+++ b/doc-src/IsarRef/logics.tex Mon Aug 20 18:07:49 2007 +0200
@@ -776,7 +776,7 @@
\indexisaratt{code inline}
\begin{matharray}{rcl}
- \isarcmd{code_gen}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{export_code}^* & : & \isarkeep{theory~|~proof} \\
\isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\
\isarcmd{code_deps}^* & : & \isarkeep{theory~|~proof} \\
\isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\
@@ -795,7 +795,7 @@
\end{matharray}
\begin{rail}
-'code\_gen' ( constexpr + ) ? \\
+'export\_code' ( constexpr + ) ? \\
( ( 'in' target ( 'module_name' string ) ? ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
'code\_thms' ( constexpr + ) ?;
@@ -849,7 +849,7 @@
\begin{descr}
-\item [$\isarcmd{code_gen}$] is the canonical interface for generating and
+\item [$\isarcmd{export_code}$] 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 currently cached code is serialized. If no serialization instruction
--- a/src/HOL/Complex/ex/MIR.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Mon Aug 20 18:07:49 2007 +0200
@@ -5772,10 +5772,10 @@
definition
"test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
-code_gen mircfrqe mirlfrqe test1 test2 test3 test4 test5
+export_code mircfrqe mirlfrqe test1 test2 test3 test4 test5
in SML module_name Mir
-(*code_gen mircfrqe mirlfrqe
+(*export_code mircfrqe mirlfrqe
in SML module_name Mir file "raw_mir.ML"*)
ML "set Toplevel.timing"
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Mon Aug 20 18:07:49 2007 +0200
@@ -1986,7 +1986,7 @@
"ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
(E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
-code_gen linrqe ferrack_test in SML module_name Ferrack
+export_code linrqe ferrack_test in SML module_name Ferrack
(*code_module Ferrack
contains
--- a/src/HOL/Extraction/Higman.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy Mon Aug 20 18:07:49 2007 +0200
@@ -427,7 +427,7 @@
code_datatype L0 L1 arbitrary_LT
code_datatype T0 T1 T2 arbitrary_TT
-code_gen higman_idx in SML module_name Higman
+export_code higman_idx in SML module_name Higman
ML {*
local
--- a/src/HOL/Extraction/Pigeonhole.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy Mon Aug 20 18:07:49 2007 +0200
@@ -309,7 +309,7 @@
test' = test'
test'' = test''
-code_gen test test' test'' in SML module_name PH2
+export_code test test' test'' in SML module_name PH2
ML "timeit (PH1.test 10)"
ML "timeit (PH2.test 10)"
--- a/src/HOL/Extraction/QuotRem.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/Extraction/QuotRem.thy Mon Aug 20 18:07:49 2007 +0200
@@ -49,6 +49,6 @@
contains
test = "division 9 2"
-code_gen division in SML
+export_code division in SML
end
--- a/src/HOL/Lambda/WeakNorm.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Mon Aug 20 18:07:49 2007 +0200
@@ -581,7 +581,7 @@
int :: "nat \<Rightarrow> int" where
"int \<equiv> of_nat"
-code_gen type_NF nat int in SML module_name Norm
+export_code type_NF nat int in SML module_name Norm
ML {*
val nat_of_int = Norm.nat o IntInf.fromInt;
--- a/src/HOL/Library/SCT_Implementation.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/Library/SCT_Implementation.thy Mon Aug 20 18:07:49 2007 +0200
@@ -190,6 +190,6 @@
Kleene_Algebras SCT
SCT_Implementation SCT
-code_gen test_SCT in SML
+export_code test_SCT in SML
end
--- a/src/HOL/ex/Classpackage.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy Mon Aug 20 18:07:49 2007 +0200
@@ -342,7 +342,7 @@
definition "x2 = X (1::int) 2 3"
definition "y2 = Y (1::int) 2 3"
-code_gen x1 x2 y2 in SML module_name Classpackage
+export_code x1 x2 y2 in SML module_name Classpackage
in OCaml file -
in Haskell file -
--- a/src/HOL/ex/Codegenerator.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/ex/Codegenerator.thy Mon Aug 20 18:07:49 2007 +0200
@@ -8,7 +8,7 @@
imports ExecutableContent
begin
-code_gen "*" in SML module_name CodegenTest
+export_code "*" in SML module_name CodegenTest
in OCaml file -
in Haskell file -
--- a/src/HOL/ex/Codegenerator_Pretty.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/ex/Codegenerator_Pretty.thy Mon Aug 20 18:07:49 2007 +0200
@@ -49,7 +49,7 @@
definition
"foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
-code_gen foobar foobar' in SML module_name Foo
+export_code foobar foobar' in SML module_name Foo
in OCaml file -
in Haskell file -
ML {* (Foo.foobar, Foo.foobar') *}
--- a/src/HOL/ex/Reflected_Presburger.thy Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Mon Aug 20 18:07:49 2007 +0200
@@ -1937,8 +1937,8 @@
(Bound 2))))))))"
code_reserved SML oo
-code_gen pa cooper_test in SML module_name GeneratedCooper
-(*code_gen pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
+export_code pa cooper_test in SML module_name GeneratedCooper
+(*export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
ML {* GeneratedCooper.cooper_test () *}
use "coopereif.ML"
--- a/src/Tools/code/code_package.ML Mon Aug 20 18:07:31 2007 +0200
+++ b/src/Tools/code/code_package.ML Mon Aug 20 18:07:49 2007 +0200
@@ -626,7 +626,7 @@
val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) =
- ("code_gen", "code_abstype", "code_axioms", "code_thms", "code_deps");
+ ("export_code", "code_abstype", "code_axioms", "code_thms", "code_deps");
in