author | haftmann |
Tue, 02 Sep 2008 20:38:17 +0200 | |
changeset 28090 | 29af3c712d2b |
parent 28064 | d4a6460c53d1 |
child 28228 | 7ebe8dc06cbb |
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 |
|
27487 | 9 |
imports Plain "~~/src/HOL/List" |
24999 | 10 |
begin |
11 |
||
25965 | 12 |
declare char.recs [code func del] char.cases [code func del] |
13 |
||
14 |
lemma [code func]: |
|
15 |
"size (c\<Colon>char) = 0" |
|
16 |
by (cases c) simp |
|
17 |
||
18 |
lemma [code func]: |
|
19 |
"char_size (c\<Colon>char) = 0" |
|
20 |
by (cases c) simp |
|
21 |
||
24999 | 22 |
code_type char |
23 |
(SML "char") |
|
24 |
(OCaml "char") |
|
25 |
(Haskell "Char") |
|
26 |
||
27 |
setup {* |
|
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
28 |
fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"] |
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
29 |
#> add_literal_list_string "Haskell" |
24999 | 30 |
*} |
31 |
||
32 |
code_instance char :: eq |
|
33 |
(Haskell -) |
|
34 |
||
35 |
code_reserved SML |
|
36 |
char |
|
37 |
||
38 |
code_reserved OCaml |
|
39 |
char |
|
40 |
||
41 |
code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
|
42 |
(SML "!((_ : char) = _)") |
|
43 |
(OCaml "!((_ : char) = _)") |
|
44 |
(Haskell infixl 4 "==") |
|
45 |
||
46 |
end |