--- a/src/Pure/Tools/codegen_package.ML Fri Mar 02 15:43:26 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML Fri Mar 02 15:43:27 2007 +0100
@@ -147,25 +147,27 @@
| ensure_def_tyco thy algbr funcgr strct tyco trns =
let
fun defgen_datatype trns =
- case CodegenData.get_datatype thy tyco
- of SOME (vs, cos) =>
- trns
- |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
- ||>> fold_map (fn (c, tys) =>
- fold_map (exprgen_type thy algbr funcgr strct) tys
- #-> (fn tys' =>
- pair ((CodegenNames.const thy o CodegenConsts.norm_of_typ thy)
- (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
- |-> (fn (vs, cos) => succeed (CodegenThingol.Datatype (vs, cos)))
- | NONE =>
- trns
- |> fail ("No such datatype: " ^ quote tyco)
+ let
+ val (vs, cos) = case CodegenData.get_datatype thy tyco
+ of SOME x => x
+ | NONE => (Name.invents Name.context "'a" (Sign.arity_number thy tyco)
+ |> map (rpair (Sign.defaultS thy)) , [])
+ (*FIXME move to CodegenData*)
+ in
+ trns
+ |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
+ ||>> fold_map (fn (c, tys) =>
+ fold_map (exprgen_type thy algbr funcgr strct) tys
+ #-> (fn tys' =>
+ pair ((CodegenNames.const thy o CodegenConsts.norm_of_typ thy)
+ (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
+ |-> (fn (vs, cos) => succeed (CodegenThingol.Datatype (vs, cos)))
+ end;
val tyco' = CodegenNames.tyco thy tyco;
- val strict = check_strict strct (CodegenSerializer.tyco_has_serialization thy) tyco';
in
trns
|> tracing (fn _ => "generating type constructor " ^ quote tyco)
- |> ensure_def thy defgen_datatype strict
+ |> ensure_def thy defgen_datatype true
("generating type constructor " ^ quote tyco) tyco'
|> pair tyco'
end
--- a/src/Pure/Tools/codegen_serializer.ML Fri Mar 02 15:43:26 2007 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Fri Mar 02 15:43:27 2007 +0100
@@ -33,7 +33,6 @@
val assert_serializer: theory -> string -> string;
val const_has_serialization: theory -> string list -> string -> bool;
- val tyco_has_serialization: theory -> string list -> string -> bool;
val eval_verbose: bool ref;
val eval_term: theory -> (theory -> string -> string) -> CodegenThingol.code
@@ -312,7 +311,8 @@
fun pr_sml tyco_syntax const_syntax labelled_name keyword_vars deresolv is_cons ml_def =
let
- val pr_label = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
+ val pr_label_classrel = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
+ val pr_label_classop = NameSpace.base o NameSpace.qualifier;
fun pr_dicts fxy ds =
let
fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
@@ -486,13 +486,20 @@
str "of",
Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
];
- fun pr_data definer (tyco, (vs, cos)) =
- concat (
- str definer
- :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
- :: str "="
- :: separate (str "|") (map pr_co cos)
- );
+ fun pr_data definer (tyco, (vs, [])) =
+ concat (
+ str definer
+ :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
+ :: str "="
+ @@ str "EMPTY__"
+ )
+ | pr_data definer (tyco, (vs, cos)) =
+ concat (
+ str definer
+ :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
+ :: str "="
+ :: separate (str "|") (map pr_co cos)
+ );
val (ps, p) = split_last (pr_data "datatype" data :: map (pr_data "and") datas');
in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
| pr_def (MLClass (class, (superclasses, (v, classops)))) =
@@ -500,11 +507,11 @@
val w = first_upper v ^ "_";
fun pr_superclass_field (class, classrel) =
(concat o map str) [
- pr_label classrel, ":", "'" ^ v, deresolv class
+ pr_label_classrel classrel, ":", "'" ^ v, deresolv class
];
fun pr_classop_field (classop, ty) =
concat [
- (str o pr_label) classop, str ":", pr_typ NOBR ty
+ (str o pr_label_classop) classop, str ":", pr_typ NOBR ty
];
fun pr_classop_proj (classop, _) =
semicolon [
@@ -512,7 +519,7 @@
(str o deresolv) classop,
Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
str "=",
- str ("#" ^ pr_label classop),
+ str ("#" ^ pr_label_classop classop),
str w
];
fun pr_superclass_proj (_, classrel) =
@@ -521,7 +528,7 @@
(str o deresolv) classrel,
Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
str "=",
- str ("#" ^ pr_label classrel),
+ str ("#" ^ pr_label_classrel classrel),
str w
];
in
@@ -542,7 +549,7 @@
let
fun pr_superclass (_, (classrel, dss)) =
concat [
- (str o pr_label) classrel,
+ (str o pr_label_classrel) classrel,
str "=",
pr_dicts NOBR [DictConst dss]
];
@@ -555,7 +562,7 @@
val vars = CodegenNames.intro_vars consts keyword_vars;
in
concat [
- (str o pr_label) classop,
+ (str o pr_label_classop) classop,
str "=",
pr_term vars NOBR t
]
@@ -789,13 +796,20 @@
str "of",
Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
];
- fun pr_data definer (tyco, (vs, cos)) =
- concat (
- str definer
- :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
- :: str "="
- :: separate (str "|") (map pr_co cos)
- );
+ fun pr_data definer (tyco, (vs, [])) =
+ concat (
+ str definer
+ :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
+ :: str "="
+ @@ str "EMPTY_"
+ )
+ | pr_data definer (tyco, (vs, cos)) =
+ concat (
+ str definer
+ :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
+ :: str "="
+ :: separate (str "|") (map pr_co cos)
+ );
val (ps, p) = split_last (pr_data "type" data :: map (pr_data "and") datas');
in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
| pr_def (MLClass (class, (superclasses, (v, classops)))) =
@@ -1210,6 +1224,15 @@
:: map pr_eq eqs
)
end
+ | pr_def (name, CodegenThingol.Datatype (vs, [])) =
+ let
+ val tyvars = CodegenNames.intro_vars (map fst vs) keyword_vars;
+ in
+ semicolon [
+ str "data",
+ pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
+ ]
+ end
| pr_def (name, CodegenThingol.Datatype (vs, [(co, [ty])])) =
let
val tyvars = CodegenNames.intro_vars (map fst vs) keyword_vars;
@@ -1649,7 +1672,6 @@
o Symtab.lookup (CodegenSerializerData.get thy)
) targets;
-val tyco_has_serialization = has_serialization #tyco;
val const_has_serialization = has_serialization #const;