# HG changeset patch # User haftmann # Date 1172846607 -3600 # Node ID 6c7f9207fa9edd61b0a0ed4cfc23f9baf0d8f69b # Parent b573f1f566e12ed5c9b1694ea0956f9c6c8f163e permitting empty datatypes diff -r b573f1f566e1 -r 6c7f9207fa9e src/Pure/Tools/codegen_package.ML --- 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 diff -r b573f1f566e1 -r 6c7f9207fa9e src/Pure/Tools/codegen_serializer.ML --- 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;