consolidated naming conventions for code generator theories
authorhaftmann
Fri Oct 12 08:21:09 2007 +0200 (2007-10-12)
changeset 24994c385c4eabb3b
parent 24993 92dfacb32053
child 24995 c26e0166e568
consolidated naming conventions for code generator theories
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
src/HOL/Complex/ex/MIR.thy
src/HOL/IsaMakefile
src/HOL/Lambda/ROOT.ML
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Eval.thy
src/HOL/Library/Library.thy
src/HOL/Library/Pure_term.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/Random.thy
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Oct 12 08:20:46 2007 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Oct 12 08:21:09 2007 +0200
     1.3 @@ -462,25 +462,25 @@
     1.4  
     1.5    \begin{description}
     1.6  
     1.7 -    \item[@{text "Pretty_Int"}] represents @{text HOL} integers by big
     1.8 +    \item[@{text "Code_Integer"}] represents @{text HOL} integers by big
     1.9         integer literals in target languages.
    1.10 -    \item[@{text "Pretty_Char"}] represents @{text HOL} characters by 
    1.11 +    \item[@{text "Code_Char"}] represents @{text HOL} characters by 
    1.12         character literals in target languages.
    1.13 -    \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"},
    1.14 +    \item[@{text "Code_Char_chr"}] like @{text "Code_Char"},
    1.15         but also offers treatment of character codes; includes
    1.16 -       @{text "Pretty_Int"}.
    1.17 -    \item[@{text "Executable_Rat"}] implements rational
    1.18 -       numbers.
    1.19 -    \item[@{text "Executable_Real"}] implements a subset of real numbers,
    1.20 -       namly those representable by rational numbers.
    1.21 +       @{text "Code_Integer"}.
    1.22      \item[@{text "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
    1.23         which in general will result in higher efficency; pattern
    1.24         matching with @{const "0\<Colon>nat"} / @{const "Suc"}
    1.25 -       is eliminated;  includes @{text "Pretty_Int"}.
    1.26 -    \item[@{text "ML_String"}] provides an additional datatype @{text "mlstring"};
    1.27 -       in the @{text HOL} default setup, strings in HOL are mapped to list
    1.28 -       of @{text HOL} characters in SML; values of type @{text "mlstring"} are
    1.29 -       mapped to strings in SML.
    1.30 +       is eliminated;  includes @{text "Code_Integer"}.
    1.31 +    \item[@{text "Code_Index"}] provides an additional datatype
    1.32 +       @{text index} which is mapped to target-language built-in integers.
    1.33 +       Useful for code setups which involve e.g. indexing of
    1.34 +       target-language arrays.
    1.35 +    \item[@{text "Code_Message"}] provides an additional datatype
    1.36 +       @{text message_string} which is isomorphic to strings;
    1.37 +       @{text message_string}s are mapped to target-language strings.
    1.38 +       Useful for code setups which involve e.g. printing (error) messages.
    1.39  
    1.40    \end{description}
    1.41  
     2.1 --- a/src/HOL/Complex/ex/MIR.thy	Fri Oct 12 08:20:46 2007 +0200
     2.2 +++ b/src/HOL/Complex/ex/MIR.thy	Fri Oct 12 08:21:09 2007 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Quatifier elimination for R(0,1,+,floor,<) *}
     2.5  
     2.6  theory MIR
     2.7 -  imports Real GCD Pretty_Int
     2.8 +  imports Real GCD Code_Integer
     2.9    uses ("mireif.ML") ("mirtac.ML")
    2.10    begin
    2.11  
     3.1 --- a/src/HOL/IsaMakefile	Fri Oct 12 08:20:46 2007 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Fri Oct 12 08:21:09 2007 +0200
     3.3 @@ -211,7 +211,7 @@
     3.4  $(LOG)/HOL-Library.gz: $(OUT)/HOL \
     3.5    Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
     3.6    Library/Efficient_Nat.thy Library/Executable_Set.thy \
     3.7 -  Library/ML_Int.thy Library/ML_String.thy Library/Infinite_Set.thy \
     3.8 +  Library/Infinite_Set.thy \
     3.9    Library/FuncSet.thy Library/Library.thy \
    3.10    Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
    3.11    Library/NatPair.thy \
    3.12 @@ -231,8 +231,9 @@
    3.13    Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
    3.14    Library/SCT_Examples.thy Library/sct.ML \
    3.15    Library/Pure_term.thy Library/Eval.thy Library/Eval_Witness.thy \
    3.16 -  Library/Pretty_Int.thy \
    3.17 -  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy\
    3.18 +  Library/Code_Index.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
    3.19 +  Library/Code_Integer.thy Library/Code_Message.thy \
    3.20 +  Library/Abstract_Rat.thy \
    3.21    Library/Numeral_Type.thy Library/Boolean_Algebra.thy
    3.22  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
    3.23  
     4.1 --- a/src/HOL/Lambda/ROOT.ML	Fri Oct 12 08:20:46 2007 +0200
     4.2 +++ b/src/HOL/Lambda/ROOT.ML	Fri Oct 12 08:21:09 2007 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  Syntax.ambiguity_level := 100;
     4.5  proofs := 2;
     4.6  
     4.7 -no_document use_thys ["Accessible_Part", "Pretty_Int"];
     4.8 +no_document use_thys ["Accessible_Part", "Code_Integer"];
     4.9  use_thys ["Eta", "StrongNorm", "Standardization"];
    4.10  if HOL_proofs < 2 then
    4.11    warning "HOL proof terms required for running theory WeakNorm"
     5.1 --- a/src/HOL/Lambda/WeakNorm.thy	Fri Oct 12 08:20:46 2007 +0200
     5.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Fri Oct 12 08:21:09 2007 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  header {* Weak normalization for simply-typed lambda calculus *}
     5.5  
     5.6  theory WeakNorm
     5.7 -imports Type NormalForm Pretty_Int
     5.8 +imports Type NormalForm Code_Integer
     5.9  begin
    5.10  
    5.11  text {*
     6.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Oct 12 08:20:46 2007 +0200
     6.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Oct 12 08:21:09 2007 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* Implementation of natural numbers by integers *}
     6.5  
     6.6  theory Efficient_Nat
     6.7 -imports Main Pretty_Int
     6.8 +imports Main Code_Integer
     6.9  begin
    6.10  
    6.11  text {*
    6.12 @@ -165,13 +165,13 @@
    6.13    then show ?thesis unfolding int_aux_def int_of_nat_def by auto
    6.14  qed
    6.15  
    6.16 -lemma ml_int_of_nat_code [code func, code inline]:
    6.17 -  "ml_int_of_nat n = ml_int_of_int (int_of_nat n)"
    6.18 -  unfolding ml_int_of_nat_def int_of_nat_def by simp
    6.19 +lemma index_of_nat_code [code func, code inline]:
    6.20 +  "index_of_nat n = index_of_int (int_of_nat n)"
    6.21 +  unfolding index_of_nat_def int_of_nat_def by simp
    6.22  
    6.23 -lemma nat_of_mlt_int_code [code func, code inline]:
    6.24 -  "nat_of_ml_int k = nat (int_of_ml_int k)"
    6.25 -  unfolding nat_of_ml_int_def by simp
    6.26 +lemma nat_of_index_code [code func, code inline]:
    6.27 +  "nat_of_index k = nat (int_of_index k)"
    6.28 +  unfolding nat_of_index_def by simp
    6.29  
    6.30  
    6.31  subsection {* Code generator setup for basic functions *}
     7.1 --- a/src/HOL/Library/Eval.thy	Fri Oct 12 08:20:46 2007 +0200
     7.2 +++ b/src/HOL/Library/Eval.thy	Fri Oct 12 08:21:09 2007 +0200
     7.3 @@ -146,9 +146,9 @@
     7.4    "term_of k \<equiv> STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k" ..
     7.5  
     7.6  
     7.7 -text {* Adaption for @{typ ml_string}s *}
     7.8 +text {* Adaption for @{typ message_string}s *}
     7.9  
    7.10 -lemmas [code func, code func del] = term_of_ml_string_def
    7.11 +lemmas [code func, code func del] = term_of_message_string_def
    7.12  
    7.13  
    7.14  subsection {* Evaluation infrastructure *}
     8.1 --- a/src/HOL/Library/Library.thy	Fri Oct 12 08:20:46 2007 +0200
     8.2 +++ b/src/HOL/Library/Library.thy	Fri Oct 12 08:21:09 2007 +0200
     8.3 @@ -8,6 +8,8 @@
     8.4    Binomial
     8.5    Boolean_Algebra
     8.6    Char_ord
     8.7 +  Code_Index
     8.8 +  Code_Message
     8.9    Coinductive_List
    8.10    Commutative_Ring
    8.11    Continuity
    8.12 @@ -18,7 +20,6 @@
    8.13    FuncSet
    8.14    GCD
    8.15    Infinite_Set
    8.16 -  ML_String
    8.17    Multiset
    8.18    NatPair
    8.19    Nat_Infinity
    8.20 @@ -27,8 +28,8 @@
    8.21    OptionalSugar
    8.22    Parity
    8.23    Permutation
    8.24 -  Pretty_Char_chr
    8.25 -  Pretty_Int
    8.26 +  Code_Integer
    8.27 +  Code_Char_chr
    8.28    Primes
    8.29    Quicksort
    8.30    Quotient
     9.1 --- a/src/HOL/Library/Pure_term.thy	Fri Oct 12 08:20:46 2007 +0200
     9.2 +++ b/src/HOL/Library/Pure_term.thy	Fri Oct 12 08:21:09 2007 +0200
     9.3 @@ -6,17 +6,17 @@
     9.4  header {* Embedding (a subset of) the Pure term algebra in HOL *}
     9.5  
     9.6  theory Pure_term
     9.7 -imports ML_String
     9.8 +imports Code_Message
     9.9  begin
    9.10  
    9.11  subsection {* Definitions *}
    9.12  
    9.13 -types vname = ml_string;
    9.14 -types "class" = ml_string;
    9.15 +types vname = message_string;
    9.16 +types "class" = message_string;
    9.17  types sort = "class list"
    9.18  
    9.19  datatype "typ" =
    9.20 -    Type ml_string "typ list" (infix "{\<struct>}" 120)
    9.21 +    Type message_string "typ list" (infix "{\<struct>}" 120)
    9.22    | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
    9.23  
    9.24  abbreviation
    9.25 @@ -27,7 +27,7 @@
    9.26    "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
    9.27  
    9.28  datatype "term" =
    9.29 -    Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112)
    9.30 +    Const message_string "typ" (infix "\<Colon>\<subseteq>" 112)
    9.31    | Fix   vname "typ" (infix ":\<epsilon>" 112)
    9.32    | App   "term" "term" (infixl "\<bullet>" 110)
    9.33    | Abs   "vname \<times> typ" "term" (infixr "\<mapsto>" 111)
    9.34 @@ -47,16 +47,16 @@
    9.35  structure Pure_term =
    9.36  struct
    9.37  
    9.38 -val mk_sort = HOLogic.mk_list @{typ class} o map ML_String.mk;
    9.39 +val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk;
    9.40  
    9.41  fun mk_typ f (Type (tyco, tys)) =
    9.42 -      @{term Type} $ ML_String.mk tyco
    9.43 +      @{term Type} $ Message_String.mk tyco
    9.44          $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys)
    9.45    | mk_typ f (TFree v) =
    9.46        f v;
    9.47  
    9.48  fun mk_term f g (Const (c, ty)) =
    9.49 -      @{term Const} $ ML_String.mk c $ g ty
    9.50 +      @{term Const} $ Message_String.mk c $ g ty
    9.51    | mk_term f g (t1 $ t2) =
    9.52        @{term App} $ mk_term f g t1 $ mk_term f g t2
    9.53    | mk_term f g (Free v) = f v;
    10.1 --- a/src/HOL/ex/ROOT.ML	Fri Oct 12 08:20:46 2007 +0200
    10.2 +++ b/src/HOL/ex/ROOT.ML	Fri Oct 12 08:21:09 2007 +0200
    10.3 @@ -10,7 +10,7 @@
    10.4    "Classpackage",
    10.5    "Eval",
    10.6    "State_Monad",
    10.7 -  "Pretty_Int",
    10.8 +  "Code_Integer",
    10.9    "Efficient_Nat",
   10.10    "Codegenerator",
   10.11    "Codegenerator_Pretty",
    11.1 --- a/src/HOL/ex/Random.thy	Fri Oct 12 08:20:46 2007 +0200
    11.2 +++ b/src/HOL/ex/Random.thy	Fri Oct 12 08:21:09 2007 +0200
    11.3 @@ -5,7 +5,7 @@
    11.4  header {* A simple random engine *}
    11.5  
    11.6  theory Random
    11.7 -imports State_Monad Pretty_Int
    11.8 +imports State_Monad Code_Integer
    11.9  begin
   11.10  
   11.11  fun