wneuper/isa: src/HOL/Library/Code

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

     2     ID:         $Id$

     3     Author:     Florian Haftmann

     4 *)

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

     8 theory Code_Char

     9 imports Plain List

    10 begin

    12 declare char.recs [code func del] char.cases [code func del]

    14 lemma [code func]:

    15   "size (c\<Colon>char) = 0"

    16   by (cases c) simp

    18 lemma [code func]:

    19   "char_size (c\<Colon>char) = 0"

    20   by (cases c) simp

    22 code_type char

    23   (SML "char")

    24   (OCaml "char")

    25   (Haskell "Char")

    27 setup {*

    28 let

    29   val charr = @{const_name Char}

    30   val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},

    31     @{const_name Nibble2}, @{const_name Nibble3},

    32     @{const_name Nibble4}, @{const_name Nibble5},

    33     @{const_name Nibble6}, @{const_name Nibble7},

    34     @{const_name Nibble8}, @{const_name Nibble9},

    35     @{const_name NibbleA}, @{const_name NibbleB},

    36     @{const_name NibbleC}, @{const_name NibbleD},

    37     @{const_name NibbleE}, @{const_name NibbleF}];

    38 in

    39   fold (fn target => CodeTarget.add_pretty_char target charr nibbles)

    40     ["SML", "OCaml", "Haskell"]

    41   #> CodeTarget.add_pretty_list_string "Haskell"

    42     @{const_name Nil} @{const_name Cons} charr nibbles

    43 end

    44 *}

    46 code_instance char :: eq

    47   (Haskell -)

    49 code_reserved SML

    50   char

    52 code_reserved OCaml

    53   char

    55 code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"

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

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

    58   (Haskell infixl 4 "==")

    60 end

author	haftmann
	Thu, 26 Jun 2008 10:07:01 +0200
changeset 27368	9f90ac19e32b
parent 25965	05df64f786a4
child 27487	c8a6ce181805
permissions	-rw-r--r--