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