# HG changeset patch
# User haftmann
# Date 1192170069 -7200
# Node ID c385c4eabb3bfdd8984bdad6f5e2408ecfa166b2
# Parent  92dfacb32053e3da17027ab84bba02cb1bbd053d
consolidated naming conventions for code generator theories

diff -r 92dfacb32053 -r c385c4eabb3b doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -462,25 +462,25 @@
 
   \begin{description}
 
-    \item[@{text "Pretty_Int"}] represents @{text HOL} integers by big
+    \item[@{text "Code_Integer"}] represents @{text HOL} integers by big
        integer literals in target languages.
-    \item[@{text "Pretty_Char"}] represents @{text HOL} characters by 
+    \item[@{text "Code_Char"}] represents @{text HOL} characters by 
        character literals in target languages.
-    \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char"},
+    \item[@{text "Code_Char_chr"}] like @{text "Code_Char"},
        but also offers treatment of character codes; includes
-       @{text "Pretty_Int"}.
-    \item[@{text "Executable_Rat"}] implements rational
-       numbers.
-    \item[@{text "Executable_Real"}] implements a subset of real numbers,
-       namly those representable by rational numbers.
+       @{text "Code_Integer"}.
     \item[@{text "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
        which in general will result in higher efficency; pattern
        matching with @{const "0\<Colon>nat"} / @{const "Suc"}
-       is eliminated;  includes @{text "Pretty_Int"}.
-    \item[@{text "ML_String"}] provides an additional datatype @{text "mlstring"};
-       in the @{text HOL} default setup, strings in HOL are mapped to list
-       of @{text HOL} characters in SML; values of type @{text "mlstring"} are
-       mapped to strings in SML.
+       is eliminated;  includes @{text "Code_Integer"}.
+    \item[@{text "Code_Index"}] provides an additional datatype
+       @{text index} which is mapped to target-language built-in integers.
+       Useful for code setups which involve e.g. indexing of
+       target-language arrays.
+    \item[@{text "Code_Message"}] provides an additional datatype
+       @{text message_string} which is isomorphic to strings;
+       @{text message_string}s are mapped to target-language strings.
+       Useful for code setups which involve e.g. printing (error) messages.
 
   \end{description}
 
diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/Complex/ex/MIR.thy
--- a/src/HOL/Complex/ex/MIR.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -5,7 +5,7 @@
 header {* Quatifier elimination for R(0,1,+,floor,<) *}
 
 theory MIR
-  imports Real GCD Pretty_Int
+  imports Real GCD Code_Integer
   uses ("mireif.ML") ("mirtac.ML")
   begin
 
diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 12 08:21:09 2007 +0200
@@ -211,7 +211,7 @@
 $(LOG)/HOL-Library.gz: $(OUT)/HOL \
   Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
   Library/Efficient_Nat.thy Library/Executable_Set.thy \
-  Library/ML_Int.thy Library/ML_String.thy Library/Infinite_Set.thy \
+  Library/Infinite_Set.thy \
   Library/FuncSet.thy Library/Library.thy \
   Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
   Library/NatPair.thy \
@@ -231,8 +231,9 @@
   Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
   Library/SCT_Examples.thy Library/sct.ML \
   Library/Pure_term.thy Library/Eval.thy Library/Eval_Witness.thy \
-  Library/Pretty_Int.thy \
-  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy\
+  Library/Code_Index.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
+  Library/Code_Integer.thy Library/Code_Message.thy \
+  Library/Abstract_Rat.thy \
   Library/Numeral_Type.thy Library/Boolean_Algebra.thy
 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
 
diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/Lambda/ROOT.ML
--- a/src/HOL/Lambda/ROOT.ML	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Fri Oct 12 08:21:09 2007 +0200
@@ -7,7 +7,7 @@
 Syntax.ambiguity_level := 100;
 proofs := 2;
 
-no_document use_thys ["Accessible_Part", "Pretty_Int"];
+no_document use_thys ["Accessible_Part", "Code_Integer"];
 use_thys ["Eta", "StrongNorm", "Standardization"];
 if HOL_proofs < 2 then
   warning "HOL proof terms required for running theory WeakNorm"
diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -7,7 +7,7 @@
 header {* Weak normalization for simply-typed lambda calculus *}
 
 theory WeakNorm
-imports Type NormalForm Pretty_Int
+imports Type NormalForm Code_Integer
 begin
 
 text {*
diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -6,7 +6,7 @@
 header {* Implementation of natural numbers by integers *}
 
 theory Efficient_Nat
-imports Main Pretty_Int
+imports Main Code_Integer
 begin
 
 text {*
@@ -165,13 +165,13 @@
   then show ?thesis unfolding int_aux_def int_of_nat_def by auto
 qed
 
-lemma ml_int_of_nat_code [code func, code inline]:
-  "ml_int_of_nat n = ml_int_of_int (int_of_nat n)"
-  unfolding ml_int_of_nat_def int_of_nat_def by simp
+lemma index_of_nat_code [code func, code inline]:
+  "index_of_nat n = index_of_int (int_of_nat n)"
+  unfolding index_of_nat_def int_of_nat_def by simp
 
-lemma nat_of_mlt_int_code [code func, code inline]:
-  "nat_of_ml_int k = nat (int_of_ml_int k)"
-  unfolding nat_of_ml_int_def by simp
+lemma nat_of_index_code [code func, code inline]:
+  "nat_of_index k = nat (int_of_index k)"
+  unfolding nat_of_index_def by simp
 
 
 subsection {* Code generator setup for basic functions *}
diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -146,9 +146,9 @@
   "term_of k \<equiv> STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k" ..
 
 
-text {* Adaption for @{typ ml_string}s *}
+text {* Adaption for @{typ message_string}s *}
 
-lemmas [code func, code func del] = term_of_ml_string_def
+lemmas [code func, code func del] = term_of_message_string_def
 
 
 subsection {* Evaluation infrastructure *}
diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Library/Library.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -8,6 +8,8 @@
   Binomial
   Boolean_Algebra
   Char_ord
+  Code_Index
+  Code_Message
   Coinductive_List
   Commutative_Ring
   Continuity
@@ -18,7 +20,6 @@
   FuncSet
   GCD
   Infinite_Set
-  ML_String
   Multiset
   NatPair
   Nat_Infinity
@@ -27,8 +28,8 @@
   OptionalSugar
   Parity
   Permutation
-  Pretty_Char_chr
-  Pretty_Int
+  Code_Integer
+  Code_Char_chr
   Primes
   Quicksort
   Quotient
diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/Library/Pure_term.thy
--- a/src/HOL/Library/Pure_term.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Library/Pure_term.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -6,17 +6,17 @@
 header {* Embedding (a subset of) the Pure term algebra in HOL *}
 
 theory Pure_term
-imports ML_String
+imports Code_Message
 begin
 
 subsection {* Definitions *}
 
-types vname = ml_string;
-types "class" = ml_string;
+types vname = message_string;
+types "class" = message_string;
 types sort = "class list"
 
 datatype "typ" =
-    Type ml_string "typ list" (infix "{\<struct>}" 120)
+    Type message_string "typ list" (infix "{\<struct>}" 120)
   | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
 
 abbreviation
@@ -27,7 +27,7 @@
   "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
 
 datatype "term" =
-    Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112)
+    Const message_string "typ" (infix "\<Colon>\<subseteq>" 112)
   | Fix   vname "typ" (infix ":\<epsilon>" 112)
   | App   "term" "term" (infixl "\<bullet>" 110)
   | Abs   "vname \<times> typ" "term" (infixr "\<mapsto>" 111)
@@ -47,16 +47,16 @@
 structure Pure_term =
 struct
 
-val mk_sort = HOLogic.mk_list @{typ class} o map ML_String.mk;
+val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk;
 
 fun mk_typ f (Type (tyco, tys)) =
-      @{term Type} $ ML_String.mk tyco
+      @{term Type} $ Message_String.mk tyco
         $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys)
   | mk_typ f (TFree v) =
       f v;
 
 fun mk_term f g (Const (c, ty)) =
-      @{term Const} $ ML_String.mk c $ g ty
+      @{term Const} $ Message_String.mk c $ g ty
   | mk_term f g (t1 $ t2) =
       @{term App} $ mk_term f g t1 $ mk_term f g t2
   | mk_term f g (Free v) = f v;
diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Oct 12 08:21:09 2007 +0200
@@ -10,7 +10,7 @@
   "Classpackage",
   "Eval",
   "State_Monad",
-  "Pretty_Int",
+  "Code_Integer",
   "Efficient_Nat",
   "Codegenerator",
   "Codegenerator_Pretty",
diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/ex/Random.thy
--- a/src/HOL/ex/Random.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/ex/Random.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -5,7 +5,7 @@
 header {* A simple random engine *}
 
 theory Random
-imports State_Monad Pretty_Int
+imports State_Monad Code_Integer
 begin
 
 fun