src/HOL/Tools/list_code.ML
author haftmann
Tue Jun 05 07:05:56 2012 +0200 (2012-06-05)
changeset 48072 ace701efe203
parent 38923 79d7f2b4cf71
permissions -rw-r--r--
prefer records with speaking labels over deeply nested tuples
haftmann@37744
     1
(*  Title:  HOL/Tools/list_code.ML
haftmann@37744
     2
    Author: Florian Haftmann, TU Muenchen
haftmann@31055
     3
haftmann@31055
     4
Code generation for list literals.
haftmann@31055
     5
*)
haftmann@31055
     6
haftmann@31055
     7
signature LIST_CODE =
haftmann@31055
     8
sig
haftmann@31055
     9
  val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
haftmann@31055
    10
  val default_list: int * string
haftmann@31055
    11
    -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
haftmann@31055
    12
    -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
haftmann@31055
    13
  val add_literal_list: string -> theory -> theory
haftmann@31055
    14
end;
haftmann@31055
    15
haftmann@31055
    16
structure List_Code : LIST_CODE =
haftmann@31055
    17
struct
haftmann@31055
    18
haftmann@31055
    19
open Basic_Code_Thingol;
haftmann@31055
    20
haftmann@31055
    21
fun implode_list nil' cons' t =
haftmann@31055
    22
  let
haftmann@48072
    23
    fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
haftmann@31055
    24
          if c = cons'
haftmann@31055
    25
          then SOME (t1, t2)
haftmann@31055
    26
          else NONE
haftmann@31055
    27
      | dest_cons _ = NONE;
haftmann@31055
    28
    val (ts, t') = Code_Thingol.unfoldr dest_cons t;
haftmann@31055
    29
  in case t'
haftmann@48072
    30
   of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
haftmann@31055
    31
    | _ => NONE
haftmann@31055
    32
  end;
haftmann@31055
    33
haftmann@31055
    34
fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
haftmann@37242
    35
  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
haftmann@31055
    36
    pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
haftmann@31055
    37
    Code_Printer.str target_cons,
haftmann@31055
    38
    pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
haftmann@37242
    39
  );
haftmann@31055
    40
haftmann@31055
    41
fun add_literal_list target =
haftmann@31055
    42
  let
haftmann@31055
    43
    fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
haftmann@31055
    44
      case Option.map (cons t1) (implode_list nil' cons' t2)
haftmann@31055
    45
       of SOME ts =>
haftmann@31055
    46
            Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
haftmann@31055
    47
        | NONE =>
haftmann@31055
    48
            default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
haftmann@38923
    49
  in Code_Target.add_const_syntax target @{const_name Cons}
haftmann@37881
    50
    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
haftmann@31055
    51
  end
haftmann@31055
    52
haftmann@31055
    53
end;