src/HOL/Library/Code_Char.thy
changeset 52435 6646bb548c6b
parent 51542 738598beeb26
child 54596 368c70ee1f46
     1.1 --- a/src/HOL/Library/Code_Char.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -8,19 +8,28 @@
     1.4  imports Main Char_ord
     1.5  begin
     1.6  
     1.7 -code_type char
     1.8 -  (SML "char")
     1.9 -  (OCaml "char")
    1.10 -  (Haskell "Prelude.Char")
    1.11 -  (Scala "Char")
    1.12 +code_printing
    1.13 +  type_constructor char \<rightharpoonup>
    1.14 +    (SML) "char"
    1.15 +    and (OCaml) "char"
    1.16 +    and (Haskell) "Prelude.Char"
    1.17 +    and (Scala) "Char"
    1.18  
    1.19  setup {*
    1.20    fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
    1.21    #> String_Code.add_literal_list_string "Haskell"
    1.22  *}
    1.23  
    1.24 -code_instance char :: equal
    1.25 -  (Haskell -)
    1.26 +code_printing
    1.27 +  class_instance char :: equal \<rightharpoonup>
    1.28 +    (Haskell) -
    1.29 +| constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
    1.30 +    (SML) "!((_ : char) = _)"
    1.31 +    and (OCaml) "!((_ : char) = _)"
    1.32 +    and (Haskell) infix 4 "=="
    1.33 +    and (Scala) infixl 5 "=="
    1.34 +| constant "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" \<rightharpoonup>
    1.35 +    (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))"
    1.36  
    1.37  code_reserved SML
    1.38    char
    1.39 @@ -31,32 +40,22 @@
    1.40  code_reserved Scala
    1.41    char
    1.42  
    1.43 -code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.44 -  (SML "!((_ : char) = _)")
    1.45 -  (OCaml "!((_ : char) = _)")
    1.46 -  (Haskell infix 4 "==")
    1.47 -  (Scala infixl 5 "==")
    1.48 -
    1.49 -code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
    1.50 -  (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
    1.51 -
    1.52 -
    1.53  definition implode :: "string \<Rightarrow> String.literal" where
    1.54    "implode = STR"
    1.55  
    1.56  code_reserved SML String
    1.57  
    1.58 -code_const implode
    1.59 -  (SML "String.implode")
    1.60 -  (OCaml "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)")
    1.61 -  (Haskell "_")
    1.62 -  (Scala "!(\"\" ++/ _)")
    1.63 -
    1.64 -code_const explode
    1.65 -  (SML "String.explode")
    1.66 -  (OCaml "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])")
    1.67 -  (Haskell "_")
    1.68 -  (Scala "!(_.toList)")
    1.69 +code_printing
    1.70 +  constant implode \<rightharpoonup>
    1.71 +    (SML) "String.implode"
    1.72 +    and (OCaml) "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)"
    1.73 +    and (Haskell) "_"
    1.74 +    and (Scala) "!(\"\" ++/ _)"
    1.75 +| constant explode \<rightharpoonup>
    1.76 +    (SML) "String.explode"
    1.77 +    and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])"
    1.78 +    and (Haskell) "_"
    1.79 +    and (Scala) "!(_.toList)"
    1.80  
    1.81  
    1.82  definition integer_of_char :: "char \<Rightarrow> integer"
    1.83 @@ -75,30 +74,29 @@
    1.84    "char_of_nat = char_of_integer o integer_of_nat"
    1.85    by (simp add: char_of_integer_def fun_eq_iff)
    1.86  
    1.87 -code_const integer_of_char and char_of_integer
    1.88 -  (SML "!(IntInf.fromInt o Char.ord)"
    1.89 -    and "!(Char.chr o IntInf.toInt)")
    1.90 -  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)"
    1.91 -    and "Char.chr (Big'_int.int'_of'_big'_int _)")
    1.92 -  (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
    1.93 -    and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
    1.94 -  (Scala "BigInt(_.toInt)"
    1.95 -    and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
    1.96 -
    1.97 -
    1.98 -code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.99 -  (SML "!((_ : char) <= _)")
   1.100 -  (OCaml "!((_ : char) <= _)")
   1.101 -  (Haskell infix 4 "<=")
   1.102 -  (Scala infixl 4 "<=")
   1.103 -  (Eval infixl 6 "<=")
   1.104 -
   1.105 -code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   1.106 -  (SML "!((_ : char) < _)")
   1.107 -  (OCaml "!((_ : char) < _)")
   1.108 -  (Haskell infix 4 "<")
   1.109 -  (Scala infixl 4 "<")
   1.110 -  (Eval infixl 6 "<")
   1.111 +code_printing
   1.112 +  constant integer_of_char \<rightharpoonup>
   1.113 +    (SML) "!(IntInf.fromInt o Char.ord)"
   1.114 +    and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
   1.115 +    and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
   1.116 +    and (Scala) "BigInt(_.toInt)"
   1.117 +| constant char_of_integer \<rightharpoonup>
   1.118 +    (SML) "!(Char.chr o IntInf.toInt)"
   1.119 +    and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
   1.120 +    and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
   1.121 +    and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))"
   1.122 +| constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
   1.123 +    (SML) "!((_ : char) <= _)"
   1.124 +    and (OCaml) "!((_ : char) <= _)"
   1.125 +    and (Haskell) infix 4 "<="
   1.126 +    and (Scala) infixl 4 "<="
   1.127 +    and (Eval) infixl 6 "<="
   1.128 +| constant "Orderings.less :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
   1.129 +    (SML) "!((_ : char) < _)"
   1.130 +    and (OCaml) "!((_ : char) < _)"
   1.131 +    and (Haskell) infix 4 "<"
   1.132 +    and (Scala) infixl 4 "<"
   1.133 +    and (Eval) infixl 6 "<"
   1.134  
   1.135  end
   1.136