wneuper/isa: src/HOL/Library/Code

     1 (*  Title:      HOL/Library/Code_Char.thy

     2     Author:     Florian Haftmann

     3 *)

     5 header {* Code generation of pretty characters (and strings) *}

     7 theory Code_Char

     8 imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"

     9 begin

    11 code_type char

    12   (SML "char")

    13   (OCaml "char")

    14   (Haskell "Char")

    16 setup {*

    17   fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"]

    18   #> add_literal_list_string "Haskell"

    19 *}

    21 code_instance char :: eq

    22   (Haskell -)

    24 code_reserved SML

    25   char

    27 code_reserved OCaml

    28   char

    30 code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"

    31   (SML "!((_ : char) = _)")

    32   (OCaml "!((_ : char) = _)")

    33   (Haskell infixl 4 "==")

    35 code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"

    36   (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")

    38 end

author	haftmann
	Fri, 20 Feb 2009 10:14:31 +0100
changeset 29944	74d83bd18977
parent 28346	b8390cd56b8f
child 30663	0b6aff7451b2
permissions	-rw-r--r--