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