improvements for lazy code generation
authorhaftmann
Tue Jul 25 16:43:47 2006 +0200 (2006-07-25)
changeset 20191b43fd26e1aaa
parent 20190 03a8d7c070d3
child 20192 956cd30ef3be
improvements for lazy code generation
src/HOL/ex/NormalForm.thy
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_theorems.ML
src/Pure/Tools/codegen_thingol.ML
src/Pure/Tools/nbe.ML
     1.1 --- a/src/HOL/ex/NormalForm.thy	Tue Jul 25 16:43:33 2006 +0200
     1.2 +++ b/src/HOL/ex/NormalForm.thy	Tue Jul 25 16:43:47 2006 +0200
     1.3 @@ -104,11 +104,7 @@
     1.4  normal_form "last[a,b,c]"
     1.5  normal_form "last([a,b,c]@xs)"
     1.6  
     1.7 -(* FIXME
     1.8 -  won't work since it relies on 
     1.9 -  polymorphically used ad-hoc overloaded function:
    1.10 -  normal_form "max 0 (0::nat)"
    1.11 -*)
    1.12 +normal_form "max 0 x"
    1.13  
    1.14  text {*
    1.15    Numerals still take their time\<dots>
     2.1 --- a/src/Pure/Tools/class_package.ML	Tue Jul 25 16:43:33 2006 +0200
     2.2 +++ b/src/Pure/Tools/class_package.ML	Tue Jul 25 16:43:47 2006 +0200
     2.3 @@ -33,6 +33,7 @@
     2.4    val certify_sort: theory -> sort -> sort
     2.5    val read_sort: theory -> string -> sort
     2.6    val operational_sort_of: theory -> sort -> sort
     2.7 +  val operational_algebra: theory -> Sorts.algebra
     2.8    val the_superclasses: theory -> class -> class list
     2.9    val the_consts_sign: theory -> class -> string * (string * typ) list
    2.10    val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
    2.11 @@ -133,6 +134,10 @@
    2.12    |> Option.map (not o null o #consts o fst)
    2.13    |> the_default false;
    2.14  
    2.15 +fun operational_algebra thy =
    2.16 +  Sorts.project_algebra (Sign.pp thy)
    2.17 +    (is_operational_class thy) (Sign.classes_of thy);
    2.18 +
    2.19  fun operational_sort_of thy =
    2.20    let
    2.21      fun get_sort class =
     3.1 --- a/src/Pure/Tools/codegen_package.ML	Tue Jul 25 16:43:33 2006 +0200
     3.2 +++ b/src/Pure/Tools/codegen_package.ML	Tue Jul 25 16:43:47 2006 +0200
     3.3 @@ -668,7 +668,7 @@
     3.4                        | SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
     3.5                            fold_map (exprgen_classlookup thy tabs)
     3.6                              (ClassPackage.sortlookup thy (sort, TFree sort_ctxt)))
     3.7 -                            (print sorts ~~ print operational_arity)
     3.8 +                            (sorts ~~ operational_arity)
     3.9                  #-> (fn lss =>
    3.10                         pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss))));
    3.11              in
    3.12 @@ -977,15 +977,18 @@
    3.13  
    3.14  fun purge_defs NONE thy =
    3.15        map_module (K CodegenThingol.empty_module) thy
    3.16 +  | purge_defs (SOME []) thy =
    3.17 +      thy
    3.18    | purge_defs (SOME cs) thy =
    3.19 -      let
    3.20 +      map_module (K CodegenThingol.empty_module) thy;
    3.21 +      (*let
    3.22          val tabs = mk_tabs thy NONE;
    3.23          val idfs = map (idf_of_const' thy tabs) cs;
    3.24          fun purge idfs modl =
    3.25            CodegenThingol.purge_module (filter (can (get_def modl)) idfs) modl
    3.26        in
    3.27          map_module (purge idfs) thy
    3.28 -      end;
    3.29 +      end;*)
    3.30  
    3.31  fun expand_module targets init gen arg thy =
    3.32    thy
    3.33 @@ -1065,7 +1068,7 @@
    3.34  
    3.35  fun read_quote get reader gen raw thy =
    3.36    thy
    3.37 -  |> expand_module NONE ((SOME o get) thy)
    3.38 +  |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) ((SOME o get) thy)
    3.39         (fn thy => fn tabs => gen thy tabs o single o reader thy) raw
    3.40    |-> (fn [x] => pair x);
    3.41  
    3.42 @@ -1216,7 +1219,7 @@
    3.43            Symtab.lookup s_class,
    3.44            (Option.map fst oo Symtab.lookup) s_tyco,
    3.45            (Option.map fst oo Symtab.lookup) s_const
    3.46 -        ) ([] (*TODO: add seri_defs here*), cs) module : unit; thy)
    3.47 +        ) (Symtab.keys s_class @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit; thy)
    3.48        end;
    3.49    in
    3.50      thy
     4.1 --- a/src/Pure/Tools/codegen_serializer.ML	Tue Jul 25 16:43:33 2006 +0200
     4.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Tue Jul 25 16:43:47 2006 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  signature CODEGEN_SERIALIZER =
     4.5  sig
     4.6    type 'a pretty_syntax;
     4.7 -  type serializer = 
     4.8 +  type serializer =
     4.9        string list list
    4.10        -> OuterParse.token list ->
    4.11        ((string -> string option)
    4.12 @@ -26,6 +26,12 @@
    4.13      haskell: string * (string * string list -> serializer)
    4.14    };
    4.15    val mk_flat_ml_resolver: string list -> string -> string;
    4.16 +  val eval_term: string -> string list list
    4.17 +      -> (string -> CodegenThingol.itype pretty_syntax option)
    4.18 +            * (string -> CodegenThingol.iterm pretty_syntax option)
    4.19 +      -> string list
    4.20 +      -> (string * 'a ref) * CodegenThingol.iterm -> CodegenThingol.module
    4.21 +      -> 'a;
    4.22    val ml_fun_datatype: string
    4.23      -> ((string -> CodegenThingol.itype pretty_syntax option)
    4.24          * (string -> CodegenThingol.iterm pretty_syntax option))
    4.25 @@ -86,7 +92,7 @@
    4.26    gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
    4.27  
    4.28  fun from_app mk_app from_expr const_syntax fxy (const as (c, _), es) =
    4.29 -  case (const_syntax c)
    4.30 +  case const_syntax c
    4.31     of NONE => brackify fxy (mk_app c es)
    4.32      | SOME ((i, k), pr) =>
    4.33          if i <= length es
    4.34 @@ -193,7 +199,7 @@
    4.35  
    4.36  (* generic abstract serializer *)
    4.37  
    4.38 -type serializer = 
    4.39 +type serializer =
    4.40      string list list
    4.41      -> OuterParse.token list ->
    4.42      ((string -> string option)
    4.43 @@ -212,6 +218,8 @@
    4.44        |> postprocess (resolv name_qual);
    4.45    in
    4.46      module
    4.47 +    |> debug_msg (fn _ => "dropping shadowed defintions...")
    4.48 +    |> CodegenThingol.delete_garbage drop
    4.49      |> debug_msg (fn _ => "selecting submodule...")
    4.50      |> (if is_some select then (CodegenThingol.project_module o the) select else I)
    4.51      |> debug_msg (fn _ => "serializing...")
    4.52 @@ -227,7 +235,7 @@
    4.53        andalso not (NameSpace.separator = c)
    4.54        then c
    4.55        else "_"
    4.56 -    fun suffix_it name =
    4.57 +    fun suffix_it name=
    4.58        name
    4.59        |> member (op =) keywords ? suffix "'"
    4.60        |> (fn name' => if name = name' then name else suffix_it name')
    4.61 @@ -363,7 +371,7 @@
    4.62                case sort
    4.63                 of [class] => mk_class class
    4.64                  | _ => Pretty.enum " *" "" "" (map mk_class sort),
    4.65 -              str ")"
    4.66 +            str ")"
    4.67              ]
    4.68            end;
    4.69      fun ml_from_sortlookup fxy lss =
    4.70 @@ -464,7 +472,7 @@
    4.71        | ml_from_expr _ (IChar (c, _)) =
    4.72            (str o prefix "#" o quote)
    4.73              (let val i = (Char.ord o the o Char.fromString) c
    4.74 -              in if i < 32 
    4.75 +              in if i < 32
    4.76                  then prefix "\\" (string_of_int i)
    4.77                  else c
    4.78                end)
    4.79 @@ -474,7 +482,7 @@
    4.80              fun mk_val ((ve, vty), se) = Pretty.block [
    4.81                  (Pretty.block o Pretty.breaks) [
    4.82                    str "val",
    4.83 -                  ml_from_expr NOBR ve,
    4.84 +            ml_from_expr NOBR ve,
    4.85                    str "=",
    4.86                    ml_from_expr NOBR se
    4.87                  ],
    4.88 @@ -574,7 +582,7 @@
    4.89                       map ml_from_tyvar sortctxt
    4.90                       @ map2 mk_arg pats
    4.91                           ((curry Library.take (length pats) o fst o CodegenThingol.unfold_fun) ty))
    4.92 -                @ [str "=", ml_from_expr NOBR expr]
    4.93 +             @ [str "=", ml_from_expr NOBR expr]
    4.94                )
    4.95            in
    4.96              (Pretty.block o Pretty.fbreaks o shift) (
    4.97 @@ -629,7 +637,7 @@
    4.98            | (name, CodegenThingol.Datatypecons _) => NONE
    4.99            | (name, def) => error ("datatype block containing illegal def: "
   4.100                  ^ (Pretty.output o CodegenThingol.pretty_def) def));
   4.101 -    fun filter_class defs = 
   4.102 +    fun filter_class defs =
   4.103        case map_filter
   4.104          (fn (name, CodegenThingol.Class info) => SOME (name, info)
   4.105            | (name, CodegenThingol.Classmember _) => NONE
   4.106 @@ -659,7 +667,7 @@
   4.107          fun from_membr_fun (m, _) =
   4.108            (Pretty.block o Pretty.breaks) [
   4.109              str "fun",
   4.110 -            (str o resolv) m, 
   4.111 +            (str o resolv) m,
   4.112              Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ resolv name)],
   4.113              str "=",
   4.114              Pretty.block [str "#", ml_from_label m],
   4.115 @@ -689,7 +697,7 @@
   4.116              ml_from_type NOBR ty,
   4.117              str ";"
   4.118              ]
   4.119 -          ) |> SOME
   4.120 +       ) |> SOME
   4.121        | ml_from_def (name, CodegenThingol.Classinst (((class, (tyco, arity)), suparities), memdefs)) =
   4.122            let
   4.123              val definer = if null arity then "val" else "fun"
   4.124 @@ -756,9 +764,7 @@
   4.125      fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon;
   4.126    in is_cons end;
   4.127  
   4.128 -in
   4.129 -
   4.130 -fun ml_from_thingol target nsp_dtcon nspgrp =
   4.131 +fun ml_serializer root_name target nsp_dtcon nspgrp =
   4.132    let
   4.133      fun ml_from_module resolv _ ((_, name), ps) =
   4.134        Pretty.chunks ([
   4.135 @@ -770,23 +776,18 @@
   4.136          str ("end; (* struct " ^ name ^ " *)")
   4.137        ]);
   4.138      val is_cons = ml_annotators nsp_dtcon;
   4.139 -    val serializer = abstract_serializer (target, nspgrp)
   4.140 -      "ROOT" (ml_from_defs is_cons, ml_from_module,
   4.141 -        abstract_validator reserved_ml, snd);
   4.142 -    fun eta_expander module const_syntax s =
   4.143 -      case const_syntax s
   4.144 -       of SOME ((i, _), _) => i
   4.145 -        | _ => if CodegenThingol.has_nsp s nsp_dtcon
   4.146 -               then case CodegenThingol.get_def module s
   4.147 -                of CodegenThingol.Datatypecons dtname =>
   4.148 -                  case CodegenThingol.get_def module dtname
   4.149 -                of CodegenThingol.Datatype (_, cs) =>
   4.150 -                  let val l = AList.lookup (op =) cs s |> the |> length
   4.151 -                  in if l >= 2 then l else 0 end
   4.152 -                else 0;
   4.153 +  in abstract_serializer (target, nspgrp)
   4.154 +    root_name (ml_from_defs is_cons, ml_from_module,
   4.155 +     abstract_validator reserved_ml, snd) end;
   4.156 +
   4.157 +in
   4.158 +
   4.159 +fun ml_from_thingol target nsp_dtcon nspgrp =
   4.160 +  let
   4.161 +    val serializer = ml_serializer "ROOT" target nsp_dtcon nspgrp
   4.162      val parse_multi =
   4.163        OuterParse.name
   4.164 -      #-> (fn "dir" => 
   4.165 +      #-> (fn "dir" =>
   4.166                 parse_multi_file
   4.167                   (K o SOME o str o suffix ";" o prefix "val _ = use "
   4.168                    o quote o suffix ".ML" o translate_string (fn "." => "/" | s => s)) "ML" serializer
   4.169 @@ -798,6 +799,19 @@
   4.170      || parse_single_file serializer
   4.171    end;
   4.172  
   4.173 +fun eval_term nsp_dtcon nspgrp (syntax_tyco, syntax_const) hidden ((ref_name, reff), e) modl =
   4.174 +  let
   4.175 +    val (val_name, modl') = CodegenThingol.add_eval_def e modl;
   4.176 +    val struct_name = "EVAL";
   4.177 +    val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp
   4.178 +      (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
   4.179 +        | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [val_name]);
   4.180 +    val _ = serializer modl';
   4.181 +    val val_name_struct = NameSpace.append struct_name val_name;
   4.182 +    val _ = use_text Context.ml_output false ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ ")");
   4.183 +    val value = ! reff;
   4.184 +  in value end;
   4.185 +
   4.186  fun mk_flat_ml_resolver names =
   4.187    let
   4.188      val mangler =
   4.189 @@ -811,6 +825,9 @@
   4.190  
   4.191  end; (* local *)
   4.192  
   4.193 +
   4.194 +(** haskell serializer **)
   4.195 +
   4.196  local
   4.197  
   4.198  fun hs_from_defs (is_cons, with_typs) (class_syntax, tyco_syntax, const_syntax)
   4.199 @@ -829,7 +846,7 @@
   4.200                |> map (fn (v, cls) => str (from_class cls ^ " " ^ v))
   4.201                |> Pretty.enum "," "(" ")"
   4.202                |> (fn p => Pretty.block [p, str " => "])
   4.203 -      in 
   4.204 +      in
   4.205          vs
   4.206          |> map (fn (v, sort) => map (pair v) sort)
   4.207          |> flat
   4.208 @@ -888,7 +905,7 @@
   4.209        | hs_from_expr fxy (IChar (c, _)) =
   4.210            (str o enclose "'" "'")
   4.211              (let val i = (Char.ord o the o Char.fromString) c
   4.212 -              in if i < 32 
   4.213 +              in if i < 32
   4.214                  then Library.prefix "\\" (string_of_int i)
   4.215                  else c
   4.216                end)
   4.217 @@ -995,7 +1012,7 @@
   4.218            end
   4.219        | hs_from_def (_, CodegenThingol.Classmember _) =
   4.220            NONE
   4.221 -      | hs_from_def (_, CodegenThingol.Classinst (((clsname, (tyco, arity)), _), memdefs)) = 
   4.222 +      | hs_from_def (_, CodegenThingol.Classinst (((clsname, (tyco, arity)), _), memdefs)) =
   4.223            Pretty.block [
   4.224              str "instance ",
   4.225              hs_from_sctxt arity,
   4.226 @@ -1041,10 +1058,6 @@
   4.227        end;
   4.228      fun serializer with_typs = abstract_serializer (target, nspgrp)
   4.229        "Main" (hs_from_defs (is_cons, with_typs), hs_from_module, abstract_validator reserved_hs, postproc);
   4.230 -    fun eta_expander const_syntax c =
   4.231 -      const_syntax c
   4.232 -      |> Option.map (fst o fst)
   4.233 -      |> the_default 0;
   4.234    in
   4.235      (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
   4.236      #-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs)))
     5.1 --- a/src/Pure/Tools/codegen_theorems.ML	Tue Jul 25 16:43:33 2006 +0200
     5.2 +++ b/src/Pure/Tools/codegen_theorems.ML	Tue Jul 25 16:43:47 2006 +0200
     5.3 @@ -28,14 +28,15 @@
     5.4    val get_datatypes: theory -> string
     5.5      -> (((string * sort) list * (string * typ list) list) * thm list) option;
     5.6  
     5.7 -  (*
     5.8    type thmtab;
     5.9 -  val get_thmtab: (string * typ) list -> theory -> thmtab * theory;
    5.10 -  val get_cons: thmtab -> string -> string option;
    5.11 -  val get_dtyp: thmtab -> string -> (string * sort) list * (string * typ list) list;
    5.12 -  val get_thms: thmtab -> string * typ -> typ * thm list;
    5.13 -  *)
    5.14 -  
    5.15 +  val mk_thmtab: (string * typ) list -> theory -> thmtab * theory;
    5.16 +  val norm_typ: theory -> string * typ -> string * typ;
    5.17 +  val get_sortalgebra: thmtab -> Sorts.algebra;
    5.18 +  val get_dtyp_of_cons: thmtab -> string * typ -> string option;
    5.19 +  val get_dtyp_spec: thmtab -> string
    5.20 +    -> ((string * sort) list * (string * typ list) list) option;
    5.21 +  val get_fun_thms: thmtab -> string * typ -> thm list;
    5.22 +
    5.23    val print_thms: theory -> unit;
    5.24  
    5.25    val init_obj: (thm * thm) * (thm * thm) -> theory -> theory;
    5.26 @@ -87,7 +88,7 @@
    5.27  fun init_obj ((TrueI, FalseE), (conjI, atomize_eq)) thy =
    5.28    case CodegenTheoremsSetup.get thy
    5.29     of SOME _ => error "code generator already set up for object logic"
    5.30 -    | NONE => 
    5.31 +    | NONE =>
    5.32          let
    5.33            fun strip_implies t = (Logic.strip_imp_prems t, Logic.strip_imp_concl t);
    5.34            fun dest_TrueI thm =
    5.35 @@ -120,7 +121,7 @@
    5.36                   #> apfst Term.dest_Const
    5.37                 )
    5.38              |> (fn (v1, ((conj, _), v2)) => if v1 = v2 then conj else error "wrong premise")
    5.39 -          fun dest_atomize_eq thm =
    5.40 +          fun dest_atomize_eq thm=
    5.41              Drule.plain_prop_of thm
    5.42              |> Logic.dest_equals
    5.43              |> apfst (
    5.44 @@ -238,7 +239,7 @@
    5.45        if v = v' orelse member (op =) set v then s
    5.46          else let
    5.47            val t = if i = ~1 then Free (v, ty) else Var (v_i, ty)
    5.48 -        in 
    5.49 +        in
    5.50            (maxidx + 1,  v :: set,
    5.51              (cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc)
    5.52          end;
    5.53 @@ -260,7 +261,7 @@
    5.54            drop (eq::eqs) (filter_out (matches eq) eqs')
    5.55    in drop [] eqs end;
    5.56  
    5.57 -fun make_eq thy = 
    5.58 +fun make_eq thy =
    5.59    let
    5.60      val ((_, atomize), _) = get_obj thy;
    5.61    in rewrite_rule [atomize] end;
    5.62 @@ -368,7 +369,7 @@
    5.63  };
    5.64  
    5.65  fun mk_T ((dirty, notify), (preproc, (extrs, funthms))) =
    5.66 -  T { dirty = dirty, notify = notify, preproc = preproc, extrs = extrs, funthms = funthms };
    5.67 +  T { dirty = dirty, notify = notify, preproc= preproc, extrs = extrs, funthms = funthms };
    5.68  fun map_T f (T { dirty, notify, preproc, extrs, funthms }) =
    5.69    mk_T (f ((dirty, notify), (preproc, (extrs, funthms))));
    5.70  fun merge_T pp (T { dirty = dirty1, notify = notify1, preproc = preproc1, extrs = extrs1, funthms = funthms1 },
    5.71 @@ -405,7 +406,7 @@
    5.72          Pretty.str "code generation theorems:",
    5.73          Pretty.str "function theorems:" ] @
    5.74          (*Pretty.fbreaks ( *)
    5.75 -          map (fn (c, thms) => 
    5.76 +          map (fn (c, thms) =>
    5.77              (Pretty.block o Pretty.fbreaks) (
    5.78                Pretty.str c :: map pretty_thm (rev thms)
    5.79              )
    5.80 @@ -522,7 +523,7 @@
    5.81           (preprocs, thm :: unfolds)), y)))
    5.82    |> notify_all NONE;
    5.83  
    5.84 -fun del_unfold thm = 
    5.85 +fun del_unfold thm =
    5.86    map_data (fn (x, (preproc, y)) =>
    5.87         (x, (preproc |> map_preproc (fn (preprocs, unfolds) =>
    5.88           (preprocs, remove eq_thm thm unfolds)), y)))
    5.89 @@ -546,6 +547,14 @@
    5.90  fun extr_typ thy thm = case dest_fun thy thm
    5.91   of (_, (ty, _)) => ty;
    5.92  
    5.93 +fun rewrite_rhs conv thm = (case (Drule.strip_comb o cprop_of) thm
    5.94 + of (ct', [ct1, ct2]) => (case term_of ct'
    5.95 +     of Const ("==", _) =>
    5.96 +          Thm.equal_elim (combination (combination (reflexive ct') (reflexive ct1))
    5.97 +            (conv ct2)) thm
    5.98 +      | _ => raise ERROR "rewrite_rhs")
    5.99 +  | _ => raise ERROR "rewrite_rhs");
   5.100 +
   5.101  fun common_typ thy _ [] = []
   5.102    | common_typ thy _ [thm] = [thm]
   5.103    | common_typ thy extract_typ thms =
   5.104 @@ -566,20 +575,13 @@
   5.105  fun preprocess thy thms =
   5.106    let
   5.107      fun burrow_thms f [] = []
   5.108 -      | burrow_thms f thms = 
   5.109 +      | burrow_thms f thms =
   5.110            thms
   5.111            |> Conjunction.intr_list
   5.112            |> f
   5.113            |> Conjunction.elim_list;
   5.114      fun cmp_thms (thm1, thm2) =
   5.115        not (Sign.typ_instance thy (extr_typ thy thm1, extr_typ thy thm2));
   5.116 -    fun rewrite_rhs conv thm = (case (Drule.strip_comb o cprop_of) thm
   5.117 -     of (ct', [ct1, ct2]) => (case term_of ct'
   5.118 -         of Const ("==", _) =>
   5.119 -              Thm.equal_elim (combination (combination (reflexive ct') (reflexive ct1))
   5.120 -                (conv ct2)) thm
   5.121 -          | _ => raise ERROR "rewrite_rhs")
   5.122 -      | _ => raise ERROR "rewrite_rhs");
   5.123      fun unvarify thms =
   5.124        #1 (Variable.import true thms (ProofContext.init thy));
   5.125      val unfold_thms = Tactic.rewrite true (map (make_eq thy) (the_unfolds thy));
   5.126 @@ -672,7 +674,7 @@
   5.127            val (_, lhs) = mk_lhs vs args;
   5.128          in (inj, mk_func thy (lhs, fals) :: dist) end;
   5.129      fun mk_eqs (vs, cos) =
   5.130 -      let val cos' = rev cos 
   5.131 +      let val cos' = rev cos
   5.132        in (op @) (fold (mk_eq vs) (product cos' cos') ([], [])) end;
   5.133      fun mk_eq_thms tac vs_cos =
   5.134        map (fn t => Goal.prove_global thy [] []
   5.135 @@ -693,42 +695,150 @@
   5.136      | _ => []
   5.137    else [];
   5.138  
   5.139 -type thmtab = ((thm list Typtab.table Symtab.table
   5.140 -  * string Symtab.table)
   5.141 -  * ((string * sort) list * (string * typ list) list) Symtab.table);
   5.142 +structure ConstTab = TableFun(type key = string * typ val ord = prod_ord fast_string_ord Term.typ_ord);
   5.143 +structure ConstGraph = GraphFun(type key = string * typ val ord = prod_ord fast_string_ord Term.typ_ord);
   5.144 +
   5.145 +type thmtab = (theory * (thm list ConstGraph.T
   5.146 +  * string ConstTab.table)
   5.147 +  * (Sorts.algebra * ((string * sort) list * (string * typ list) list) Symtab.table));
   5.148 +
   5.149 +fun thmtab_empty thy = (thy, (ConstGraph.empty, ConstTab.empty),
   5.150 +  (ClassPackage.operational_algebra thy, Symtab.empty));
   5.151 +
   5.152 +fun norm_typ thy (c, ty) =
   5.153 +  (*more clever: use ty_insts*)
   5.154 +  case get_first (fn ty' => if Sign.typ_instance thy (ty, (*Logic.varifyT*) ty')
   5.155 +    then SOME ty' else NONE) (map #lhs (Theory.definitions_of thy c))
   5.156 +   of NONE => (c, ty)
   5.157 +    | SOME ty => (c, ty);
   5.158 +
   5.159 +fun get_sortalgebra (_, _, (algebra, _)) =
   5.160 +  algebra;
   5.161  
   5.162 -(*
   5.163 -fun mk_thmtab thy cs =
   5.164 +fun get_dtyp_of_cons (thy, (_, dtcotab), _) (c, ty) =
   5.165 +  let
   5.166 +    val (_, ty') = norm_typ thy (c, ty);
   5.167 +  in ConstTab.lookup dtcotab (c, ty') end;
   5.168 +
   5.169 +fun get_dtyp_spec (_, _, (_, dttab)) tyco =
   5.170 +  Symtab.lookup dttab tyco;
   5.171 +
   5.172 +fun has_fun_thms (thy, (fungr, _), _) (c, ty) =
   5.173 +  let
   5.174 +    val (_, ty') = norm_typ thy (c, ty);
   5.175 +  in can (ConstGraph.get_node fungr) (c, ty') end;
   5.176 +
   5.177 +fun get_fun_thms (thy, (fungr, _), _) (c, ty) =
   5.178 +  let
   5.179 +    val (_, ty') = norm_typ thy (c, ty);
   5.180 +  in these (try (ConstGraph.get_node fungr) (c, ty')) end;
   5.181 +
   5.182 +fun mk_thmtab' thy cs =
   5.183    let
   5.184 -    fun add_c (c, ty) gr =
   5.185 -    (*
   5.186 -      Das ist noch viel komplizierter: Zyklen
   5.187 -      und die aktuellen Instantiierungen muss man auch noch mitschleppen
   5.188 -      man sieht: man braucht zusätzlich ein Mapping
   5.189 -        c ~> [ty] (Symtab)
   5.190 -      wobei dort immer die bislang allgemeinsten... ???
   5.191 -    *)
   5.192 -    (*
   5.193 -      thm holen für bestimmten typ
   5.194 -      typ dann behalten
   5.195 -      typ normalisieren
   5.196 -      damit haben wir den key
   5.197 -      hier den check machen, ob schon prozessiert wurde
   5.198 -      NEIN:
   5.199 -        ablegen
   5.200 -        consts der rechten Seiten
   5.201 -        in die Rekursion gehen für alles
   5.202 -      JA:
   5.203 -        fertig
   5.204 -    *)
   5.205 -  in fold add_c cs Constgraph.empty end;
   5.206 +    fun get_dtco_candidate ty =
   5.207 +      case strip_type ty
   5.208 +       of (_, Type (tyco, _)) => SOME tyco
   5.209 +        | _ => NONE;
   5.210 +    fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys
   5.211 +      | add_tycos _ = I;
   5.212 +    val add_consts = fold_aterms
   5.213 +      (fn Const c_ty => insert (op =) (norm_typ thy c_ty)
   5.214 +         | _ => I);
   5.215 +    fun add_dtyps_of_type ty thmtab =
   5.216 +      let
   5.217 +        val tycos = add_tycos ty [];
   5.218 +        val tycos_new = filter (is_some o get_dtyp_spec thmtab) tycos;
   5.219 +        fun add_dtyp_spec dtco (dtyp_spec as (vs, cs)) ((thy, (fungr, dtcotab), (algebra, dttab))) =
   5.220 +          let
   5.221 +            fun mk_co (c, tys) =
   5.222 +              (c, Logic.varifyT (tys ---> Type (dtco, map TFree vs)));
   5.223 +          in
   5.224 +            (thy, (fungr, dtcotab |> fold (fn c_tys => ConstTab.update_new (mk_co c_tys, dtco)) cs),
   5.225 +              (algebra, dttab |> Symtab.update_new (dtco, dtyp_spec)))
   5.226 +          end;
   5.227 +      in
   5.228 +        thmtab
   5.229 +        |> fold (fn tyco => case get_datatypes thy tyco
   5.230 +             of SOME (dtyp_spec, _) => add_dtyp_spec tyco dtyp_spec
   5.231 +              | NONE => I) tycos_new
   5.232 +      end;
   5.233 +    fun known thmtab (c, ty) =
   5.234 +      is_some (get_dtyp_of_cons thmtab (c, ty)) orelse has_fun_thms thmtab (c, ty);
   5.235 +    fun add_funthms (c, ty) (thmtab as (thy, (fungr, dtcotab), algebra_dttab))=
   5.236 +      if known thmtab (norm_typ thy (c, ty)) then thmtab
   5.237 +      else let
   5.238 +        val thms = get_funs thy (c, ty)
   5.239 +        val cs_dep = fold (add_consts o Thm.prop_of) thms [];
   5.240 +      in
   5.241 +        (thy, (fungr |> ConstGraph.new_node ((c, ty), thms)
   5.242 +        , dtcotab), algebra_dttab)
   5.243 +        |> fold add_c cs_dep
   5.244 +      end
   5.245 +    and add_c (c, ty) thmtab =
   5.246 +      let
   5.247 +        val (_, ty') = norm_typ thy (c, ty);
   5.248 +      in
   5.249 +        thmtab
   5.250 +        |> add_dtyps_of_type ty
   5.251 +        |> add_funthms (c, ty)
   5.252 +      end;
   5.253 +    fun narrow_typs fungr =
   5.254 +      let
   5.255 +        (*
   5.256 +        (*!!!remember whether any instantiation had been applied!!!*)
   5.257 +        fun narrow_thms insts thms =
   5.258 +          let
   5.259 +            val (c_def, ty_def) =
   5.260 +              (norm_typ thy o dest_Const o fst o Logic.dest_equals o Thm.prop_of o hd) thms;
   5.261 +            val cs = fold (add_consts o snd o Logic.dest_equals o Thm.prop_of) thms [];
   5.262 +            fun eval_inst c (inst, ty) =
   5.263 +              let
   5.264 +                val inst_ctxt = Sign.const_typargs thy (c, ty);
   5.265 +                val inst_zip = fold (fn (v, ty) => (ty, (the o AList.lookup (op =) inst_ctxt) v)) inst
   5.266 +                fun add_inst (ty_inst, ty_ctxt) =
   5.267 +                  if Sign.typ_instance thy (ty_inst, ty_ctxt)
   5.268 +                  then I
   5.269 +                  else Sign.typ_match thy (ty_ctxt, ty_inst);
   5.270 +              in fold add_inst inst_zip end;
   5.271 +            val inst =
   5.272 +              Vartab.empty
   5.273 +              |> fold (fn c_ty as (c, ty) =>
   5.274 +                    case ConstTab.lookup insts (norm_typ thy c_ty)
   5.275 +                     of NONE => I
   5.276 +                      | SOME inst => eval_inst c (inst, ty)) cs
   5.277 +              |> Vartab.dest
   5.278 +              |> map (fn (v, (_, ty)) => (v, ty));
   5.279 +            val instT = map (fn (v, ty) =>
   5.280 +                (Thm.ctyp_of thy (TVar v, Thm.ctyp_of thy ty))) inst;
   5.281 +            val thms' =
   5.282 +              if null inst then NONE thms else
   5.283 +                map Thm.instantiate (instT, []) thms;
   5.284 +            val inst' = if null inst then NONE
   5.285 +              else SOME inst;
   5.286 +          in (inst', thms') end;
   5.287 +        fun narrow_css [c] (insts, fungr) =
   5.288 +              (* HIER GEHTS WEITER *)
   5.289 +              (insts, fungr)
   5.290 +          | narrow_css css (insts, fungr) =
   5.291 +              (insts, fungr)
   5.292 +        *)
   5.293 +        val css = rev (Graph.strong_conn fungr);
   5.294 +      in
   5.295 +        (ConstTab.empty, fungr)
   5.296 +        (*|> fold narrow_css css*)
   5.297 +        |> snd
   5.298 +      end;
   5.299 +  in
   5.300 +    thmtab_empty thy
   5.301 +    |> fold add_c cs
   5.302 +(*     |> (apfst o apfst) narrow_typs  *)
   5.303 +  end;
   5.304  
   5.305 -fun get_thmtab cs thy =
   5.306 +fun mk_thmtab cs thy =
   5.307    thy
   5.308    |> get_reset_dirty
   5.309 -  |-> (fn _ => I)
   5.310 -  |> `mk_thmtab;
   5.311 -*)
   5.312 +  |> snd
   5.313 +  |> `(fn thy => mk_thmtab' thy cs);
   5.314  
   5.315  
   5.316  (** code attributes and setup **)
     6.1 --- a/src/Pure/Tools/codegen_thingol.ML	Tue Jul 25 16:43:33 2006 +0200
     6.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Tue Jul 25 16:43:47 2006 +0200
     6.3 @@ -67,7 +67,7 @@
     6.4    datatype def =
     6.5        Bot
     6.6      | Fun of funn
     6.7 -    | Typesyn of (vname * sort) list * itype
     6.8 +    | Typesyn of sortcontext * itype
     6.9      | Datatype of datatyp
    6.10      | Datatypecons of string
    6.11      | Class of class list * (vname * (string * (sortcontext * itype)) list)
    6.12 @@ -80,7 +80,7 @@
    6.13    type transact;
    6.14    type 'dst transact_fin;
    6.15    val pretty_def: def -> Pretty.T;
    6.16 -  val pretty_module: module -> Pretty.T; 
    6.17 +  val pretty_module: module -> Pretty.T;
    6.18    val pretty_deps: module -> Pretty.T;
    6.19    val empty_module: module;
    6.20    val get_def: module -> string -> def;
    6.21 @@ -88,6 +88,8 @@
    6.22    val diff_module: module * module -> (string * def) list;
    6.23    val project_module: string list -> module -> module;
    6.24    val purge_module: string list -> module -> module;
    6.25 +  val add_eval_def: iterm -> module -> string * module;
    6.26 +  val delete_garbage: string list (*hidden definitions*) -> module -> module;
    6.27    val has_nsp: string -> string -> bool;
    6.28    val ensure_def: (string -> transact -> def transact_fin) -> bool -> string
    6.29      -> string -> transact -> transact;
    6.30 @@ -232,7 +234,7 @@
    6.31      | _ => NONE);
    6.32  
    6.33  val unfold_abs = unfoldr
    6.34 -  (fn (v, ty) `|-> (e as ICase (((IVar w, _), [(se, be)]), _)) => 
    6.35 +  (fn (v, ty) `|-> (e as ICase (((IVar w, _), [(se, be)]), _)) =>
    6.36          if v = w then SOME ((se, ty), be) else SOME ((IVar v, ty), e)
    6.37      | (v, ty) `|-> e => SOME ((IVar v, ty), e)
    6.38      | _ => NONE)
    6.39 @@ -241,7 +243,7 @@
    6.40    (fn ICase (((de, dty), [(se, be)]), _) => SOME (((se, dty), de), be)
    6.41      | _ => NONE);
    6.42  
    6.43 -fun unfold_const_app e = 
    6.44 +fun unfold_const_app e =
    6.45   case unfold_app e
    6.46    of (IConst x, es) => SOME (x, es)
    6.47     | _ => NONE;
    6.48 @@ -323,8 +325,8 @@
    6.49        add_constnames e
    6.50    | add_constnames (INum _) =
    6.51        I
    6.52 -  | add_constnames (IChar _) =
    6.53 -      I
    6.54 +  | add_constnames (IChar (_, e)) =
    6.55 +      add_constnames e
    6.56    | add_constnames (ICase (_, e)) =
    6.57        add_constnames e;
    6.58  
    6.59 @@ -383,10 +385,10 @@
    6.60  datatype def =
    6.61      Bot
    6.62    | Fun of funn
    6.63 -  | Typesyn of (vname * sort) list * itype
    6.64 +  | Typesyn of sortcontext * itype
    6.65    | Datatype of datatyp
    6.66    | Datatypecons of string
    6.67 -  | Class of class list * (vname * (string * (sortcontext * itype)) list)
    6.68 +| Class of class list * (vname * (string * (sortcontext * itype)) list)
    6.69    | Classmember of class
    6.70    | Classinst of ((class * (string * (vname * sort) list))
    6.71          * (class * iclasslookup list) list)
    6.72 @@ -633,7 +635,7 @@
    6.73  
    6.74  fun diff_module modl12 =
    6.75    let
    6.76 -    fun diff_entry prefix modl2 (name, Def def1) = 
    6.77 +    fun diff_entry prefix modl2 (name, Def def1) =
    6.78            let
    6.79              val e2 = try (Graph.get_node modl2) name
    6.80            in if is_some e2 andalso eq_def (def1, (dest_def o the) e2)
    6.81 @@ -660,7 +662,7 @@
    6.82            |> (pair defs #> PN);
    6.83      fun select (PN (defs, modls)) (Module module) =
    6.84        module
    6.85 -      |> Graph.project (member (op =) (Graph.all_succs module (defs @ map fst modls)))
    6.86 +      |> Graph.project (member (op =) ((*!*) Graph.all_succs module (defs @ map fst modls)))
    6.87        |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
    6.88        |> Module;
    6.89    in
    6.90 @@ -682,8 +684,10 @@
    6.91        let
    6.92          val (ndefs, nmodls) = split_names names;
    6.93        in
    6.94 -        modl 
    6.95 +        modl
    6.96          |> Graph.del_nodes (Graph.all_preds modl ndefs)
    6.97 +        |> Graph.del_nodes ndefs
    6.98 +        |> Graph.del_nodes (Graph.all_preds modl (map fst nmodls))
    6.99          |> fold (fn (nmodl, names') => Graph.map_node nmodl (purge names')) nmodls
   6.100          |> Module
   6.101        end;
   6.102 @@ -693,6 +697,145 @@
   6.103      |> dest_modl
   6.104    end;
   6.105  
   6.106 +val add_deps_of_sortctxt =
   6.107 +  fold (fn (v : vname, sort : sort) => fold (insert (op =)) sort);
   6.108 +
   6.109 +fun add_deps_of_classlookup (Instance (tyco, lss)) =
   6.110 +      insert (op =) tyco
   6.111 +      #> (fold o fold) add_deps_of_classlookup lss
   6.112 +  | add_deps_of_classlookup (Lookup (clss, _)) =
   6.113 +      fold (insert (op =)) clss;
   6.114 +
   6.115 +fun add_deps_of_type (tyco `%% tys) =
   6.116 +      insert (op =) tyco
   6.117 +      #> fold add_deps_of_type tys
   6.118 +  | add_deps_of_type  (ty1 `-> ty2) =
   6.119 +      add_deps_of_type ty1
   6.120 +      #> add_deps_of_type ty2
   6.121 +  | add_deps_of_type (ITyVar v) =
   6.122 +      I;
   6.123 +
   6.124 +fun add_deps_of_term (IConst (c, (lss, ty))) =
   6.125 +      insert (op =) c
   6.126 +      #> add_deps_of_type ty
   6.127 +      #> (fold o fold) add_deps_of_classlookup lss
   6.128 +  | add_deps_of_term (IVar _) =
   6.129 +      I
   6.130 +  | add_deps_of_term (e1 `$ e2) =
   6.131 +      add_deps_of_term e1 #> add_deps_of_term e2
   6.132 +  | add_deps_of_term ((_, ty) `|-> e) =
   6.133 +      add_deps_of_type ty
   6.134 +      #> add_deps_of_term e
   6.135 +  | add_deps_of_term (INum _) =
   6.136 +      I
   6.137 +  | add_deps_of_term (IChar (_, e)) =
   6.138 +      add_deps_of_term e
   6.139 +  | add_deps_of_term (ICase (_, e)) =
   6.140 +      add_deps_of_term e;
   6.141 +
   6.142 +fun deps_of Bot =
   6.143 +      []
   6.144 +  | deps_of (Fun (eqs, (sctxt, ty))) =
   6.145 +      []
   6.146 +      |> add_deps_of_sortctxt sctxt
   6.147 +      |> add_deps_of_type ty
   6.148 +      |> fold (fn (lhs, rhs) => fold add_deps_of_term lhs #> add_deps_of_term rhs) eqs
   6.149 +  | deps_of (Typesyn (sctxt, ty)) =
   6.150 +      []
   6.151 +      |> add_deps_of_sortctxt sctxt
   6.152 +      |> add_deps_of_type ty
   6.153 +  | deps_of (Datatype (sctxt, cos)) =
   6.154 +      []
   6.155 +      |> add_deps_of_sortctxt sctxt
   6.156 +      |> fold (fn (c, tys) => insert (op =) c #> fold add_deps_of_type tys) cos
   6.157 +  | deps_of (Datatypecons dtco) =
   6.158 +      [dtco]
   6.159 +  | deps_of (Class (supclss, (_, memdecls))) =
   6.160 +      []
   6.161 +      |> fold (insert (op =)) supclss
   6.162 +      |> fold (fn (name, (sctxt, ty)) =>
   6.163 +            insert (op =) name
   6.164 +            #> add_deps_of_sortctxt sctxt
   6.165 +            #> add_deps_of_type ty
   6.166 +      ) memdecls
   6.167 +  | deps_of (Classmember class) =
   6.168 +      [class]
   6.169 +  | deps_of (Classinst (((class, (tyco, sctxt)), suparities), memdefs)) =
   6.170 +      []
   6.171 +      |> insert (op =) class
   6.172 +      |> insert (op =) tyco
   6.173 +      |> add_deps_of_sortctxt sctxt
   6.174 +      |> fold (fn (supclass, ls) =>
   6.175 +            insert (op =) supclass
   6.176 +            #> fold add_deps_of_classlookup ls
   6.177 +      ) suparities
   6.178 +      |> fold (fn (name, ((_, (eqs, (sctxt, ty))), lss)) =>
   6.179 +            insert (op =) name
   6.180 +            #> add_deps_of_sortctxt sctxt
   6.181 +            #> add_deps_of_type ty
   6.182 +            #> fold (fn (lhs, rhs) => fold add_deps_of_term lhs #> add_deps_of_term rhs) eqs
   6.183 +            #> (fold o fold) add_deps_of_classlookup lss
   6.184 +      ) memdefs
   6.185 +  | deps_of Classinstmember =
   6.186 +      [];
   6.187 +
   6.188 +fun delete_garbage hidden modl =
   6.189 +  let
   6.190 +    fun allnames modl =
   6.191 +      let
   6.192 +        val entries = AList.make (Graph.get_node modl) (Graph.keys modl)
   6.193 +        fun is_def (name, Module _) = NONE
   6.194 +          | is_def (name, _) = SOME name;
   6.195 +        fun is_modl (name, Module modl) = SOME (name, modl)
   6.196 +          | is_modl (name, _) = NONE;
   6.197 +        val defs = map_filter is_def entries;
   6.198 +        val modls = map_filter is_modl entries;
   6.199 +      in
   6.200 +        defs
   6.201 +        @ maps (fn (name, modl) => map (NameSpace.append name) (allnames modl)) modls
   6.202 +      end;
   6.203 +    fun alldeps modl =
   6.204 +      let
   6.205 +        val entries = AList.make (Graph.get_node modl) (Graph.keys modl)
   6.206 +        fun is_def (name, Module _) = NONE
   6.207 +          | is_def (name, _) = SOME name;
   6.208 +        fun is_modl (name, Module modl) = SOME (name, modl)
   6.209 +          | is_modl (name, _) = NONE;
   6.210 +        val defs = map_filter is_def entries;
   6.211 +        val modls = map_filter is_modl entries;
   6.212 +      in
   6.213 +        maps (fn name => map (pair (name)) (Graph.imm_succs modl name)) defs
   6.214 +        @ maps (fn (name, modl) => (map o pairself) (NameSpace.append name) (alldeps modl)) modls
   6.215 +      end;
   6.216 +    val names = subtract (op =) hidden (allnames modl);
   6.217 +    (*val _ = writeln "HIDDEN";
   6.218 +    val _ = (writeln o commas) hidden;
   6.219 +    val _ = writeln "NAMES";
   6.220 +    val _ = (writeln o commas) names;*)
   6.221 +    fun is_bot name =
   6.222 +      case get_def modl name of Bot => true | _ => false;
   6.223 +    val bots = filter is_bot names;
   6.224 +    val defs = filter (not o is_bot) names;
   6.225 +    val expldeps =
   6.226 +      Graph.empty
   6.227 +      |> fold (fn name => Graph.new_node (name, ())) names
   6.228 +      |> fold (fn name => fold (curry Graph.add_edge name)
   6.229 +            (deps_of (get_def modl name) |> subtract (op =) hidden)) names
   6.230 +    val bots' = fold (insert op =) bots (Graph.all_preds expldeps bots);
   6.231 +    val selected = subtract (op =) bots' names;
   6.232 +(*     val deps = filter (fn (x, y) => member (op =) selected x andalso member (op =) selected y)  *)
   6.233 +    val adddeps = maps (fn (n, ns) => map (pair n) ns) (expldeps |> Graph.del_nodes bots' |> Graph.dest);
   6.234 +    (*val _ = writeln "SELECTED";
   6.235 +    val _ = (writeln o commas) selected;
   6.236 +    val _ = writeln "DEPS";
   6.237 +    val _ = (writeln o cat_lines o map (fn (x, y) => x ^ " -> " ^ y)) adddeps;*)
   6.238 +  in
   6.239 +    empty_module
   6.240 +    |> fold (fn name => add_def (name, get_def modl name)) selected
   6.241 +(*     |> fold ensure_bot (hidden @ bots')  *)
   6.242 +    |> fold (fn (x, y) => (writeln ("adding " ^ x ^ " -> " ^ y); add_dep (x, y))) adddeps
   6.243 +  end;
   6.244 +
   6.245  fun allimports_of modl =
   6.246    let
   6.247      fun imps_of prfx (Module modl) imps tab =
   6.248 @@ -704,10 +847,10 @@
   6.249              |> pair []
   6.250              |> fold (fn names => fn (imps', tab) =>
   6.251                  tab
   6.252 -                |> fold_map (fn name => 
   6.253 +                |> fold_map (fn name =>
   6.254                       imps_of (prfx @ [name]) (Graph.get_node modl name) (imps' @ imps)) names
   6.255                  |-> (fn imps'' => pair (flat imps'' @ imps'))) name_con
   6.256 -            |-> (fn imps' => 
   6.257 +            |-> (fn imps' =>
   6.258                 Symtab.update_new (this, imps' @ imps)
   6.259              #> pair (this :: imps'))
   6.260            end
   6.261 @@ -769,7 +912,7 @@
   6.262                  in if eq_ityp ((sortctxt'', ty''), (sortctxt', ty'))
   6.263                  then (m, ((m', (check_funeqs eqs, (sortctxt', ty'))), lss))
   6.264                  else
   6.265 -                  error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: "
   6.266 +       error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: "
   6.267                      ^ (Pretty.output o Pretty.block o Pretty.breaks) [
   6.268                        pretty_sortcontext sortctxt'',
   6.269                        Pretty.str "|=>",
   6.270 @@ -826,12 +969,12 @@
   6.271      fun prep_def def modl =
   6.272        (check_prep_def modl def, modl);
   6.273      fun invoke_generator name defgen modl =
   6.274 -      if ! soft_exc (*that's ! isn't a "not"...*)
   6.275 +      if ! soft_exc (*that "!" isn't a "not"...*)
   6.276        then defgen name (SOME name, modl)
   6.277          handle FAIL (msgs, exc) =>
   6.278                  if strict then raise FAIL (msg' :: msgs, exc)
   6.279                  else (Bot, modl)
   6.280 -             | e => raise 
   6.281 +             | e => raise
   6.282                  FAIL (["definition generator for " ^ quote name, msg'], SOME e)
   6.283        else defgen name (SOME name, modl)
   6.284          handle FAIL (msgs, exc) =>
   6.285 @@ -885,6 +1028,15 @@
   6.286      |-> (fn x => fn (_, modl) => (x, modl))
   6.287    end;
   6.288  
   6.289 +fun add_eval_def e modl =
   6.290 +  let
   6.291 +    val name = hd (Name.invent_list (Graph.keys modl) "VALUE" 1);
   6.292 +  in
   6.293 +    modl
   6.294 +    |> add_def (name, Fun ([([], e)], ([], "" `%% [])))
   6.295 +    |> fold (curry add_dep name) (add_deps_of_term e [])
   6.296 +    |> pair name
   6.297 +  end;
   6.298  
   6.299  
   6.300  (** generic serialization **)
   6.301 @@ -954,7 +1106,7 @@
   6.302            in ([p'], tab') end
   6.303        | get_path_name [p1, p2] tab =
   6.304            (case Symtab.lookup tab p1
   6.305 -           of SOME (N (p', SOME tab')) => 
   6.306 +           of SOME (N (p', SOME tab')) =>
   6.307                  let
   6.308                    val (ps', tab'') = get_path_name [p2] tab'
   6.309                  in (p' :: ps', tab'') end
   6.310 @@ -987,16 +1139,19 @@
   6.311        let
   6.312          val name_qual = NameSpace.pack (prfx @ [name])
   6.313        in (name_qual, resolver prfx name_qual) end;
   6.314 +    fun is_bot (_, (Def Bot)) = true
   6.315 +      | is_bot _ = false;
   6.316      fun mk_contents prfx module =
   6.317        map_filter (seri prfx)
   6.318          ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
   6.319      and seri prfx [(name, Module modl)] =
   6.320            seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) (NameSpace.pack (prfx @ [name]))))
   6.321              (mk_name prfx name, mk_contents (prfx @ [name]) modl)
   6.322 -      | seri prfx [(_, Def Bot)] = NONE
   6.323        | seri prfx ds =
   6.324 -          seri_defs sresolver (NameSpace.pack prfx)
   6.325 -            (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
   6.326 +          case filter_out is_bot ds
   6.327 +           of [] => NONE
   6.328 +            | ds' => seri_defs sresolver (NameSpace.pack prfx)
   6.329 +                (map (fn (name, Def def) => (fst (mk_name prfx name), def (*|> tap (Pretty.writeln o pretty_def)*))) ds')
   6.330    in
   6.331      seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) ""))
   6.332        (("", name_root), (mk_contents [] module))
     7.1 --- a/src/Pure/Tools/nbe.ML	Tue Jul 25 16:43:33 2006 +0200
     7.2 +++ b/src/Pure/Tools/nbe.ML	Tue Jul 25 16:43:47 2006 +0200
     7.3 @@ -83,12 +83,11 @@
     7.4      val _ = trace (fn () => "Input:\n" ^ Display.raw_string_of_term t);
     7.5      fun compile_term t thy =
     7.6        let
     7.7 -        val (modl_this, thy') = CodegenPackage.get_root_module thy;
     7.8 +        val thy' = CodegenPackage.purge_code thy;
     7.9          val nbe_tab = NBE_Data.get thy';
    7.10 -        val modl_old = CodegenThingol.project_module (Symtab.keys nbe_tab) modl_this;
    7.11          val (t', thy'') = CodegenPackage.codegen_term t thy';
    7.12          val (modl_new, thy''') = CodegenPackage.get_root_module thy'';
    7.13 -        val diff = CodegenThingol.diff_module (modl_new, modl_old);
    7.14 +        val diff = CodegenThingol.diff_module (modl_new, CodegenThingol.empty_module);
    7.15          val _ = trace (fn () => "new definitions: " ^ (commas o map fst) diff);
    7.16          val _ = (tab := nbe_tab;
    7.17               Library.seq (use_code o NBE_Codegen.generate defined) diff);