--- a/doc-src/Codegen/Thy/Adaptation.thy Tue May 19 13:57:51 2009 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Tue May 19 16:54:55 2009 +0200
@@ -127,8 +127,8 @@
Useful for code setups which involve e.g. indexing of
target-language arrays.
\item[@{theory "String"}] provides an additional datatype
- @{typ message_string} which is isomorphic to strings;
- @{typ message_string}s are mapped to target-language strings.
+ @{typ String.literal} which is isomorphic to strings;
+ @{typ String.literal}s are mapped to target-language strings.
Useful for code setups which involve e.g. printing (error) messages.
\end{description}
--- a/src/HOL/Code_Eval.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Code_Eval.thy Tue May 19 16:54:55 2009 +0200
@@ -5,7 +5,7 @@
header {* Term evaluation using the generic code generator *}
theory Code_Eval
-imports Plain Typerep Code_Index
+imports Plain Typerep Code_Numeral
begin
subsection {* Term representation *}
@@ -14,7 +14,7 @@
datatype "term" = dummy_term
-definition Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" where
+definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
"Const _ _ = dummy_term"
definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
@@ -63,10 +63,7 @@
let
val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
- in
- thy
- |> need_inst ? add_term_of tyco raw_vs
- end;
+ in if need_inst then add_term_of tyco raw_vs thy else thy end;
in
Code.type_interpretation ensure_term_of
end
@@ -102,10 +99,7 @@
fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
let
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
- in
- thy
- |> has_inst ? add_term_of_code tyco raw_vs cs
- end;
+ in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
in
Code.type_interpretation ensure_term_of_code
end
@@ -119,7 +113,7 @@
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
lemma [code, code del]:
"(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
lemma [code, code del]:
@@ -137,7 +131,7 @@
code_const Const and App
(Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)")
-code_const "term_of \<Colon> message_string \<Rightarrow> term"
+code_const "term_of \<Colon> String.literal \<Rightarrow> term"
(Eval "HOLogic.mk'_message'_string")
code_reserved Eval HOLogic
@@ -215,8 +209,8 @@
else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
by (simp only: term_of_anything)
-lemma (in term_syntax) term_of_index_code [code]:
- "term_of (k::index) = termify (number_of :: int \<Rightarrow> index) <\<cdot>> term_of_num (2::index) k"
+lemma (in term_syntax) term_of_code_numeral_code [code]:
+ "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
by (simp only: term_of_anything)
subsection {* Obfuscate *}
--- a/src/HOL/Code_Index.thy Tue May 19 13:57:51 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,325 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Type of indices *}
-
-theory Code_Index
-imports Nat_Numeral
-begin
-
-text {*
- Indices are isomorphic to HOL @{typ nat} but
- mapped to target-language builtin integers.
-*}
-
-subsection {* Datatype of indices *}
-
-typedef (open) index = "UNIV \<Colon> nat set"
- morphisms nat_of of_nat by rule
-
-lemma of_nat_nat_of [simp]:
- "of_nat (nat_of k) = k"
- by (rule nat_of_inverse)
-
-lemma nat_of_of_nat [simp]:
- "nat_of (of_nat n) = n"
- by (rule of_nat_inverse) (rule UNIV_I)
-
-lemma [measure_function]:
- "is_measure nat_of" by (rule is_measure_trivial)
-
-lemma index:
- "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
-proof
- fix n :: nat
- assume "\<And>n\<Colon>index. PROP P n"
- then show "PROP P (of_nat n)" .
-next
- fix n :: index
- assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
- then have "PROP P (of_nat (nat_of n))" .
- then show "PROP P n" by simp
-qed
-
-lemma index_case:
- assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
- shows P
- by (rule assms [of "nat_of k"]) simp
-
-lemma index_induct_raw:
- assumes "\<And>n. P (of_nat n)"
- shows "P k"
-proof -
- from assms have "P (of_nat (nat_of k))" .
- then show ?thesis by simp
-qed
-
-lemma nat_of_inject [simp]:
- "nat_of k = nat_of l \<longleftrightarrow> k = l"
- by (rule nat_of_inject)
-
-lemma of_nat_inject [simp]:
- "of_nat n = of_nat m \<longleftrightarrow> n = m"
- by (rule of_nat_inject) (rule UNIV_I)+
-
-instantiation index :: zero
-begin
-
-definition [simp, code del]:
- "0 = of_nat 0"
-
-instance ..
-
-end
-
-definition [simp]:
- "Suc_index k = of_nat (Suc (nat_of k))"
-
-rep_datatype "0 \<Colon> index" Suc_index
-proof -
- fix P :: "index \<Rightarrow> bool"
- fix k :: index
- assume "P 0" then have init: "P (of_nat 0)" by simp
- assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
- then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
- then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
- from init step have "P (of_nat (nat_of k))"
- by (induct "nat_of k") simp_all
- then show "P k" by simp
-qed simp_all
-
-declare index_case [case_names nat, cases type: index]
-declare index.induct [case_names nat, induct type: index]
-
-lemma index_decr [termination_simp]:
- "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
- by (cases k) simp
-
-lemma [simp, code]:
- "index_size = nat_of"
-proof (rule ext)
- fix k
- have "index_size k = nat_size (nat_of k)"
- by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
- also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
- finally show "index_size k = nat_of k" .
-qed
-
-lemma [simp, code]:
- "size = nat_of"
-proof (rule ext)
- fix k
- show "size k = nat_of k"
- by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
-qed
-
-lemmas [code del] = index.recs index.cases
-
-lemma [code]:
- "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
- by (cases k, cases l) (simp add: eq)
-
-lemma [code nbe]:
- "eq_class.eq (k::index) k \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
-
-
-subsection {* Indices as datatype of ints *}
-
-instantiation index :: number
-begin
-
-definition
- "number_of = of_nat o nat"
-
-instance ..
-
-end
-
-lemma nat_of_number [simp]:
- "nat_of (number_of k) = number_of k"
- by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
-
-code_datatype "number_of \<Colon> int \<Rightarrow> index"
-
-
-subsection {* Basic arithmetic *}
-
-instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
-begin
-
-definition [simp, code del]:
- "(1\<Colon>index) = of_nat 1"
-
-definition [simp, code del]:
- "n + m = of_nat (nat_of n + nat_of m)"
-
-definition [simp, code del]:
- "n - m = of_nat (nat_of n - nat_of m)"
-
-definition [simp, code del]:
- "n * m = of_nat (nat_of n * nat_of m)"
-
-definition [simp, code del]:
- "n div m = of_nat (nat_of n div nat_of m)"
-
-definition [simp, code del]:
- "n mod m = of_nat (nat_of n mod nat_of m)"
-
-definition [simp, code del]:
- "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
-
-definition [simp, code del]:
- "n < m \<longleftrightarrow> nat_of n < nat_of m"
-
-instance proof
-qed (auto simp add: index left_distrib div_mult_self1)
-
-end
-
-lemma zero_index_code [code inline, code]:
- "(0\<Colon>index) = Numeral0"
- by (simp add: number_of_index_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>index)"
- using zero_index_code ..
-
-lemma one_index_code [code inline, code]:
- "(1\<Colon>index) = Numeral1"
- by (simp add: number_of_index_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>index)"
- using one_index_code ..
-
-lemma plus_index_code [code nbe]:
- "of_nat n + of_nat m = of_nat (n + m)"
- by simp
-
-definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
- [simp, code del]: "subtract_index = op -"
-
-lemma subtract_index_code [code nbe]:
- "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
- by simp
-
-lemma minus_index_code [code]:
- "n - m = subtract_index n m"
- by simp
-
-lemma times_index_code [code nbe]:
- "of_nat n * of_nat m = of_nat (n * m)"
- by simp
-
-lemma less_eq_index_code [code nbe]:
- "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
- by simp
-
-lemma less_index_code [code nbe]:
- "of_nat n < of_nat m \<longleftrightarrow> n < m"
- by simp
-
-lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
-
-lemma of_nat_code [code]:
- "of_nat = Nat.of_nat"
-proof
- fix n :: nat
- have "Nat.of_nat n = of_nat n"
- by (induct n) simp_all
- then show "of_nat n = Nat.of_nat n"
- by (rule sym)
-qed
-
-lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
- by (cases i) auto
-
-definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
- "nat_of_aux i n = nat_of i + n"
-
-lemma nat_of_aux_code [code]:
- "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
- by (auto simp add: nat_of_aux_def index_not_eq_zero)
-
-lemma nat_of_code [code]:
- "nat_of i = nat_of_aux i 0"
- by (simp add: nat_of_aux_def)
-
-definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
- [code del]: "div_mod_index n m = (n div m, n mod m)"
-
-lemma [code]:
- "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
- unfolding div_mod_index_def by auto
-
-lemma [code]:
- "n div m = fst (div_mod_index n m)"
- unfolding div_mod_index_def by simp
-
-lemma [code]:
- "n mod m = snd (div_mod_index n m)"
- unfolding div_mod_index_def by simp
-
-definition int_of :: "index \<Rightarrow> int" where
- "int_of = Nat.of_nat o nat_of"
-
-lemma int_of_code [code]:
- "int_of k = (if k = 0 then 0
- else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
- by (auto simp add: int_of_def mod_div_equality')
-
-hide (open) const of_nat nat_of int_of
-
-
-subsection {* Code generator setup *}
-
-text {* Implementation of indices by bounded integers *}
-
-code_type index
- (SML "int")
- (OCaml "int")
- (Haskell "Int")
-
-code_instance index :: eq
- (Haskell -)
-
-setup {*
- fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
- false false) ["SML", "OCaml", "Haskell"]
-*}
-
-code_reserved SML Int int
-code_reserved OCaml Pervasives int
-
-code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.+/ ((_),/ (_))")
- (OCaml "Pervasives.( + )")
- (Haskell infixl 6 "+")
-
-code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.max/ (_/ -/ _,/ 0 : int)")
- (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
- (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
-
-code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.*/ ((_),/ (_))")
- (OCaml "Pervasives.( * )")
- (Haskell infixl 7 "*")
-
-code_const div_mod_index
- (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
- (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
- (Haskell "divMod")
-
-code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "!((_ : Int.int) = _)")
- (OCaml "!((_ : int) = _)")
- (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "Int.<=/ ((_),/ (_))")
- (OCaml "!((_ : int) <= _)")
- (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "Int.</ ((_),/ (_))")
- (OCaml "!((_ : int) < _)")
- (Haskell infix 4 "<")
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Code_Numeral.thy Tue May 19 16:54:55 2009 +0200
@@ -0,0 +1,325 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Type of target language numerals *}
+
+theory Code_Numeral
+imports Nat_Numeral
+begin
+
+text {*
+ Code numerals are isomorphic to HOL @{typ nat} but
+ mapped to target-language builtin numerals.
+*}
+
+subsection {* Datatype of target language numerals *}
+
+typedef (open) code_numeral = "UNIV \<Colon> nat set"
+ morphisms nat_of of_nat by rule
+
+lemma of_nat_nat_of [simp]:
+ "of_nat (nat_of k) = k"
+ by (rule nat_of_inverse)
+
+lemma nat_of_of_nat [simp]:
+ "nat_of (of_nat n) = n"
+ by (rule of_nat_inverse) (rule UNIV_I)
+
+lemma [measure_function]:
+ "is_measure nat_of" by (rule is_measure_trivial)
+
+lemma code_numeral:
+ "(\<And>n\<Colon>code_numeral. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
+proof
+ fix n :: nat
+ assume "\<And>n\<Colon>code_numeral. PROP P n"
+ then show "PROP P (of_nat n)" .
+next
+ fix n :: code_numeral
+ assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
+ then have "PROP P (of_nat (nat_of n))" .
+ then show "PROP P n" by simp
+qed
+
+lemma code_numeral_case:
+ assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
+ shows P
+ by (rule assms [of "nat_of k"]) simp
+
+lemma code_numeral_induct_raw:
+ assumes "\<And>n. P (of_nat n)"
+ shows "P k"
+proof -
+ from assms have "P (of_nat (nat_of k))" .
+ then show ?thesis by simp
+qed
+
+lemma nat_of_inject [simp]:
+ "nat_of k = nat_of l \<longleftrightarrow> k = l"
+ by (rule nat_of_inject)
+
+lemma of_nat_inject [simp]:
+ "of_nat n = of_nat m \<longleftrightarrow> n = m"
+ by (rule of_nat_inject) (rule UNIV_I)+
+
+instantiation code_numeral :: zero
+begin
+
+definition [simp, code del]:
+ "0 = of_nat 0"
+
+instance ..
+
+end
+
+definition [simp]:
+ "Suc_code_numeral k = of_nat (Suc (nat_of k))"
+
+rep_datatype "0 \<Colon> code_numeral" Suc_code_numeral
+proof -
+ fix P :: "code_numeral \<Rightarrow> bool"
+ fix k :: code_numeral
+ assume "P 0" then have init: "P (of_nat 0)" by simp
+ assume "\<And>k. P k \<Longrightarrow> P (Suc_code_numeral k)"
+ then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
+ then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
+ from init step have "P (of_nat (nat_of k))"
+ by (induct "nat_of k") simp_all
+ then show "P k" by simp
+qed simp_all
+
+declare code_numeral_case [case_names nat, cases type: code_numeral]
+declare code_numeral.induct [case_names nat, induct type: code_numeral]
+
+lemma code_numeral_decr [termination_simp]:
+ "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Suc 0 < nat_of k"
+ by (cases k) simp
+
+lemma [simp, code]:
+ "code_numeral_size = nat_of"
+proof (rule ext)
+ fix k
+ have "code_numeral_size k = nat_size (nat_of k)"
+ by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
+ also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
+ finally show "code_numeral_size k = nat_of k" .
+qed
+
+lemma [simp, code]:
+ "size = nat_of"
+proof (rule ext)
+ fix k
+ show "size k = nat_of k"
+ by (induct k) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
+qed
+
+lemmas [code del] = code_numeral.recs code_numeral.cases
+
+lemma [code]:
+ "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
+ by (cases k, cases l) (simp add: eq)
+
+lemma [code nbe]:
+ "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
+ by (rule HOL.eq_refl)
+
+
+subsection {* Indices as datatype of ints *}
+
+instantiation code_numeral :: number
+begin
+
+definition
+ "number_of = of_nat o nat"
+
+instance ..
+
+end
+
+lemma nat_of_number [simp]:
+ "nat_of (number_of k) = number_of k"
+ by (simp add: number_of_code_numeral_def nat_number_of_def number_of_is_id)
+
+code_datatype "number_of \<Colon> int \<Rightarrow> code_numeral"
+
+
+subsection {* Basic arithmetic *}
+
+instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}"
+begin
+
+definition [simp, code del]:
+ "(1\<Colon>code_numeral) = of_nat 1"
+
+definition [simp, code del]:
+ "n + m = of_nat (nat_of n + nat_of m)"
+
+definition [simp, code del]:
+ "n - m = of_nat (nat_of n - nat_of m)"
+
+definition [simp, code del]:
+ "n * m = of_nat (nat_of n * nat_of m)"
+
+definition [simp, code del]:
+ "n div m = of_nat (nat_of n div nat_of m)"
+
+definition [simp, code del]:
+ "n mod m = of_nat (nat_of n mod nat_of m)"
+
+definition [simp, code del]:
+ "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
+
+definition [simp, code del]:
+ "n < m \<longleftrightarrow> nat_of n < nat_of m"
+
+instance proof
+qed (auto simp add: code_numeral left_distrib div_mult_self1)
+
+end
+
+lemma zero_code_numeral_code [code inline, code]:
+ "(0\<Colon>code_numeral) = Numeral0"
+ by (simp add: number_of_code_numeral_def Pls_def)
+lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
+ using zero_code_numeral_code ..
+
+lemma one_code_numeral_code [code inline, code]:
+ "(1\<Colon>code_numeral) = Numeral1"
+ by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
+lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
+ using one_code_numeral_code ..
+
+lemma plus_code_numeral_code [code nbe]:
+ "of_nat n + of_nat m = of_nat (n + m)"
+ by simp
+
+definition subtract_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
+ [simp, code del]: "subtract_code_numeral = op -"
+
+lemma subtract_code_numeral_code [code nbe]:
+ "subtract_code_numeral (of_nat n) (of_nat m) = of_nat (n - m)"
+ by simp
+
+lemma minus_code_numeral_code [code]:
+ "n - m = subtract_code_numeral n m"
+ by simp
+
+lemma times_code_numeral_code [code nbe]:
+ "of_nat n * of_nat m = of_nat (n * m)"
+ by simp
+
+lemma less_eq_code_numeral_code [code nbe]:
+ "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
+ by simp
+
+lemma less_code_numeral_code [code nbe]:
+ "of_nat n < of_nat m \<longleftrightarrow> n < m"
+ by simp
+
+lemma Suc_code_numeral_minus_one: "Suc_code_numeral n - 1 = n" by simp
+
+lemma of_nat_code [code]:
+ "of_nat = Nat.of_nat"
+proof
+ fix n :: nat
+ have "Nat.of_nat n = of_nat n"
+ by (induct n) simp_all
+ then show "of_nat n = Nat.of_nat n"
+ by (rule sym)
+qed
+
+lemma code_numeral_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
+ by (cases i) auto
+
+definition nat_of_aux :: "code_numeral \<Rightarrow> nat \<Rightarrow> nat" where
+ "nat_of_aux i n = nat_of i + n"
+
+lemma nat_of_aux_code [code]:
+ "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
+ by (auto simp add: nat_of_aux_def code_numeral_not_eq_zero)
+
+lemma nat_of_code [code]:
+ "nat_of i = nat_of_aux i 0"
+ by (simp add: nat_of_aux_def)
+
+definition div_mod_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
+ [code del]: "div_mod_code_numeral n m = (n div m, n mod m)"
+
+lemma [code]:
+ "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))"
+ unfolding div_mod_code_numeral_def by auto
+
+lemma [code]:
+ "n div m = fst (div_mod_code_numeral n m)"
+ unfolding div_mod_code_numeral_def by simp
+
+lemma [code]:
+ "n mod m = snd (div_mod_code_numeral n m)"
+ unfolding div_mod_code_numeral_def by simp
+
+definition int_of :: "code_numeral \<Rightarrow> int" where
+ "int_of = Nat.of_nat o nat_of"
+
+lemma int_of_code [code]:
+ "int_of k = (if k = 0 then 0
+ else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
+ by (auto simp add: int_of_def mod_div_equality')
+
+hide (open) const of_nat nat_of int_of
+
+
+subsection {* Code generator setup *}
+
+text {* Implementation of indices by bounded integers *}
+
+code_type code_numeral
+ (SML "int")
+ (OCaml "int")
+ (Haskell "Int")
+
+code_instance code_numeral :: eq
+ (Haskell -)
+
+setup {*
+ fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+ false false) ["SML", "OCaml", "Haskell"]
+*}
+
+code_reserved SML Int int
+code_reserved OCaml Pervasives int
+
+code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (SML "Int.+/ ((_),/ (_))")
+ (OCaml "Pervasives.( + )")
+ (Haskell infixl 6 "+")
+
+code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (SML "Int.max/ (_/ -/ _,/ 0 : int)")
+ (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
+ (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
+
+code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+ (SML "Int.*/ ((_),/ (_))")
+ (OCaml "Pervasives.( * )")
+ (Haskell infixl 7 "*")
+
+code_const div_mod_code_numeral
+ (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+ (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
+ (Haskell "divMod")
+
+code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (SML "!((_ : Int.int) = _)")
+ (OCaml "!((_ : int) = _)")
+ (Haskell infixl 4 "==")
+
+code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (SML "Int.<=/ ((_),/ (_))")
+ (OCaml "!((_ : int) <= _)")
+ (Haskell infix 4 "<=")
+
+code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+ (SML "Int.</ ((_),/ (_))")
+ (OCaml "!((_ : int) < _)")
+ (Haskell infix 4 "<")
+
+end
--- a/src/HOL/Imperative_HOL/Array.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Tue May 19 16:54:55 2009 +0200
@@ -115,47 +115,47 @@
subsubsection {* Logical intermediate layer *}
definition new' where
- [code del]: "new' = Array.new o Code_Index.nat_of"
+ [code del]: "new' = Array.new o Code_Numeral.nat_of"
hide (open) const new'
lemma [code]:
- "Array.new = Array.new' o Code_Index.of_nat"
+ "Array.new = Array.new' o Code_Numeral.of_nat"
by (simp add: new'_def o_def)
definition of_list' where
- [code del]: "of_list' i xs = Array.of_list (take (Code_Index.nat_of i) xs)"
+ [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
hide (open) const of_list'
lemma [code]:
- "Array.of_list xs = Array.of_list' (Code_Index.of_nat (List.length xs)) xs"
+ "Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs"
by (simp add: of_list'_def)
definition make' where
- [code del]: "make' i f = Array.make (Code_Index.nat_of i) (f o Code_Index.of_nat)"
+ [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
hide (open) const make'
lemma [code]:
- "Array.make n f = Array.make' (Code_Index.of_nat n) (f o Code_Index.nat_of)"
+ "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
by (simp add: make'_def o_def)
definition length' where
- [code del]: "length' = Array.length \<guillemotright>== liftM Code_Index.of_nat"
+ [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
hide (open) const length'
lemma [code]:
- "Array.length = Array.length' \<guillemotright>== liftM Code_Index.nat_of"
+ "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
by (simp add: length'_def monad_simp',
simp add: liftM_def comp_def monad_simp,
simp add: monad_simp')
definition nth' where
- [code del]: "nth' a = Array.nth a o Code_Index.nat_of"
+ [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
hide (open) const nth'
lemma [code]:
- "Array.nth a n = Array.nth' a (Code_Index.of_nat n)"
+ "Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)"
by (simp add: nth'_def)
definition upd' where
- [code del]: "upd' a i x = Array.upd (Code_Index.nat_of i) x a \<guillemotright> return ()"
+ [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()"
hide (open) const upd'
lemma [code]:
- "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \<guillemotright> return a"
+ "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
by (simp add: upd'_def monad_simp upd_return)
--- a/src/HOL/Imperative_HOL/Heap.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Tue May 19 16:54:55 2009 +0200
@@ -28,11 +28,11 @@
instance int :: heap ..
-instance message_string :: countable
- by (rule countable_classI [of "message_string_case to_nat"])
- (auto split: message_string.splits)
+instance String.literal :: countable
+ by (rule countable_classI [of "String.literal_case to_nat"])
+ (auto split: String.literal.splits)
-instance message_string :: heap ..
+instance String.literal :: heap ..
text {* Reflected types themselves are heap-representable *}
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue May 19 16:54:55 2009 +0200
@@ -274,7 +274,7 @@
subsubsection {* Logical intermediate layer *}
definition
- Fail :: "message_string \<Rightarrow> exception"
+ Fail :: "String.literal \<Rightarrow> exception"
where
[code del]: "Fail s = Exn"
--- a/src/HOL/IsaMakefile Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/IsaMakefile Tue May 19 16:54:55 2009 +0200
@@ -206,7 +206,7 @@
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
ATP_Linkup.thy \
Code_Eval.thy \
- Code_Index.thy \
+ Code_Numeral.thy \
Equiv_Relations.thy \
Groebner_Basis.thy \
Hilbert_Choice.thy \
--- a/src/HOL/Library/Code_Integer.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Library/Code_Integer.thy Tue May 19 16:54:55 2009 +0200
@@ -91,7 +91,7 @@
(OCaml "Big'_int.lt'_big'_int")
(Haskell infix 4 "<")
-code_const Code_Index.int_of
+code_const Code_Numeral.int_of
(SML "IntInf.fromInt")
(OCaml "Big'_int.big'_int'_of'_int")
(Haskell "toEnum")
--- a/src/HOL/Library/Efficient_Nat.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue May 19 16:54:55 2009 +0200
@@ -369,12 +369,12 @@
text {* Conversion from and to indices. *}
-code_const Code_Index.of_nat
+code_const Code_Numeral.of_nat
(SML "IntInf.toInt")
(OCaml "Big'_int.int'_of'_big'_int")
(Haskell "fromEnum")
-code_const Code_Index.nat_of
+code_const Code_Numeral.nat_of
(SML "IntInf.fromInt")
(OCaml "Big'_int.big'_int'_of'_int")
(Haskell "toEnum")
--- a/src/HOL/Quickcheck.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Quickcheck.thy Tue May 19 16:54:55 2009 +0200
@@ -13,7 +13,7 @@
subsection {* The @{text random} class *}
class random = typerep +
- fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+ fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
subsection {* Quickcheck generator *}
@@ -49,7 +49,7 @@
(mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
(Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
- in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
+ in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
fun compile_generator_expr thy t =
let
@@ -84,7 +84,7 @@
instantiation itself :: (typerep) random
begin
-definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
"random_itself _ = Pair (Code_Eval.valtermify TYPE('a))"
instance ..
@@ -139,7 +139,7 @@
instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
begin
-definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
"random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
instance ..
@@ -154,9 +154,9 @@
instantiation nat :: random
begin
-definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
+definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
"random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
- let n = Code_Index.nat_of k
+ let n = Code_Numeral.nat_of k
in (n, \<lambda>_. Code_Eval.term_of n)))"
instance ..
@@ -168,7 +168,7 @@
definition
"random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
- let j = (if k \<ge> i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k))
+ let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
in (j, \<lambda>_. Code_Eval.term_of j)))"
instance ..
--- a/src/HOL/Random.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Random.thy Tue May 19 16:54:55 2009 +0200
@@ -3,7 +3,7 @@
header {* A HOL random engine *}
theory Random
-imports Code_Index List
+imports Code_Numeral List
begin
notation fcomp (infixl "o>" 60)
@@ -12,21 +12,21 @@
subsection {* Auxiliary functions *}
-definition inc_shift :: "index \<Rightarrow> index \<Rightarrow> index" where
+definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"inc_shift v k = (if v = k then 1 else k + 1)"
-definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where
+definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"minus_shift r k l = (if k < l then r + k - l else k - l)"
-fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
+fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
"log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
subsection {* Random seeds *}
-types seed = "index \<times> index"
+types seed = "code_numeral \<times> code_numeral"
-primrec "next" :: "seed \<Rightarrow> index \<times> seed" where
+primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
"next (v, w) = (let
k = v div 53668;
v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
@@ -55,10 +55,10 @@
subsection {* Base selectors *}
-fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
"iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
-definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
+definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
"range k = iterate (log 2147483561 k)
(\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
o\<rightarrow> (\<lambda>v. Pair (v mod k))"
@@ -68,23 +68,23 @@
by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
- "select xs = range (Code_Index.of_nat (length xs))
- o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
+ "select xs = range (Code_Numeral.of_nat (length xs))
+ o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
lemma select:
assumes "xs \<noteq> []"
shows "fst (select xs s) \<in> set xs"
proof -
- from assms have "Code_Index.of_nat (length xs) > 0" by simp
+ from assms have "Code_Numeral.of_nat (length xs) > 0" by simp
with range have
- "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
+ "fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" by best
then have
- "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
+ "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
then show ?thesis
by (simp add: scomp_apply split_beta select_def)
qed
-primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
+primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
"pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
lemma pick_member:
@@ -96,14 +96,14 @@
by (induct xs) (auto simp add: expand_fun_eq)
lemma pick_same:
- "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Index.of_nat l) = nth xs l"
+ "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l"
proof (induct xs arbitrary: l)
case Nil then show ?case by simp
next
case (Cons x xs) then show ?case by (cases l) simp_all
qed
-definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
"select_weight xs = range (listsum (map fst xs))
o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
@@ -130,16 +130,16 @@
assumes "xs \<noteq> []"
shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
proof -
- have less: "\<And>s. fst (Random.range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)"
+ have less: "\<And>s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
using assms by (intro range) simp
- moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Index.of_nat (length xs)"
+ moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
by (induct xs) simp_all
ultimately show ?thesis
by (auto simp add: select_weight_def select_def scomp_def split_def
expand_fun_eq pick_same [symmetric])
qed
-definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+definition select_default :: "code_numeral \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
[code del]: "select_default k x y = range k
o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
@@ -153,7 +153,7 @@
else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
proof
fix s
- have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
+ have "snd (range (Code_Numeral.of_nat 0) s) = snd (range (Code_Numeral.of_nat 1) s)"
by (simp add: range_def scomp_Pair scomp_apply split_beta)
then show "select_default k x y s = (if k = 0
then range 1 o\<rightarrow> (\<lambda>_. Pair y)
--- a/src/HOL/Rational.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Rational.thy Tue May 19 16:54:55 2009 +0200
@@ -1013,7 +1013,7 @@
definition
"random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
- let j = Code_Index.int_of (denom + 1)
+ let j = Code_Numeral.int_of (denom + 1)
in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
instance ..
--- a/src/HOL/String.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/String.thy Tue May 19 16:54:55 2009 +0200
@@ -85,15 +85,14 @@
subsection {* Strings as dedicated datatype *}
-datatype message_string = STR string
+datatype literal = STR string
-lemmas [code del] =
- message_string.recs message_string.cases
+lemmas [code del] = literal.recs literal.cases
-lemma [code]: "size (s\<Colon>message_string) = 0"
+lemma [code]: "size (s\<Colon>literal) = 0"
by (cases s) simp_all
-lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
+lemma [code]: "literal_size (s\<Colon>literal) = 0"
by (cases s) simp_all
@@ -101,19 +100,19 @@
use "Tools/string_code.ML"
-code_type message_string
+code_type literal
(SML "string")
(OCaml "string")
(Haskell "String")
setup {*
- fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
+ fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
*}
-code_instance message_string :: eq
+code_instance literal :: eq
(Haskell -)
-code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
(SML "!((_ : string) = _)")
(OCaml "!((_ : string) = _)")
(Haskell infixl 4 "==")
@@ -147,4 +146,6 @@
in Codegen.add_codegen "char_codegen" char_codegen end
*}
+hide (open) type literal
+
end
\ No newline at end of file
--- a/src/HOL/Tools/hologic.ML Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Tue May 19 16:54:55 2009 +0200
@@ -87,7 +87,7 @@
val dest_nat: term -> int
val class_size: string
val size_const: typ -> term
- val indexT: typ
+ val code_numeralT: typ
val intT: typ
val pls_const: term
val min_const: term
@@ -116,9 +116,9 @@
val stringT: typ
val mk_string: string -> term
val dest_string: term -> string
- val message_stringT: typ
- val mk_message_string: string -> term
- val dest_message_string: term -> string
+ val literalT: typ
+ val mk_literal: string -> term
+ val dest_literal: term -> string
val mk_typerep: typ -> term
val mk_term_of: typ -> term -> term
val reflect_term: term -> term
@@ -461,9 +461,9 @@
fun size_const T = Const ("Nat.size_class.size", T --> natT);
-(* index *)
+(* code numeral *)
-val indexT = Type ("Code_Index.index", []);
+val code_numeralT = Type ("Code_Numeral.code_numeral", []);
(* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
@@ -586,15 +586,15 @@
val dest_string = implode o map (chr o dest_char) o dest_list;
-(* message_string *)
+(* literal *)
-val message_stringT = Type ("String.message_string", []);
+val literalT = Type ("String.literal", []);
-fun mk_message_string s = Const ("String.message_string.STR", stringT --> message_stringT)
+fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
$ mk_string s;
-fun dest_message_string (Const ("String.message_string.STR", _) $ t) =
+fun dest_literal (Const ("String.literal.STR", _) $ t) =
dest_string t
- | dest_message_string t = raise TERM ("dest_message_string", [t]);
+ | dest_literal t = raise TERM ("dest_literal", [t]);
(* typerep and term *)
@@ -609,8 +609,8 @@
fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
fun reflect_term (Const (c, T)) =
- Const ("Code_Eval.Const", message_stringT --> typerepT --> termT)
- $ mk_message_string c $ mk_typerep T
+ Const ("Code_Eval.Const", literalT --> typerepT --> termT)
+ $ mk_literal c $ mk_typerep T
| reflect_term (t1 $ t2) =
Const ("Code_Eval.App", termT --> termT --> termT)
$ reflect_term t1 $ reflect_term t2
--- a/src/HOL/Tools/string_code.ML Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Tools/string_code.ML Tue May 19 16:54:55 2009 +0200
@@ -7,7 +7,7 @@
sig
val add_literal_list_string: string -> theory -> theory
val add_literal_char: string -> theory -> theory
- val add_literal_message: string -> theory -> theory
+ val add_literal_string: string -> theory -> theory
end;
structure String_Code : STRING_CODE =
@@ -72,7 +72,7 @@
@{const_name Char} (SOME (2, (cs_nibbles, pretty)))
end;
-fun add_literal_message target =
+fun add_literal_string target =
let
fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
case List_Code.implode_list nil' cons' t
--- a/src/HOL/Typerep.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Typerep.thy Tue May 19 16:54:55 2009 +0200
@@ -6,7 +6,7 @@
imports Plain String
begin
-datatype typerep = Typerep message_string "typerep list"
+datatype typerep = Typerep String.literal "typerep list"
class typerep =
fixes typerep :: "'a itself \<Rightarrow> typerep"
@@ -45,7 +45,7 @@
val ty = Type (tyco, map TFree vs);
val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
$ Free ("T", Term.itselfT ty);
- val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco
+ val rhs = @{term Typerep} $ HOLogic.mk_literal tyco
$ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
in