--- 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}
--- 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
--- 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
--- 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"
--- 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 {*
--- 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 *}
--- 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 *}
--- 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
--- 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;
--- 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",
--- 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