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