src/HOL/Library/Code_Char.thy
author haftmann
Thu, 25 Sep 2008 09:28:03 +0200
changeset 28346 b8390cd56b8f
parent 28244 f433e544a855
child 30007 74d83bd18977
permissions -rw-r--r--
discontinued special treatment of op = vs. eq_class.eq
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24999
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/Code_Char.thy
haftmann
parents:
diff changeset
     2
    ID:         $Id$
haftmann
parents:
diff changeset
     3
    Author:     Florian Haftmann
haftmann
parents:
diff changeset
     4
*)
haftmann
parents:
diff changeset
     5
haftmann
parents:
diff changeset
     6
header {* Code generation of pretty characters (and strings) *}
haftmann
parents:
diff changeset
     7
haftmann
parents:
diff changeset
     8
theory Code_Char
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 28090
diff changeset
     9
imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
24999
haftmann
parents:
diff changeset
    10
begin
haftmann
parents:
diff changeset
    11
haftmann
parents:
diff changeset
    12
code_type char
haftmann
parents:
diff changeset
    13
  (SML "char")
haftmann
parents:
diff changeset
    14
  (OCaml "char")
haftmann
parents:
diff changeset
    15
  (Haskell "Char")
haftmann
parents:
diff changeset
    16
haftmann
parents:
diff changeset
    17
setup {*
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    18
  fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"] 
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    19
  #> add_literal_list_string "Haskell"
24999
haftmann
parents:
diff changeset
    20
*}
haftmann
parents:
diff changeset
    21
haftmann
parents:
diff changeset
    22
code_instance char :: eq
haftmann
parents:
diff changeset
    23
  (Haskell -)
haftmann
parents:
diff changeset
    24
haftmann
parents:
diff changeset
    25
code_reserved SML
haftmann
parents:
diff changeset
    26
  char
haftmann
parents:
diff changeset
    27
haftmann
parents:
diff changeset
    28
code_reserved OCaml
haftmann
parents:
diff changeset
    29
  char
haftmann
parents:
diff changeset
    30
28346
b8390cd56b8f discontinued special treatment of op = vs. eq_class.eq
haftmann
parents: 28244
diff changeset
    31
code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
24999
haftmann
parents:
diff changeset
    32
  (SML "!((_ : char) = _)")
haftmann
parents:
diff changeset
    33
  (OCaml "!((_ : char) = _)")
haftmann
parents:
diff changeset
    34
  (Haskell infixl 4 "==")
haftmann
parents:
diff changeset
    35
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 28090
diff changeset
    36
code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 28090
diff changeset
    37
  (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 28090
diff changeset
    38
24999
haftmann
parents:
diff changeset
    39
end