# HG changeset patch
# User haftmann
# Date 1139298463 -3600
# Node ID 3adfc9dfb30a03ea2a127e651b9948abfa83621a
# Parent  d6ecc5828b14d256a1a3bfc9777f926429239055
slight improvements in code generation

diff -r d6ecc5828b14 -r 3adfc9dfb30a src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Tue Feb 07 08:47:43 2006 +0100
@@ -62,123 +62,70 @@
 fun Ball S P = Library.forall P S;
 *}
 
-code_generate "op mem"
+consts
+  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
+  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  insert_ :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  remove :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
-code_primconst "insert"
-  depending_on ("List.const.member")
-ml {*
-fun insert x xs =
-  if List.member x xs then xs
-  else x::xs;
-*}
-haskell {*
-insert x xs =
-  if elem x xs then xs else x:xs
-*}
+defs
+  flip_def: "flip f a b == f b a"
+  member_def: "member xs x == x mem xs"
+  insert_def: "insert_ x xs == if member xs x then xs else x#xs"
 
-code_primconst "op Un"
-  depending_on ("Set.const.insert")
-ml {*
-nonfix union;
-fun union xs [] = xs
-  | union [] ys = ys
-  | union (x::xs) ys = union xs (insert x ys);
-*}
-haskell {*
-union xs [] = xs
-union [] ys = ys
-union (x:xs) ys = union xs (insert x ys)
-*}
+primrec
+  "remove x [] = []"
+  "remove x (y#ys) = (if x = y then ys else y # remove x ys)"
 
-code_primconst "op Int"
-  depending_on ("List.const.member")
-ml {*
-nonfix inter;
-fun inter [] ys = []
-  | inter (x::xs) ys =
-      if List.member x ys
-      then x :: inter xs ys
-      else inter xs ys;
-*}
-haskell {*
-inter [] ys = []
-inter (x:xs) ys =
-  if elem x ys
-  then x : inter xs ys
-  else inter xs ys
-*}
+primrec
+  "inter [] ys = []"
+  "inter (x#xs) ys = (let xs' = inter xs ys in if member ys x then x#xs' else xs')"
+
+code_syntax_const "insert"
+  ml ("{*insert_*} _ _")
+  haskell ("{*insert_*} _ _")
 
-code_primconst  "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-ml {*
-fun op_minus ys [] = ys
-  | op_minus ys (x::xs) =
-      let
-        fun minus [] x = []
-          | minus (y::ys) x = if x = y then ys else y :: minus ys x
-      in
-        op_minus (minus ys x) xs
-      end;
-*}
-haskell {*
-op_minus ys [] = ys
-op_minus ys (x:xs) = op_minus (minus ys x) xs where
-  minus [] x = []
-  minus (y:ys) x = if x = y then ys else y : minus ys x
-*}
+code_syntax_const "op Un"
+  ml ("{*foldr insert_*} _ _")
+  haskell ("{*foldr insert_*} _ _")
+
+code_syntax_const "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+  ml ("{*(flip o foldr) remove*} _ _")
+  haskell ("{*(flip o foldr) remove*} _ _")
+
+code_syntax_const "op Int"
+  ml ("{*inter*} _ _")
+  haskell ("{*inter*} _ _")
 
-code_primconst "image"
-  depending_on ("List.const.insert")
-ml {*
-fun image f =
-  let
-    fun img xs [] = xs
-      | img xs (y::ys) = img (insert (f y) xs) ys;
-  in img [] end;;
-*}
-haskell {*
-image f = img [] where
-  img xs [] = xs
-  img xs (y:ys) = img (insert (f y) xs) ys;
-*}
+code_syntax_const "image"
+  ml ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _")
+  haskell ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _")
 
-code_primconst "INTER"
-  depending_on ("Set.const.inter")
-ml {*
-fun INTER [] f = []
-  | INTER (x::xs) f = inter (f x) (INTER xs f);
-*}
-haskell {*
-INTER [] f = []
-INTER (x:xs) f = inter (f x) (INTER xs f);
-*}
+code_syntax_const "INTER"
+  ml ("{*\<lambda>xs f.  foldr (inter o f) xs*} _ _")
+  haskell ("{*\<lambda>xs f.  foldr (inter o f) xs*} _ _")
 
-code_primconst "UNION"
-  depending_on ("Set.const.union")
-ml {*
-fun UNION [] f = []
-  | UNION (x::xs) f = union (f x) (UNION xs f);
-*}
-haskell {*
-UNION [] f = []
-UNION (x:xs) f = union (f x) (UNION xs f);
-*}
+code_syntax_const "UNION"
+  ml ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*} _ _")
+  haskell ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*} _ _")
 
 code_primconst "Ball"
 ml {*
-fun Ball [] f = true
-  | Ball (x::xs) f = f x andalso Ball xs f;
+fun `_` [] f = true
+  | `_` (x::xs) f = f x andalso `_` xs f;
 *}
 haskell {*
-Ball = all . flip
+`_` = flip all
 *}
 
 code_primconst "Bex"
 ml {*
-fun Bex [] f = false
-  | Bex (x::xs) f = f x orelse Bex xs f;
+fun `_` [] f = false
+  | `_` (x::xs) f = f x orelse `_` xs f;
 *}
 haskell {*
-Ball = any . flip
+`_` = flip any
 *}
 
 end
diff -r d6ecc5828b14 -r 3adfc9dfb30a src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Product_Type.thy	Tue Feb 07 08:47:43 2006 +0100
@@ -787,12 +787,12 @@
 
 code_primconst fst
 ml {*
-fun fst (x, y) = x;
+fun `_` (x, y) = x;
 *}
 
 code_primconst snd
 ml {*
-fun snd (x, y) = y;
+fun `_` (x, y) = y;
 *}
 
 code_syntax_tyco
diff -r d6ecc5828b14 -r 3adfc9dfb30a src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Feb 07 08:47:43 2006 +0100
@@ -300,12 +300,10 @@
 val setup =
   add_codegen "datatype" datatype_codegen #>
   add_tycodegen "datatype" datatype_tycodegen #>
-  CodegenPackage.set_is_datatype
-    DatatypePackage.is_datatype #>
+  CodegenPackage.set_get_datatype
+    DatatypePackage.get_datatype #>
   CodegenPackage.set_get_all_datatype_cons
     DatatypePackage.get_all_datatype_cons #>
-  CodegenPackage.set_defgen_datatype
-    (CodegenPackage.defgen_datatype_proto DatatypePackage.get_datatype DatatypePackage.get_datatype_cons) #>
   CodegenPackage.ensure_datatype_case_consts
     DatatypePackage.get_datatype_case_consts
     DatatypePackage.get_case_const_data;
diff -r d6ecc5828b14 -r 3adfc9dfb30a src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Feb 07 08:47:43 2006 +0100
@@ -66,9 +66,7 @@
   val print_datatypes : theory -> unit
   val datatype_info : theory -> string -> DatatypeAux.datatype_info option
   val datatype_info_err : theory -> string -> DatatypeAux.datatype_info
-  val is_datatype : theory -> string -> bool
-  val get_datatype : theory -> string -> ((string * sort) list * string list) option
-  val get_datatype_cons : theory -> string * string -> typ list option
+  val get_datatype : theory -> string -> ((string * sort) list * (string * typ list) list) option
   val get_datatype_case_consts : theory -> string list
   val get_case_const_data : theory -> string -> (string * int) list option
   val get_all_datatype_cons : theory -> (string * string) list
@@ -129,42 +127,20 @@
 
 val weak_case_congs_of = map (#weak_case_cong o #2) o Symtab.dest o get_datatypes;
 
-fun is_datatype thy dtco =
-  Symtab.lookup (get_datatypes thy) dtco
-  |> is_some;
-
 fun get_datatype thy dtco =
-  dtco
-  |> Symtab.lookup (get_datatypes thy)
-  |> Option.map (fn info => (#sorts info,
-      (get_first (fn (_, (dtco', _, cs)) =>
-        if dtco = dtco'
-        then SOME (map fst cs)
-        else NONE) (#descr info) |> the)));
-  
-fun get_datatype_cons thy (co, dtco) =
   let
-    val descr =
-      dtco
-      |> Symtab.lookup (get_datatypes thy)
-      |> Option.map #descr
-      |> these
-    val one_descr =
-      descr
-      |> get_first (fn (_, (dtco', vs, cs)) =>
-          if dtco = dtco'
-          then SOME (vs, cs)
-          else NONE);
-  in
-    if is_some one_descr
-    then
-      the one_descr
-      |> (fn (vs, cs) =>
-          co
-          |> AList.lookup (op =) cs
-          |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair [])
-               (map DatatypeAux.dest_DtTFree vs)))))
-    else NONE
+    fun get_cons descr vs =
+      apsnd (map (DatatypeAux.typ_of_dtyp descr
+        ((map (rpair []) o map DatatypeAux.dest_DtTFree) vs)));
+    fun get_info ({ sorts, descr, ... } : DatatypeAux.datatype_info) =
+      (sorts,
+        ((the oo get_first) (fn (_, (dtco', tys, cs)) =>
+            if dtco = dtco'
+            then SOME (map (get_cons descr tys) cs)
+            else NONE) descr));
+  in case Symtab.lookup (get_datatypes thy) dtco
+   of SOME info => (SOME o get_info) info
+    | NONE => NONE
   end;
 
 fun get_datatype_case_consts thy =
@@ -180,7 +156,7 @@
 
 fun get_all_datatype_cons thy =
   Symtab.fold (fn (dtco, _) => fold
-    (fn co => cons (co, dtco))
+    (fn (co, _) => cons (co, dtco))
       ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
 
 fun find_tname var Bi =
diff -r d6ecc5828b14 -r 3adfc9dfb30a src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Tue Feb 07 08:47:43 2006 +0100
@@ -290,10 +290,10 @@
 
 code_primconst wfrec
 ml {*
-fun wfrec f x = f (wfrec f) x;
+fun `_` f x = f (`_` f) x;
 *}
 haskell {*
-wfrec f x = f (wfrec f) x
+`_` f x = f (`_` f) x
 *}
 
 (* code_syntax_const
diff -r d6ecc5828b14 -r 3adfc9dfb30a src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Mon Feb 06 21:02:01 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Feb 07 08:47:43 2006 +0100
@@ -267,8 +267,11 @@
       end;
     fun check_defs raw_defs c_req thy =
       let
-        val thy' = Sign.add_arities_i [(tyco, asorts, sort)] thy;
-        val c_given = map (fst o Sign.cert_def pp o snd o tap_def thy' o fst) raw_defs;
+        val thy' = thy |> Theory.copy |> Sign.add_arities_i [(tyco, asorts, sort)];
+        fun get_c raw_def =
+          (fst o Sign.cert_def pp o snd o tap_def thy' o fst) raw_def;
+        val c_given = map get_c raw_defs;
+(*         spec_opt_name   *)
         fun eq_c ((c1, ty1), (c2, ty2)) = 
           let
             val ty1' = Type.varifyT ty1;
@@ -298,8 +301,8 @@
     |-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity)
   end;
 
-val add_instance_arity = fn x => gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm x;
-val add_instance_arity_i = fn x => gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I) x;
+val add_instance_arity = gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm;
+val add_instance_arity_i = gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I);
 
 
 (* queries *)
@@ -521,7 +524,7 @@
     P.name --| P.$$$ "="
     -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
     -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
-      >> (Toplevel.theory_to_proof
+      >> (Toplevel.print oo Toplevel.theory_to_proof
           o (fn ((bname, supclasses), elems) => add_class_exp bname supclasses elems)));
 
 val instanceP =
diff -r d6ecc5828b14 -r 3adfc9dfb30a src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Mon Feb 06 21:02:01 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Tue Feb 07 08:47:43 2006 +0100
@@ -19,21 +19,21 @@
   val add_appconst: string * ((int * int) * appgen) -> theory -> theory;
   val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory;
   val add_eqextr: string * eqextr -> theory -> theory;
-  val add_prim_class: xstring -> string list -> (string * string)
+  val add_prim_class: xstring -> (string * string)
     -> theory -> theory;
-  val add_prim_tyco: xstring -> string list -> (string * string)
+  val add_prim_tyco: xstring -> (string * string)
     -> theory -> theory;
-  val add_prim_const: xstring * string option -> string list -> (string * string)
+  val add_prim_const: xstring * string option -> (string * string)
     -> theory -> theory;
-  val add_prim_i: string -> string list -> (string * Pretty.T)
+  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;
-  val set_is_datatype: (theory -> string -> bool) -> theory -> theory;
   val set_get_all_datatype_cons : (theory -> (string * string) list)
     -> theory -> theory;
-  val set_defgen_datatype: defgen -> theory -> theory;
+  val set_get_datatype: (theory -> string -> ((string * sort) list * (string * typ list) list) option)
+    -> theory -> theory;
   val set_int_tyco: string -> theory -> theory;
 
   val appgen_default: appgen;
@@ -47,9 +47,6 @@
     -> theory -> theory;
   val add_case_const_i: (theory -> string -> (string * int) list option) -> string
     -> theory -> theory;
-  val defgen_datatype_proto: (theory -> string -> ((string * sort) list * string list) option)
-    -> (theory -> string * string -> typ list option)
-    -> defgen;
 
   val print_codegen_generated: theory -> unit;
   val rename_inconsistent: theory -> theory;
@@ -214,30 +211,29 @@
   } : gens;
 
 type logic_data = {
-  is_datatype: ((theory -> string -> bool) * stamp) option,
   get_all_datatype_cons: ((theory -> (string * string) list) * stamp) option,
-  defgen_datatype: (defgen * stamp) option,
+  get_datatype: ((theory -> string -> ((string * sort) list * (string * typ list) list) option) * stamp) option,
   alias: string Symtab.table * string Symtab.table
 };
 
-fun map_logic_data f { is_datatype, get_all_datatype_cons, defgen_datatype, alias } =
+fun map_logic_data f { get_all_datatype_cons, get_datatype, alias } =
   let
-    val ((is_datatype, get_all_datatype_cons, defgen_datatype), alias) =
-      f ((is_datatype, get_all_datatype_cons, defgen_datatype), alias)
-  in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons,
-    defgen_datatype = defgen_datatype, alias = alias } : logic_data end;
+    val ((get_all_datatype_cons, get_datatype), alias) =
+      f ((get_all_datatype_cons, get_datatype), alias)
+  in { get_all_datatype_cons = get_all_datatype_cons,
+    get_datatype = get_datatype, alias = alias } : logic_data end;
 
 fun merge_logic_data
-  ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1,
-       defgen_datatype = defgen_datatype1, alias = alias1 },
-   { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2,
-       defgen_datatype = defgen_datatype2, alias = alias2 }) =
+  ({ get_all_datatype_cons = get_all_datatype_cons1,
+       get_datatype = get_datatype1, alias = alias1 },
+   { get_all_datatype_cons = get_all_datatype_cons2,
+       get_datatype = get_datatype2, alias = alias2 }) =
   let
   in
-    { is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2),
-      get_all_datatype_cons = merge_opt (eq_snd (op =))
+    { get_all_datatype_cons = merge_opt (eq_snd (op =))
         (get_all_datatype_cons1, get_all_datatype_cons2),
-      defgen_datatype = merge_opt (eq_snd (op =)) (defgen_datatype1, defgen_datatype2),
+      get_datatype = merge_opt (eq_snd (op =))
+        (get_datatype1, get_datatype2),
       alias = (Symtab.merge (op =) (fst alias1, fst alias2),
                Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data
   end;
@@ -277,8 +273,8 @@
   val empty = {
     modl = empty_module,
     gens = { appconst = Symtab.empty, eqextrs = [] } : gens,
-    logic_data = { is_datatype = NONE, get_all_datatype_cons = NONE,
-      defgen_datatype = NONE,
+    logic_data = { get_all_datatype_cons = NONE,
+      get_datatype = NONE,
       alias = (Symtab.empty, Symtab.empty) } : logic_data,
     target_data =
       Symtab.empty
@@ -437,48 +433,31 @@
 fun get_eqextrs thy tabs =
   (map (fn (_, (eqx, _)) => eqx thy tabs) o #eqextrs o #gens o CodegenData.get) thy;
 
-fun set_is_datatype f =
-  map_codegen_data
-    (fn (modl, gens, target_data, logic_data) =>
-       (modl, gens, target_data,
-        logic_data
-        |> map_logic_data (apfst (fn (is_datatype, get_all_datatype_cons, defgen_datatype)
-             => (SOME (f, stamp ()), get_all_datatype_cons, defgen_datatype)))));
-
-fun is_datatype thy =
-  case (#is_datatype o #logic_data o CodegenData.get) thy
-   of NONE => K false
-    | SOME (f, _) => f thy;
-
 fun set_get_all_datatype_cons f =
   map_codegen_data
     (fn (modl, gens, target_data, logic_data) =>
        (modl, gens, target_data,
         logic_data
-        |> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons, defgen_datatype)
-             => (is_datatype, SOME (f, stamp ()), defgen_datatype))))));
+        |> map_logic_data ((apfst (fn (get_all_datatype_cons, get_datatype)
+             => (SOME (f, stamp ()), get_datatype))))));
 
 fun get_all_datatype_cons thy =
   case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy
    of NONE => []
     | SOME (f, _) => f thy;
 
-fun set_defgen_datatype f =
+fun set_get_datatype f =
   map_codegen_data
     (fn (modl, gens, target_data, logic_data) =>
        (modl, gens, target_data,
         logic_data
-        |> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons, defgen_datatype)
-             => (is_datatype, get_all_datatype_cons, SOME (f, stamp ())))))));
+        |> map_logic_data ((apfst (fn (get_all_datatype_cons, get_datatype)
+             => (get_all_datatype_cons, SOME (f, stamp ())))))));
 
-fun defgen_datatype thy tabs dtco trns =
-  case (#defgen_datatype o #logic_data o CodegenData.get) thy
-   of NONE =>
-        trns
-        |> fail ("no datatype definition generator present")
-    | SOME (f, _) => 
-        trns
-        |> f thy tabs dtco;
+fun get_datatype thy =
+  case (#get_datatype o #logic_data o CodegenData.get) thy
+   of NONE => K NONE
+    | SOME (f, _) => f thy;
 
 fun set_int_tyco tyco thy =
   (serializers := (
@@ -594,6 +573,28 @@
   end
 and ensure_def_tyco thy tabs tyco trns =
   let
+    fun defgen_datatype thy (tabs as (_, (_, _, dtcontab))) dtco trns =
+      case name_of_idf thy nsp_tyco dtco
+       of SOME dtco =>
+            (case get_datatype thy dtco
+             of SOME (vars, cos) =>
+                  let
+                    val cos' = map (fn (co, tys) => (DatatypeconsNameMangler.get thy dtcontab (co, dtco) |>
+                      idf_of_name thy nsp_dtcon, tys)) cos;
+                  in
+                    trns
+                    |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
+                    |> fold_map (exprgen_tyvar_sort thy tabs) vars
+                    ||>> fold_map (fn (c, ty) => codegen_type thy tabs ty #-> (fn ty' => pair (c, ty'))) cos'
+                    |-> (fn (sorts, cos'') => succeed (Datatype
+                         ((sorts, cos''), [])))
+                  end
+              | NONE =>
+                  trns
+                  |> fail ("no datatype found for " ^ quote dtco))
+        | NONE =>
+            trns
+            |> fail ("not a type constructor: " ^ quote dtco)
     val tyco' = idf_of_name thy nsp_tyco tyco;
   in
     trns
@@ -709,6 +710,15 @@
         | NONE =>
             trns
             |> fail ("not a constant: " ^ quote c);
+    fun defgen_clsmem thy tabs m trns =
+      case name_of_idf thy nsp_mem m
+       of SOME m =>
+            trns
+            |> debug 5 (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)
+        | _ =>
+            trns |> fail ("no class member found for " ^ quote m)
     fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns =
       case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co)
        of SOME (co, dtco) =>
@@ -719,25 +729,21 @@
         | _ =>
             trns
             |> fail ("not a datatype constructor: " ^ quote co);
-    fun defgen_clsmem thy tabs m trns =
-      case name_of_idf thy nsp_mem m
-       of SOME m =>
-            trns
-            |> debug 5 (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)
-        | _ =>
-            trns |> fail ("no class member found for " ^ quote m)
-    val c' = idf_of_const thy tabs (c, ty);
+    fun get_defgen idf =
+      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)
+      else if (is_some oo name_of_idf thy) nsp_mem idf
+      then ("clsmem", defgen_clsmem thy tabs)
+      else if (is_some oo name_of_idf thy) nsp_dtcon idf
+      then ("datatypecons", defgen_datatypecons thy tabs)
+      else error ("illegal shallow name space for constant: " ^ quote idf);
+    val idf = idf_of_const thy tabs (c, ty);
   in
     trns
     |> debug 4 (fn _ => "generating constant " ^ quote c)
-    |> gen_ensure_def
-         [("funs", defgen_funs thy tabs),
-          ("clsmem", defgen_clsmem thy tabs),
-          ("datatypecons", defgen_datatypecons thy tabs)]
-         ("generating constant " ^ quote c) c'
-    |> pair c'
+    |> gen_ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf
+    |> pair idf
   end
 and exprgen_term thy tabs (Const (f, ty)) trns =
       trns
@@ -950,30 +956,6 @@
 val add_case_const = gen_add_case_const Sign.intern_const;
 val add_case_const_i = gen_add_case_const (K I);
 
-fun defgen_datatype_proto get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns =
-  case name_of_idf thy nsp_tyco dtco
-   of SOME dtco =>
-        (case get_datatype thy dtco
-         of SOME (vars, cos) =>
-              let
-                val cotys = map (the o get_datacons thy o rpair dtco) cos;
-                val coidfs = map (fn co => (DatatypeconsNameMangler.get thy dtcontab (co, dtco)) |>
-                  idf_of_name thy nsp_dtcon) cos;
-              in
-                trns
-                |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
-                |> fold_map (exprgen_tyvar_sort thy tabs) vars
-                ||>> fold_map (codegen_type thy tabs) cotys
-                |-> (fn (sorts, tys) => succeed (Datatype
-                     ((sorts, coidfs ~~ tys), [])))
-              end
-          | NONE =>
-              trns
-              |> fail ("no datatype found for " ^ quote dtco))
-    | NONE =>
-        trns
-        |> fail ("not a type constructor: " ^ quote dtco)
-
 
 
 (** theory interface **)
@@ -1054,9 +1036,9 @@
   map_codegen_data (fn (modl, gens, target_data, logic_data) =>
     (f modl, gens, target_data, logic_data));
 
-fun expand_module gen thy =
+fun expand_module init gen thy =
   (#modl o CodegenData.get) thy
-  |> start_transact (gen thy (mk_tabs thy))
+  |> start_transact init (gen thy (mk_tabs thy))
   |-> (fn x:'a => fn modl => (x, map_module (K modl) thy));
 
 fun rename_inconsistent thy =
@@ -1116,13 +1098,13 @@
       | SOME raw_ty => read_typ thy raw_ty;
   in (c, ty) end;
 
-fun read_quote reader gen raw thy =
+fun read_quote get reader gen raw thy =
   thy
-  |> expand_module
+  |> expand_module ((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 deps (target, raw_primdef) thy =
+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);
@@ -1131,19 +1113,19 @@
     val primdef = prep_primdef raw_primdef;
   in
     thy
-    |> map_module (CodegenThingol.add_prim name deps (target, primdef))
+    |> 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))
-  (Pretty.str o CodegenSerializer.parse_targetdef I);
+  CodegenSerializer.parse_targetdef;
 val add_prim_tyco = gen_add_prim
   (fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy))
-  (Pretty.str o CodegenSerializer.parse_targetdef I);
+  CodegenSerializer.parse_targetdef;
 val add_prim_const = gen_add_prim
   (fn thy => fn tabs => idf_of_const thy tabs o read_const thy)
-  (Pretty.str o CodegenSerializer.parse_targetdef I);
+  CodegenSerializer.parse_targetdef;
 
 val ensure_prim = (map_module oo CodegenThingol.ensure_prim);
 
@@ -1164,20 +1146,20 @@
 
 val add_syntax_class = gen_add_syntax_class Sign.intern_class;
 
-val parse_syntax_tyco =
+fun parse_syntax_tyco raw_tyco =
   let
-    fun mk reader raw_tyco target thy =
+    fun check_tyco thy tyco =
+      if Sign.declared_tyname thy tyco
+      then tyco
+      else error ("no such type constructor: " ^ quote tyco);
+    fun prep_tyco thy tyco =
+      tyco
+      |> Sign.intern_type thy
+      |> check_tyco thy
+      |> idf_of_name thy nsp_tyco;
+    fun mk reader target thy =
       let
         val _ = get_serializer target;
-        fun check_tyco tyco =
-          if Sign.declared_tyname thy tyco
-          then tyco
-          else error ("no such type constructor: " ^ quote tyco);
-        fun prep_tyco thy tyco =
-          tyco
-          |> Sign.intern_type thy
-          |> check_tyco
-          |> idf_of_name thy nsp_tyco;
         val tyco = prep_tyco thy raw_tyco;
       in
         thy
@@ -1195,7 +1177,7 @@
               logic_data)))
       end;
   in
-    CodegenSerializer.parse_syntax (read_quote read_typ codegen_type)
+    CodegenSerializer.parse_syntax (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ codegen_type)
     #-> (fn reader => pair (mk reader))
   end;
 
@@ -1212,13 +1194,14 @@
                  (c, (pretty, stamp ()))))),
         logic_data));
 
-val parse_syntax_const =
+fun parse_syntax_const raw_const =
   let
-    fun mk reader raw_const target thy =
+    fun prep_const thy raw_const =
+      idf_of_const thy (mk_tabs thy) (read_const thy raw_const);
+    fun mk reader target thy =
       let
         val _ = get_serializer target;
-        val tabs = mk_tabs thy;
-        val c = idf_of_const thy tabs (read_const thy raw_const);
+        val c = prep_const thy raw_const;
       in
         thy
         |> ensure_prim c target
@@ -1226,7 +1209,7 @@
         |-> (fn pretty => add_pretty_syntax_const c target pretty)
       end;
   in
-    CodegenSerializer.parse_syntax (read_quote Sign.read_term codegen_term)
+    CodegenSerializer.parse_syntax (read_quote (fn thy => prep_const thy raw_const) Sign.read_term codegen_term)
     #-> (fn reader => pair (mk reader))
   end;
 
@@ -1259,7 +1242,7 @@
         fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts
       in
         thy
-        |> expand_module generate
+        |> expand_module NONE generate
         |-> (fn cs => pair (SOME cs))
       end
   | generate_code NONE thy =
@@ -1297,8 +1280,6 @@
   ("code_generate", "code_serialize",
    "code_primclass", "code_primtyco", "code_primconst",
    "code_syntax_class", "code_syntax_tyco", "code_syntax_const", "code_alias");
-val dependingK =
-  ("depending_on");
 
 val generateP =
   OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
@@ -1329,31 +1310,25 @@
 val primclassP =
   OuterSyntax.command primclassK "define target-lanugage specific class" K.thy_decl (
     P.xname
-    -- Scan.optional (P.$$$ dependingK |--
-         P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
     -- Scan.repeat1 (P.name -- P.text)
-      >> (fn ((raw_class, depends), primdefs) =>
-            (Toplevel.theory oo fold) (add_prim_class raw_class depends) primdefs)
+      >> (fn (raw_class, primdefs) =>
+            (Toplevel.theory oo fold) (add_prim_class raw_class) primdefs)
   );
 
 val primtycoP =
   OuterSyntax.command primtycoK "define target-lanugage specific type constructor" K.thy_decl (
     P.xname
-    -- Scan.optional (P.$$$ dependingK |--
-         P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
     -- Scan.repeat1 (P.name -- P.text)
-      >> (fn ((raw_tyco, depends), primdefs) =>
-            (Toplevel.theory oo fold) (add_prim_tyco raw_tyco depends) primdefs)
+      >> (fn (raw_tyco, primdefs) =>
+            (Toplevel.theory oo fold) (add_prim_tyco raw_tyco) primdefs)
   );
 
 val primconstP =
   OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl (
     (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
-    -- Scan.optional (P.$$$ dependingK |--
-         P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
     -- Scan.repeat1 (P.name -- P.text)
-      >> (fn ((raw_const, depends), primdefs) =>
-            (Toplevel.theory oo fold) (add_prim_const raw_const depends) primdefs)
+      >> (fn (raw_const, primdefs) =>
+            (Toplevel.theory oo fold) (add_prim_const raw_const) primdefs)
   );
 
 val syntax_classP =
@@ -1372,29 +1347,28 @@
   OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
     Scan.repeat1 (
       P.xname
-      -- Scan.repeat1 (
-           P.name -- parse_syntax_tyco
-         )
+      #-> (fn raw_tyco => Scan.repeat1 (
+             P.name -- parse_syntax_tyco raw_tyco
+          ))
     )
-    >> (Toplevel.theory oo fold) (fn (raw_tyco, syns) =>
-          fold (fn (target, modifier) => modifier raw_tyco target) syns)
+    >> (Toplevel.theory oo fold o fold)
+          (fn (target, modifier) => modifier target)
   );
 
 val syntax_constP =
   OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
     Scan.repeat1 (
       (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
-      -- Scan.repeat1 (
-           P.name -- parse_syntax_const
-         )
+      #-> (fn raw_const => Scan.repeat1 (
+             P.name -- parse_syntax_const raw_const
+          ))
     )
-    >> (Toplevel.theory oo fold) (fn (raw_c, syns) =>
-          fold (fn (target, modifier) => modifier raw_c target) syns)
+    >> (Toplevel.theory oo fold o fold) 
+          (fn (target, modifier) => modifier target)
   );
 
 val _ = OuterSyntax.add_parsers [generateP, serializeP, aliasP,
   primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP];
-val _ = OuterSyntax.add_keywords [dependingK];
 
 
 
diff -r d6ecc5828b14 -r 3adfc9dfb30a src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Mon Feb 06 21:02:01 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Feb 07 08:47:43 2006 +0100
@@ -20,7 +20,7 @@
       * OuterParse.token list;
   val parse_syntax: (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
     ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
-  val parse_targetdef: (string -> string) -> string -> string;
+  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),
@@ -207,18 +207,16 @@
                       | xs => xs) o explode)
   |> space_implode "\n";
 
-fun parse_named_quote resolv s =
+fun parse_targetdef s =
   case Scan.finite Symbol.stopper (Scan.repeat (
-         ($$ "`" |-- $$ "`")
+         ($$ "`" |-- $$ "`" >> (CodegenThingol.Pretty o str))
       || ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof))
-            --| $$ "`" >> (resolv o implode))
+            --| $$ "`" >> (fn ["_"] => Name | s => error ("malformed antiquote: " ^ implode s)))
       || Scan.repeat1
-           (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> implode
-    ) >> implode) (Symbol.explode s)
+           (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> (CodegenThingol.Pretty o str o implode)
+    )) (Symbol.explode s)
    of (p, []) => p
-    | (p, ss) => error ("Malformed definition: " ^ quote p ^ " - " ^ commas ss);
-
-fun parse_targetdef resolv = parse_named_quote resolv o newline_correct;
+    | (p, ss) => error ("Malformed definition: " ^ quote s ^ " - " ^ commas ss);
 
 
 (* abstract serializer *)
@@ -227,29 +225,26 @@
     string list list
     -> OuterParse.token list ->
     ((string -> string option)
-      * (string -> CodegenThingol.itype pretty_syntax option)
-      * (string -> CodegenThingol.iexpr pretty_syntax option)
+      * (string -> itype pretty_syntax option)
+      * (string -> iexpr pretty_syntax option)
     -> string list option
-    -> CodegenThingol.module -> unit)
+    -> module -> unit)
     * OuterParse.token list;
 
-fun pretty_of_prim target resolv (name, primdef) =
-  let
-    fun pr (CodegenThingol.Pretty p) = p
-      | pr (CodegenThingol.Name s) = resolv s;
-  in case AList.lookup (op = : string * string -> bool) primdef target
-   of NONE => error ("no primitive definition for " ^ quote name)
-    | SOME ps => (Pretty.block o map pr) ps
-  end;
-
 fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)
-    postprocess preprocess (class_syntax : string -> string option, tyco_syntax, const_syntax)
+    postprocess preprocess (class_syntax, tyco_syntax, const_syntax)
     select module =
   let
-    fun from_prim (name, prim) =
-      case AList.lookup (op = : string * string -> bool) prim target
+    fun pretty_of_prim resolv (name, primdef) =
+      let
+        fun pr (CodegenThingol.Pretty p) = p
+          | pr 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 p => p;
+        | SOME ps => (case map pr ps
+           of [] => NONE
+            | ps => (SOME o Pretty.block) ps)
+      end;
     fun from_module' imps ((name_qual, name), defs) =
       from_module imps ((name_qual, name), defs) |> postprocess name_qual;
   in
@@ -260,7 +255,7 @@
     |> debug 3 (fn _ => "preprocessing...")
     |> preprocess
     |> debug 3 (fn _ => "serializing...")
-    |> serialize (from_defs (from_prim, (class_syntax, tyco_syntax, const_syntax)))
+    |> serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
          from_module' validator postproc nspgrp name_root
     |> K ()
   end;
@@ -400,16 +395,17 @@
       #> NameSpace.base
       #> translate_string (fn "_" => "__" | "." => "_" | c => c)
       #> str;
-    fun ml_from_type fxy (IType (tyco, tys)) =
+    fun ml_from_tycoexpr fxy (tyco, tys) =
+      let
+        val tyco' = (str o resolv) tyco
+      in case map (ml_from_type BR) tys
+       of [] => tyco'
+        | [p] => Pretty.block [p, Pretty.brk 1, tyco']
+        | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
+      end
+    and ml_from_type fxy (IType (tycoexpr as (tyco, tys))) =
           (case tyco_syntax tyco
-           of NONE =>
-                let
-                  val tyco' = (str o resolv) tyco
-                in case map (ml_from_type BR) tys
-                 of [] => tyco'
-                  | [p] => Pretty.block [p, Pretty.brk 1, tyco']
-                  | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
-                end
+           of NONE => ml_from_tycoexpr fxy (tyco, tys)
             | SOME ((i, k), pr) =>
                 if not (i <= length tys andalso length tys <= k)
                 then error ("number of argument mismatch in customary serialization: "
@@ -563,7 +559,7 @@
         fun mk_datatype definer (t, ((vs, cs), _)) =
           (Pretty.block o Pretty.breaks) (
             str definer
-            :: ml_from_type NOBR (t `%% map IVarT vs)
+            :: ml_from_tycoexpr NOBR (t, map IVarT vs)
             :: str "="
             :: separate (str "|") (map mk_cons cs)
           )
@@ -579,13 +575,13 @@
     fun ml_from_def (name, Undef) =
           error ("empty definition during serialization: " ^ quote name)
       | ml_from_def (name, Prim prim) =
-          from_prim (name, prim)
+          from_prim resolv (name, prim)
       | ml_from_def (name, Typesyn (vs, ty)) =
         (map (fn (vname, []) => () | _ =>
             error "can't serialize sort constrained type declaration to ML") vs;
           Pretty.block [
             str "type ",
-            ml_from_type NOBR (name `%% map IVarT vs),
+            ml_from_tycoexpr NOBR (name, map IVarT vs),
             str " =",
             Pretty.brk 1,
             ml_from_type NOBR ty,
@@ -723,7 +719,7 @@
       |> debug 3 (fn _ => "eta-expanding polydefs...")
       |> eta_expand_poly
       |> debug 3 (fn _ => "unclashing expression/type variables...")
-      |> unclash_vars;
+      |> unclash_vars_tvars;
     val parse_multi =
       OuterParse.name
       #-> (fn "dir" => 
@@ -743,7 +739,7 @@
 
 local
 
-fun hs_from_defs (from_prim, (class_syntax, tyco_syntax, const_syntax))
+fun hs_from_defs with_typs (from_prim, (class_syntax, tyco_syntax, const_syntax))
     resolv defs =
   let
     fun hs_from_sctxt vs =
@@ -763,10 +759,12 @@
         |> Library.flat
         |> from_sctxt
       end;
-    fun hs_from_type fxy (IType (tyco, tys)) =
+    fun hs_from_tycoexpr fxy (tyco, tys) =
+      brackify fxy ((str o resolv) tyco :: map (hs_from_type BR) tys)
+    and hs_from_type fxy (IType (tycoexpr as (tyco, tys))) =
           (case tyco_syntax tyco
            of NONE =>
-                brackify fxy ((str o resolv) tyco :: map (hs_from_type BR) tys)
+                hs_from_tycoexpr fxy tycoexpr
             | SOME ((i, k), pr) =>
                 if not (i <= length tys andalso length tys <= k)
                 then error ("number of argument mismatch in customary serialization: "
@@ -782,6 +780,8 @@
           ]
       | hs_from_type fxy (IVarT (v, _)) =
           str v;
+    fun hs_from_sctxt_tycoexpr (sctxt, tycoexpr) =
+      Pretty.block [hs_from_sctxt sctxt, hs_from_tycoexpr NOBR tycoexpr]
     fun hs_from_sctxt_type (sctxt, ty) =
       Pretty.block [hs_from_sctxt sctxt, hs_from_type NOBR ty]
     fun hs_from_expr fxy (e as IApp (e1, e2)) =
@@ -857,20 +857,24 @@
     fun hs_from_def (name, Undef) =
           error ("empty statement during serialization: " ^ quote name)
       | hs_from_def (name, Prim prim) =
-          from_prim (name, prim)
+          from_prim resolv (name, prim)
       | hs_from_def (name, Fun (eqs, (sctxt, ty))) =
-          Pretty.chunks [
-            Pretty.block [
-              (str o suffix " ::" o resolv) name,
-              Pretty.brk 1,
-              hs_from_sctxt_type (sctxt, ty)
-            ],
-            hs_from_funeqs (name, eqs)
-          ] |> SOME
+          let
+            val body = hs_from_funeqs (name, eqs);
+          in if with_typs then
+            Pretty.chunks [
+              Pretty.block [
+                (str o suffix " ::" o resolv) name,
+                Pretty.brk 1,
+                hs_from_sctxt_type (sctxt, ty)
+              ],
+              body
+            ] |> SOME
+          else SOME body end
       | hs_from_def (name, Typesyn (vs, ty)) =
           Pretty.block [
             str "type ",
-            hs_from_sctxt_type (vs, CodegenThingol.IType (name, map CodegenThingol.IVarT vs)),
+            hs_from_sctxt_tycoexpr (vs, (name, map IVarT vs)),
             str " =",
             Pretty.brk 1,
             hs_from_sctxt_type ([], ty)
@@ -885,7 +889,7 @@
           in
             Pretty.block ((
               str "data "
-              :: hs_from_sctxt_type (vs, CodegenThingol.IType (name, map CodegenThingol.IVarT vs))
+              :: hs_from_sctxt_type (vs, IType (name, map IVarT vs))
               :: str " ="
               :: Pretty.brk 1
               :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
@@ -919,9 +923,9 @@
       | hs_from_def (_, Classinst (((clsname, (tyco, arity)), _), memdefs)) = 
           Pretty.block [
             str "instance ",
-            hs_from_sctxt_type (arity, IType (clsname, map (IVarT o rpair [] o fst) arity)),
+            hs_from_sctxt_tycoexpr (arity, (clsname, map (IVarT o rpair [] o fst) arity)),
             str " ",
-            hs_from_sctxt_type (arity, IType (tyco, map (IVarT o rpair [] o fst) arity)),
+            hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o rpair [] o fst) arity)),
             str " where",
             Pretty.fbrk,
             Pretty.chunks (map (fn (m, (eqs, _)) => hs_from_funeqs (m, eqs)) memdefs)
@@ -946,7 +950,7 @@
     fun hs_from_module imps ((_, name), ps) =
       (Pretty.block o Pretty.fbreaks) (
           str ("module " ^ name ^ " where")
-      :: map (str o prefix "import ") imps @ [
+      :: map (str o prefix "import qualified ") imps @ [
           str "",
           Pretty.chunks (separate (str "") ps)
       ]);
@@ -957,8 +961,8 @@
         then ch_first Char.toUpper n
         else ch_first Char.toLower n
       end;
-    val serializer = abstract_serializer (target, nspgrp)
-      "Main" (hs_from_defs, hs_from_module, abstract_validator reserved_hs, postproc);
+    fun serializer with_typs = abstract_serializer (target, nspgrp)
+      "Main" (hs_from_defs with_typs, hs_from_module, abstract_validator reserved_hs, postproc);
     fun eta_expander const_syntax c =
       const_syntax c
       |> Option.map (fst o fst)
@@ -967,10 +971,11 @@
       module
       |> tap (Pretty.writeln o pretty_deps)
       |> debug 3 (fn _ => "eta-expanding...")
-      |> eta_expand (eta_expander const_syntax);
+      |> eta_expand (eta_expander const_syntax)
   in
-    parse_multi_file ((K o K) NONE) "hs" serializer
-    >> (fn seri => fn (class_syntax, tyco_syntax, const_syntax) => seri 
+    (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
+    #-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs)))
+    >> (fn (seri) => fn (class_syntax, tyco_syntax, const_syntax) => seri 
          (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax))
   end;
 
diff -r d6ecc5828b14 -r 3adfc9dfb30a src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Mon Feb 06 21:02:01 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Tue Feb 07 08:47:43 2006 +0100
@@ -47,10 +47,10 @@
   type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
   datatype prim =
       Pretty of Pretty.T
-    | Name of string;
+    | Name;
   datatype def =
       Undef
-    | Prim of (string * Pretty.T option) list
+    | Prim of (string * prim list) list
     | Fun of funn
     | Typesyn of (vname * string list) list * itype
     | Datatype of ((vname * string list) list * (string * itype list) list)
@@ -70,7 +70,7 @@
   val pretty_module: module -> Pretty.T; 
   val pretty_deps: module -> Pretty.T;
   val empty_module: module;
-  val add_prim: string -> string list -> (string * Pretty.T) -> module -> module;
+  val add_prim: string -> (string * prim list) -> module -> module;
   val ensure_prim: string -> string -> module -> module;
   val get_def: module -> string -> def;
   val merge_module: module * module -> module;
@@ -80,11 +80,11 @@
   val fail: string -> transact -> 'a transact_fin;
   val gen_ensure_def: (string * gen_defgen) list -> string
     -> string -> transact -> transact;
-  val start_transact: (transact -> 'a * transact) -> module -> 'a * module;
+  val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
 
   val eta_expand: (string -> int) -> module -> module;
   val eta_expand_poly: module -> module;
-  val unclash_vars: module -> module;
+  val unclash_vars_tvars: module -> module;
 
   val debug_level: int ref;
   val debug: int -> ('a -> string) -> 'a -> 'a;
@@ -417,11 +417,11 @@
 
 datatype prim =
     Pretty of Pretty.T
-  | Name of string;
+  | Name;
 
 datatype def =
     Undef
-  | Prim of (string * Pretty.T option) list
+  | Prim of (string * prim list) list
   | Fun of funn
   | Typesyn of (vname * string list) list * itype
   | Datatype of ((vname * string list) list * (string * itype list) list)
@@ -660,14 +660,14 @@
             then module
             else error ("tried to overwrite definition " ^ name));
 
-fun add_prim name deps (target, primdef) =
+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, SOME primdef)])
+                |> 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
@@ -675,16 +675,13 @@
                 else
                   module
                   |> Graph.map_node base ((K o Def o Prim) (AList.update (op =)
-                       (target, SOME primdef) prim))
+                       (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
-    #> fold (curry add_dep name) deps
-  end;
+  in add modl end;
 
 fun ensure_prim name target =
   let
@@ -693,11 +690,11 @@
           (case try (Graph.get_node module) base
            of NONE =>
                 module
-                |> Graph.new_node (base, (Def o Prim) [(target, NONE)])
+                |> 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, NONE) prim))
+                     (target, []) prim))
             | _ => module)
       | ensure (m::ms) module =
           module
@@ -908,16 +905,16 @@
     |> pair dep
   end;
 
-fun start_transact f modl =
+fun start_transact init f modl =
   let
-    fun handle_fail f modl =
-      (((NONE, modl) |> f)
+    fun handle_fail f x =
+      (f x
       handle FAIL (msgs, NONE) =>
         (error o cat_lines) ("code generation failed, while:" :: msgs))
       handle FAIL (msgs, SOME e) =>
         ((writeln o cat_lines) ("code generation failed, while:" :: msgs); raise e);
   in
-    modl
+    (init, modl)
     |> handle_fail f
     |-> (fn x => fn (_, module) => (x, module))
   end;
@@ -966,7 +963,7 @@
       | eta funn = funn;
   in (map_defs o map_def_fun) eta end;
 
-val unclash_vars = 
+val unclash_vars_tvars = 
   let
     fun unclash (eqs, (sortctxt, ty)) =
       let
@@ -986,7 +983,6 @@
   in (map_defs o map_def_fun) unclash end;
 
 
-
 (** generic serialization **)
 
 (* resolving *)
@@ -995,22 +991,25 @@
   type ctxt = (string * string -> string) * (string -> string option);
   type src = string * string;
   val ord = prod_ord string_ord string_ord;
-  fun mk (preprocess, validate) ((shallow, name), 0) =
-        (case validate (preprocess (shallow, name))
-         of NONE => name
-          | _ => mk (preprocess, validate) ((shallow, name), 1))
-    | mk (preprocess, validate) (("", name), i) =
-        preprocess ("", name ^ "_" ^ string_of_int (i+1))
+  fun mk (postprocess, validate) ((shallow, name), 0) =
+        let
+          val name' = postprocess (shallow, name);
+        in case validate name'
+         of NONE => name'
+          | _ => mk (postprocess, validate) ((shallow, name), 1)
+        end
+    | mk (postprocess, validate) (("", name), i) =
+        postprocess ("", name ^ "_" ^ string_of_int (i+1))
         |> perhaps validate
-    | mk (preprocess, validate) ((shallow, name), i) =
-        preprocess (shallow, shallow ^ "_" ^ name ^ "_" ^ string_of_int (i+1))
+    | mk (postprocess, validate) ((shallow, name), i) =
+        postprocess (shallow, shallow ^ "_" ^ name ^ "_" ^ string_of_int (i+1))
         |> perhaps validate;
   fun is_valid _ _ = true;
   fun maybe_unique _ _ = NONE;
   fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
 );
 
-fun mk_deresolver module nsp_conn preprocess validate =
+fun mk_deresolver module nsp_conn postprocess validate =
   let
     datatype tabnode = N of string * tabnode Symtab.table option;
     fun mk module manglers tab =
@@ -1024,12 +1023,11 @@
         fun add_name name =
           let
             val n as (shallow, _) = mk_name name;
-            fun diag (nm as (name, n')) = (writeln ("resolving " ^ quote name ^ " to " ^ quote n'); nm);
           in
             AList.map_entry_yield in_conn shallow (
-              NameMangler.declare (preprocess, validate) n
+              NameMangler.declare (postprocess, validate) n
               #-> (fn n' => pair (name, n'))
-            ) #> apfst the #> apfst diag
+            ) #> apfst the
           end;
         val (renamings, manglers') =
           fold_map add_name (Graph.keys module) manglers;
@@ -1075,9 +1073,9 @@
 
 (* serialization *)
 
-fun serialize seri_defs seri_module validate preprocess nsp_conn name_root module =
+fun serialize seri_defs seri_module validate postprocess nsp_conn name_root module =
   let
-    val resolver = mk_deresolver module nsp_conn preprocess validate;
+    val resolver = mk_deresolver module nsp_conn postprocess validate;
     fun mk_name prfx name =
       let
         val name_qual = NameSpace.pack (prfx @ [name])