author | haftmann |
Fri, 10 Aug 2007 17:04:34 +0200 | |
changeset 24219 | e558fe311376 |
parent 22799 | ed7d53db2170 |
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 |
24219 | 29 |
fold (fn target => CodeTarget.add_pretty_char target charr nibbles) |
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
diff
changeset
|
30 |
["SML", "OCaml", "Haskell"] |
24219 | 31 |
#> CodeTarget.add_pretty_list_string "Haskell" |
22799
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 |