author | haftmann |
Thu, 28 Jan 2010 11:48:43 +0100 | |
changeset 34973 | ae634fad947e |
parent 33234 | a5eba0447559 |
child 37222 | 4d984bc33c66 |
permissions | -rw-r--r-- |
24999 | 1 |
(* Title: HOL/Library/Code_Char.thy |
2 |
Author: Florian Haftmann |
|
3 |
*) |
|
4 |
||
5 |
header {* Code generation of pretty characters (and strings) *} |
|
6 |
||
7 |
theory Code_Char |
|
32657 | 8 |
imports List Code_Evaluation Main |
24999 | 9 |
begin |
10 |
||
11 |
code_type char |
|
12 |
(SML "char") |
|
13 |
(OCaml "char") |
|
14 |
(Haskell "Char") |
|
15 |
||
16 |
setup {* |
|
31053 | 17 |
fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] |
18 |
#> String_Code.add_literal_list_string "Haskell" |
|
24999 | 19 |
*} |
20 |
||
21 |
code_instance char :: eq |
|
22 |
(Haskell -) |
|
23 |
||
24 |
code_reserved SML |
|
25 |
char |
|
26 |
||
27 |
code_reserved OCaml |
|
28 |
char |
|
29 |
||
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28244
diff
changeset
|
30 |
code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
24999 | 31 |
(SML "!((_ : char) = _)") |
32 |
(OCaml "!((_ : char) = _)") |
|
33 |
(Haskell infixl 4 "==") |
|
34 |
||
32657 | 35 |
code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" |
31046 | 36 |
(Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") |
28228 | 37 |
|
33234 | 38 |
|
39 |
definition implode :: "string \<Rightarrow> String.literal" where |
|
40 |
"implode = STR" |
|
41 |
||
42 |
primrec explode :: "String.literal \<Rightarrow> string" where |
|
43 |
"explode (STR s) = s" |
|
44 |
||
45 |
lemma [code]: |
|
46 |
"literal_case f s = f (explode s)" |
|
47 |
"literal_rec f s = f (explode s)" |
|
48 |
by (cases s, simp)+ |
|
49 |
||
50 |
code_reserved SML String |
|
51 |
||
52 |
code_const implode |
|
53 |
(SML "String.implode") |
|
54 |
(OCaml "failwith/ \"implode\"") |
|
55 |
(Haskell "_") |
|
56 |
||
57 |
code_const explode |
|
58 |
(SML "String.explode") |
|
59 |
(OCaml "failwith/ \"explode\"") |
|
60 |
(Haskell "_") |
|
61 |
||
24999 | 62 |
end |