| author | wenzelm |
| Thu, 23 Oct 2008 15:28:05 +0200 | |
| changeset 28675 | fb68c0767004 |
| parent 28346 | b8390cd56b8f |
| child 30007 | 74d83bd18977 |
| permissions | -rw-r--r-- |
| 24999 | 1 |
(* Title: HOL/Library/Code_Char.thy |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann |
|
4 |
*) |
|
5 |
||
6 |
header {* Code generation of pretty characters (and strings) *}
|
|
7 |
||
8 |
theory Code_Char |
|
| 28228 | 9 |
imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval" |
| 24999 | 10 |
begin |
11 |
||
12 |
code_type char |
|
13 |
(SML "char") |
|
14 |
(OCaml "char") |
|
15 |
(Haskell "Char") |
|
16 |
||
17 |
setup {*
|
|
|
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
18 |
fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"] |
|
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
19 |
#> add_literal_list_string "Haskell" |
| 24999 | 20 |
*} |
21 |
||
22 |
code_instance char :: eq |
|
23 |
(Haskell -) |
|
24 |
||
25 |
code_reserved SML |
|
26 |
char |
|
27 |
||
28 |
code_reserved OCaml |
|
29 |
char |
|
30 |
||
|
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28244
diff
changeset
|
31 |
code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
| 24999 | 32 |
(SML "!((_ : char) = _)") |
33 |
(OCaml "!((_ : char) = _)") |
|
34 |
(Haskell infixl 4 "==") |
|
35 |
||
| 28228 | 36 |
code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term" |
37 |
(SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") |
|
38 |
||
| 24999 | 39 |
end |