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