author | haftmann |
Tue, 02 Sep 2008 20:38:17 +0200 | |
changeset 28090 | 29af3c712d2b |
parent 28064 | d4a6460c53d1 |
child 28228 | 7ebe8dc06cbb |
permissions | -rw-r--r-- |
haftmann@24999 | 1 |
(* Title: HOL/Library/Code_Char.thy |
haftmann@24999 | 2 |
ID: $Id$ |
haftmann@24999 | 3 |
Author: Florian Haftmann |
haftmann@24999 | 4 |
*) |
haftmann@24999 | 5 |
|
haftmann@24999 | 6 |
header {* Code generation of pretty characters (and strings) *} |
haftmann@24999 | 7 |
|
haftmann@24999 | 8 |
theory Code_Char |
haftmann@27487 | 9 |
imports Plain "~~/src/HOL/List" |
haftmann@24999 | 10 |
begin |
haftmann@24999 | 11 |
|
haftmann@25965 | 12 |
declare char.recs [code func del] char.cases [code func del] |
haftmann@25965 | 13 |
|
haftmann@25965 | 14 |
lemma [code func]: |
haftmann@25965 | 15 |
"size (c\<Colon>char) = 0" |
haftmann@25965 | 16 |
by (cases c) simp |
haftmann@25965 | 17 |
|
haftmann@25965 | 18 |
lemma [code func]: |
haftmann@25965 | 19 |
"char_size (c\<Colon>char) = 0" |
haftmann@25965 | 20 |
by (cases c) simp |
haftmann@25965 | 21 |
|
haftmann@24999 | 22 |
code_type char |
haftmann@24999 | 23 |
(SML "char") |
haftmann@24999 | 24 |
(OCaml "char") |
haftmann@24999 | 25 |
(Haskell "Char") |
haftmann@24999 | 26 |
|
haftmann@24999 | 27 |
setup {* |
haftmann@28090 | 28 |
fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"] |
haftmann@28090 | 29 |
#> add_literal_list_string "Haskell" |
haftmann@24999 | 30 |
*} |
haftmann@24999 | 31 |
|
haftmann@24999 | 32 |
code_instance char :: eq |
haftmann@24999 | 33 |
(Haskell -) |
haftmann@24999 | 34 |
|
haftmann@24999 | 35 |
code_reserved SML |
haftmann@24999 | 36 |
char |
haftmann@24999 | 37 |
|
haftmann@24999 | 38 |
code_reserved OCaml |
haftmann@24999 | 39 |
char |
haftmann@24999 | 40 |
|
haftmann@24999 | 41 |
code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
haftmann@24999 | 42 |
(SML "!((_ : char) = _)") |
haftmann@24999 | 43 |
(OCaml "!((_ : char) = _)") |
haftmann@24999 | 44 |
(Haskell infixl 4 "==") |
haftmann@24999 | 45 |
|
haftmann@24999 | 46 |
end |