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