simplified, tuned
authorhaftmann
Tue Jul 10 09:23:17 2007 +0200 (2007-07-10)
changeset 23691cedf9610b71d
parent 23690 a5ffe85460af
child 23692 b784849811fc
simplified, tuned
src/Pure/Tools/codegen_consts.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/src/Pure/Tools/codegen_consts.ML	Tue Jul 10 09:23:16 2007 +0200
     1.2 +++ b/src/Pure/Tools/codegen_consts.ML	Tue Jul 10 09:23:17 2007 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val read_bare_const: theory -> string -> string * typ
     1.5    val read_const: theory -> string -> const
     1.6    val read_const_exprs: theory -> (const list -> const list)
     1.7 -    -> string list -> const list
     1.8 +    -> string list -> bool * const list
     1.9  
    1.10    val co_of_const: theory -> const
    1.11      -> string * ((string * sort) list * (string * typ list))
    1.12 @@ -120,8 +120,10 @@
    1.13  
    1.14  in
    1.15  
    1.16 -fun read_const_exprs thy select =
    1.17 -  (op @) o apsnd select o pairself flat o split_list o map (read_const_expr thy);
    1.18 +fun read_const_exprs thy select exprs =
    1.19 +  case (pairself flat o split_list o map (read_const_expr thy)) exprs
    1.20 +   of (consts, []) => (false, consts)
    1.21 +    | (consts, consts') => (true, consts @ select consts');
    1.22  
    1.23  end; (*local*)
    1.24  
     2.1 --- a/src/Pure/Tools/codegen_package.ML	Tue Jul 10 09:23:16 2007 +0200
     2.2 +++ b/src/Pure/Tools/codegen_package.ML	Tue Jul 10 09:23:17 2007 +0200
     2.3 @@ -37,7 +37,6 @@
     2.4  
     2.5  type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
     2.6    -> CodegenFuncgr.T
     2.7 -  -> bool * string list option
     2.8    -> (string * typ) * term list -> CodegenThingol.transact -> iterm * CodegenThingol.transact;
     2.9  
    2.10  type appgens = (int * (appgen * stamp)) Symtab.table;
    2.11 @@ -108,34 +107,15 @@
    2.12  );
    2.13  
    2.14  
    2.15 -
    2.16 -(* preparing defining equations *)
    2.17 -
    2.18 -fun prep_eqs thy (thms as thm :: _) =
    2.19 -  let
    2.20 -    val ty = (Logic.unvarifyT o snd o CodegenFunc.head_func) thm;
    2.21 -    val thms' = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
    2.22 -      then thms
    2.23 -      else map (CodegenFunc.expand_eta 1) thms;
    2.24 -  in (ty, thms') end;
    2.25 -
    2.26 -
    2.27  (* translation kernel *)
    2.28  
    2.29 -fun check_strict (false, _) has_seri x =
    2.30 -      false
    2.31 -  | check_strict (_, SOME targets) has_seri x =
    2.32 -      not (has_seri targets x)
    2.33 -  | check_strict (true, _) has_seri x =
    2.34 -      true;
    2.35 -
    2.36  fun get_abstype thy (tyco, tys) = case Symtab.lookup ((fst o snd o CodegenPackageData.get) thy) tyco
    2.37   of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty)
    2.38    | NONE => NONE;
    2.39  
    2.40  fun ensure_def thy = CodegenThingol.ensure_def (CodegenNames.labelled_name thy);
    2.41  
    2.42 -fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr strct class =
    2.43 +fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr class =
    2.44    let
    2.45      val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
    2.46      val (v, cs) = AxClass.params_of_class thy class;
    2.47 @@ -143,32 +123,31 @@
    2.48      val classrels' = map (curry (CodegenNames.classrel thy) class) superclasses;
    2.49      val classops' = map (CodegenNames.const thy o CodegenConsts.const_of_cexpr thy) cs;
    2.50      val defgen_class =
    2.51 -      fold_map (ensure_def_class thy algbr funcgr strct) superclasses
    2.52 -      ##>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs
    2.53 +      fold_map (ensure_def_class thy algbr funcgr) superclasses
    2.54 +      ##>> (fold_map (exprgen_type thy algbr funcgr) o map snd) cs
    2.55        #-> (fn (superclasses, classoptyps) => succeed
    2.56          (CodegenThingol.Class (superclasses ~~ classrels', (unprefix "'" v, classops' ~~ classoptyps))))
    2.57    in
    2.58      tracing (fn _ => "generating class " ^ quote class)
    2.59 -    #> ensure_def thy defgen_class true
    2.60 -        ("generating class " ^ quote class) class'
    2.61 +    #> ensure_def thy defgen_class ("generating class " ^ quote class) class'
    2.62      #> pair class'
    2.63    end
    2.64 -and ensure_def_classrel thy algbr funcgr strct (subclass, superclass) =
    2.65 -  ensure_def_class thy algbr funcgr strct subclass
    2.66 +and ensure_def_classrel thy algbr funcgr (subclass, superclass) =
    2.67 +  ensure_def_class thy algbr funcgr subclass
    2.68    #>> (fn _ => CodegenNames.classrel thy (subclass, superclass))
    2.69 -and ensure_def_tyco thy algbr funcgr strct "fun" trns =
    2.70 +and ensure_def_tyco thy algbr funcgr "fun" trns =
    2.71        trns
    2.72        |> pair "fun"
    2.73 -  | ensure_def_tyco thy algbr funcgr strct tyco trns =
    2.74 +  | ensure_def_tyco thy algbr funcgr tyco trns =
    2.75        let
    2.76          fun defgen_datatype trns =
    2.77            let
    2.78              val (vs, cos) = CodegenData.get_datatype thy tyco;
    2.79            in
    2.80              trns
    2.81 -            |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
    2.82 +            |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
    2.83              ||>> fold_map (fn (c, tys) =>
    2.84 -              fold_map (exprgen_type thy algbr funcgr strct) tys
    2.85 +              fold_map (exprgen_type thy algbr funcgr) tys
    2.86                #-> (fn tys' =>
    2.87                  pair ((CodegenNames.const thy o CodegenConsts.const_of_cexpr thy)
    2.88                    (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
    2.89 @@ -178,33 +157,32 @@
    2.90        in
    2.91          trns
    2.92          |> tracing (fn _ => "generating type constructor " ^ quote tyco)
    2.93 -        |> ensure_def thy defgen_datatype true
    2.94 -            ("generating type constructor " ^ quote tyco) tyco'
    2.95 +        |> ensure_def thy defgen_datatype ("generating type constructor " ^ quote tyco) tyco'
    2.96          |> pair tyco'
    2.97        end
    2.98 -and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr strct (v, sort) trns =
    2.99 +and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) trns =
   2.100    trns
   2.101 -  |> fold_map (ensure_def_class thy algbr funcgr strct) (proj_sort sort)
   2.102 +  |> fold_map (ensure_def_class thy algbr funcgr) (proj_sort sort)
   2.103    |>> (fn sort => (unprefix "'" v, sort))
   2.104 -and exprgen_type thy algbr funcgr strct (TFree vs) trns =
   2.105 +and exprgen_type thy algbr funcgr (TFree vs) trns =
   2.106        trns
   2.107 -      |> exprgen_tyvar_sort thy algbr funcgr strct vs
   2.108 +      |> exprgen_tyvar_sort thy algbr funcgr vs
   2.109        |>> (fn (v, sort) => ITyVar v)
   2.110 -  | exprgen_type thy algbr funcgr strct (Type (tyco, tys)) trns =
   2.111 +  | exprgen_type thy algbr funcgr (Type (tyco, tys)) trns =
   2.112        case get_abstype thy (tyco, tys)
   2.113         of SOME ty =>
   2.114              trns
   2.115 -            |> exprgen_type thy algbr funcgr strct ty
   2.116 +            |> exprgen_type thy algbr funcgr ty
   2.117          | NONE =>
   2.118              trns
   2.119 -            |> ensure_def_tyco thy algbr funcgr strct tyco
   2.120 -            ||>> fold_map (exprgen_type thy algbr funcgr strct) tys
   2.121 +            |> ensure_def_tyco thy algbr funcgr tyco
   2.122 +            ||>> fold_map (exprgen_type thy algbr funcgr) tys
   2.123              |>> (fn (tyco, tys) => tyco `%% tys);
   2.124  
   2.125  exception CONSTRAIN of (string * typ) * typ;
   2.126  val timing = ref false;
   2.127  
   2.128 -fun exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) =
   2.129 +fun exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
   2.130    let
   2.131      val pp = Sign.pp thy;
   2.132      datatype typarg =
   2.133 @@ -225,16 +203,16 @@
   2.134         type_variable = type_variable}
   2.135        (ty_ctxt, proj_sort sort_decl);
   2.136      fun mk_dict (Global (inst, yss)) =
   2.137 -          ensure_def_inst thy algbr funcgr strct inst
   2.138 +          ensure_def_inst thy algbr funcgr inst
   2.139            ##>> (fold_map o fold_map) mk_dict yss
   2.140            #>> (fn (inst, dss) => DictConst (inst, dss))
   2.141        | mk_dict (Local (classrels, (v, (k, sort)))) =
   2.142 -          fold_map (ensure_def_classrel thy algbr funcgr strct) classrels
   2.143 +          fold_map (ensure_def_classrel thy algbr funcgr) classrels
   2.144            #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
   2.145    in
   2.146      fold_map mk_dict typargs
   2.147    end
   2.148 -and exprgen_dict_parms thy (algbr as (_, consts)) funcgr strct (c, ty_ctxt) =
   2.149 +and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
   2.150    let
   2.151      val c' = CodegenConsts.const_of_cexpr thy (c, ty_ctxt)
   2.152      val idf = CodegenNames.const thy c';
   2.153 @@ -242,9 +220,9 @@
   2.154      val (tys, tys_decl) = pairself (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
   2.155      val sorts = map (snd o dest_TVar) tys_decl;
   2.156    in
   2.157 -    fold_map (exprgen_dicts thy algbr funcgr strct) (tys ~~ sorts)
   2.158 +    fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
   2.159    end
   2.160 -and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr strct (class, tyco) trns =
   2.161 +and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) trns =
   2.162    let
   2.163      val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
   2.164      val (var, classops) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
   2.165 @@ -252,20 +230,20 @@
   2.166      val arity_typ = Type (tyco, map TFree vs);
   2.167      fun gen_superarity superclass trns =
   2.168        trns
   2.169 -      |> ensure_def_class thy algbr funcgr strct superclass
   2.170 -      ||>> ensure_def_classrel thy algbr funcgr strct (class, superclass)
   2.171 -      ||>> exprgen_dicts thy algbr funcgr strct (arity_typ, [superclass])
   2.172 +      |> ensure_def_class thy algbr funcgr superclass
   2.173 +      ||>> ensure_def_classrel thy algbr funcgr (class, superclass)
   2.174 +      ||>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
   2.175        |>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
   2.176              (superclass, (classrel, (inst, dss))));
   2.177      fun gen_classop_def (classop as (c, ty)) trns =
   2.178        trns
   2.179 -      |> ensure_def_const thy algbr funcgr strct (CodegenConsts.const_of_cexpr thy classop)
   2.180 -      ||>> exprgen_term thy algbr funcgr strct (Const (c, map_type_tfree (K arity_typ) ty));
   2.181 +      |> ensure_def_const thy algbr funcgr (CodegenConsts.const_of_cexpr thy classop)
   2.182 +      ||>> exprgen_term thy algbr funcgr (Const (c, map_type_tfree (K arity_typ) ty));
   2.183      fun defgen_inst trns =
   2.184        trns
   2.185 -      |> ensure_def_class thy algbr funcgr strct class
   2.186 -      ||>> ensure_def_tyco thy algbr funcgr strct tyco
   2.187 -      ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
   2.188 +      |> ensure_def_class thy algbr funcgr class
   2.189 +      ||>> ensure_def_tyco thy algbr funcgr tyco
   2.190 +      ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   2.191        ||>> fold_map gen_superarity superclasses
   2.192        ||>> fold_map gen_classop_def classops
   2.193        |-> (fn ((((class, tyco), arity), superarities), classops) =>
   2.194 @@ -274,99 +252,95 @@
   2.195    in
   2.196      trns
   2.197      |> tracing (fn _ => "generating instance " ^ quote class ^ " / " ^ quote tyco)
   2.198 -    |> ensure_def thy defgen_inst true ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
   2.199 +    |> ensure_def thy defgen_inst ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
   2.200      |> pair inst
   2.201    end
   2.202 -and ensure_def_const thy (algbr as (_, consts)) funcgr strct (const as (c, opt_tyco)) trns =
   2.203 +and ensure_def_const thy (algbr as (_, consts)) funcgr (const as (c, opt_tyco)) trns =
   2.204    let
   2.205      val c' = CodegenNames.const thy const;
   2.206      fun defgen_datatypecons trns =
   2.207        trns
   2.208 -      |> ensure_def_tyco thy algbr funcgr strct
   2.209 +      |> ensure_def_tyco thy algbr funcgr
   2.210            ((the o CodegenData.get_datatype_of_constr thy) const)
   2.211        |-> (fn _ => succeed CodegenThingol.Bot);
   2.212      fun defgen_classop trns =
   2.213        trns
   2.214 -      |> ensure_def_class thy algbr funcgr strct ((the o AxClass.class_of_param thy) c)
   2.215 +      |> ensure_def_class thy algbr funcgr ((the o AxClass.class_of_param thy) c)
   2.216        |-> (fn _ => succeed CodegenThingol.Bot);
   2.217      fun defgen_fun trns =
   2.218 -      case CodegenFuncgr.funcs funcgr
   2.219 -        (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) const)
   2.220 -       of thms as _ :: _ =>
   2.221 -            let
   2.222 -              val (ty, eq_thms) = prep_eqs thy thms;
   2.223 -              val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
   2.224 -                else I;
   2.225 -              val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
   2.226 -              val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
   2.227 -              val dest_eqthm =
   2.228 -                apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
   2.229 -              fun exprgen_eq (args, rhs) trns =
   2.230 -                trns
   2.231 -                |> fold_map (exprgen_term thy algbr funcgr strct) args
   2.232 -                ||>> exprgen_term thy algbr funcgr strct rhs;
   2.233 -            in
   2.234 -              trns
   2.235 -              |> CodegenThingol.message msg (fn trns => trns
   2.236 -              |> timeap (fold_map (exprgen_eq o dest_eqthm) eq_thms)
   2.237 -              ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs
   2.238 -              ||>> exprgen_type thy algbr funcgr strct ty
   2.239 -              |-> (fn ((eqs, vs), ty) => succeed (CodegenThingol.Fun (eqs, (vs, ty)))))
   2.240 -            end
   2.241 -        | [] =>
   2.242 -              trns
   2.243 -              |> fail ("No defining equations found for "
   2.244 -                   ^ (quote o CodegenConsts.string_of_const thy) const);
   2.245 +      let
   2.246 +        val const' = perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) const;
   2.247 +        val raw_thms = CodegenFuncgr.funcs funcgr const';
   2.248 +        val ty = (Logic.unvarifyT o CodegenFuncgr.typ funcgr) const';
   2.249 +        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
   2.250 +          then raw_thms
   2.251 +          else map (CodegenFunc.expand_eta 1) raw_thms;
   2.252 +        val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
   2.253 +          else I;
   2.254 +        val msg = cat_lines ("generating code for theorems " :: map string_of_thm thms);
   2.255 +        val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
   2.256 +        val dest_eqthm =
   2.257 +          apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
   2.258 +        fun exprgen_eq (args, rhs) trns =
   2.259 +          trns
   2.260 +          |> fold_map (exprgen_term thy algbr funcgr) args
   2.261 +          ||>> exprgen_term thy algbr funcgr rhs;
   2.262 +      in
   2.263 +        trns
   2.264 +        |> CodegenThingol.message msg (fn trns => trns
   2.265 +        |> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
   2.266 +        ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   2.267 +        ||>> exprgen_type thy algbr funcgr ty
   2.268 +        |-> (fn ((eqs, vs), ty) => succeed (CodegenThingol.Fun (eqs, (vs, ty)))))
   2.269 +      end;
   2.270      val defgen = if (is_some o CodegenData.get_datatype_of_constr thy) const
   2.271        then defgen_datatypecons
   2.272        else if is_some opt_tyco
   2.273          orelse (not o is_some o AxClass.class_of_param thy) c
   2.274        then defgen_fun
   2.275        else defgen_classop
   2.276 -    val strict = check_strict strct (CodegenSerializer.const_has_serialization thy) c';
   2.277    in
   2.278      trns
   2.279      |> tracing (fn _ => "generating constant "
   2.280          ^ (quote o CodegenConsts.string_of_const thy) const)
   2.281 -    |> ensure_def thy defgen strict ("generating constant "
   2.282 -         ^ CodegenConsts.string_of_const thy const) c'
   2.283 +    |> ensure_def thy defgen ("generating constant " ^ CodegenConsts.string_of_const thy const) c'
   2.284      |> pair c'
   2.285    end
   2.286 -and exprgen_term thy algbr funcgr strct (Const (c, ty)) trns =
   2.287 +and exprgen_term thy algbr funcgr (Const (c, ty)) trns =
   2.288        trns
   2.289 -      |> select_appgen thy algbr funcgr strct ((c, ty), [])
   2.290 -  | exprgen_term thy algbr funcgr strct (Free (v, ty)) trns =
   2.291 +      |> select_appgen thy algbr funcgr ((c, ty), [])
   2.292 +  | exprgen_term thy algbr funcgr (Free (v, ty)) trns =
   2.293        trns
   2.294 -      |> exprgen_type thy algbr funcgr strct ty
   2.295 +      |> exprgen_type thy algbr funcgr ty
   2.296        |>> (fn _ => IVar v)
   2.297 -  | exprgen_term thy algbr funcgr strct (Abs (raw_v, ty, raw_t)) trns =
   2.298 +  | exprgen_term thy algbr funcgr (Abs (raw_v, ty, raw_t)) trns =
   2.299        let
   2.300          val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t);
   2.301        in
   2.302          trns
   2.303 -        |> exprgen_type thy algbr funcgr strct ty
   2.304 -        ||>> exprgen_term thy algbr funcgr strct t
   2.305 +        |> exprgen_type thy algbr funcgr ty
   2.306 +        ||>> exprgen_term thy algbr funcgr t
   2.307          |>> (fn (ty, t) => (v, ty) `|-> t)
   2.308        end
   2.309 -  | exprgen_term thy algbr funcgr strct (t as _ $ _) trns =
   2.310 +  | exprgen_term thy algbr funcgr (t as _ $ _) trns =
   2.311        case strip_comb t
   2.312         of (Const (c, ty), ts) =>
   2.313              trns
   2.314 -            |> select_appgen thy algbr funcgr strct ((c, ty), ts)
   2.315 +            |> select_appgen thy algbr funcgr ((c, ty), ts)
   2.316          | (t', ts) =>
   2.317              trns
   2.318 -            |> exprgen_term thy algbr funcgr strct t'
   2.319 -            ||>> fold_map (exprgen_term thy algbr funcgr strct) ts
   2.320 +            |> exprgen_term thy algbr funcgr t'
   2.321 +            ||>> fold_map (exprgen_term thy algbr funcgr) ts
   2.322              |>> (fn (t, ts) => t `$$ ts)
   2.323 -and appgen_default thy algbr funcgr strct ((c, ty), ts) trns =
   2.324 +and appgen_default thy algbr funcgr ((c, ty), ts) trns =
   2.325    trns
   2.326 -  |> ensure_def_const thy algbr funcgr strct (CodegenConsts.const_of_cexpr thy (c, ty))
   2.327 -  ||>> fold_map (exprgen_type thy algbr funcgr strct) ((fst o Term.strip_type) ty)
   2.328 -  ||>> exprgen_type thy algbr funcgr strct ((snd o Term.strip_type) ty)
   2.329 -  ||>> exprgen_dict_parms thy algbr funcgr strct (c, ty)
   2.330 -  ||>> fold_map (exprgen_term thy algbr funcgr strct) ts
   2.331 +  |> ensure_def_const thy algbr funcgr (CodegenConsts.const_of_cexpr thy (c, ty))
   2.332 +  ||>> fold_map (exprgen_type thy algbr funcgr) ((fst o Term.strip_type) ty)
   2.333 +  ||>> exprgen_type thy algbr funcgr ((snd o Term.strip_type) ty)
   2.334 +  ||>> exprgen_dict_parms thy algbr funcgr (c, ty)
   2.335 +  ||>> fold_map (exprgen_term thy algbr funcgr) ts
   2.336    |>> (fn ((((c, tys), ty), iss), ts) => IConst (c, (iss, tys)) `$$ ts)
   2.337 -and select_appgen thy algbr funcgr strct ((c, ty), ts) trns =
   2.338 +and select_appgen thy algbr funcgr ((c, ty), ts) trns =
   2.339    case Symtab.lookup (fst (CodegenPackageData.get thy)) c
   2.340     of SOME (i, (appgen, _)) =>
   2.341          if length ts < i then
   2.342 @@ -378,40 +352,40 @@
   2.343              val vs = Name.names ctxt "a" tys;
   2.344            in
   2.345              trns
   2.346 -            |> fold_map (exprgen_type thy algbr funcgr strct) tys
   2.347 -            ||>> appgen thy algbr funcgr strct ((c, ty), ts @ map Free vs)
   2.348 +            |> fold_map (exprgen_type thy algbr funcgr) tys
   2.349 +            ||>> appgen thy algbr funcgr ((c, ty), ts @ map Free vs)
   2.350              |>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
   2.351            end
   2.352          else if length ts > i then
   2.353            trns
   2.354 -          |> appgen thy algbr funcgr strct ((c, ty), Library.take (i, ts))
   2.355 -          ||>> fold_map (exprgen_term thy algbr funcgr strct) (Library.drop (i, ts))
   2.356 +          |> appgen thy algbr funcgr ((c, ty), Library.take (i, ts))
   2.357 +          ||>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
   2.358            |>> (fn (t, ts) => t `$$ ts)
   2.359          else
   2.360            trns
   2.361 -          |> appgen thy algbr funcgr strct ((c, ty), ts)
   2.362 +          |> appgen thy algbr funcgr ((c, ty), ts)
   2.363      | NONE =>
   2.364          trns
   2.365 -        |> appgen_default thy algbr funcgr strct ((c, ty), ts);
   2.366 +        |> appgen_default thy algbr funcgr ((c, ty), ts);
   2.367  
   2.368  
   2.369  (* entrance points into translation kernel *)
   2.370  
   2.371 -fun ensure_def_const' thy algbr funcgr strct c trns =
   2.372 -  ensure_def_const thy algbr funcgr strct c trns
   2.373 +fun ensure_def_const' thy algbr funcgr c trns =
   2.374 +  ensure_def_const thy algbr funcgr c trns
   2.375    handle CONSTRAIN ((c, ty), ty_decl) => error (
   2.376      "Constant " ^ c ^ " with most general type\n"
   2.377      ^ CodegenConsts.string_of_typ thy ty
   2.378      ^ "\noccurs with type\n"
   2.379      ^ CodegenConsts.string_of_typ thy ty_decl);
   2.380  
   2.381 -fun perhaps_def_const thy algbr funcgr strct c trns =
   2.382 -  case try (ensure_def_const thy algbr funcgr strct c) trns
   2.383 +fun perhaps_def_const thy algbr funcgr c trns =
   2.384 +  case try (ensure_def_const thy algbr funcgr c) trns
   2.385     of SOME (c, trns) => (SOME c, trns)
   2.386      | NONE => (NONE, trns);
   2.387  
   2.388 -fun exprgen_term' thy algbr funcgr strct t trns =
   2.389 -  exprgen_term thy algbr funcgr strct t trns
   2.390 +fun exprgen_term' thy algbr funcgr t trns =
   2.391 +  exprgen_term thy algbr funcgr t trns
   2.392    handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t
   2.393      ^ ",\nconstant " ^ c ^ " with most general type\n"
   2.394      ^ CodegenConsts.string_of_typ thy ty
   2.395 @@ -422,27 +396,27 @@
   2.396  (* parametrized application generators, for instantiation in object logic *)
   2.397  (* (axiomatic extensions of translation kernel) *)
   2.398  
   2.399 -fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns =
   2.400 +fun appgen_case dest_case_expr thy algbr funcgr (app as (c_ty, ts)) trns =
   2.401    let
   2.402      val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
   2.403      fun clausegen (dt, bt) trns =
   2.404        trns
   2.405 -      |> exprgen_term thy algbr funcgr strct dt
   2.406 -      ||>> exprgen_term thy algbr funcgr strct bt;
   2.407 +      |> exprgen_term thy algbr funcgr dt
   2.408 +      ||>> exprgen_term thy algbr funcgr bt;
   2.409    in
   2.410      trns
   2.411 -    |> exprgen_term thy algbr funcgr strct st
   2.412 -    ||>> exprgen_type thy algbr funcgr strct sty
   2.413 +    |> exprgen_term thy algbr funcgr st
   2.414 +    ||>> exprgen_type thy algbr funcgr sty
   2.415      ||>> fold_map clausegen ds
   2.416      |>> (fn ((se, sty), ds) => ICase ((se, sty), ds))
   2.417    end;
   2.418  
   2.419 -fun appgen_let thy algbr funcgr strct (app as (_, [st, ct])) trns =
   2.420 +fun appgen_let thy algbr funcgr (app as (_, [st, ct])) trns =
   2.421    trns
   2.422 -  |> exprgen_term thy algbr funcgr strct ct
   2.423 -  ||>> exprgen_term thy algbr funcgr strct st
   2.424 +  |> exprgen_term thy algbr funcgr ct
   2.425 +  ||>> exprgen_term thy algbr funcgr st
   2.426    |-> (fn ((v, ty) `|-> be, se) => pair (CodegenThingol.collapse_let (((v, ty), se), be))
   2.427 -        | _ => appgen_default thy algbr funcgr strct app);
   2.428 +        | _ => appgen_default thy algbr funcgr app);
   2.429  
   2.430  fun add_appconst (c, appgen) thy =
   2.431    let
   2.432 @@ -534,7 +508,7 @@
   2.433  
   2.434  (* generic generation combinators *)
   2.435  
   2.436 -fun generate thy funcgr targets gen it =
   2.437 +fun generate thy funcgr gen it =
   2.438    let
   2.439      val cs = map_filter (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy))
   2.440        (CodegenFuncgr.all funcgr);
   2.441 @@ -546,8 +520,8 @@
   2.442             (CodegenFuncgr.all funcgr');
   2.443      val algbr = (CodegenData.operational_algebra thy, consttab);
   2.444    in   
   2.445 -    Code.change_yield thy (CodegenThingol.start_transact (gen thy algbr funcgr'
   2.446 -        (true, targets) it))
   2.447 +    Code.change_yield thy
   2.448 +      (CodegenThingol.start_transact (gen thy algbr funcgr' it))
   2.449      |> fst
   2.450    end;
   2.451  
   2.452 @@ -556,7 +530,7 @@
   2.453      val ct = Thm.cterm_of thy t;
   2.454      val (ct', funcgr) = Funcgr.make_term thy (K (K K)) ct;
   2.455      val t' = Thm.term_of ct';
   2.456 -  in generate thy funcgr (SOME []) exprgen_term' t' end;
   2.457 +  in generate thy funcgr exprgen_term' t' end;
   2.458  
   2.459  fun raw_eval_term thy (ref_spec, t) args =
   2.460    let
   2.461 @@ -575,10 +549,10 @@
   2.462  fun satisfies thy t witnesses = raw_eval_term thy
   2.463    (("CodegenPackage.satisfies_ref", satisfies_ref), t) witnesses;
   2.464  
   2.465 -fun filter_generatable thy targets consts =
   2.466 +fun filter_generatable thy consts =
   2.467    let
   2.468      val (consts', funcgr) = Funcgr.make_consts thy consts;
   2.469 -    val consts'' = generate thy funcgr targets (fold_map oooo perhaps_def_const) consts';
   2.470 +    val consts'' = generate thy funcgr (fold_map ooo perhaps_def_const) consts';
   2.471      val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE)
   2.472        (consts' ~~ consts'');
   2.473    in consts''' end;
   2.474 @@ -593,40 +567,37 @@
   2.475  
   2.476  fun code raw_cs seris thy =
   2.477    let
   2.478 -    val seris' = map (fn ((target, file), args) =>
   2.479 -      (target, SOME (CodegenSerializer.get_serializer thy target file args
   2.480 -        CodegenNames.labelled_name))) seris;
   2.481 -    val targets = case map fst seris' of [] => NONE | xs => SOME xs;
   2.482 -    val cs = CodegenConsts.read_const_exprs thy
   2.483 -      (filter_generatable thy targets) raw_cs;
   2.484 -    fun generate' thy = case cs
   2.485 -     of [] => []
   2.486 -      | _ =>
   2.487 -          generate thy (Funcgr.make thy cs) targets
   2.488 -            (fold_map oooo ensure_def_const') cs;
   2.489 -    fun serialize' [] code seri =
   2.490 -          seri NONE code 
   2.491 -      | serialize' cs code seri =
   2.492 -          seri (SOME cs) code;
   2.493 -    val cs = generate' thy;
   2.494 +    val (perm1, cs) = CodegenConsts.read_const_exprs thy
   2.495 +      (filter_generatable thy) raw_cs;
   2.496 +    val (perm2, cs') = case generate thy (Funcgr.make thy cs) (fold_map ooo ensure_def_const') cs
   2.497 +     of [] => (true, NONE)
   2.498 +      | cs => (false, SOME cs);
   2.499      val code = Code.get thy;
   2.500 +    val seris' = map (fn (((target, module), file), args) =>
   2.501 +      CodegenSerializer.get_serializer thy target (perm1 orelse perm2) module file args
   2.502 +        CodegenNames.labelled_name cs') seris;
   2.503    in
   2.504 -    (map (serialize' cs code) (map_filter snd seris'); ())
   2.505 +    (map (fn f => f code) seris' : unit list; ())
   2.506    end;
   2.507  
   2.508  fun code_thms_cmd thy =
   2.509 -  code_thms thy o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy);
   2.510 +  code_thms thy o snd o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy);
   2.511  
   2.512  fun code_deps_cmd thy =
   2.513 -  code_deps thy o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy);
   2.514 +  code_deps thy o snd o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy);
   2.515 +
   2.516 +val (inK, toK, fileK) = ("in", "to", "file");
   2.517  
   2.518  val code_exprP =
   2.519    (Scan.repeat P.term
   2.520 -  -- Scan.repeat (P.$$$ "in" |-- P.name
   2.521 -     -- Scan.option (P.$$$ "file" |-- P.name)
   2.522 +  -- Scan.repeat (P.$$$ inK |-- P.name
   2.523 +     -- Scan.option (P.$$$ toK |-- P.name)
   2.524 +     -- Scan.option (P.$$$ fileK |-- P.name)
   2.525       -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
   2.526    ) >> (fn (raw_cs, seris) => code raw_cs seris));
   2.527  
   2.528 +val _ = OuterSyntax.add_keywords [inK, toK, fileK];
   2.529 +
   2.530  val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) =
   2.531    ("code_gen", "code_abstype", "code_axioms", "code_thms", "code_deps");
   2.532  
     3.1 --- a/src/Pure/Tools/codegen_serializer.ML	Tue Jul 10 09:23:16 2007 +0200
     3.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Tue Jul 10 09:23:17 2007 +0200
     3.3 @@ -31,12 +31,10 @@
     3.4  
     3.5    type serializer;
     3.6    val add_serializer: string * serializer -> theory -> theory;
     3.7 -  val get_serializer: theory -> string -> string option -> Args.T list -> (theory -> string -> string)
     3.8 -    -> string list option -> CodegenThingol.code -> unit;
     3.9 +  val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
    3.10 +    -> (theory -> string -> string) -> string list option -> CodegenThingol.code -> unit;
    3.11    val assert_serializer: theory -> string -> string;
    3.12  
    3.13 -  val const_has_serialization: theory -> string list -> string -> bool;
    3.14 -
    3.15    val eval_verbose: bool ref;
    3.16    val eval_term: theory -> (theory -> string -> string) -> CodegenThingol.code
    3.17      -> (string * 'a option ref) * CodegenThingol.iterm -> string list -> 'a;
    3.18 @@ -860,9 +858,10 @@
    3.19  val code_width = ref 80;
    3.20  fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
    3.21  
    3.22 -fun seri_ml pr_def pr_modl output labelled_name reserved_syms module_alias module_prolog
    3.23 +fun seri_ml pr_def pr_modl module output labelled_name reserved_syms raw_module_alias module_prolog
    3.24    (_ : string -> class_syntax option) tyco_syntax const_syntax code =
    3.25    let
    3.26 +    val module_alias = if is_some module then K module else raw_module_alias;
    3.27      val is_cons = fn node => case CodegenThingol.get_def code node
    3.28       of CodegenThingol.Datatypecons _ => true
    3.29        | _ => false;
    3.30 @@ -1022,22 +1021,27 @@
    3.31            SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
    3.32              @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
    3.33                  o rev o flat o Graph.strong_conn) nodes)));
    3.34 -    val p = pr_modl "ROOT" (the_prolog "" @ separate (str "") ((map_filter
    3.35 +    val mk_frame = if is_some module
    3.36 +      then Pretty.chunks
    3.37 +      else pr_modl "ROOT"
    3.38 +    val p = mk_frame (the_prolog "" @ separate (str "") ((map_filter
    3.39        (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes))
    3.40    in output p end;
    3.41  
    3.42 -fun isar_seri_sml file =
    3.43 +val eval_verbose = ref false;
    3.44 +
    3.45 +fun isar_seri_sml module file =
    3.46    let
    3.47      val output = case file
    3.48 -     of NONE => use_text "generated code" Output.ml_output false o code_output
    3.49 +     of NONE => use_text "generated code" Output.ml_output (!eval_verbose) o code_output
    3.50        | SOME "-" => writeln o code_output
    3.51        | SOME file => File.write (Path.explode file) o code_output;
    3.52    in
    3.53      parse_args (Scan.succeed ())
    3.54 -    #> (fn () => seri_ml pr_sml pr_sml_modl output)
    3.55 +    #> (fn () => seri_ml pr_sml pr_sml_modl module output)
    3.56    end;
    3.57  
    3.58 -fun isar_seri_ocaml file =
    3.59 +fun isar_seri_ocaml module file =
    3.60    let
    3.61      val output = case file
    3.62       of NONE => error "OCaml: no internal compilation"
    3.63 @@ -1047,7 +1051,7 @@
    3.64      val output_diag = writeln o code_output;
    3.65    in
    3.66      parse_args (Scan.succeed ())
    3.67 -    #> (fn () => seri_ml pr_ocaml pr_ocaml_modl output)
    3.68 +    #> (fn () => seri_ml pr_ocaml pr_ocaml_modl module output)
    3.69    end;
    3.70  
    3.71  
    3.72 @@ -1296,10 +1300,11 @@
    3.73  
    3.74  end; (*local*)
    3.75  
    3.76 -fun seri_haskell module_prefix destination string_classes labelled_name reserved_syms module_alias module_prolog
    3.77 -  class_syntax tyco_syntax const_syntax code =
    3.78 +fun seri_haskell module_prefix module destination string_classes labelled_name
    3.79 +  reserved_syms raw_module_alias module_prolog class_syntax tyco_syntax const_syntax code =
    3.80    let
    3.81      val _ = Option.map File.check destination;
    3.82 +    val module_alias = if is_some module then K module else raw_module_alias;
    3.83      val init_names = Name.make_context reserved_syms;
    3.84      val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;
    3.85      fun add_def (name, (def, deps)) =
    3.86 @@ -1413,7 +1418,7 @@
    3.87        end;
    3.88    in Symtab.fold (fn modl => fn () => seri_module modl) code' () end;
    3.89  
    3.90 -fun isar_seri_haskell file =
    3.91 +fun isar_seri_haskell module file =
    3.92    let
    3.93      val destination = case file
    3.94       of NONE => error ("Haskell: no internal compilation")
    3.95 @@ -1423,13 +1428,13 @@
    3.96      parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
    3.97        -- Scan.optional (Args.$$$ "string_classes" >> K true) false
    3.98        >> (fn (module_prefix, string_classes) =>
    3.99 -        seri_haskell module_prefix destination string_classes))
   3.100 +        seri_haskell module_prefix module destination string_classes))
   3.101    end;
   3.102  
   3.103  
   3.104  (** diagnosis serializer **)
   3.105  
   3.106 -fun seri_diagnosis labelled_name _ _ _ _ _ code =
   3.107 +fun seri_diagnosis labelled_name _ _ _ _ _ _ code =
   3.108    let
   3.109      val init_names = CodegenNames.make_vars [];
   3.110      fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
   3.111 @@ -1490,6 +1495,7 @@
   3.112  
   3.113  type serializer =
   3.114    string option
   3.115 +  -> string option
   3.116    -> Args.T list
   3.117    -> (string -> string)
   3.118    -> string list
   3.119 @@ -1577,7 +1583,7 @@
   3.120    #> add_serializer (target_diag, (fn _ => fn _ => fn _ => seri_diagnosis))
   3.121  );
   3.122  
   3.123 -fun get_serializer thy target file args labelled_name = fn cs =>
   3.124 +fun get_serializer thy target permissive module file args labelled_name = fn cs =>
   3.125    let
   3.126      val data = case Symtab.lookup (CodegenSerializerData.get thy) target
   3.127       of SOME data => data
   3.128 @@ -1587,31 +1593,29 @@
   3.129      val { alias, prolog } = the_syntax_modl data;
   3.130      val { class, inst, tyco, const } = the_syntax_expr data;
   3.131      val project = if target = target_diag then I
   3.132 -      else CodegenThingol.project_code
   3.133 +      else CodegenThingol.project_code permissive
   3.134          (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs;
   3.135 +    fun check_empty_funs code = case CodegenThingol.empty_funs code
   3.136 +     of [] => code
   3.137 +      | names => error ("No defining equations for " ^ commas (map (labelled_name thy) names));
   3.138    in
   3.139 -    project #> seri file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
   3.140 +    project
   3.141 +    #> check_empty_funs
   3.142 +    #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
   3.143        (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   3.144    end;
   3.145  
   3.146 -val eval_verbose = ref false;
   3.147 -
   3.148  fun eval_term thy labelled_name code ((ref_name, reff), t) args =
   3.149    let
   3.150 -    val val_name = "eval.EVAL.EVAL";
   3.151 -    val val_name' = "ROOT.eval.EVAL";
   3.152 +    val val_name = "Isabelle_Eval.EVAL.EVAL";
   3.153 +    val val_name' = "Isabelle_Eval.EVAL";
   3.154      val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
   3.155 -    val data = (the o Symtab.lookup (CodegenSerializerData.get thy)) "SML"
   3.156 -    val reserved_syms = the_reserved data;
   3.157 -    val { alias, prolog } = the_syntax_modl data;
   3.158 -    val { class, inst, tyco, const } = the_syntax_expr data;
   3.159 -    fun eval p = (
   3.160 +    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] labelled_name;
   3.161 +    fun eval code = (
   3.162        reff := NONE;
   3.163 -      if !eval_verbose then Pretty.writeln p else ();
   3.164 +      seri (SOME [val_name]) code;
   3.165        use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
   3.166 -        ((Pretty.output o Pretty.chunks) [p,
   3.167 -          str ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name'_args ^ "))")
   3.168 -        ]);
   3.169 +        ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name'_args ^ "))");
   3.170        case !reff
   3.171         of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
   3.172              ^ " (reference probably has been shadowed)")
   3.173 @@ -1620,20 +1624,9 @@
   3.174    in
   3.175      code
   3.176      |> CodegenThingol.add_eval_def (val_name, t)
   3.177 -    |> CodegenThingol.project_code
   3.178 -        (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const)
   3.179 -          (SOME [val_name])
   3.180 -    |> seri_ml pr_sml pr_sml_modl I (labelled_name thy) reserved_syms
   3.181 -        (Symtab.lookup alias) (Symtab.lookup prolog)
   3.182 -        (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   3.183      |> eval
   3.184    end;
   3.185  
   3.186 -fun const_has_serialization thy targets name =
   3.187 -  forall (
   3.188 -    is_some o (fn tab => Symtab.lookup tab name) o #const o the_syntax_expr o the
   3.189 -      o Symtab.lookup (CodegenSerializerData.get thy)
   3.190 -  ) targets;
   3.191  
   3.192  
   3.193  (** optional pretty serialization **)
     4.1 --- a/src/Pure/Tools/codegen_thingol.ML	Tue Jul 10 09:23:16 2007 +0200
     4.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Tue Jul 10 09:23:17 2007 +0200
     4.3 @@ -72,11 +72,13 @@
     4.4    val empty_code: code;
     4.5    val get_def: code -> string -> def;
     4.6    val merge_code: code * code -> code;
     4.7 -  val project_code: string list (*hidden*) -> string list option (*selected*)
     4.8 +  val project_code: bool (*delete empty funs*)
     4.9 +    -> string list (*hidden*) -> string list option (*selected*)
    4.10      -> code -> code;
    4.11 +  val empty_funs: code -> string list;
    4.12    val add_eval_def: string (*bind name*) * iterm -> code -> code;
    4.13  
    4.14 -  val ensure_def: (string -> string) -> (transact -> def * code) -> bool -> string
    4.15 +  val ensure_def: (string -> string) -> (transact -> def * code) -> string
    4.16      -> string -> transact -> transact;
    4.17    val succeed: 'a -> transact -> 'a * code;
    4.18    val fail: string -> transact -> 'a * code;
    4.19 @@ -262,7 +264,6 @@
    4.20    | Classinst of (class * (string * (vname * sort) list))
    4.21          * ((class * (string * (string * dict list list))) list
    4.22        * (string * iterm) list);
    4.23 -val eq_def = (op =) : def * def -> bool;
    4.24  
    4.25  type code = def Graph.T;
    4.26  type transact = Graph.key option * code;
    4.27 @@ -277,44 +278,45 @@
    4.28  
    4.29  fun ensure_bot name = Graph.default_node (name, Bot);
    4.30  
    4.31 -fun add_def_incr strict (name, Bot) code =
    4.32 +fun add_def_incr (name, Bot) code =
    4.33        (case the_default Bot (try (get_def code) name)
    4.34 -       of Bot => if strict then error "Attempted to add Bot to code"
    4.35 -            else Graph.map_node name (K Bot) code
    4.36 +       of Bot => error "Attempted to add Bot to code"
    4.37          | _ => code)
    4.38 -  | add_def_incr _ (name, def) code =
    4.39 +  | add_def_incr (name, def) code =
    4.40        (case try (get_def code) name
    4.41         of NONE => Graph.new_node (name, def) code
    4.42          | SOME Bot => Graph.map_node name (K def) code
    4.43 -        | SOME def' => if eq_def (def, def')
    4.44 -            then code
    4.45 -            else error ("Tried to overwrite definition " ^ quote name));
    4.46 +        | SOME _ => error ("Tried to overwrite definition " ^ quote name));
    4.47  
    4.48  fun add_dep (dep as (name1, name2)) =
    4.49    if name1 = name2 then I else Graph.add_edge dep;
    4.50  
    4.51 -val merge_code = Graph.join (fn _ => fn def12 => if eq_def def12 then fst def12 else Bot);
    4.52 +val merge_code : code * code -> code = Graph.merge (K true);
    4.53  
    4.54 -fun project_code hidden raw_selected code =
    4.55 +fun project_code delete_empty_funs hidden raw_selected code =
    4.56    let
    4.57 -    fun is_bot name = case get_def code name
    4.58 -     of Bot => true
    4.59 +    fun is_empty_fun name = case get_def code name
    4.60 +     of Fun ([], _) => true
    4.61        | _ => false;
    4.62      val names = subtract (op =) hidden (Graph.keys code);
    4.63 -    val deleted = Graph.all_preds code (filter is_bot names);
    4.64 +    val deleted = Graph.all_preds code (filter is_empty_fun names);
    4.65      val selected = case raw_selected
    4.66       of NONE => names |> subtract (op =) deleted 
    4.67        | SOME sel => sel
    4.68 -          |> subtract (op =) deleted
    4.69 +          |> delete_empty_funs ? subtract (op =) deleted
    4.70            |> subtract (op =) hidden
    4.71            |> Graph.all_succs code
    4.72 -          |> subtract (op =) deleted
    4.73 +          |> delete_empty_funs ? subtract (op =) deleted
    4.74            |> subtract (op =) hidden;
    4.75    in
    4.76      code
    4.77      |> Graph.subgraph (member (op =) selected)
    4.78    end;
    4.79  
    4.80 +fun empty_funs code =
    4.81 +  Graph.fold (fn (name, (Fun ([], _), _)) => cons name
    4.82 +               | _ => I) code [];
    4.83 +
    4.84  fun check_samemodule names =
    4.85    fold (fn name =>
    4.86      let
    4.87 @@ -366,19 +368,19 @@
    4.88  fun postprocess_def (name, Datatype (_, constrs)) =
    4.89        tap (fn _ => check_samemodule (name :: map fst constrs))
    4.90        #> fold (fn (co, _) =>
    4.91 -        add_def_incr true (co, Datatypecons name)
    4.92 +        add_def_incr (co, Datatypecons name)
    4.93          #> add_dep (co, name)
    4.94          #> add_dep (name, co)
    4.95        ) constrs
    4.96    | postprocess_def (name, Class (classrels, (_, classops))) =
    4.97        tap (fn _ => check_samemodule (name :: map fst classops @ map snd classrels))
    4.98        #> fold (fn (f, _) =>
    4.99 -        add_def_incr true (f, Classop name)
   4.100 +        add_def_incr (f, Classop name)
   4.101          #> add_dep (f, name)
   4.102          #> add_dep (name, f)
   4.103        ) classops
   4.104        #> fold (fn (superclass, classrel) =>
   4.105 -        add_def_incr true (classrel, Classrel (name, superclass))
   4.106 +        add_def_incr (classrel, Classrel (name, superclass))
   4.107          #> add_dep (classrel, name)
   4.108          #> add_dep (name, classrel)
   4.109        ) classrels
   4.110 @@ -388,12 +390,11 @@
   4.111  
   4.112  (* transaction protocol *)
   4.113  
   4.114 -fun ensure_def labelled_name defgen strict msg name (dep, code) =
   4.115 +fun ensure_def labelled_name defgen msg name (dep, code) =
   4.116    let
   4.117      val msg' = (case dep
   4.118       of NONE => msg
   4.119 -      | SOME dep => msg ^ ", required for " ^ labelled_name dep)
   4.120 -      ^ (if strict then " (strict)" else " (non-strict)");
   4.121 +      | SOME dep => msg ^ ", required for " ^ labelled_name dep);
   4.122      fun add_dp NONE = I
   4.123        | add_dp (SOME dep) =
   4.124            tracing (fn _ => "adding dependency " ^ labelled_name dep
   4.125 @@ -402,24 +403,19 @@
   4.126      fun prep_def def code =
   4.127        (check_prep_def code def, code);
   4.128      fun invoke_generator name defgen code =
   4.129 -      defgen (SOME name, code)
   4.130 -        handle FAIL msgs =>
   4.131 -          if strict then raise FAIL (msg' :: msgs)
   4.132 -          else (Bot, code);
   4.133 -  in
   4.134 -    code
   4.135 -    |> (if can (get_def code) name
   4.136 -        then
   4.137 -          add_dp dep
   4.138 -        else
   4.139 +      defgen (SOME name, code) handle FAIL msgs => raise FAIL (msg' :: msgs);
   4.140 +    fun add_def false =
   4.141            ensure_bot name
   4.142            #> add_dp dep
   4.143            #> invoke_generator name defgen
   4.144            #-> (fn def => prep_def def)
   4.145 -          #-> (fn def =>
   4.146 -             add_def_incr strict (name, def)
   4.147 -          #> postprocess_def (name, def)
   4.148 -       ))
   4.149 +          #-> (fn def => add_def_incr (name, def)
   4.150 +          #> postprocess_def (name, def))
   4.151 +      | add_def true =
   4.152 +          add_dp dep;
   4.153 +  in
   4.154 +    code
   4.155 +    |> add_def (can (get_def code) name)
   4.156      |> pair dep
   4.157    end;
   4.158