author | haftmann |
Tue, 01 Jun 2010 10:30:53 +0200 | |
changeset 37221 | 4d984bc33c66 |
parent 33226 | a5eba0447559 |
child 37434 | 7a3610dca96b |
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@32657 | 8 |
imports List Code_Evaluation 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@37221 | 15 |
(Scala "Char") |
haftmann@24999 | 16 |
|
haftmann@24999 | 17 |
setup {* |
haftmann@37221 | 18 |
fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] |
haftmann@31053 | 19 |
#> String_Code.add_literal_list_string "Haskell" |
haftmann@24999 | 20 |
*} |
haftmann@24999 | 21 |
|
haftmann@24999 | 22 |
code_instance char :: eq |
haftmann@24999 | 23 |
(Haskell -) |
haftmann@24999 | 24 |
|
haftmann@24999 | 25 |
code_reserved SML |
haftmann@24999 | 26 |
char |
haftmann@24999 | 27 |
|
haftmann@24999 | 28 |
code_reserved OCaml |
haftmann@24999 | 29 |
char |
haftmann@24999 | 30 |
|
haftmann@37221 | 31 |
code_reserved Scala |
haftmann@37221 | 32 |
char |
haftmann@37221 | 33 |
|
haftmann@28346 | 34 |
code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
haftmann@24999 | 35 |
(SML "!((_ : char) = _)") |
haftmann@24999 | 36 |
(OCaml "!((_ : char) = _)") |
haftmann@24999 | 37 |
(Haskell infixl 4 "==") |
haftmann@37221 | 38 |
(Scala infixl 5 "==") |
haftmann@24999 | 39 |
|
haftmann@32657 | 40 |
code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" |
haftmann@31046 | 41 |
(Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") |
haftmann@28228 | 42 |
|
haftmann@33226 | 43 |
|
haftmann@33226 | 44 |
definition implode :: "string \<Rightarrow> String.literal" where |
haftmann@33226 | 45 |
"implode = STR" |
haftmann@33226 | 46 |
|
haftmann@33226 | 47 |
primrec explode :: "String.literal \<Rightarrow> string" where |
haftmann@33226 | 48 |
"explode (STR s) = s" |
haftmann@33226 | 49 |
|
haftmann@33226 | 50 |
lemma [code]: |
haftmann@33226 | 51 |
"literal_case f s = f (explode s)" |
haftmann@33226 | 52 |
"literal_rec f s = f (explode s)" |
haftmann@33226 | 53 |
by (cases s, simp)+ |
haftmann@33226 | 54 |
|
haftmann@33226 | 55 |
code_reserved SML String |
haftmann@33226 | 56 |
|
haftmann@33226 | 57 |
code_const implode |
haftmann@33226 | 58 |
(SML "String.implode") |
haftmann@33226 | 59 |
(OCaml "failwith/ \"implode\"") |
haftmann@33226 | 60 |
(Haskell "_") |
haftmann@37221 | 61 |
(Scala "List.toString((_))") |
haftmann@33226 | 62 |
|
haftmann@33226 | 63 |
code_const explode |
haftmann@33226 | 64 |
(SML "String.explode") |
haftmann@33226 | 65 |
(OCaml "failwith/ \"explode\"") |
haftmann@33226 | 66 |
(Haskell "_") |
haftmann@37221 | 67 |
(Scala "List.fromString((_))") |
haftmann@33226 | 68 |
|
haftmann@24999 | 69 |
end |