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