src/HOL/Library/Code_Char.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (18 months ago)
changeset 67951 655aa11359dc
parent 65884 d76937b773d9
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
     1 (*  Title:      HOL/Library/Code_Char.thy
     2     Author:     Florian Haftmann
     3 *)
     4 
     5 section \<open>Code generation of pretty characters (and strings)\<close>
     6 
     7 theory Code_Char
     8 imports Main Char_ord
     9 begin
    10 
    11 code_printing
    12   type_constructor char \<rightharpoonup>
    13     (SML) "char"
    14     and (OCaml) "char"
    15     and (Haskell) "Prelude.Char"
    16     and (Scala) "Char"
    17 
    18 setup \<open>
    19   fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"]
    20   #> String_Code.add_literal_list_string "Haskell"
    21 \<close>
    22 
    23 code_printing
    24   constant integer_of_char \<rightharpoonup>
    25     (SML) "!(IntInf.fromInt o Char.ord)"
    26     and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
    27     and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
    28     and (Scala) "BigInt(_.toInt)"
    29 | constant char_of_integer \<rightharpoonup>
    30     (SML) "!(Char.chr o IntInf.toInt)"
    31     and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
    32     and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
    33     and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else sys.error(\"character value out of range\"))"
    34 | class_instance char :: equal \<rightharpoonup>
    35     (Haskell) -
    36 | constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
    37     (SML) "!((_ : char) = _)"
    38     and (OCaml) "!((_ : char) = _)"
    39     and (Haskell) infix 4 "=="
    40     and (Scala) infixl 5 "=="
    41 | constant "Code_Evaluation.term_of :: char \<Rightarrow> term" \<rightharpoonup>
    42     (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))"
    43 
    44 code_reserved SML
    45   char
    46 
    47 code_reserved OCaml
    48   char
    49 
    50 code_reserved Scala
    51   char
    52 
    53 code_reserved SML String
    54 
    55 code_printing
    56   constant String.implode \<rightharpoonup>
    57     (SML) "String.implode"
    58     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)"
    59     and (Haskell) "_"
    60     and (Scala) "!(\"\" ++/ _)"
    61 | constant String.explode \<rightharpoonup>
    62     (SML) "String.explode"
    63     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) [])"
    64     and (Haskell) "_"
    65     and (Scala) "!(_.toList)"
    66 
    67 code_printing
    68   constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
    69     (SML) "!((_ : char) <= _)"
    70     and (OCaml) "!((_ : char) <= _)"
    71     and (Haskell) infix 4 "<="
    72     and (Scala) infixl 4 "<="
    73     and (Eval) infixl 6 "<="
    74 | constant "Orderings.less :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
    75     (SML) "!((_ : char) < _)"
    76     and (OCaml) "!((_ : char) < _)"
    77     and (Haskell) infix 4 "<"
    78     and (Scala) infixl 4 "<"
    79     and (Eval) infixl 6 "<"
    80 |  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
    81     (SML) "!((_ : string) <= _)"
    82     and (OCaml) "!((_ : string) <= _)"
    83     \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only
    84           if no type class instance needs to be generated, because String = [Char] in Haskell
    85           and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
    86     and (Haskell) infix 4 "<="
    87     and (Scala) infixl 4 "<="
    88     and (Eval) infixl 6 "<="
    89 | constant "Orderings.less :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
    90     (SML) "!((_ : string) < _)"
    91     and (OCaml) "!((_ : string) < _)"
    92     and (Haskell) infix 4 "<"
    93     and (Scala) infixl 4 "<"
    94     and (Eval) infixl 6 "<"
    95 
    96 end