author | wenzelm |
Tue, 03 Sep 2013 01:12:40 +0200 | |
changeset 53374 | a14d2a854c02 |
parent 52435 | 6646bb548c6b |
child 54596 | 368c70ee1f46 |
permissions | -rw-r--r-- |
24999 | 1 |
(* Title: HOL/Library/Code_Char.thy |
2 |
Author: Florian Haftmann |
|
3 |
*) |
|
4 |
||
5 |
header {* Code generation of pretty characters (and strings) *} |
|
6 |
||
7 |
theory Code_Char |
|
51542 | 8 |
imports Main Char_ord |
24999 | 9 |
begin |
10 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
11 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
12 |
type_constructor char \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
13 |
(SML) "char" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
14 |
and (OCaml) "char" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
15 |
and (Haskell) "Prelude.Char" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
16 |
and (Scala) "Char" |
24999 | 17 |
|
18 |
setup {* |
|
37222 | 19 |
fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] |
31053 | 20 |
#> String_Code.add_literal_list_string "Haskell" |
24999 | 21 |
*} |
22 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
23 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
24 |
class_instance char :: equal \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
25 |
(Haskell) - |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
26 |
| constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
27 |
(SML) "!((_ : char) = _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
28 |
and (OCaml) "!((_ : char) = _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
29 |
and (Haskell) infix 4 "==" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
30 |
and (Scala) infixl 5 "==" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
31 |
| constant "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
32 |
(Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))" |
24999 | 33 |
|
34 |
code_reserved SML |
|
35 |
char |
|
36 |
||
37 |
code_reserved OCaml |
|
38 |
char |
|
39 |
||
37222 | 40 |
code_reserved Scala |
41 |
char |
|
42 |
||
33234 | 43 |
definition implode :: "string \<Rightarrow> String.literal" where |
44 |
"implode = STR" |
|
45 |
||
46 |
code_reserved SML String |
|
47 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
48 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
49 |
constant implode \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
50 |
(SML) "String.implode" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
51 |
and (OCaml) "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
52 |
and (Haskell) "_" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
53 |
and (Scala) "!(\"\" ++/ _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
54 |
| constant explode \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
55 |
(SML) "String.explode" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
56 |
and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
57 |
and (Haskell) "_" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
58 |
and (Scala) "!(_.toList)" |
33234 | 59 |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
60 |
|
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
61 |
definition integer_of_char :: "char \<Rightarrow> integer" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
62 |
where |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
63 |
"integer_of_char = integer_of_nat o nat_of_char" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
64 |
|
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
65 |
definition char_of_integer :: "integer \<Rightarrow> char" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
66 |
where |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
67 |
"char_of_integer = char_of_nat \<circ> nat_of_integer" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
68 |
|
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
69 |
lemma [code]: |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
70 |
"nat_of_char = nat_of_integer o integer_of_char" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
71 |
by (simp add: integer_of_char_def fun_eq_iff) |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
72 |
|
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
73 |
lemma [code]: |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
74 |
"char_of_nat = char_of_integer o integer_of_nat" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
75 |
by (simp add: char_of_integer_def fun_eq_iff) |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
76 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
77 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
78 |
constant integer_of_char \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
79 |
(SML) "!(IntInf.fromInt o Char.ord)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
80 |
and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
81 |
and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
82 |
and (Scala) "BigInt(_.toInt)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
83 |
| constant char_of_integer \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
84 |
(SML) "!(Char.chr o IntInf.toInt)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
85 |
and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
86 |
and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
87 |
and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
88 |
| constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
89 |
(SML) "!((_ : char) <= _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
90 |
and (OCaml) "!((_ : char) <= _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
91 |
and (Haskell) infix 4 "<=" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
92 |
and (Scala) infixl 4 "<=" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
93 |
and (Eval) infixl 6 "<=" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
94 |
| constant "Orderings.less :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
95 |
(SML) "!((_ : char) < _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
96 |
and (OCaml) "!((_ : char) < _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
97 |
and (Haskell) infix 4 "<" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
98 |
and (Scala) infixl 4 "<" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51542
diff
changeset
|
99 |
and (Eval) infixl 6 "<" |
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
100 |
|
24999 | 101 |
end |
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48431
diff
changeset
|
102 |