|
1 (* Title: HOL/Library/Pretty_Char.thy |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann |
|
4 *) |
|
5 |
|
6 header {* Code generation of pretty characters (and strings) *} |
|
7 |
|
8 theory Pretty_Char |
|
9 imports List |
|
10 begin |
|
11 |
|
12 code_type char |
|
13 (SML "char") |
|
14 (OCaml "char") |
|
15 (Haskell "Char") |
|
16 |
|
17 setup {* |
|
18 let |
|
19 val charr = @{const_name Char} |
|
20 val nibbles = [@{const_name Nibble0}, @{const_name Nibble1}, |
|
21 @{const_name Nibble2}, @{const_name Nibble3}, |
|
22 @{const_name Nibble4}, @{const_name Nibble5}, |
|
23 @{const_name Nibble6}, @{const_name Nibble7}, |
|
24 @{const_name Nibble8}, @{const_name Nibble9}, |
|
25 @{const_name NibbleA}, @{const_name NibbleB}, |
|
26 @{const_name NibbleC}, @{const_name NibbleD}, |
|
27 @{const_name NibbleE}, @{const_name NibbleF}]; |
|
28 in |
|
29 fold (fn target => CodegenSerializer.add_pretty_char target charr nibbles) |
|
30 ["SML", "OCaml", "Haskell"] |
|
31 #> CodegenSerializer.add_pretty_list_string "Haskell" |
|
32 @{const_name Nil} @{const_name Cons} charr nibbles |
|
33 end |
|
34 *} |
|
35 |
|
36 code_instance char :: eq |
|
37 (Haskell -) |
|
38 |
|
39 code_reserved SML |
|
40 char |
|
41 |
|
42 code_reserved OCaml |
|
43 char |
|
44 |
|
45 code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
|
46 (SML "!((_ : char) = _)") |
|
47 (OCaml "!((_ : char) = _)") |
|
48 (Haskell infixl 4 "==") |
|
49 |
|
50 end |