src/HOL/Tools/string_code.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 62597 b3f2b8c906a6
child 67620 3817a93a3e5e
permissions -rw-r--r--
tuned;
haftmann@37744
     1
(*  Title:      HOL/Tools/string_code.ML
haftmann@37744
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@31055
     3
haftmann@31055
     4
Code generation for character and string literals.
haftmann@31055
     5
*)
haftmann@31055
     6
haftmann@31055
     7
signature STRING_CODE =
haftmann@31055
     8
sig
haftmann@31055
     9
  val add_literal_list_string: string -> theory -> theory
haftmann@31055
    10
  val add_literal_char: string -> theory -> theory
haftmann@31205
    11
  val add_literal_string: string -> theory -> theory
haftmann@31055
    12
end;
haftmann@31055
    13
haftmann@31055
    14
structure String_Code : STRING_CODE =
haftmann@31055
    15
struct
haftmann@31055
    16
haftmann@31055
    17
open Basic_Code_Thingol;
haftmann@31055
    18
haftmann@62597
    19
fun decode_char_nonzero t =
haftmann@62597
    20
  case Numeral.dest_num t of
haftmann@62597
    21
    SOME n => if 0 < n andalso n < 256 then SOME n else NONE
haftmann@62597
    22
  | _ => NONE;
haftmann@55148
    23
haftmann@62597
    24
fun decode_char (IConst { sym = Code_Symbol.Constant @{const_name Groups.zero}, ... }) =
haftmann@62597
    25
     SOME 0
haftmann@62597
    26
  | decode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t) =
haftmann@62597
    27
      decode_char_nonzero t
haftmann@62597
    28
  | decode_char _ = NONE
haftmann@62597
    29
haftmann@55148
    30
fun implode_string literals ts =
haftmann@55148
    31
  let
haftmann@62597
    32
    val is = map_filter decode_char ts;
haftmann@62597
    33
  in if length ts = length is
haftmann@62597
    34
    then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode o map chr) is
haftmann@55148
    35
    else NONE
haftmann@55148
    36
  end;
haftmann@31055
    37
haftmann@31055
    38
fun add_literal_list_string target =
haftmann@31055
    39
  let
haftmann@55148
    40
    fun pretty literals pr _ vars fxy [(t1, _), (t2, _)] =
haftmann@55148
    41
      case Option.map (cons t1) (List_Code.implode_list t2)
haftmann@55148
    42
       of SOME ts => (case implode_string literals ts
haftmann@31055
    43
             of SOME p => p
haftmann@31055
    44
              | NONE =>
haftmann@31055
    45
                  Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
haftmann@31055
    46
        | NONE =>
haftmann@31055
    47
            List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
haftmann@52435
    48
  in
haftmann@52435
    49
    Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
haftmann@55148
    50
      [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
haftmann@31055
    51
  end;
haftmann@31055
    52
wenzelm@55236
    53
fun add_literal_char target thy =
haftmann@31055
    54
  let
haftmann@62597
    55
    fun pr literals =
haftmann@62597
    56
      Code_Printer.str o Code_Printer.literal_char literals o chr;
haftmann@62597
    57
    fun pretty_zero literals _ _ _ _ [] =
haftmann@62597
    58
      pr literals 0
haftmann@62597
    59
    fun pretty_Char literals _ thm _ _ [(t, _)] =
haftmann@62597
    60
      case decode_char_nonzero t
haftmann@62597
    61
       of SOME i => pr literals i
wenzelm@55236
    62
        | NONE => Code_Printer.eqn_error thy thm "Illegal character expression";
haftmann@52435
    63
  in
haftmann@62597
    64
    thy
haftmann@62597
    65
    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name String.zero_char_inst.zero_char},
haftmann@62597
    66
      [(target, SOME (Code_Printer.complex_const_syntax (0, pretty_zero)))]))
haftmann@62597
    67
    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
haftmann@62597
    68
      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty_Char)))]))
haftmann@31055
    69
  end;
haftmann@31055
    70
wenzelm@55236
    71
fun add_literal_string target thy =
haftmann@31055
    72
  let
haftmann@55148
    73
    fun pretty literals _ thm _ _ [(t, _)] =
haftmann@55148
    74
      case List_Code.implode_list t
haftmann@55148
    75
       of SOME ts => (case implode_string literals ts
haftmann@31055
    76
             of SOME p => p
wenzelm@55236
    77
              | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression")
wenzelm@55236
    78
        | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
haftmann@52435
    79
  in
haftmann@62597
    80
    thy
haftmann@62597
    81
    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
haftmann@62597
    82
      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
haftmann@31055
    83
  end;
haftmann@31055
    84
haftmann@31055
    85
end;