# HG changeset patch
# User haftmann
# Date 1149692070 -7200
# Node ID a8c8ed1c85e0556891dbf20c89761f13fd35df5e
# Parent  4820c3d5254859e957b6cdaabd05f807af5965f9
removed 'primitive definitions' added (non)strict generation, minor fixes

diff -r 4820c3d52548 -r a8c8ed1c85e0 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Jun 07 16:53:31 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Wed Jun 07 16:54:30 2006 +0200
@@ -15,14 +15,6 @@
 
   val add_appconst: xstring * ((int * int) * appgen) -> theory -> theory;
   val add_appconst_i: string * ((int * int) * appgen) -> theory -> theory;
-  val add_prim_class: xstring -> (string * string)
-    -> theory -> theory;
-  val add_prim_tyco: xstring -> (string * string)
-    -> theory -> theory;
-  val add_prim_const: xstring -> (string * string)
-    -> theory -> theory;
-  val add_prim_i: string -> (string * CodegenThingol.prim list)
-    -> theory -> theory;
   val add_pretty_list: string -> string -> string * (int * string)
     -> theory -> theory;
   val add_alias: string * string -> theory -> theory;
@@ -59,7 +51,7 @@
   structure ConstNameMangler: NAME_MANGLER;
   structure DatatypeconsNameMangler: NAME_MANGLER;
   structure CodegenData: THEORY_DATA;
-  val mk_tabs: theory -> auxtab;
+  val mk_tabs: theory -> string option -> auxtab;
   val alias_get: theory -> string -> string;
   val idf_of_name: theory -> string -> string -> string;
   val idf_of_const: theory -> auxtab -> string * typ -> string;
@@ -208,7 +200,7 @@
   fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst);
 );
 
-type auxtab = deftab
+type auxtab = (string option * deftab)
   * (InstNameMangler.T * (typ list Symtab.table * ConstNameMangler.T)
   * DatatypeconsNameMangler.T);
 type eqextr = theory -> auxtab
@@ -497,7 +489,7 @@
                 let
                   val (vars, cos) = (fst o the o CodegenTheorems.get_datatypes thy) dtco
                 in
-                  SOME (c, (the o AList.lookup (op =) cos) c ---> Type (dtco, map TFree vars))
+                  SOME (c, (the o AList.lookup (op =) cos) c ---> Type (dtco, map TFree vars) |> Logic.varifyT)
                 end
             | NONE => NONE;
 
@@ -516,6 +508,17 @@
 
 (* definition and expression generators *)
 
+fun check_strict thy f x (tabs as ((SOME target, deftab), tabs')) =
+      thy
+      |> CodegenData.get
+      |> #target_data
+      |> (fn data => (the oo Symtab.lookup) data target)
+      |> f
+      |> (fn tab => Symtab.lookup tab x)
+      |> is_none
+  | check_strict _ _ _ (tabs as ((NONE, _), _)) =
+      false;
+
 fun ensure_def_class thy tabs cls trns =
   let
     fun defgen_class thy (tabs as (_, (insttab, _, _))) cls trns =
@@ -529,7 +532,7 @@
               trns
               |> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls)
               |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls)
-              ||>> (exprsgen_type thy tabs o map snd) cs
+              ||>> (fold_map (exprgen_type thy tabs) o map snd) cs
               ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
               |-> (fn ((supcls, memtypes), sortctxts) => succeed
                 (Class (supcls, (unprefix "'" v, idfs ~~ (sortctxts ~~ memtypes)))))
@@ -541,22 +544,24 @@
   in
     trns
     |> debug_msg (fn _ => "generating class " ^ quote cls)
-    |> ensure_def [("class", defgen_class thy tabs)] ("generating class " ^ quote cls) cls'
+    |> ensure_def (defgen_class thy tabs) true ("generating class " ^ quote cls) cls'
     |> pair cls'
   end
 and ensure_def_tyco thy tabs tyco trns =
   let
+    val tyco' = idf_of_name thy nsp_tyco tyco;
+    val strict = check_strict thy #syntax_tyco tyco' tabs;
     fun defgen_datatype thy (tabs as (_, (_, _, dtcontab))) dtco trns =
       case name_of_idf thy nsp_tyco dtco
        of SOME dtco =>
-        (case CodegenTheorems.get_datatypes thy dtco
+         (case CodegenTheorems.get_datatypes thy dtco
              of SOME ((vars, cos), _) =>
                   trns
                   |> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco)
                   |> fold_map (exprgen_tyvar_sort thy tabs) vars
-                  ||>> fold_map (fn (c, ty) =>
-                    exprsgen_type thy tabs ty
-                    #-> (fn ty' => pair ((the o idf_of_co thy tabs) (c, dtco), ty'))) cos
+                  ||>> fold_map (fn (c, tys) =>
+                    fold_map (exprgen_type thy tabs) tys
+                    #-> (fn tys' => pair ((the o idf_of_co thy tabs) (c, dtco), tys'))) cos
                   |-> (fn (vars, cos) => succeed (Datatype
                        (vars, cos)))
               | NONE =>
@@ -565,11 +570,10 @@
         | NONE =>
             trns
             |> fail ("not a type constructor: " ^ quote dtco)
-    val tyco' = idf_of_name thy nsp_tyco tyco;
   in
     trns
     |> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
-    |> ensure_def [("datatype", defgen_datatype thy tabs)] ("generating type constructor " ^ quote tyco) tyco'
+    |> ensure_def (defgen_datatype thy tabs) strict ("generating type constructor " ^ quote tyco) tyco'
     |> pair tyco'
   end
 and exprgen_tyvar_sort thy tabs (v, sort) trns =
@@ -591,9 +595,7 @@
       trns
       |> ensure_def_tyco thy tabs tyco
       ||>> fold_map (exprgen_type thy tabs) tys
-      |-> (fn (tyco, tys) => pair (tyco `%% tys))
-and exprsgen_type thy tabs =
-  fold_map (exprgen_type thy tabs);
+      |-> (fn (tyco, tys) => pair (tyco `%% tys));
 
 fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns =
       trns
@@ -620,12 +622,16 @@
                    ^ ", actually defining " ^ quote c')
               | _ => error ("illegal function equation for " ^ quote c)
             end;
+          fun exprgen_eq (args, rhs) trns =
+            trns
+            |> fold_map (exprgen_term thy tabs) args
+            ||>> exprgen_term thy tabs rhs
         in
           trns
-          |> (exprsgen_eqs thy tabs o map dest_eqthm) eq_thms
-          ||>> exprsgen_type thy tabs [ty]
+          |> fold_map (exprgen_eq o dest_eqthm) eq_thms
+          ||>> exprgen_type thy tabs ty
           ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
-          |-> (fn ((eqs, [ity]), sortctxt) => (pair o SOME) ((eqs, (sortctxt, ity)), ty))
+          |-> (fn ((eqs, ity), sortctxt) => (pair o SOME) ((eqs, (sortctxt, ity)), ty))
         end
     | NONE => (NONE, trns)
 and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
@@ -670,7 +676,7 @@
   in
     trns
     |> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
-    |> ensure_def [("instance", defgen_inst thy tabs)]
+    |> ensure_def (defgen_inst thy tabs) true
          ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
     |> pair inst
   end
@@ -682,7 +688,8 @@
             trns
             |> mk_fun thy tabs (c, ty)
             |-> (fn SOME (funn, _) => succeed (Fun funn)
-                  | NONE => fail ("no defining equations found for " ^ quote c))
+                  | NONE => fail ("no defining equations found for " ^
+                      (quote o Display.raw_string_of_term o Const) (c, ty)))
         | NONE =>
             trns
             |> fail ("not a constant: " ^ quote c);
@@ -692,7 +699,7 @@
             trns
             |> debug_msg (fn _ => "trying defgen class member for " ^ quote m)
             |> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m)
-            |-> (fn cls => succeed Undef)
+            |-> (fn cls => succeed Bot)
         | _ =>
             trns |> fail ("no class member found for " ^ quote m)
     fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns =
@@ -701,24 +708,25 @@
             trns
             |> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co)
             |> ensure_def_tyco thy tabs dtco
-            |-> (fn dtco => succeed Undef)
+            |-> (fn dtco => succeed Bot)
         | _ =>
             trns
             |> fail ("not a datatype constructor: " ^ quote co);
-    fun get_defgen idf =
+    fun get_defgen tabs idf strict =
       if (is_some oo name_of_idf thy) nsp_const idf
         orelse (is_some oo name_of_idf thy) nsp_overl idf
-      then ("funs", defgen_funs thy tabs)
+      then defgen_funs thy tabs strict
       else if (is_some oo name_of_idf thy) nsp_mem idf
-      then ("clsmem", defgen_clsmem thy tabs)
+      then defgen_clsmem thy tabs strict
       else if (is_some oo name_of_idf thy) nsp_dtcon idf
-      then ("datatypecons", defgen_datatypecons thy tabs)
+      then defgen_datatypecons thy tabs strict
       else error ("illegal shallow name space for constant: " ^ quote idf);
     val idf = idf_of_const thy tabs (c, ty);
+    val strict = check_strict thy #syntax_const idf tabs;
   in
     trns
-    |> debug_msg (fn _ => "generating constant " ^ quote c)
-    |> ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf
+    |> debug_msg (fn _ => "generating constant " ^ (quote o Display.raw_string_of_term o Const) (c, ty))
+    |> ensure_def (get_defgen tabs idf) strict ("generating constant " ^ quote c) idf
     |> pair idf
   end
 and exprgen_term thy tabs (Const (f, ty)) trns =
@@ -754,20 +762,14 @@
             ||>> fold_map (exprgen_term thy tabs) ts
             |-> (fn (e, es) => pair (e `$$ es))
       end
-and exprsgen_term thy tabs =
-  fold_map (exprgen_term thy tabs)
-and exprsgen_eqs thy tabs =
-  apfst (map (fn (rhs::args) => (args, rhs)))
-    oo fold_burrow (exprsgen_term thy tabs)
-    o map (fn (args, rhs) => (rhs :: args))
 and appgen_default thy tabs ((c, ty), ts) trns =
   trns
   |> ensure_def_const thy tabs (c, ty)
-  ||>> exprsgen_type thy tabs [ty]
+  ||>> exprgen_type thy tabs ty
   ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
          (ClassPackage.extract_classlookup thy (c, ty))
   ||>> fold_map (exprgen_term thy tabs) ts
-  |-> (fn (((c, [ty]), ls), es) =>
+  |-> (fn (((c, ty), ls), es) =>
          pair (IConst (c, (ls, ty)) `$$ es))
 and appgen thy tabs ((f, ty), ts) trns =
   case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
@@ -854,14 +856,14 @@
     val idf = idf_of_const thy tabs (c, ty);
   in
     trns
-    |> ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf
+    |> ensure_def ((K o succeed) Bot) true ("generating wfrec") idf
     |> exprgen_type thy tabs ty'
     ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
            (ClassPackage.extract_classlookup thy (c, ty))
-    ||>> exprsgen_type thy tabs [ty_def]
+    ||>> exprgen_type thy tabs ty_def
     ||>> exprgen_term thy tabs tf
     ||>> exprgen_term thy tabs tx
-    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
+    |-> (fn ((((_, ls), ty), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
   end;
 
 fun appgen_datatype_case cos thy tabs (app as ((_, ty), ts)) trns =
@@ -904,7 +906,7 @@
 
 (** theory interface **)
 
-fun mk_tabs thy =
+fun mk_tabs thy target =
   let
     fun mk_insttab thy =
       InstNameMangler.empty
@@ -968,7 +970,7 @@
     val insttab = mk_insttab thy;
     val overltabs = mk_overltabs thy;
     val dtcontab = mk_dtcontab thy;
-  in (Symtab.empty, (insttab, overltabs, dtcontab)) end;
+  in ((target, Symtab.empty), (insttab, overltabs, dtcontab)) end;
 
 fun get_serializer target =
   case Symtab.lookup (!serializers) target
@@ -983,7 +985,7 @@
       map_module (K CodegenThingol.empty_module) thy
   | delete_defs (SOME c) thy =
       let
-        val tabs = mk_tabs thy;
+        val tabs = mk_tabs thy NONE;
       in
         map_module (CodegenThingol.purge_module []) thy
       end;
@@ -993,12 +995,12 @@
 * precondition: improved representation of definitions hidden by customary serializations
 *)
 
-fun expand_module init gen arg thy =
+fun expand_module target init gen arg thy =
   thy
   |> CodegenTheorems.notify_dirty
   |> `(#modl o CodegenData.get)
   |> (fn (modl, thy) =>
-        (start_transact init (gen thy (mk_tabs thy) arg) modl, thy))
+        (start_transact init (gen thy (mk_tabs thy target) arg) modl, thy))
   |-> (fn (x, modl) => map_module (K modl) #> pair x);
 
 fun rename_inconsistent thy =
@@ -1025,18 +1027,16 @@
       else add_alias (src, dst) thy
   in fold add inconsistent thy end;
 
-fun codegen_term t thy =
-  thy
-  |> expand_module NONE exprsgen_term [CodegenTheorems.preprocess_term thy t]
-  |-> (fn [t] => pair t);
+fun codegen_term t =
+  expand_module NONE NONE exprgen_term t;
 
 val is_dtcon = has_nsp nsp_dtcon;
 
 fun consts_of_idfs thy =
-  map (the o const_of_idf thy (mk_tabs thy));
+  map (the o const_of_idf thy (mk_tabs thy NONE));
 
 fun idfs_of_consts thy =
-  map (idf_of_const thy (mk_tabs thy));
+  map (idf_of_const thy (mk_tabs thy NONE));
 
 val get_root_module = (#modl o CodegenData.get);
 
@@ -1054,7 +1054,9 @@
 
 (** target languages **)
 
-(* primitive definitions *)
+val ensure_bot = map_module o CodegenThingol.ensure_bot;
+
+(* syntax *)
 
 fun read_typ thy =
   Sign.read_typ (thy, K NONE);
@@ -1069,38 +1071,10 @@
 
 fun read_quote get reader gen raw thy =
   thy
-  |> expand_module ((SOME o get) thy)
+  |> expand_module NONE ((SOME o get) thy)
        (fn thy => fn tabs => gen thy tabs o single o reader thy) raw
   |-> (fn [x] => pair x);
 
-fun gen_add_prim prep_name prep_primdef raw_name (target, raw_primdef) thy =
-  let
-    val _ = if Symtab.defined ((#target_data o CodegenData.get) thy) target
-      then () else error ("unknown target language: " ^ quote target);
-    val tabs = mk_tabs thy;
-    val name = prep_name thy tabs raw_name;
-    val primdef = prep_primdef raw_primdef;
-  in
-    thy
-    |> map_module (CodegenThingol.add_prim name (target, primdef))
-  end;
-
-val add_prim_i = gen_add_prim ((K o K) I) I;
-val add_prim_class = gen_add_prim
-  (fn thy => K (idf_of_name thy nsp_class o Sign.intern_class thy))
-  CodegenSerializer.parse_targetdef;
-val add_prim_tyco = gen_add_prim
-  (fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy))
-  CodegenSerializer.parse_targetdef;
-val add_prim_const = gen_add_prim
-  (fn thy => fn tabs => idf_of_const thy tabs o read_const thy)
-  CodegenSerializer.parse_targetdef;
-
-val ensure_prim = map_module oo CodegenThingol.ensure_prim;
-
-
-(* syntax *)
-
 fun gen_add_syntax_class prep_class class target pretty thy =
   thy
   |> map_codegen_data
@@ -1136,7 +1110,7 @@
         val tyco = prep_tyco thy raw_tyco;
       in
         thy
-        |> ensure_prim tyco target
+        |> ensure_bot tyco
         |> reader
         |-> (fn pretty => map_codegen_data
           (fn (modl, gens, target_data, logic_data) =>
@@ -1151,7 +1125,8 @@
       end;
   in
     CodegenSerializer.parse_syntax (fn thy => no_args_tyco thy raw_tyco)
-    (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ exprsgen_type)
+    (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ 
+      (fn thy => fn tabs => fold_map (exprgen_type thy tabs)))
     #-> (fn reader => pair (mk reader))
   end;
 
@@ -1171,7 +1146,7 @@
 fun parse_syntax_const raw_const =
   let
     fun prep_const thy raw_const =
-      idf_of_const thy (mk_tabs thy) (read_const thy raw_const);
+      idf_of_const thy (mk_tabs thy NONE) (read_const thy raw_const);
     fun no_args_const thy raw_const =
       (length o fst o strip_type o snd o read_const thy) raw_const;
     fun mk reader target thy =
@@ -1180,20 +1155,21 @@
         val c = prep_const thy raw_const;
       in
         thy
-        |> ensure_prim c target
+        |> ensure_bot c
         |> reader
         |-> (fn pretty => add_pretty_syntax_const c target pretty)
       end;
   in
     CodegenSerializer.parse_syntax (fn thy => no_args_const thy raw_const)
-      (read_quote (fn thy => prep_const thy raw_const) Sign.read_term exprsgen_term)
+      (read_quote (fn thy => prep_const thy raw_const) Sign.read_term
+      (fn thy => fn tabs => fold_map (exprgen_term thy tabs)))
     #-> (fn reader => pair (mk reader))
   end;
 
 fun add_pretty_list raw_nil raw_cons (target, seri) thy =
   let
     val _ = get_serializer target;
-    val tabs = mk_tabs thy;
+    val tabs = mk_tabs thy NONE;
     fun mk_const raw_name =
       let
         val name = Sign.intern_const thy raw_name;
@@ -1203,7 +1179,6 @@
     val pr' = CodegenSerializer.pretty_list nil' cons' seri;
   in
     thy
-    |> ensure_prim cons' target
     |> add_pretty_syntax_const cons' target pr'
   end;
 
@@ -1213,15 +1188,16 @@
 
 local
 
-fun generate_code (SOME raw_consts) thy =
-   let
+fun generate_code target (SOME raw_consts) thy =
+      let
         val consts = map (read_const thy) raw_consts;
+        val _ = case target of SOME target => (get_serializer target; ()) | _ => ();
       in
         thy
-        |> expand_module NONE (fold_map oo ensure_def_const) consts
+        |> expand_module target NONE (fold_map oo ensure_def_const) consts
         |-> (fn cs => pair (SOME cs))
       end
-  | generate_code NONE thy =
+  | generate_code _ NONE thy =
       (NONE, thy);
 
 fun serialize_code target seri raw_consts thy =
@@ -1241,7 +1217,7 @@
         ) cs module : unit; thy) end;
   in
     thy
-    |> generate_code raw_consts
+    |> generate_code (SOME target) raw_consts
     |-> (fn cs => serialize cs)
   end;
 
@@ -1266,9 +1242,10 @@
 
 val generateP =
   OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
-    Scan.repeat1 P.term
-    >> (fn raw_consts =>
-          Toplevel.theory (generate_code (SOME raw_consts) #> snd))
+    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")")
+    -- Scan.repeat1 P.term
+    >> (fn (target, raw_consts) =>
+          Toplevel.theory (generate_code target (SOME raw_consts) #> snd))
   );
 
 val serializeP =
@@ -1284,30 +1261,6 @@
           ))
   );
 
-val primclassP =
-  OuterSyntax.command primclassK "define target-language specific class" K.thy_decl (
-    P.xname
-    -- Scan.repeat1 (P.name -- P.text)
-      >> (fn (raw_class, primdefs) =>
-            (Toplevel.theory oo fold) (add_prim_class raw_class) primdefs)
-  );
-
-val primtycoP =
-  OuterSyntax.command primtycoK "define target-language specific type constructor" K.thy_decl (
-    P.xname
-    -- Scan.repeat1 (P.name -- P.text)
-      >> (fn (raw_tyco, primdefs) =>
-            (Toplevel.theory oo fold) (add_prim_tyco raw_tyco) primdefs)
-  );
-
-val primconstP =
-  OuterSyntax.command primconstK "define target-language specific constant" K.thy_decl (
-    P.term
-    -- Scan.repeat1 (P.name -- P.text)
-      >> (fn (raw_const, primdefs) =>
-            (Toplevel.theory oo fold) (add_prim_const raw_const) primdefs)
-  );
-
 val syntax_classP =
   OuterSyntax.command syntax_tycoK "define code syntax for class" K.thy_decl (
     Scan.repeat1 (
@@ -1356,8 +1309,7 @@
       >> (Toplevel.theory oo fold) add_alias
   );
 
-val _ = OuterSyntax.add_parsers [generateP, serializeP,
-  primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP,
+val _ = OuterSyntax.add_parsers [generateP, serializeP, syntax_tycoP, syntax_constP,
   purgeP, aliasP];
 
 end; (* local *)
diff -r 4820c3d52548 -r a8c8ed1c85e0 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Wed Jun 07 16:53:31 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Jun 07 16:54:30 2006 +0200
@@ -20,7 +20,6 @@
       * OuterParse.token list;
   val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
     ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
-  val parse_targetdef: string -> CodegenThingol.prim list;
   val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax;
   val serializers: {
     ml: string * (string * string * (string -> bool) -> serializer),
@@ -191,26 +190,6 @@
     )
   end;
 
-fun newline_correct s =
-  s
-  |> Symbol.strip_blanks
-  |> space_explode "\n"
-  |> map (implode o (fn [] => []
-                      | (" "::xs) => xs
-                      | xs => xs) o explode)
-  |> space_implode "\n";
-
-fun parse_targetdef s =
-  case Scan.finite Symbol.stopper (Scan.repeat (
-         ($$ "`" |-- $$ "`" >> (CodegenThingol.Pretty o str))
-      || ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof))
-            --| $$ "`" >> (fn ["_"] => CodegenThingol.Name | s => error ("malformed antiquote: " ^ implode s)))
-      || Scan.repeat1
-           (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> (CodegenThingol.Pretty o str o implode)
-    )) ((Symbol.explode o Symbol.strip_blanks) s)
-   of (p, []) => p
-    | (p, ss) => error ("Malformed definition: " ^ quote s ^ " - " ^ commas ss);
-
 
 (* generic abstract serializer *)
 
@@ -228,16 +207,6 @@
     postprocess (class_syntax, tyco_syntax, const_syntax)
     select module =
   let
-    fun pretty_of_prim resolv (name, primdef) =
-      let
-        fun pr (CodegenThingol.Pretty p) = p
-          | pr CodegenThingol.Name = (str o resolv) name;
-      in case AList.lookup (op = : string * string -> bool) primdef target
-       of NONE => error ("no primitive definition for " ^ quote name)
-        | SOME ps => (case map pr ps
-           of [] => NONE
-            | ps => (SOME o Pretty.block) ps)
-      end;
     fun from_module' resolv imps ((name_qual, name), defs) =
       from_module resolv imps ((name_qual, name), defs)
       |> postprocess (resolv name_qual);
@@ -246,7 +215,7 @@
     |> debug_msg (fn _ => "selecting submodule...")
     |> (if is_some select then (CodegenThingol.project_module o the) select else I)
     |> debug_msg (fn _ => "serializing...")
-    |> CodegenThingol.serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
+    |> CodegenThingol.serialize (from_defs (class_syntax : string -> string option, tyco_syntax, const_syntax))
          from_module' validator postproc nspgrp name_root
     |> K ()
   end;
@@ -660,7 +629,7 @@
   in (ml_from_funs, ml_from_datatypes) end;
 
 fun ml_from_defs (is_cons, needs_type)
-    (from_prim, (_, tyco_syntax, const_syntax)) resolver prefix defs =
+    (_, tyco_syntax, const_syntax) resolver prefix defs =
   let
     val resolv = resolver prefix;
     val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
@@ -721,11 +690,7 @@
           ]
         :: map from_membr_fun membrs)
       end
-    fun ml_from_def (name, CodegenThingol.Undef) =
-          error ("empty definition during serialization: " ^ quote name)
-      | ml_from_def (name, CodegenThingol.Prim prim) =
-          from_prim resolv (name, prim)
-      | ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
+    fun ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
         (map (fn (vname, []) => () | _ =>
             error "can't serialize sort constrained type declaration to ML") vs;
           Pretty.block [
@@ -867,7 +832,7 @@
 
 local
 
-fun hs_from_defs with_typs (from_prim, (class_syntax, tyco_syntax, const_syntax))
+fun hs_from_defs with_typs (class_syntax, tyco_syntax, const_syntax)
     resolver prefix defs =
   let
     val resolv = resolver "";
@@ -1002,11 +967,7 @@
             hs_from_expr NOBR rhs
           ]
       in Pretty.chunks ((map from_eq o fst o snd o constructive_fun) def) end;
-    fun hs_from_def (name, CodegenThingol.Undef) =
-          error ("empty statement during serialization: " ^ quote name)
-      | hs_from_def (name, CodegenThingol.Prim prim) =
-          from_prim resolv_here (name, prim)
-      | hs_from_def (name, CodegenThingol.Fun (def as (_, (sctxt, ty)))) =
+    fun hs_from_def (name, CodegenThingol.Fun (def as (_, (sctxt, ty)))) =
           let
             val body = hs_from_funeqs (name, def);
           in if with_typs then
@@ -1038,6 +999,7 @@
             (Pretty.block o Pretty.breaks) [
               str "data",
               hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
+              str "=",
               Pretty.block (separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs))
             ]
           end |> SOME
diff -r 4820c3d52548 -r a8c8ed1c85e0 src/Pure/Tools/codegen_theorems.ML
--- a/src/Pure/Tools/codegen_theorems.ML	Wed Jun 07 16:53:31 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML	Wed Jun 07 16:54:30 2006 +0200
@@ -23,7 +23,6 @@
   val proper_name: string -> string;
   val common_typ: theory -> (thm -> typ) -> thm list -> thm list;
   val preprocess: theory -> thm list -> (typ * thm list) option;
-  val preprocess_term: theory -> term -> term;
 
   val get_funs: theory -> string * typ -> (typ * thm list) option;
   val get_datatypes: theory -> string
@@ -579,7 +578,7 @@
 fun tap_typ thy [] = NONE
   | tap_typ thy (thms as (thm::_)) = SOME (extr_typ thy thm, thms);
 
-fun preprocess' thy extr_ty thms =
+fun preprocess thy thms =
   let
     fun burrow_thms f [] = []
       | burrow_thms f thms = 
@@ -587,19 +586,27 @@
           |> Conjunction.intr_list
           |> f
           |> Conjunction.elim_list;
+    fun rewrite_rhs conv thm = (case (Drule.strip_comb o cprop_of) thm
+     of (ct', [ct1, ct2]) => (case term_of ct'
+         of Const ("==", _) =>
+              Thm.equal_elim (combination (combination (reflexive ct') (reflexive ct1)) (conv ct2)) thm
+          | _ => raise ERROR "rewrite_rhs")
+      | _ => raise ERROR "rewrite_rhs");
+    val unfold_thms = Tactic.rewrite true (map (make_eq thy) (the_unfolds thy));
   in
     thms
     |> map (make_eq thy)
     |> map (Thm.transfer thy)
     |> fold (fn f => f thy) (the_preprocs thy)
-    |> map (rewrite_rule (map (make_eq thy) (the_unfolds thy)))
+    |> map (rewrite_rhs unfold_thms)
     |> debug_msg (fn _ => "[cg_thm] filter")
     |> debug_msg (commas o map string_of_thm)
-    |> debug_msg (fn _ => "[cg_thm] extr_typ")
+    |> debug_msg (fn _ => "[cg_thm] common_typ")
     |> debug_msg (commas o map string_of_thm)
-    |> debug_msg (fn _ => "[cg_thm] common_typ / abs_norm")
+    |> common_typ thy (extr_typ thy)
+    |> debug_msg (fn _ => "[cg_thm] abs_norm")
     |> debug_msg (commas o map string_of_thm)
-    |> (if extr_ty then common_typ thy (extr_typ thy) #> map (abs_norm thy) else I)
+    |> map (abs_norm thy)
     |> burrow_thms (
         debug_msg (fn _ => "[cg_thm] canonical tvars")
         #> debug_msg (string_of_thm)
@@ -613,27 +620,7 @@
        )
     |> map Drule.unvarifyT
     |> map Drule.unvarify
-  end;
-
-fun preprocess thy = preprocess' thy true #> tap_typ thy;
-
-fun preprocess_term thy raw_t =
-  let
-    val t = Logic.legacy_varify raw_t;
-    val x = variant (add_term_names (t, [])) "a";
-    val t_eq = Logic.mk_equals (Free (x, fastype_of t), t);
-    (*fake definition*)
-    val thm_eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
-      t_eq;
-    fun err ts' = error ("preprocess_term: bad preprocessor; started with "
-        ^ (quote o Sign.string_of_term thy) t_eq ^ ", ended up with "
-        ^ (quote o commas o map (Sign.string_of_term thy)) ts'
-      )
-  in case preprocess' thy false [thm_eq]
-   of [thm] => (case Drule.plain_prop_of thm
-       of t_res as (Const ("==", _) $ Free (x', _) $ t') => if x = x' then t' else err [t_res]
-        | t_res => err [t_res])
-    | thms => (err o map Drule.plain_prop_of) thms
+    |> tap_typ thy
   end;
 
 
@@ -709,8 +696,11 @@
 
 fun get_eq thy (c, ty) =
   if is_obj_eq thy c
-  then case get_datatypes thy ((fst o dest_Type o hd o fst o strip_type) ty)
-   of SOME (_, thms) => thms
+  then case strip_type ty
+   of (Type (tyco, _) :: _, _) =>
+     (case get_datatypes thy tyco
+       of SOME (_, thms) => thms
+        | _ => [])
     | _ => []
   else [];
 
diff -r 4820c3d52548 -r a8c8ed1c85e0 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Jun 07 16:53:31 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Jun 07 16:54:30 2006 +0200
@@ -62,16 +62,11 @@
   val resolve_tycos: (string -> string) -> itype * iexpr list -> itype * iexpr list;
   val resolve_consts: (string -> string) -> iexpr -> iexpr;
   val eta_expand: (string * (iclasslookup list list * itype)) * iexpr list -> int -> iexpr;
-  
 
   type funn = (iexpr list * iexpr) list * (sortcontext * itype);
   type datatyp = sortcontext * (string * itype list) list;
-  datatype prim =
-      Pretty of Pretty.T
-    | Name;
   datatype def =
-      Undef
-    | Prim of (string * prim list) list
+      Bot
     | Fun of funn
     | Typesyn of (vname * sort) list * itype
     | Datatype of datatyp
@@ -90,16 +85,15 @@
   val pretty_deps: module -> Pretty.T;
   val empty_module: module;
   val get_def: module -> string -> def;
-  val add_prim: string -> (string * prim list) -> module -> module;
-  val ensure_prim: string -> string -> module -> module;
   val merge_module: module * module -> module;
   val diff_module: module * module -> (string * def) list;
   val project_module: string list -> module -> module;
   val purge_module: string list -> module -> module;
   val has_nsp: string -> string -> bool;
+  val ensure_bot: string -> module -> module;
   val succeed: 'a -> transact -> 'a transact_fin;
   val fail: string -> transact -> 'a transact_fin;
-  val ensure_def: (string * (string -> transact -> def transact_fin)) list -> string
+  val ensure_def: (string -> transact -> def transact_fin) -> bool -> string
     -> string -> transact -> transact;
   val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
 
@@ -394,13 +388,8 @@
 type funn = (iexpr list * iexpr) list * (sortcontext * itype);
 type datatyp = sortcontext * (string * itype list) list;
 
-datatype prim =
-    Pretty of Pretty.T
-  | Name;
-
 datatype def =
-    Undef
-  | Prim of (string * prim list) list
+    Bot
   | Fun of funn
   | Typesyn of (vname * sort) list * itype
   | Datatype of datatyp
@@ -415,18 +404,15 @@
 datatype node = Def of def | Module of node Graph.T;
 type module = node Graph.T;
 type transact = Graph.key option * module;
-datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option;
-type 'dst transact_fin = 'dst transact_res * module;
+type 'dst transact_fin = 'dst * module;
 exception FAIL of string list * exn option;
 
 val eq_def = (op =) : def * def -> bool;
 
 (* simple diagnosis *)
 
-fun pretty_def Undef =
-      Pretty.str "<UNDEF>"
-  | pretty_def (Prim prims) =
-      Pretty.str ("<PRIM " ^ (commas o map fst) prims ^ ">")
+fun pretty_def Bot =
+      Pretty.str "<Bot>"
   | pretty_def (Fun (eqs, (sortctxt, ty))) =
       Pretty.enum " |" "" "" (
         map (fn (ps, body) =>
@@ -565,6 +551,12 @@
                 get (Graph.get_node node m) ms
         in get (Module modl) modlname end;
 
+fun is_def modl name =
+  case try (get_def modl) name
+   of NONE => false
+    | SOME Bot => false
+    | _ => true;
+
 fun add_def (name, def) =
   let
     val (modl, base) = dest_name name;
@@ -575,6 +567,46 @@
           #> Graph.map_node m (Module o add ms o dest_modl)
   in add modl end;
 
+fun map_def name f =
+  let
+    val (modl, base) = dest_name name;
+    fun mapp [] =
+          Graph.map_node base (Def o f o dest_def)
+      | mapp (m::ms) =
+          Graph.map_node m (Module o mapp ms o dest_modl)
+  in mapp modl end;
+
+fun ensure_bot name =
+  let
+    val (modl, base) = dest_name name;
+    fun ensure [] module =
+          (case try (Graph.get_node module) base
+           of NONE =>
+                module
+                |> Graph.new_node (base, Def Bot)
+            | SOME (Module _) => error ("module already present: " ^ quote name)
+            | _ => module)
+      | ensure (m::ms) module =
+          module
+          |> Graph.default_node (m, Module empty_module)
+          |> Graph.map_node m (Module o ensure ms o dest_modl)
+  in ensure modl end;
+
+fun add_def_incr strict (name, Bot) module =
+      (case try (get_def module) name
+       of NONE => if strict then error "attempted to add Bot to module"
+            else map_def name (K Bot) module
+        | SOME Bot => if strict then error "attempted to add Bot to module"
+            else map_def name (K Bot) module
+        | SOME _ => module)
+  | add_def_incr _ (name, def) module =
+      (case try (get_def module) name
+       of NONE => add_def (name, def) module
+        | SOME Bot => map_def name (K def) module
+        | SOME def' => if eq_def (def, def')
+            then module
+            else error ("tried to overwrite definition " ^ quote name));
+
 fun add_dep (name1, name2) modl =
   if name1 = name2 then modl
   else
@@ -597,90 +629,6 @@
             |> Graph.map_node m (Module o add ms o dest_modl);
     in add ms modl end;
 
-fun map_def name f =
-  let
-    val (modl, base) = dest_name name;
-    fun mapp [] =
-          Graph.map_node base (Def o f o dest_def)
-      | mapp (m::ms) =
-          Graph.map_node m (Module o mapp ms o dest_modl)
-  in mapp modl end;
-
-fun map_defs f =
-  let
-    fun mapp (Def def) =
-          (Def o f) def
-      | mapp (Module modl) =
-          (Module o Graph.map_nodes mapp) modl
-  in dest_modl o mapp o Module end;
-
-fun fold_defs f =
-  let
-    fun fol prfix (name, (Def def, _)) =
-          f (NameSpace.pack (prfix @ [name]), def)
-      | fol prfix (name, (Module modl, _)) =
-          Graph.fold (fol (prfix @ [name])) modl
-  in Graph.fold (fol []) end;
-
-fun add_deps f modl =
-  modl
-  |> fold add_dep ([] |> fold_defs (append o f) modl);
-
-fun add_def_incr (name, Undef) module =
-      (case try (get_def module) name
-       of NONE => (error "attempted to add Undef to module")
-        | SOME Undef => (error "attempted to add Undef to module")
-        | SOME def' => map_def name (K def') module)
-  | add_def_incr (name, def) module =
-      (case try (get_def module) name
-       of NONE => add_def (name, def) module
-        | SOME Undef => map_def name (K def) module
-        | SOME def' => if eq_def (def, def')
-            then module
-            else error ("tried to overwrite definition " ^ name));
-
-fun add_prim name (target, primdef as _::_) =
-  let
-    val (modl, base) = dest_name name;
-    fun add [] module =
-          (case try (Graph.get_node module) base
-           of NONE =>
-                module
-                |> Graph.new_node (base, (Def o Prim) [(target, primdef)])
-            | SOME (Def (Prim prim)) =>
-                if AList.defined (op =) prim target
-                then error ("already primitive definition (" ^ target
-                  ^ ") present for " ^ name)
-                else
-                  module
-                  |> Graph.map_node base ((K o Def o Prim) (AList.update (op =)
-                       (target, primdef) prim))
-            | _ => error ("already non-primitive definition present for " ^ name))
-      | add (m::ms) module =
-          module
-          |> Graph.default_node (m, Module empty_module)
-          |> Graph.map_node m (Module o add ms o dest_modl)
-  in add modl end;
-
-fun ensure_prim name target =
-  let
-    val (modl, base) = dest_name name;
-    fun ensure [] module =
-          (case try (Graph.get_node module) base
-           of NONE =>
-                module
-                |> Graph.new_node (base, (Def o Prim) [(target, [])])
-            | SOME (Def (Prim prim)) =>
-                module
-                |> Graph.map_node base ((K o Def o Prim) (AList.default (op =)
-                     (target, []) prim))
-            | _ => module)
-      | ensure (m::ms) module =
-          module
-          |> Graph.default_node (m, Module empty_module)
-          |> Graph.map_node m (Module o ensure ms o dest_modl)
-  in ensure modl end;
-
 fun merge_module modl12 =
   let
     fun join_module _ (Module m1, Module m2) =
@@ -784,10 +732,8 @@
     end
   ) eqs NONE; eqs);
 
-fun check_prep_def modl Undef =
-      Undef
-  | check_prep_def modl (d as Prim _) =
-      d
+fun check_prep_def modl Bot =
+      Bot
   | check_prep_def modl (Fun (eqs, d)) =
       Fun (check_funeqs eqs, d)
   | check_prep_def modl (d as Typesyn _) =
@@ -837,7 +783,7 @@
 fun postprocess_def (name, Datatype (_, constrs)) =
       (check_samemodule (name :: map fst constrs);
       fold (fn (co, _) =>
-        add_def_incr (co, Datatypecons name)
+        add_def_incr true (co, Datatypecons name)
         #> add_dep (co, name)
         #> add_dep (name, co)
       ) constrs
@@ -845,7 +791,7 @@
   | postprocess_def (name, Class (_, (_, membrs))) =
       (check_samemodule (name :: map fst membrs);
       fold (fn (m, _) =>
-        add_def_incr (m, Classmember name)
+        add_def_incr true (m, Classmember name)
         #> add_dep (m, name)
         #> add_dep (name, m)
       ) membrs
@@ -853,57 +799,40 @@
   | postprocess_def (name, Classinst (_, memdefs)) =
       (check_samemodule (name :: map (fst o fst o snd) memdefs);
       fold (fn (_, ((m', _), _)) =>
-        add_def_incr (m', Classinstmember)
+        add_def_incr true (m', Classinstmember)
       ) memdefs
       )
   | postprocess_def _ =
       I;
 
-fun succeed some (_, modl) = (Succeed some, modl);
-fun fail msg (_, modl) = (Fail ([msg], NONE), modl);
-
-fun check_fail _ (Succeed dst, trns) = (dst, trns)
-  | check_fail msg (Fail (msgs, e), _) = raise FAIL (msg::msgs, e);
+fun succeed some (_, modl) = (some, modl);
+fun fail msg (_, modl) = raise FAIL ([msg], NONE);
 
-fun select_generator _ src [] modl =
-      (SOME src, modl) |> fail ("no code generator available")
-  | select_generator mk_msg src gens modl =
-      let
-        fun handle_fail msgs f =
-          let
-            in
-              if ! soft_exc
-              then
-                (SOME src, modl) |> f
-                handle FAIL exc => (Fail exc, modl)
-                     | e => (Fail (msgs, SOME e), modl)
-              else
-                (SOME src, modl) |> f
-                handle FAIL exc => (Fail exc, modl)
-            end;
-        fun select msgs [(gname, gen)] =
-              handle_fail (msgs @ [mk_msg gname]) (gen src)
-          | select msgs ((gname, gen)::gens) =
-              let
-                val msgs' = msgs @ [mk_msg gname]
-              in case handle_fail msgs' (gen src)
-               of (Fail (_, NONE), _) =>
-                   select msgs' gens
-               | result => result
-          end;
-      in select [] gens end;
-
-fun ensure_def defgens msg name (dep, modl) =
+fun ensure_def defgen strict msg name (dep, modl) =
   let
-    val msg' = case dep
+    val msg' = (case dep
      of NONE => msg
-      | SOME dep => msg ^ ", with dependency " ^ quote dep;
+      | SOME dep => msg ^ ", with dependency " ^ quote dep)
+      ^ (if strict then " (strict)" else " (non-strict)");
     fun add_dp NONE = I
       | add_dp (SOME dep) =
           debug_msg (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
           #> add_dep (dep, name);
     fun prep_def def modl =
       (check_prep_def modl def, modl);
+    fun invoke_generator name defgen modl =
+      if ! soft_exc
+      then
+        defgen name (SOME name, modl)
+        handle FAIL exc =>
+                if strict then raise FAIL exc
+                else (Bot, modl)
+             | e => raise FAIL (["definition generator for " ^ quote name], SOME e)
+      else
+        defgen name (SOME name, modl)
+        handle FAIL exc =>
+                if strict then raise FAIL exc
+                else (Bot, modl);
   in
     modl
     |> (if can (get_def modl) name
@@ -911,19 +840,16 @@
           debug_msg (fn _ => "asserting node " ^ quote name)
           #> add_dp dep
         else
-          debug_msg (fn _ => "allocating node " ^ quote name)
-          #> add_def (name, Undef)
+          debug_msg (fn _ => "allocating node " ^ quote name ^ (if strict then " (strict)" else " (non-strict)"))
+          #> ensure_bot name
           #> add_dp dep
           #> debug_msg (fn _ => "creating node " ^ quote name)
-          #> select_generator (fn gname => "trying code generator "
-               ^ gname ^ " for definition of " ^ quote name) name defgens
-          #> debug_msg (fn _ => "checking creation of node " ^ quote name)
-          #> check_fail msg'
+          #> invoke_generator name defgen
           #-> (fn def => prep_def def)
           #-> (fn def =>
              debug_msg (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def)
           #> debug_msg (fn _ => "adding")
-          #> add_def_incr (name, def)
+          #> add_def_incr strict (name, def)
           #> debug_msg (fn _ => "postprocessing")
           #> postprocess_def (name, def)
           #> debug_msg (fn _ => "adding done")
@@ -1049,9 +975,10 @@
     fun mk_contents prfx module =
       map_filter (seri prfx)
         ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
-    and seri prfx ([(name, Module modl)]) =
+    and seri prfx [(name, Module modl)] =
           seri_module (resolver []) (map (resolver []) (imports_of module (prfx @ [name])))
             (mk_name prfx name, mk_contents (prfx @ [name]) modl)
+      | seri prfx [(_, Def Bot)] = NONE
       | seri prfx ds =
           seri_defs sresolver (NameSpace.pack prfx)
             (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)