added
authorhaftmann
Fri Oct 12 10:26:18 2007 +0200 (2007-10-12)
changeset 249991dbe785ed529
parent 24998 a339b33adfaf
child 25000 1ab44e69652f
added
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Char_chr.thy
src/HOL/Library/Code_Index.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Code_Message.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Fri Oct 12 10:26:18 2007 +0200
     1.3 @@ -0,0 +1,50 @@
     1.4 +(*  Title:      HOL/Library/Code_Char.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Haftmann
     1.7 +*)
     1.8 +
     1.9 +header {* Code generation of pretty characters (and strings) *}
    1.10 +
    1.11 +theory Code_Char
    1.12 +imports List
    1.13 +begin
    1.14 +
    1.15 +code_type char
    1.16 +  (SML "char")
    1.17 +  (OCaml "char")
    1.18 +  (Haskell "Char")
    1.19 +
    1.20 +setup {*
    1.21 +let
    1.22 +  val charr = @{const_name Char}
    1.23 +  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    1.24 +    @{const_name Nibble2}, @{const_name Nibble3},
    1.25 +    @{const_name Nibble4}, @{const_name Nibble5},
    1.26 +    @{const_name Nibble6}, @{const_name Nibble7},
    1.27 +    @{const_name Nibble8}, @{const_name Nibble9},
    1.28 +    @{const_name NibbleA}, @{const_name NibbleB},
    1.29 +    @{const_name NibbleC}, @{const_name NibbleD},
    1.30 +    @{const_name NibbleE}, @{const_name NibbleF}];
    1.31 +in
    1.32 +  fold (fn target => CodeTarget.add_pretty_char target charr nibbles)
    1.33 +    ["SML", "OCaml", "Haskell"]
    1.34 +  #> CodeTarget.add_pretty_list_string "Haskell"
    1.35 +    @{const_name Nil} @{const_name Cons} charr nibbles
    1.36 +end
    1.37 +*}
    1.38 +
    1.39 +code_instance char :: eq
    1.40 +  (Haskell -)
    1.41 +
    1.42 +code_reserved SML
    1.43 +  char
    1.44 +
    1.45 +code_reserved OCaml
    1.46 +  char
    1.47 +
    1.48 +code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.49 +  (SML "!((_ : char) = _)")
    1.50 +  (OCaml "!((_ : char) = _)")
    1.51 +  (Haskell infixl 4 "==")
    1.52 +
    1.53 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Fri Oct 12 10:26:18 2007 +0200
     2.3 @@ -0,0 +1,45 @@
     2.4 +(*  Title:      HOL/Library/Code_Char_chr.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Florian Haftmann
     2.7 +*)
     2.8 +
     2.9 +header {* Code generation of pretty characters with character codes *}
    2.10 +
    2.11 +theory Code_Char_chr
    2.12 +imports Char_nat Code_Char Code_Integer
    2.13 +begin
    2.14 +
    2.15 +definition
    2.16 +  "int_of_char = int o nat_of_char"
    2.17 +
    2.18 +lemma [code func]:
    2.19 +  "nat_of_char = nat o int_of_char"
    2.20 +  unfolding int_of_char_def by (simp add: expand_fun_eq)
    2.21 +
    2.22 +definition
    2.23 +  "char_of_int = char_of_nat o nat"
    2.24 +
    2.25 +lemma [code func]:
    2.26 +  "char_of_nat = char_of_int o int"
    2.27 +  unfolding char_of_int_def by (simp add: expand_fun_eq)
    2.28 +
    2.29 +lemmas [code func del] = char.recs char.cases char.size
    2.30 +
    2.31 +lemma [code func, code inline]:
    2.32 +  "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
    2.33 +  by (cases c) (auto simp add: nibble_pair_of_nat_char)
    2.34 +
    2.35 +lemma [code func, code inline]:
    2.36 +  "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
    2.37 +  by (cases c) (auto simp add: nibble_pair_of_nat_char)
    2.38 +
    2.39 +lemma [code func]:
    2.40 +  "size (c\<Colon>char) = 0"
    2.41 +  by (cases c) auto
    2.42 +
    2.43 +code_const int_of_char and char_of_int
    2.44 +  (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
    2.45 +  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
    2.46 +  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
    2.47 +
    2.48 +end
    2.49 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Code_Index.thy	Fri Oct 12 10:26:18 2007 +0200
     3.3 @@ -0,0 +1,255 @@
     3.4 +(*  ID:         $Id$
     3.5 +    Author:     Florian Haftmann, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +header {* Type of indices *}
     3.9 +
    3.10 +theory Code_Index
    3.11 +imports PreList
    3.12 +begin
    3.13 +
    3.14 +text {*
    3.15 +  Indices are isomorphic to HOL @{typ int} but
    3.16 +  mapped to target-language builtin integers
    3.17 +*}
    3.18 +
    3.19 +subsection {* Datatype of indices *}
    3.20 +
    3.21 +datatype index = index_of_int int
    3.22 +
    3.23 +lemmas [code func del] = index.recs index.cases
    3.24 +
    3.25 +fun
    3.26 +  int_of_index :: "index \<Rightarrow> int"
    3.27 +where
    3.28 +  "int_of_index (index_of_int k) = k"
    3.29 +lemmas [code func del] = int_of_index.simps
    3.30 +
    3.31 +lemma index_id [simp]:
    3.32 +  "index_of_int (int_of_index k) = k"
    3.33 +  by (cases k) simp_all
    3.34 +
    3.35 +lemma index:
    3.36 +  "(\<And>k\<Colon>index. PROP P k) \<equiv> (\<And>k\<Colon>int. PROP P (index_of_int k))"
    3.37 +proof
    3.38 +  fix k :: int
    3.39 +  assume "\<And>k\<Colon>index. PROP P k"
    3.40 +  then show "PROP P (index_of_int k)" .
    3.41 +next
    3.42 +  fix k :: index
    3.43 +  assume "\<And>k\<Colon>int. PROP P (index_of_int k)"
    3.44 +  then have "PROP P (index_of_int (int_of_index k))" .
    3.45 +  then show "PROP P k" by simp
    3.46 +qed
    3.47 +
    3.48 +lemma [code func]: "size (k\<Colon>index) = 0"
    3.49 +  by (cases k) simp_all
    3.50 +
    3.51 +
    3.52 +subsection {* Built-in integers as datatype on numerals *}
    3.53 +
    3.54 +instance index :: number
    3.55 +  "number_of \<equiv> index_of_int" ..
    3.56 +
    3.57 +code_datatype "number_of \<Colon> int \<Rightarrow> index"
    3.58 +
    3.59 +lemma number_of_index_id [simp]:
    3.60 +  "number_of (int_of_index k) = k"
    3.61 +  unfolding number_of_index_def by simp
    3.62 +
    3.63 +lemma number_of_index_shift:
    3.64 +  "number_of k = index_of_int (number_of k)"
    3.65 +  by (simp add: number_of_is_id number_of_index_def)
    3.66 +
    3.67 +
    3.68 +subsection {* Basic arithmetic *}
    3.69 +
    3.70 +instance index :: zero
    3.71 +  [simp]: "0 \<equiv> index_of_int 0" ..
    3.72 +lemmas [code func del] = zero_index_def
    3.73 +
    3.74 +instance index :: one
    3.75 +  [simp]: "1 \<equiv> index_of_int 1" ..
    3.76 +lemmas [code func del] = one_index_def
    3.77 +
    3.78 +instance index :: plus
    3.79 +  [simp]: "k + l \<equiv> index_of_int (int_of_index k + int_of_index l)" ..
    3.80 +lemmas [code func del] = plus_index_def
    3.81 +lemma plus_index_code [code func]:
    3.82 +  "index_of_int k + index_of_int l = index_of_int (k + l)"
    3.83 +  unfolding plus_index_def by simp
    3.84 +
    3.85 +instance index :: minus
    3.86 +  [simp]: "- k \<equiv> index_of_int (- int_of_index k)"
    3.87 +  [simp]: "k - l \<equiv> index_of_int (int_of_index k - int_of_index l)" ..
    3.88 +lemmas [code func del] = uminus_index_def minus_index_def
    3.89 +lemma uminus_index_code [code func]:
    3.90 +  "- index_of_int k \<equiv> index_of_int (- k)"
    3.91 +  unfolding uminus_index_def by simp
    3.92 +lemma minus_index_code [code func]:
    3.93 +  "index_of_int k - index_of_int l = index_of_int (k - l)"
    3.94 +  unfolding minus_index_def by simp
    3.95 +
    3.96 +instance index :: times
    3.97 +  [simp]: "k * l \<equiv> index_of_int (int_of_index k * int_of_index l)" ..
    3.98 +lemmas [code func del] = times_index_def
    3.99 +lemma times_index_code [code func]:
   3.100 +  "index_of_int k * index_of_int l = index_of_int (k * l)"
   3.101 +  unfolding times_index_def by simp
   3.102 +
   3.103 +instance index :: ord
   3.104 +  [simp]: "k \<le> l \<equiv> int_of_index k \<le> int_of_index l"
   3.105 +  [simp]: "k < l \<equiv> int_of_index k < int_of_index l" ..
   3.106 +lemmas [code func del] = less_eq_index_def less_index_def
   3.107 +lemma less_eq_index_code [code func]:
   3.108 +  "index_of_int k \<le> index_of_int l \<longleftrightarrow> k \<le> l"
   3.109 +  unfolding less_eq_index_def by simp
   3.110 +lemma less_index_code [code func]:
   3.111 +  "index_of_int k < index_of_int l \<longleftrightarrow> k < l"
   3.112 +  unfolding less_index_def by simp
   3.113 +
   3.114 +instance index :: ring_1
   3.115 +  by default (auto simp add: left_distrib right_distrib)
   3.116 +
   3.117 +lemma of_nat_index: "of_nat n = index_of_int (of_nat n)"
   3.118 +proof (induct n)
   3.119 +  case 0 show ?case by simp
   3.120 +next
   3.121 +  case (Suc n)
   3.122 +  then have "int_of_index (index_of_int (int n))
   3.123 +    = int_of_index (of_nat n)" by simp
   3.124 +  then have "int n = int_of_index (of_nat n)" by simp
   3.125 +  then show ?case by simp
   3.126 +qed
   3.127 +
   3.128 +instance index :: number_ring
   3.129 +  by default
   3.130 +    (simp_all add: left_distrib number_of_index_def of_int_of_nat of_nat_index)
   3.131 +
   3.132 +lemma zero_index_code [code inline, code func]:
   3.133 +  "(0\<Colon>index) = Numeral0"
   3.134 +  by simp
   3.135 +
   3.136 +lemma one_index_code [code inline, code func]:
   3.137 +  "(1\<Colon>index) = Numeral1"
   3.138 +  by simp
   3.139 +
   3.140 +instance index :: abs
   3.141 +  "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" ..
   3.142 +
   3.143 +lemma index_of_int [code func]:
   3.144 +  "index_of_int k = (if k = 0 then 0
   3.145 +    else if k = -1 then -1
   3.146 +    else let (l, m) = divAlg (k, 2) in 2 * index_of_int l +
   3.147 +      (if m = 0 then 0 else 1))"
   3.148 +  by (simp add: number_of_index_shift Let_def split_def divAlg_mod_div) arith
   3.149 +
   3.150 +
   3.151 +subsection {* Conversion to and from @{typ nat} *}
   3.152 +
   3.153 +definition
   3.154 +  nat_of_index :: "index \<Rightarrow> nat"
   3.155 +where
   3.156 +  [code func del]: "nat_of_index = nat o int_of_index"
   3.157 +
   3.158 +definition
   3.159 +  nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
   3.160 +  [code func del]: "nat_of_index_aux i n = nat_of_index i + n"
   3.161 +
   3.162 +lemma nat_of_index_aux_code [code]:
   3.163 +  "nat_of_index_aux i n = (if i \<le> 0 then n else nat_of_index_aux (i - 1) (Suc n))"
   3.164 +  by (auto simp add: nat_of_index_aux_def nat_of_index_def)
   3.165 +
   3.166 +lemma nat_of_index_code [code]:
   3.167 +  "nat_of_index i = nat_of_index_aux i 0"
   3.168 +  by (simp add: nat_of_index_aux_def)
   3.169 +
   3.170 +definition
   3.171 +  index_of_nat :: "nat \<Rightarrow> index"
   3.172 +where
   3.173 +  [code func del]: "index_of_nat = index_of_int o of_nat"
   3.174 +
   3.175 +lemma index_of_nat [code func]:
   3.176 +  "index_of_nat 0 = 0"
   3.177 +  "index_of_nat (Suc n) = index_of_nat n + 1"
   3.178 +  unfolding index_of_nat_def by simp_all
   3.179 +
   3.180 +lemma index_nat_id [simp]:
   3.181 +  "nat_of_index (index_of_nat n) = n"
   3.182 +  "index_of_nat (nat_of_index i) = (if i \<le> 0 then 0 else i)"
   3.183 +  unfolding index_of_nat_def nat_of_index_def by simp_all
   3.184 +
   3.185 +
   3.186 +subsection {* ML interface *}
   3.187 +
   3.188 +ML {*
   3.189 +structure Index =
   3.190 +struct
   3.191 +
   3.192 +fun mk k = @{term index_of_int} $ HOLogic.mk_number @{typ index} k;
   3.193 +
   3.194 +end;
   3.195 +*}
   3.196 +
   3.197 +
   3.198 +subsection {* Code serialization *}
   3.199 +
   3.200 +code_type index
   3.201 +  (SML "int")
   3.202 +  (OCaml "int")
   3.203 +  (Haskell "Integer")
   3.204 +
   3.205 +code_instance index :: eq
   3.206 +  (Haskell -)
   3.207 +
   3.208 +setup {*
   3.209 +  fold (fn target => CodeTarget.add_pretty_numeral target true
   3.210 +    @{const_name number_index_inst.number_of_index}
   3.211 +    @{const_name Numeral.B0} @{const_name Numeral.B1}
   3.212 +    @{const_name Numeral.Pls} @{const_name Numeral.Min}
   3.213 +    @{const_name Numeral.Bit}
   3.214 +  ) ["SML", "OCaml", "Haskell"]
   3.215 +*}
   3.216 +
   3.217 +code_reserved SML int
   3.218 +code_reserved OCaml int
   3.219 +
   3.220 +code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   3.221 +  (SML "Int.+ ((_), (_))")
   3.222 +  (OCaml "Pervasives.+")
   3.223 +  (Haskell infixl 6 "+")
   3.224 +
   3.225 +code_const "uminus \<Colon> index \<Rightarrow> index"
   3.226 +  (SML "Int.~")
   3.227 +  (OCaml "Pervasives.~-")
   3.228 +  (Haskell "negate")
   3.229 +
   3.230 +code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   3.231 +  (SML "Int.- ((_), (_))")
   3.232 +  (OCaml "Pervasives.-")
   3.233 +  (Haskell infixl 6 "-")
   3.234 +
   3.235 +code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   3.236 +  (SML "Int.* ((_), (_))")
   3.237 +  (OCaml "Pervasives.*")
   3.238 +  (Haskell infixl 7 "*")
   3.239 +
   3.240 +code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   3.241 +  (SML "!((_ : Int.int) = _)")
   3.242 +  (OCaml "!((_ : Pervasives.int) = _)")
   3.243 +  (Haskell infixl 4 "==")
   3.244 +
   3.245 +code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   3.246 +  (SML "Int.<= ((_), (_))")
   3.247 +  (OCaml "!((_ : Pervasives.int) <= _)")
   3.248 +  (Haskell infix 4 "<=")
   3.249 +
   3.250 +code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   3.251 +  (SML "Int.< ((_), (_))")
   3.252 +  (OCaml "!((_ : Pervasives.int) < _)")
   3.253 +  (Haskell infix 4 "<")
   3.254 +
   3.255 +code_reserved SML Int
   3.256 +code_reserved OCaml Pervasives
   3.257 +
   3.258 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Code_Integer.thy	Fri Oct 12 10:26:18 2007 +0200
     4.3 @@ -0,0 +1,99 @@
     4.4 +(*  Title:      HOL/Library/Code_Integer.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Florian Haftmann, TU Muenchen
     4.7 +*)
     4.8 +
     4.9 +header {* Pretty integer literals for code generation *}
    4.10 +
    4.11 +theory Code_Integer
    4.12 +imports IntArith Code_Index
    4.13 +begin
    4.14 +
    4.15 +text {*
    4.16 +  HOL numeral expressions are mapped to integer literals
    4.17 +  in target languages, using predefined target language
    4.18 +  operations for abstract integer operations.
    4.19 +*}
    4.20 +
    4.21 +code_type int
    4.22 +  (SML "IntInf.int")
    4.23 +  (OCaml "Big'_int.big'_int")
    4.24 +  (Haskell "Integer")
    4.25 +
    4.26 +code_instance int :: eq
    4.27 +  (Haskell -)
    4.28 +
    4.29 +setup {*
    4.30 +  fold (fn target => CodeTarget.add_pretty_numeral target true
    4.31 +    @{const_name number_int_inst.number_of_int}
    4.32 +    @{const_name Numeral.B0} @{const_name Numeral.B1}
    4.33 +    @{const_name Numeral.Pls} @{const_name Numeral.Min}
    4.34 +    @{const_name Numeral.Bit}
    4.35 +  ) ["SML", "OCaml", "Haskell"]
    4.36 +*}
    4.37 +
    4.38 +code_const "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit"
    4.39 +  (SML "raise/ Fail/ \"Pls\""
    4.40 +     and "raise/ Fail/ \"Min\""
    4.41 +     and "!((_);/ (_);/ raise/ Fail/ \"Bit\")")
    4.42 +  (OCaml "failwith/ \"Pls\""
    4.43 +     and "failwith/ \"Min\""
    4.44 +     and "!((_);/ (_);/ failwith/ \"Bit\")")
    4.45 +  (Haskell "error/ \"Pls\""
    4.46 +     and "error/ \"Min\""
    4.47 +     and "error/ \"Bit\"")
    4.48 +
    4.49 +code_const Numeral.pred
    4.50 +  (SML "IntInf.- ((_), 1)")
    4.51 +  (OCaml "Big'_int.pred'_big'_int")
    4.52 +  (Haskell "!(_/ -/ 1)")
    4.53 +
    4.54 +code_const Numeral.succ
    4.55 +  (SML "IntInf.+ ((_), 1)")
    4.56 +  (OCaml "Big'_int.succ'_big'_int")
    4.57 +  (Haskell "!(_/ +/ 1)")
    4.58 +
    4.59 +code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    4.60 +  (SML "IntInf.+ ((_), (_))")
    4.61 +  (OCaml "Big'_int.add'_big'_int")
    4.62 +  (Haskell infixl 6 "+")
    4.63 +
    4.64 +code_const "uminus \<Colon> int \<Rightarrow> int"
    4.65 +  (SML "IntInf.~")
    4.66 +  (OCaml "Big'_int.minus'_big'_int")
    4.67 +  (Haskell "negate")
    4.68 +
    4.69 +code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    4.70 +  (SML "IntInf.- ((_), (_))")
    4.71 +  (OCaml "Big'_int.sub'_big'_int")
    4.72 +  (Haskell infixl 6 "-")
    4.73 +
    4.74 +code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    4.75 +  (SML "IntInf.* ((_), (_))")
    4.76 +  (OCaml "Big'_int.mult'_big'_int")
    4.77 +  (Haskell infixl 7 "*")
    4.78 +
    4.79 +code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    4.80 +  (SML "!((_ : IntInf.int) = _)")
    4.81 +  (OCaml "Big'_int.eq'_big'_int")
    4.82 +  (Haskell infixl 4 "==")
    4.83 +
    4.84 +code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    4.85 +  (SML "IntInf.<= ((_), (_))")
    4.86 +  (OCaml "Big'_int.le'_big'_int")
    4.87 +  (Haskell infix 4 "<=")
    4.88 +
    4.89 +code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    4.90 +  (SML "IntInf.< ((_), (_))")
    4.91 +  (OCaml "Big'_int.lt'_big'_int")
    4.92 +  (Haskell infix 4 "<")
    4.93 +
    4.94 +code_const index_of_int and int_of_index
    4.95 +  (SML "IntInf.toInt" and "IntInf.fromInt")
    4.96 +  (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int")
    4.97 +  (Haskell "_" and "_")
    4.98 +
    4.99 +code_reserved SML IntInf
   4.100 +code_reserved OCaml Big_int
   4.101 +
   4.102 +end
   4.103 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/Code_Message.thy	Fri Oct 12 10:26:18 2007 +0200
     5.3 @@ -0,0 +1,68 @@
     5.4 +(*  ID:         $Id$
     5.5 +    Author:     Florian Haftmann, TU Muenchen
     5.6 +*)
     5.7 +
     5.8 +header {* Monolithic strings (message strings) for code generation *}
     5.9 +
    5.10 +theory Code_Message
    5.11 +imports List
    5.12 +begin
    5.13 +
    5.14 +subsection {* Datatype of messages *}
    5.15 +
    5.16 +datatype message_string = STR string
    5.17 +
    5.18 +lemmas [code func del] = message_string.recs message_string.cases
    5.19 +
    5.20 +lemma [code func]: "size (s\<Colon>message_string) = 0"
    5.21 +  by (cases s) simp_all
    5.22 +
    5.23 +subsection {* ML interface *}
    5.24 +
    5.25 +ML {*
    5.26 +structure Message_String =
    5.27 +struct
    5.28 +
    5.29 +fun mk s = @{term STR} $ HOLogic.mk_string s;
    5.30 +
    5.31 +end;
    5.32 +*}
    5.33 +
    5.34 +
    5.35 +subsection {* Code serialization *}
    5.36 +
    5.37 +code_type message_string
    5.38 +  (SML "string")
    5.39 +  (OCaml "string")
    5.40 +  (Haskell "String")
    5.41 +
    5.42 +setup {*
    5.43 +let
    5.44 +  val charr = @{const_name Char}
    5.45 +  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    5.46 +    @{const_name Nibble2}, @{const_name Nibble3},
    5.47 +    @{const_name Nibble4}, @{const_name Nibble5},
    5.48 +    @{const_name Nibble6}, @{const_name Nibble7},
    5.49 +    @{const_name Nibble8}, @{const_name Nibble9},
    5.50 +    @{const_name NibbleA}, @{const_name NibbleB},
    5.51 +    @{const_name NibbleC}, @{const_name NibbleD},
    5.52 +    @{const_name NibbleE}, @{const_name NibbleF}];
    5.53 +in
    5.54 +  fold (fn target => CodeTarget.add_pretty_message target
    5.55 +    charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR})
    5.56 +  ["SML", "OCaml", "Haskell"]
    5.57 +end
    5.58 +*}
    5.59 +
    5.60 +code_reserved SML string
    5.61 +code_reserved OCaml string
    5.62 +
    5.63 +code_instance message_string :: eq
    5.64 +  (Haskell -)
    5.65 +
    5.66 +code_const "op = \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
    5.67 +  (SML "!((_ : string) = _)")
    5.68 +  (OCaml "!((_ : string) = _)")
    5.69 +  (Haskell infixl 4 "==")
    5.70 +
    5.71 +end