# HG changeset patch # User haftmann # Date 1242744895 -7200 # Node ID 98370b26c2ce5b11406f65b388c8fe6aaf05878b # Parent 46c0c741c8c2d61b243bb0380587b80534e0aa43 String.literal replaces message_string, code_numeral replaces (code_)index diff -r 46c0c741c8c2 -r 98370b26c2ce doc-src/Codegen/Thy/Adaptation.thy --- 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} diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Code_Eval.thy --- 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 \ typerep \ term" where +definition Const :: "String.literal \ typerep \ term" where "Const _ _ = dummy_term" definition App :: "term \ term \ 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 \ typerep \ term) = term_of" .. lemma [code, code del]: "(term_of \ term \ term) = term_of" .. -lemma [code, code del]: "(term_of \ message_string \ term) = term_of" .. +lemma [code, code del]: "(term_of \ String.literal \ term) = term_of" .. lemma [code, code del]: "(Code_Eval.term_of \ 'a::{type, term_of} Predicate.pred \ 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 \ message_string \ term" +code_const "term_of \ String.literal \ term" (Eval "HOLogic.mk'_message'_string") code_reserved Eval HOLogic @@ -215,8 +209,8 @@ else termify (uminus :: int \ int) <\> (termify (number_of :: int \ int) <\> 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 \ index) <\> 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 \ code_numeral) <\> term_of_num (2::code_numeral) k" by (simp only: term_of_anything) subsection {* Obfuscate *} diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Code_Index.thy --- 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 \ 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: - "(\n\index. PROP P n) \ (\n\nat. PROP P (of_nat n))" -proof - fix n :: nat - assume "\n\index. PROP P n" - then show "PROP P (of_nat n)" . -next - fix n :: index - assume "\n\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 "\n. k = of_nat n \ P" - shows P - by (rule assms [of "nat_of k"]) simp - -lemma index_induct_raw: - assumes "\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 \ k = l" - by (rule nat_of_inject) - -lemma of_nat_inject [simp]: - "of_nat n = of_nat m \ 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 \ index" Suc_index -proof - - fix P :: "index \ bool" - fix k :: index - assume "P 0" then have init: "P (of_nat 0)" by simp - assume "\k. P k \ P (Suc_index k)" - then have "\n. P (of_nat n) \ P (Suc_index (of_nat n))" . - then have step: "\n. P (of_nat n) \ 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 \ Code_Index.of_nat 0 \ 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 \ 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 \ 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 \ int \ index" - - -subsection {* Basic arithmetic *} - -instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}" -begin - -definition [simp, code del]: - "(1\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 \ m \ nat_of n \ nat_of m" - -definition [simp, code del]: - "n < m \ 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\index) = Numeral0" - by (simp add: number_of_index_def Pls_def) -lemma [code post]: "Numeral0 = (0\index)" - using zero_index_code .. - -lemma one_index_code [code inline, code]: - "(1\index) = Numeral1" - by (simp add: number_of_index_def Pls_def Bit1_def) -lemma [code post]: "Numeral1 = (1\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 \ index \ 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 \ of_nat m \ n \ m" - by simp - -lemma less_index_code [code nbe]: - "of_nat n < of_nat m \ 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 \ of_nat 0 \ i \ 1" - by (cases i) auto - -definition nat_of_aux :: "index \ nat \ 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 \ index \ index \ 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 \ 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 + \ index \ index \ index" - (SML "Int.+/ ((_),/ (_))") - (OCaml "Pervasives.( + )") - (Haskell infixl 6 "+") - -code_const "subtract_index \ index \ index \ index" - (SML "Int.max/ (_/ -/ _,/ 0 : int)") - (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ") - (Haskell "max/ (_/ -/ _)/ (0 :: Int)") - -code_const "op * \ index \ index \ 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 \ index \ index \ bool" - (SML "!((_ : Int.int) = _)") - (OCaml "!((_ : int) = _)") - (Haskell infixl 4 "==") - -code_const "op \ \ index \ index \ bool" - (SML "Int.<=/ ((_),/ (_))") - (OCaml "!((_ : int) <= _)") - (Haskell infix 4 "<=") - -code_const "op < \ index \ index \ bool" - (SML "Int. 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: + "(\n\code_numeral. PROP P n) \ (\n\nat. PROP P (of_nat n))" +proof + fix n :: nat + assume "\n\code_numeral. PROP P n" + then show "PROP P (of_nat n)" . +next + fix n :: code_numeral + assume "\n\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 "\n. k = of_nat n \ P" + shows P + by (rule assms [of "nat_of k"]) simp + +lemma code_numeral_induct_raw: + assumes "\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 \ k = l" + by (rule nat_of_inject) + +lemma of_nat_inject [simp]: + "of_nat n = of_nat m \ 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 \ code_numeral" Suc_code_numeral +proof - + fix P :: "code_numeral \ bool" + fix k :: code_numeral + assume "P 0" then have init: "P (of_nat 0)" by simp + assume "\k. P k \ P (Suc_code_numeral k)" + then have "\n. P (of_nat n) \ P (Suc_code_numeral (of_nat n))" . + then have step: "\n. P (of_nat n) \ 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 \ of_nat 0 \ 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 \ 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 \ 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 \ int \ code_numeral" + + +subsection {* Basic arithmetic *} + +instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}" +begin + +definition [simp, code del]: + "(1\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 \ m \ nat_of n \ nat_of m" + +definition [simp, code del]: + "n < m \ 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\code_numeral) = Numeral0" + by (simp add: number_of_code_numeral_def Pls_def) +lemma [code post]: "Numeral0 = (0\code_numeral)" + using zero_code_numeral_code .. + +lemma one_code_numeral_code [code inline, code]: + "(1\code_numeral) = Numeral1" + by (simp add: number_of_code_numeral_def Pls_def Bit1_def) +lemma [code post]: "Numeral1 = (1\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 \ code_numeral \ 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 \ of_nat m \ n \ m" + by simp + +lemma less_code_numeral_code [code nbe]: + "of_nat n < of_nat m \ 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 \ of_nat 0 \ i \ 1" + by (cases i) auto + +definition nat_of_aux :: "code_numeral \ nat \ 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 \ code_numeral \ code_numeral \ 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 \ 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 + \ code_numeral \ code_numeral \ code_numeral" + (SML "Int.+/ ((_),/ (_))") + (OCaml "Pervasives.( + )") + (Haskell infixl 6 "+") + +code_const "subtract_code_numeral \ code_numeral \ code_numeral \ code_numeral" + (SML "Int.max/ (_/ -/ _,/ 0 : int)") + (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ") + (Haskell "max/ (_/ -/ _)/ (0 :: Int)") + +code_const "op * \ code_numeral \ code_numeral \ 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 \ code_numeral \ code_numeral \ bool" + (SML "!((_ : Int.int) = _)") + (OCaml "!((_ : int) = _)") + (Haskell infixl 4 "==") + +code_const "op \ \ code_numeral \ code_numeral \ bool" + (SML "Int.<=/ ((_),/ (_))") + (OCaml "!((_ : int) <= _)") + (Haskell infix 4 "<=") + +code_const "op < \ code_numeral \ code_numeral \ bool" + (SML "Int.== liftM Code_Index.of_nat" + [code del]: "length' = Array.length \== liftM Code_Numeral.of_nat" hide (open) const length' lemma [code]: - "Array.length = Array.length' \== liftM Code_Index.nat_of" + "Array.length = Array.length' \== 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 \ return ()" + [code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \ return ()" hide (open) const upd' lemma [code]: - "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \ return a" + "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \ return a" by (simp add: upd'_def monad_simp upd_return) diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Imperative_HOL/Heap.thy --- 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 *} diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 \ exception" + Fail :: "String.literal \ exception" where [code del]: "Fail s = Exn" diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/IsaMakefile --- 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 \ diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Library/Code_Integer.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") diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Library/Efficient_Nat.thy --- 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") diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Quickcheck.thy --- 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 \ Random.seed \ ('a \ (unit \ term)) \ Random.seed" + fixes random :: "code_numeral \ Random.seed \ ('a \ (unit \ term)) \ Random.seed" subsection {* Quickcheck generator *} @@ -49,7 +49,7 @@ (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \ 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 \ Random.seed \ ('a itself \ (unit \ term)) \ Random.seed" where +definition random_itself :: "code_numeral \ Random.seed \ ('a itself \ (unit \ term)) \ 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 \ Random.seed \ (('a \ 'b) \ (unit \ term)) \ Random.seed" where +definition random_fun :: "code_numeral \ Random.seed \ (('a \ 'b) \ (unit \ term)) \ 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 \ Random.seed \ (nat \ (unit \ Code_Eval.term)) \ Random.seed" where +definition random_nat :: "code_numeral \ Random.seed \ (nat \ (unit \ Code_Eval.term)) \ Random.seed" where "random_nat i = Random.range (i + 1) o\ (\k. Pair ( - let n = Code_Index.nat_of k + let n = Code_Numeral.nat_of k in (n, \_. Code_Eval.term_of n)))" instance .. @@ -168,7 +168,7 @@ definition "random i = Random.range (2 * i + 1) o\ (\k. Pair ( - let j = (if k \ i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k)) + let j = (if k \ i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k)) in (j, \_. Code_Eval.term_of j)))" instance .. diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Random.thy --- 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 \ index \ index" where +definition inc_shift :: "code_numeral \ code_numeral \ code_numeral" where "inc_shift v k = (if v = k then 1 else k + 1)" -definition minus_shift :: "index \ index \ index \ index" where +definition minus_shift :: "code_numeral \ code_numeral \ code_numeral \ code_numeral" where "minus_shift r k l = (if k < l then r + k - l else k - l)" -fun log :: "index \ index \ index" where +fun log :: "code_numeral \ code_numeral \ code_numeral" where "log b i = (if b \ 1 \ i < b then 1 else 1 + log b (i div b))" subsection {* Random seeds *} -types seed = "index \ index" +types seed = "code_numeral \ code_numeral" -primrec "next" :: "seed \ index \ seed" where +primrec "next" :: "seed \ code_numeral \ 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 \ ('b \ 'a \ 'b \ 'a) \ 'b \ 'a \ 'b \ 'a" where +fun iterate :: "code_numeral \ ('b \ 'a \ 'b \ 'a) \ 'b \ 'a \ 'b \ 'a" where "iterate k f x = (if k = 0 then Pair x else f x o\ iterate (k - 1) f)" -definition range :: "index \ seed \ index \ seed" where +definition range :: "code_numeral \ seed \ code_numeral \ seed" where "range k = iterate (log 2147483561 k) (\l. next o\ (\v. Pair (v + l * 2147483561))) 1 o\ (\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 \ seed \ 'a \ seed" where - "select xs = range (Code_Index.of_nat (length xs)) - o\ (\k. Pair (nth xs (Code_Index.nat_of k)))" + "select xs = range (Code_Numeral.of_nat (length xs)) + o\ (\k. Pair (nth xs (Code_Numeral.nat_of k)))" lemma select: assumes "xs \ []" shows "fst (select xs s) \ 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 \ 'a) list \ index \ 'a" where +primrec pick :: "(code_numeral \ 'a) list \ code_numeral \ '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 \ Random.pick (map (Pair 1) xs) (Code_Index.of_nat l) = nth xs l" + "l < length xs \ 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 \ 'a) list \ seed \ 'a \ seed" where +definition select_weight :: "(code_numeral \ 'a) list \ seed \ 'a \ seed" where "select_weight xs = range (listsum (map fst xs)) o\ (\k. Pair (pick xs k))" @@ -130,16 +130,16 @@ assumes "xs \ []" shows "Random.select_weight (map (Pair 1) xs) = Random.select xs" proof - - have less: "\s. fst (Random.range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" + have less: "\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 \ 'a \ 'a \ seed \ 'a \ seed" where +definition select_default :: "code_numeral \ 'a \ 'a \ seed \ 'a \ seed" where [code del]: "select_default k x y = range k o\ (\l. Pair (if l + 1 < k then x else y))" @@ -153,7 +153,7 @@ else range k o\ (\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\ (\_. Pair y) diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Rational.thy --- 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\ (\num. Random.range i o\ (\denom. Pair ( - let j = Code_Index.int_of (denom + 1) + let j = Code_Numeral.int_of (denom + 1) in valterm_fract num (j, \u. Code_Eval.term_of j))))" instance .. diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/String.thy --- 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\message_string) = 0" +lemma [code]: "size (s\literal) = 0" by (cases s) simp_all -lemma [code]: "message_string_size (s\message_string) = 0" +lemma [code]: "literal_size (s\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 \ message_string \ message_string \ bool" +code_const "eq_class.eq \ literal \ literal \ 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 diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Tools/hologic.ML --- 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 diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Tools/string_code.ML --- 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 diff -r 46c0c741c8c2 -r 98370b26c2ce src/HOL/Typerep.thy --- 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 \ 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