--- a/src/HOL/List.thy Wed May 06 19:09:14 2009 +0200
+++ b/src/HOL/List.thy Wed May 06 19:09:31 2009 +0200
@@ -6,6 +6,7 @@
theory List
imports Plain Presburger Recdef ATP_Linkup
+uses ("Tools/list_code.ML")
begin
datatype 'a list =
@@ -3460,6 +3461,8 @@
subsubsection {* Setup *}
+use "Tools/list_code.ML"
+
code_type list
(SML "_ list")
(OCaml "_ list")
@@ -3470,11 +3473,6 @@
(OCaml "[]")
(Haskell "[]")
-code_const Cons
- (SML infixr 7 "::")
- (OCaml infixr 6 "::")
- (Haskell infixr 5 ":")
-
code_instance list :: eq
(Haskell -)
@@ -3503,22 +3501,22 @@
and gen_list aG aT i = gen_list' aG aT i i;
*}
-consts_code Nil ("[]")
consts_code Cons ("(_ ::/ _)")
setup {*
let
-
-fun list_codegen thy defs dep thyname b t gr =
- let
- val ts = HOLogic.dest_list t;
- val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
- (fastype_of t) gr;
- val (ps, gr'') = fold_map
- (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
- in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
-
-in Codegen.add_codegen "list_codegen" list_codegen end
+ fun list_codegen thy defs dep thyname b t gr =
+ let
+ val ts = HOLogic.dest_list t;
+ val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
+ (fastype_of t) gr;
+ val (ps, gr'') = fold_map
+ (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
+ in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
+in
+ fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell"]
+ #> Codegen.add_codegen "list_codegen" list_codegen
+end
*}