removing old code generator setup for lists
authorbulwahn
Wed Oct 19 08:37:27 2011 +0200 (2011-10-19)
changeset 45181c8eb935e2e87
parent 45180 3e2befc10748
child 45182 10202ca034b0
removing old code generator setup for lists
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Wed Oct 19 08:37:26 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Oct 19 08:37:27 2011 +0200
     1.3 @@ -5261,39 +5261,7 @@
     1.4  code_reserved OCaml
     1.5    list
     1.6  
     1.7 -types_code
     1.8 -  "list" ("_ list")
     1.9 -attach (term_of) {*
    1.10 -fun term_of_list f T = HOLogic.mk_list T o map f;
    1.11 -*}
    1.12 -attach (test) {*
    1.13 -fun gen_list' aG aT i j = frequency
    1.14 -  [(i, fn () =>
    1.15 -      let
    1.16 -        val (x, t) = aG j;
    1.17 -        val (xs, ts) = gen_list' aG aT (i-1) j
    1.18 -      in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
    1.19 -   (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
    1.20 -and gen_list aG aT i = gen_list' aG aT i i;
    1.21 -*}
    1.22 -
    1.23 -consts_code Cons ("(_ ::/ _)")
    1.24 -
    1.25 -setup {*
    1.26 -let
    1.27 -  fun list_codegen thy mode defs dep thyname b t gr =
    1.28 -    let
    1.29 -      val ts = HOLogic.dest_list t;
    1.30 -      val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
    1.31 -        (fastype_of t) gr;
    1.32 -      val (ps, gr'') = fold_map
    1.33 -        (Codegen.invoke_codegen thy mode defs dep thyname false) ts gr'
    1.34 -    in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
    1.35 -in
    1.36 -  fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]
    1.37 -  #> Codegen.add_codegen "list_codegen" list_codegen
    1.38 -end
    1.39 -*}
    1.40 +setup {* fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"] *}
    1.41  
    1.42  
    1.43  subsubsection {* Use convenient predefined operations *}