renamed code_gen to export_code
authorhaftmann
Mon Aug 20 18:07:49 2007 +0200 (2007-08-20)
changeset 24348c708ea5b109a
parent 24347 245ff8661b8c
child 24349 0dd8782fb02d
renamed code_gen to export_code
doc-src/IsarAdvanced/Classes/Thy/Classes.thy
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
doc-src/IsarAdvanced/Codegen/codegen.tex
doc-src/IsarRef/logics.tex
src/HOL/Complex/ex/MIR.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Extraction/Higman.thy
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Extraction/QuotRem.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/SCT_Implementation.thy
src/HOL/ex/Classpackage.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/Codegenerator_Pretty.thy
src/HOL/ex/Reflected_Presburger.thy
src/Tools/code/code_package.ML
     1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Mon Aug 20 18:07:31 2007 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Mon Aug 20 18:07:49 2007 +0200
     1.3 @@ -504,7 +504,7 @@
     1.4    \noindent This maps to Haskell as:
     1.5  *}
     1.6  
     1.7 -code_gen example in Haskell to Classes file "code_examples/"
     1.8 +export_code example in Haskell to Classes file "code_examples/"
     1.9    (* NOTE: you may use Haskell only once in this document, otherwise
    1.10    you have to work in distinct subdirectories *)
    1.11  
    1.12 @@ -514,7 +514,7 @@
    1.13    \noindent The whole code in SML with explicit dictionary passing:
    1.14  *}
    1.15  
    1.16 -code_gen example (*<*)in SML to Classes(*>*)in SML to Classes file "code_examples/classes.ML"
    1.17 +export_code example (*<*)in SML to Classes(*>*)in SML to Classes file "code_examples/classes.ML"
    1.18  
    1.19  text {*
    1.20    \lstsml{Thy/code_examples/classes.ML}
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Aug 20 18:07:31 2007 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Aug 20 18:07:49 2007 +0200
     2.3 @@ -146,7 +146,7 @@
     2.4    \noindent Then we generate code
     2.5  *}
     2.6  
     2.7 -code_gen example (*<*)in SML(*>*)in SML file "examples/tree.ML"
     2.8 +export_code example (*<*)in SML(*>*)in SML file "examples/tree.ML"
     2.9  
    2.10  text {*
    2.11    \noindent which looks like:
    2.12 @@ -224,10 +224,10 @@
    2.13    \noindent This executable specification is now turned to SML code:
    2.14  *}
    2.15  
    2.16 -code_gen fac (*<*)in SML(*>*)in SML file "examples/fac.ML"
    2.17 +export_code fac (*<*)in SML(*>*)in SML file "examples/fac.ML"
    2.18  
    2.19  text {*
    2.20 -  \noindent  The @{text "\<CODEGEN>"} command takes a space-separated list of
    2.21 +  \noindent  The @{text "\<EXPORTCODE>"} command takes a space-separated list of
    2.22    constants together with \qn{serialization directives}
    2.23    These start with a \qn{target language}
    2.24    identifier, followed by a file specification
    2.25 @@ -262,7 +262,7 @@
    2.26    pick_some :: "'a list \<Rightarrow> 'a" where
    2.27    "pick_some = hd"
    2.28  (*>*)
    2.29 -code_gen pick_some in SML file "examples/fail_const.ML"
    2.30 +export_code pick_some in SML file "examples/fail_const.ML"
    2.31  
    2.32  text {* \noindent will fail. *}
    2.33  
    2.34 @@ -306,7 +306,7 @@
    2.35    "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
    2.36    by simp
    2.37  
    2.38 -code_gen pick (*<*)in SML(*>*) in SML file "examples/pick1.ML"
    2.39 +export_code pick (*<*)in SML(*>*) in SML file "examples/pick1.ML"
    2.40  
    2.41  text {*
    2.42    \noindent This theorem now is used for generating code:
    2.43 @@ -319,7 +319,7 @@
    2.44  
    2.45  lemmas [code func del] = pick.simps 
    2.46  
    2.47 -code_gen pick (*<*)in SML(*>*) in SML file "examples/pick2.ML"
    2.48 +export_code pick (*<*)in SML(*>*) in SML file "examples/pick2.ML"
    2.49  
    2.50  text {*
    2.51    \lstsml{Thy/examples/pick2.ML}
    2.52 @@ -335,7 +335,7 @@
    2.53    "fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)"
    2.54    by (cases n) simp_all
    2.55  
    2.56 -code_gen fac (*<*)in SML(*>*)in SML file "examples/fac_case.ML"
    2.57 +export_code fac (*<*)in SML(*>*)in SML file "examples/fac_case.ML"
    2.58  
    2.59  text {*
    2.60    \lstsml{Thy/examples/fac_case.ML}
    2.61 @@ -397,7 +397,7 @@
    2.62    the file system, with root directory given as file specification.
    2.63  *}
    2.64  
    2.65 -code_gen dummy in Haskell file "examples/"
    2.66 +export_code dummy in Haskell file "examples/"
    2.67    (* NOTE: you may use Haskell only once in this document, otherwise
    2.68    you have to work in distinct subdirectories *)
    2.69  
    2.70 @@ -410,7 +410,7 @@
    2.71    The whole code in SML with explicit dictionary passing:
    2.72  *}
    2.73  
    2.74 -code_gen dummy (*<*)in SML(*>*)in SML file "examples/class.ML"
    2.75 +export_code dummy (*<*)in SML(*>*)in SML file "examples/class.ML"
    2.76  
    2.77  text {*
    2.78    \lstsml{Thy/examples/class.ML}
    2.79 @@ -420,7 +420,7 @@
    2.80    \noindent or in OCaml:
    2.81  *}
    2.82  
    2.83 -code_gen dummy in OCaml file "examples/class.ocaml"
    2.84 +export_code dummy in OCaml file "examples/class.ocaml"
    2.85  
    2.86  text {*
    2.87    \lstsml{Thy/examples/class.ocaml}
    2.88 @@ -596,7 +596,7 @@
    2.89    performs an explicit equality check.
    2.90  *}
    2.91  
    2.92 -code_gen collect_duplicates (*<*)in SML(*>*)in SML file "examples/collect_duplicates.ML"
    2.93 +export_code collect_duplicates (*<*)in SML(*>*)in SML file "examples/collect_duplicates.ML"
    2.94  
    2.95  text {*
    2.96    \lstsml{Thy/examples/collect_duplicates.ML}
    2.97 @@ -668,7 +668,7 @@
    2.98    \noindent Then code generation succeeds:
    2.99  *}
   2.100  
   2.101 -code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   2.102 +export_code "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   2.103    (*<*)in SML(*>*)in SML file "examples/lexicographic.ML"
   2.104  
   2.105  text {*
   2.106 @@ -722,7 +722,7 @@
   2.107    does not depend on instance @{text "monotype \<Colon> eq"}:
   2.108  *}
   2.109  
   2.110 -code_gen "op = :: monotype \<Rightarrow> monotype \<Rightarrow> bool"
   2.111 +export_code "op = :: monotype \<Rightarrow> monotype \<Rightarrow> bool"
   2.112    (*<*)in SML(*>*)in SML file "examples/monotype.ML"
   2.113  
   2.114  text {*
   2.115 @@ -771,7 +771,7 @@
   2.116  code_const %tt True and False and "op \<and>" and Not
   2.117    (SML and and and)
   2.118  (*>*)
   2.119 -code_gen in_interval (*<*)in SML(*>*)in SML file "examples/bool_literal.ML"
   2.120 +export_code in_interval (*<*)in SML(*>*)in SML file "examples/bool_literal.ML"
   2.121  
   2.122  text {*
   2.123    \lstsml{Thy/examples/bool_literal.ML}
   2.124 @@ -804,7 +804,7 @@
   2.125    for the type constructor's (the constant's) arguments.
   2.126  *}
   2.127  
   2.128 -code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_mlbool.ML"
   2.129 +export_code in_interval (*<*)in SML(*>*) in SML file "examples/bool_mlbool.ML"
   2.130  
   2.131  text {*
   2.132    \lstsml{Thy/examples/bool_mlbool.ML}
   2.133 @@ -820,7 +820,7 @@
   2.134  code_const %tt "op \<and>"
   2.135    (SML infixl 1 "andalso")
   2.136  
   2.137 -code_gen in_interval (*<*)in SML(*>*) in SML file "examples/bool_infix.ML"
   2.138 +export_code in_interval (*<*)in SML(*>*) in SML file "examples/bool_infix.ML"
   2.139  
   2.140  text {*
   2.141    \lstsml{Thy/examples/bool_infix.ML}
   2.142 @@ -949,7 +949,7 @@
   2.143  
   2.144  lemma [code func]: "\<Union>set xs = foldr (op \<union>) xs {}" by (induct xs) simp_all
   2.145  
   2.146 -code_gen "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML"
   2.147 +export_code "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML"
   2.148  
   2.149  text {*
   2.150    \lstsml{Thy/examples/set_list.ML}
   2.151 @@ -997,7 +997,7 @@
   2.152    hid away the details from the user.  Anyway, caching
   2.153    reaches the surface by using a slightly more general form
   2.154    of the @{text "\<CODETHMS>"}, @{text "\<CODEDEPS>"}
   2.155 -  and @{text "\<CODEGEN>"} commands: the list of constants
   2.156 +  and @{text "\<EXPORTCODE>"} commands: the list of constants
   2.157    may be omitted.  Then, all constants with code theorems
   2.158    in the current cache are referred to.
   2.159  *}
     3.1 --- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Aug 20 18:07:31 2007 +0200
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Aug 20 18:07:49 2007 +0200
     3.3 @@ -32,7 +32,7 @@
     3.4  \newcommand{\isasymSHOW}{\cmd{show}}
     3.5  \newcommand{\isasymNOTE}{\cmd{note}}
     3.6  \newcommand{\isasymIN}{\cmd{in}}
     3.7 -\newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
     3.8 +\newcommand{\isasymEXPORTCODE}{\cmd{export\_code}}
     3.9  \newcommand{\isasymCODEDATATYPE}{\cmd{code\_datatype}}
    3.10  \newcommand{\isasymCODECONST}{\cmd{code\_const}}
    3.11  \newcommand{\isasymCODETYPE}{\cmd{code\_type}}
     4.1 --- a/doc-src/IsarRef/logics.tex	Mon Aug 20 18:07:31 2007 +0200
     4.2 +++ b/doc-src/IsarRef/logics.tex	Mon Aug 20 18:07:49 2007 +0200
     4.3 @@ -776,7 +776,7 @@
     4.4  \indexisaratt{code inline}
     4.5  
     4.6  \begin{matharray}{rcl}
     4.7 -  \isarcmd{code_gen}^* & : & \isarkeep{theory~|~proof} \\
     4.8 +  \isarcmd{export_code}^* & : & \isarkeep{theory~|~proof} \\
     4.9    \isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\
    4.10    \isarcmd{code_deps}^* & : & \isarkeep{theory~|~proof} \\
    4.11    \isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\
    4.12 @@ -795,7 +795,7 @@
    4.13  \end{matharray}
    4.14  
    4.15  \begin{rail}
    4.16 -'code\_gen' ( constexpr + ) ? \\
    4.17 +'export\_code' ( constexpr + ) ? \\
    4.18    ( ( 'in' target ( 'module_name' string ) ? ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?;
    4.19  
    4.20  'code\_thms' ( constexpr + ) ?;
    4.21 @@ -849,7 +849,7 @@
    4.22  
    4.23  \begin{descr}
    4.24  
    4.25 -\item [$\isarcmd{code_gen}$] is the canonical interface for generating and
    4.26 +\item [$\isarcmd{export_code}$] is the canonical interface for generating and
    4.27    serializing code: for a given list of constants, code is generated for the specified
    4.28    target language(s).  Abstract code is cached incrementally.  If no constant is given,
    4.29    the currently cached code is serialized.  If no serialization instruction
     5.1 --- a/src/HOL/Complex/ex/MIR.thy	Mon Aug 20 18:07:31 2007 +0200
     5.2 +++ b/src/HOL/Complex/ex/MIR.thy	Mon Aug 20 18:07:49 2007 +0200
     5.3 @@ -5772,10 +5772,10 @@
     5.4  definition
     5.5    "test5 (u\<Colon>unit) = mircfrqe (A(E(And (Ge(Sub (Bound 1) (Bound 0))) (Eq (Add (Floor (Bound 1)) (Floor (Neg(Bound 0))))))))"
     5.6  
     5.7 -code_gen mircfrqe mirlfrqe test1 test2 test3 test4 test5
     5.8 +export_code mircfrqe mirlfrqe test1 test2 test3 test4 test5
     5.9    in SML module_name Mir
    5.10  
    5.11 -(*code_gen mircfrqe mirlfrqe
    5.12 +(*export_code mircfrqe mirlfrqe
    5.13    in SML module_name Mir file "raw_mir.ML"*)
    5.14  
    5.15  ML "set Toplevel.timing"
     6.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 20 18:07:31 2007 +0200
     6.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 20 18:07:49 2007 +0200
     6.3 @@ -1986,7 +1986,7 @@
     6.4    "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     6.5      (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
     6.6  
     6.7 -code_gen linrqe ferrack_test in SML module_name Ferrack
     6.8 +export_code linrqe ferrack_test in SML module_name Ferrack
     6.9  
    6.10  (*code_module Ferrack
    6.11    contains
     7.1 --- a/src/HOL/Extraction/Higman.thy	Mon Aug 20 18:07:31 2007 +0200
     7.2 +++ b/src/HOL/Extraction/Higman.thy	Mon Aug 20 18:07:49 2007 +0200
     7.3 @@ -427,7 +427,7 @@
     7.4  code_datatype L0 L1 arbitrary_LT
     7.5  code_datatype T0 T1 T2 arbitrary_TT
     7.6  
     7.7 -code_gen higman_idx in SML module_name Higman
     7.8 +export_code higman_idx in SML module_name Higman
     7.9  
    7.10  ML {*
    7.11  local
     8.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Mon Aug 20 18:07:31 2007 +0200
     8.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Mon Aug 20 18:07:49 2007 +0200
     8.3 @@ -309,7 +309,7 @@
     8.4    test' = test'
     8.5    test'' = test''
     8.6  
     8.7 -code_gen test test' test'' in SML module_name PH2
     8.8 +export_code test test' test'' in SML module_name PH2
     8.9  
    8.10  ML "timeit (PH1.test 10)"
    8.11  ML "timeit (PH2.test 10)"
     9.1 --- a/src/HOL/Extraction/QuotRem.thy	Mon Aug 20 18:07:31 2007 +0200
     9.2 +++ b/src/HOL/Extraction/QuotRem.thy	Mon Aug 20 18:07:49 2007 +0200
     9.3 @@ -49,6 +49,6 @@
     9.4  contains
     9.5    test = "division 9 2"
     9.6  
     9.7 -code_gen division in SML
     9.8 +export_code division in SML
     9.9  
    9.10  end
    10.1 --- a/src/HOL/Lambda/WeakNorm.thy	Mon Aug 20 18:07:31 2007 +0200
    10.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Mon Aug 20 18:07:49 2007 +0200
    10.3 @@ -581,7 +581,7 @@
    10.4    int :: "nat \<Rightarrow> int" where
    10.5    "int \<equiv> of_nat"
    10.6  
    10.7 -code_gen type_NF nat int in SML module_name Norm
    10.8 +export_code type_NF nat int in SML module_name Norm
    10.9  
   10.10  ML {*
   10.11  val nat_of_int = Norm.nat o IntInf.fromInt;
    11.1 --- a/src/HOL/Library/SCT_Implementation.thy	Mon Aug 20 18:07:31 2007 +0200
    11.2 +++ b/src/HOL/Library/SCT_Implementation.thy	Mon Aug 20 18:07:49 2007 +0200
    11.3 @@ -190,6 +190,6 @@
    11.4    Kleene_Algebras SCT
    11.5    SCT_Implementation SCT
    11.6  
    11.7 -code_gen test_SCT in SML
    11.8 +export_code test_SCT in SML
    11.9  
   11.10  end
    12.1 --- a/src/HOL/ex/Classpackage.thy	Mon Aug 20 18:07:31 2007 +0200
    12.2 +++ b/src/HOL/ex/Classpackage.thy	Mon Aug 20 18:07:49 2007 +0200
    12.3 @@ -342,7 +342,7 @@
    12.4  definition "x2 = X (1::int) 2 3"
    12.5  definition "y2 = Y (1::int) 2 3"
    12.6  
    12.7 -code_gen x1 x2 y2 in SML module_name Classpackage
    12.8 +export_code x1 x2 y2 in SML module_name Classpackage
    12.9    in OCaml file -
   12.10    in Haskell file -
   12.11  
    13.1 --- a/src/HOL/ex/Codegenerator.thy	Mon Aug 20 18:07:31 2007 +0200
    13.2 +++ b/src/HOL/ex/Codegenerator.thy	Mon Aug 20 18:07:49 2007 +0200
    13.3 @@ -8,7 +8,7 @@
    13.4  imports ExecutableContent
    13.5  begin
    13.6  
    13.7 -code_gen "*" in SML module_name CodegenTest
    13.8 +export_code "*" in SML module_name CodegenTest
    13.9    in OCaml file -
   13.10    in Haskell file -
   13.11  
    14.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy	Mon Aug 20 18:07:31 2007 +0200
    14.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy	Mon Aug 20 18:07:49 2007 +0200
    14.3 @@ -49,7 +49,7 @@
    14.4  definition
    14.5    "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
    14.6  
    14.7 -code_gen foobar foobar' in SML module_name Foo
    14.8 +export_code foobar foobar' in SML module_name Foo
    14.9    in OCaml file -
   14.10    in Haskell file -
   14.11  ML {* (Foo.foobar, Foo.foobar') *}
    15.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Mon Aug 20 18:07:31 2007 +0200
    15.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Aug 20 18:07:49 2007 +0200
    15.3 @@ -1937,8 +1937,8 @@
    15.4        (Bound 2))))))))"
    15.5  
    15.6  code_reserved SML oo
    15.7 -code_gen pa cooper_test in SML module_name GeneratedCooper
    15.8 -(*code_gen pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
    15.9 +export_code pa cooper_test in SML module_name GeneratedCooper
   15.10 +(*export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
   15.11  
   15.12  ML {* GeneratedCooper.cooper_test () *}
   15.13  use "coopereif.ML"
    16.1 --- a/src/Tools/code/code_package.ML	Mon Aug 20 18:07:31 2007 +0200
    16.2 +++ b/src/Tools/code/code_package.ML	Mon Aug 20 18:07:49 2007 +0200
    16.3 @@ -626,7 +626,7 @@
    16.4  val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
    16.5  
    16.6  val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) =
    16.7 -  ("code_gen", "code_abstype", "code_axioms", "code_thms", "code_deps");
    16.8 +  ("export_code", "code_abstype", "code_axioms", "code_thms", "code_deps");
    16.9  
   16.10  in
   16.11