| author | haftmann |
| Fri, 29 Oct 2010 14:06:10 +0200 | |
| changeset 40268 | af22d99f4446 |
| parent 39272 | 0b61951d2682 |
| child 42231 | bc1891226d00 |
| 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 |
|
| 32657 | 8 |
imports List Code_Evaluation Main |
| 24999 | 9 |
begin |
10 |
||
11 |
code_type char |
|
12 |
(SML "char") |
|
13 |
(OCaml "char") |
|
14 |
(Haskell "Char") |
|
| 37222 | 15 |
(Scala "Char") |
| 24999 | 16 |
|
17 |
setup {*
|
|
| 37222 | 18 |
fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] |
| 31053 | 19 |
#> String_Code.add_literal_list_string "Haskell" |
| 24999 | 20 |
*} |
21 |
||
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37459
diff
changeset
|
22 |
code_instance char :: equal |
| 24999 | 23 |
(Haskell -) |
24 |
||
25 |
code_reserved SML |
|
26 |
char |
|
27 |
||
28 |
code_reserved OCaml |
|
29 |
char |
|
30 |
||
| 37222 | 31 |
code_reserved Scala |
32 |
char |
|
33 |
||
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37459
diff
changeset
|
34 |
code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
| 24999 | 35 |
(SML "!((_ : char) = _)") |
36 |
(OCaml "!((_ : char) = _)") |
|
| 39272 | 37 |
(Haskell infix 4 "==") |
| 37222 | 38 |
(Scala infixl 5 "==") |
| 24999 | 39 |
|
| 32657 | 40 |
code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" |
| 31046 | 41 |
(Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") |
| 28228 | 42 |
|
| 33234 | 43 |
|
44 |
definition implode :: "string \<Rightarrow> String.literal" where |
|
45 |
"implode = STR" |
|
46 |
||
47 |
code_reserved SML String |
|
48 |
||
49 |
code_const implode |
|
50 |
(SML "String.implode") |
|
51 |
(OCaml "failwith/ \"implode\"") |
|
52 |
(Haskell "_") |
|
| 37459 | 53 |
(Scala "!(\"\" ++/ _)") |
| 33234 | 54 |
|
55 |
code_const explode |
|
56 |
(SML "String.explode") |
|
57 |
(OCaml "failwith/ \"explode\"") |
|
58 |
(Haskell "_") |
|
| 37459 | 59 |
(Scala "!(_.toList)") |
| 33234 | 60 |
|
| 24999 | 61 |
end |