| author | haftmann |
| Wed, 06 May 2009 16:01:05 +0200 | |
| changeset 31046 | c1969f609bf7 |
| parent 30663 | 0b6aff7451b2 |
| child 31053 | b7e1c065b6e4 |
| permissions | -rw-r--r-- |
| haftmann@24999 | 1 |
(* Title: HOL/Library/Code_Char.thy |
| haftmann@24999 | 2 |
Author: Florian Haftmann |
| haftmann@24999 | 3 |
*) |
| haftmann@24999 | 4 |
|
| haftmann@24999 | 5 |
header {* Code generation of pretty characters (and strings) *}
|
| haftmann@24999 | 6 |
|
| haftmann@24999 | 7 |
theory Code_Char |
| haftmann@30663 | 8 |
imports List Code_Eval Main |
| haftmann@24999 | 9 |
begin |
| haftmann@24999 | 10 |
|
| haftmann@24999 | 11 |
code_type char |
| haftmann@24999 | 12 |
(SML "char") |
| haftmann@24999 | 13 |
(OCaml "char") |
| haftmann@24999 | 14 |
(Haskell "Char") |
| haftmann@24999 | 15 |
|
| haftmann@24999 | 16 |
setup {*
|
| haftmann@28090 | 17 |
fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"] |
| haftmann@28090 | 18 |
#> add_literal_list_string "Haskell" |
| haftmann@24999 | 19 |
*} |
| haftmann@24999 | 20 |
|
| haftmann@24999 | 21 |
code_instance char :: eq |
| haftmann@24999 | 22 |
(Haskell -) |
| haftmann@24999 | 23 |
|
| haftmann@24999 | 24 |
code_reserved SML |
| haftmann@24999 | 25 |
char |
| haftmann@24999 | 26 |
|
| haftmann@24999 | 27 |
code_reserved OCaml |
| haftmann@24999 | 28 |
char |
| haftmann@24999 | 29 |
|
| haftmann@28346 | 30 |
code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
| haftmann@24999 | 31 |
(SML "!((_ : char) = _)") |
| haftmann@24999 | 32 |
(OCaml "!((_ : char) = _)") |
| haftmann@24999 | 33 |
(Haskell infixl 4 "==") |
| haftmann@24999 | 34 |
|
| haftmann@28228 | 35 |
code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term" |
| haftmann@31046 | 36 |
(Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") |
| haftmann@28228 | 37 |
|
| haftmann@24999 | 38 |
end |