src/HOL/Tools/list_code.ML
changeset 31055 2cf6efca6c71
child 37242 97097e589715
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/list_code.ML	Wed May 06 19:09:31 2009 +0200
     1.3 @@ -0,0 +1,52 @@
     1.4 +(* Author: Florian Haftmann, TU Muenchen
     1.5 +
     1.6 +Code generation for list literals.
     1.7 +*)
     1.8 +
     1.9 +signature LIST_CODE =
    1.10 +sig
    1.11 +  val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
    1.12 +  val default_list: int * string
    1.13 +    -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
    1.14 +    -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
    1.15 +  val add_literal_list: string -> theory -> theory
    1.16 +end;
    1.17 +
    1.18 +structure List_Code : LIST_CODE =
    1.19 +struct
    1.20 +
    1.21 +open Basic_Code_Thingol;
    1.22 +
    1.23 +fun implode_list nil' cons' t =
    1.24 +  let
    1.25 +    fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
    1.26 +          if c = cons'
    1.27 +          then SOME (t1, t2)
    1.28 +          else NONE
    1.29 +      | dest_cons _ = NONE;
    1.30 +    val (ts, t') = Code_Thingol.unfoldr dest_cons t;
    1.31 +  in case t'
    1.32 +   of IConst (c, _) => if c = nil' then SOME ts else NONE
    1.33 +    | _ => NONE
    1.34 +  end;
    1.35 +
    1.36 +fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
    1.37 +  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
    1.38 +    pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
    1.39 +    Code_Printer.str target_cons,
    1.40 +    pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
    1.41 +  ];
    1.42 +
    1.43 +fun add_literal_list target =
    1.44 +  let
    1.45 +    fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
    1.46 +      case Option.map (cons t1) (implode_list nil' cons' t2)
    1.47 +       of SOME ts =>
    1.48 +            Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
    1.49 +        | NONE =>
    1.50 +            default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    1.51 +  in Code_Target.add_syntax_const target
    1.52 +    @{const_name Cons} (SOME (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))
    1.53 +  end
    1.54 +
    1.55 +end;