# HG changeset patch # User haftmann # Date 1187626069 -7200 # Node ID c708ea5b109a83bdfa5b1a9bb5e24e5281a6d225 # Parent 245ff8661b8cb06bb13269b81a04bbcdf01464b8 renamed code_gen to export_code diff -r 245ff8661b8c -r c708ea5b109a doc-src/IsarAdvanced/Classes/Thy/Classes.thy --- 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} diff -r 245ff8661b8c -r c708ea5b109a doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- 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 "\"} command takes a space-separated list of + \noindent The @{text "\"} 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 \ '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 \ 1 | Suc m \ 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 \ \ 'a\{eq, ord} \ 'b\ord \ 'a \ 'b \ bool" +export_code "op \ \ 'a\{eq, ord} \ 'b\ord \ 'a \ 'b \ bool" (*<*)in SML(*>*)in SML file "examples/lexicographic.ML" text {* @@ -722,7 +722,7 @@ does not depend on instance @{text "monotype \ eq"}: *} -code_gen "op = :: monotype \ monotype \ bool" +export_code "op = :: monotype \ monotype \ bool" (*<*)in SML(*>*)in SML file "examples/monotype.ML" text {* @@ -771,7 +771,7 @@ code_const %tt True and False and "op \" 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 \" (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]: "\set xs = foldr (op \) xs {}" by (induct xs) simp_all -code_gen "{}" insert "op \" "op \" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML" +export_code "{}" insert "op \" "op \" "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 "\"}, @{text "\"} - and @{text "\"} commands: the list of constants + and @{text "\"} commands: the list of constants may be omitted. Then, all constants with code theorems in the current cache are referred to. *} diff -r 245ff8661b8c -r c708ea5b109a doc-src/IsarAdvanced/Codegen/codegen.tex --- 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}} diff -r 245ff8661b8c -r c708ea5b109a doc-src/IsarRef/logics.tex --- 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 diff -r 245ff8661b8c -r c708ea5b109a src/HOL/Complex/ex/MIR.thy --- 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\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" diff -r 245ff8661b8c -r c708ea5b109a src/HOL/Complex/ex/ReflectedFerrack.thy --- 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 diff -r 245ff8661b8c -r c708ea5b109a src/HOL/Extraction/Higman.thy --- 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 diff -r 245ff8661b8c -r c708ea5b109a src/HOL/Extraction/Pigeonhole.thy --- 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)" diff -r 245ff8661b8c -r c708ea5b109a src/HOL/Extraction/QuotRem.thy --- 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 diff -r 245ff8661b8c -r c708ea5b109a src/HOL/Lambda/WeakNorm.thy --- 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 \ int" where "int \ 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; diff -r 245ff8661b8c -r c708ea5b109a src/HOL/Library/SCT_Implementation.thy --- 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 diff -r 245ff8661b8c -r c708ea5b109a src/HOL/ex/Classpackage.thy --- 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 - diff -r 245ff8661b8c -r c708ea5b109a src/HOL/ex/Codegenerator.thy --- 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 - diff -r 245ff8661b8c -r c708ea5b109a src/HOL/ex/Codegenerator_Pretty.thy --- 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') *} diff -r 245ff8661b8c -r c708ea5b109a src/HOL/ex/Reflected_Presburger.thy --- 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" diff -r 245ff8661b8c -r c708ea5b109a src/Tools/code/code_package.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