minor refinements in serialization

--- a/src/Pure/Tools/codegen_package.ML	Wed Oct 11 14:51:41 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Wed Oct 11 20:35:54 2006 +0200
@@ -417,10 +417,31 @@
 fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns =
   let
     val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
-    fun clausegen (dt, bt) trns =
-      trns
-      |> exprgen_term thy algbr funcgr strct dt
-      ||>> exprgen_term thy algbr funcgr strct bt;
+    fun fold_map_aterms f (t $ u) s =
+          s
+          |> fold_map_aterms f t
+          ||>> fold_map_aterms f u
+          |-> (fn (t1, t2) => pair (t1 $ t2))
+      | fold_map_aterms f (Abs (v, ty, t)) s =
+          s
+          |> fold_map_aterms f t
+          |-> (fn t' => pair (Abs (v, ty, t')))
+      | fold_map_aterms f a s = f a s;
+    fun purify_term_frees (Free (v, ty)) ctxt = 
+          let
+            val ([v'], ctxt') = Name.variants [CodegenNames.purify_var v] ctxt;
+          in (Free (v, ty), ctxt') end
+      | purify_term_frees t ctxt = (t, ctxt);
+    fun clausegen (raw_dt, raw_bt) trns =
+      let
+        val ((dt, bt), _) = Name.context
+          |> fold_map_aterms purify_term_frees raw_dt
+          ||>> fold_map_aterms purify_term_frees raw_bt;
+      in
+        trns
+        |> exprgen_term thy algbr funcgr strct dt
+        ||>> exprgen_term thy algbr funcgr strct bt
+      end;
   in
     trns
     |> exprgen_term thy algbr funcgr strct st

--- a/src/Pure/Tools/codegen_serializer.ML	Wed Oct 11 14:51:41 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Oct 11 20:35:54 2006 +0200
@@ -76,16 +76,16 @@
 fun brackify_infix infx fxy_ctxt ps =
   gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
 
-fun mk_app mk_app' from_expr const_syntax fxy (const as (c, (_, ty)), es) =
+fun mk_app mk_app' from_expr const_syntax fxy (app as ((c, (_, ty)), ts)) =
   case const_syntax c
-   of NONE => brackify fxy (mk_app' c es)
+   of NONE => brackify fxy (mk_app' app)
     | SOME (i, pr) =>
         let
           val k = if i < 0 then (length o fst o CodegenThingol.unfold_fun) ty else i
-        in if k <= length es
-          then case chop i es of (es1, es2) =>
-            brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
-          else from_expr fxy (CodegenThingol.eta_expand (const, es) i)
+        in if k <= length ts
+          then case chop i ts of (ts1, ts2) =>
+            brackify fxy (pr fxy from_expr ts1 :: map (from_expr BR) ts2)
+          else from_expr fxy (CodegenThingol.eta_expand app k)
         end;
 
 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
@@ -353,15 +353,19 @@
           (case CodegenThingol.unfold_const_app t
            of SOME c_ts => pr_app vars fxy c_ts
             | NONE =>
-                brackify fxy [pr_term vars NOBR t1, pr_term vars BR t2 ])
+                brackify fxy [pr_term vars NOBR t1, pr_term vars BR t2])
       | pr_term vars fxy (t as _ `|-> _) =
           let
             val (ts, t') = CodegenThingol.unfold_abs t;
-            val vs = fold (CodegenThingol.fold_varnames (insert (op =)) o fst) ts [];
-            val vars' = intro_vars vs vars;
-            fun mk_abs (t, ty) = (Pretty.block o Pretty.breaks)
-              [str "fn", pr_term vars' NOBR t, str "=>"];
-          in brackify BR (map mk_abs ts @ [pr_term vars' NOBR t']) end
+            fun pr (p, _) vars =
+              let
+                val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
+                val vars' = intro_vars vs vars;
+              in
+                ((Pretty.block o Pretty.breaks) [str "fn", pr_term vars' NOBR p, str "=>"], vars')
+              end;
+            val (ps, vars') = fold_map pr ts vars;
+          in brackify BR (ps @ [pr_term vars' NOBR t']) end
       | pr_term vars fxy (INum (n, _)) =
           brackify BR [(str o IntInf.toString) n, str ":", str "IntInf.int"]
       | pr_term vars _ (IChar (c, _)) =
@@ -373,8 +377,8 @@
               end)
       | pr_term vars fxy (t as ICase ((_, [_]), _)) =
           let
-            val (ts, t) = CodegenThingol.unfold_let t;
-            fun mk ((p, _), t) vars =
+            val (ts, t') = CodegenThingol.unfold_let t;
+            fun mk ((p, _), t'') vars =
               let
                 val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
                 val vars' = intro_vars vs vars;
@@ -384,7 +388,7 @@
                     str "val",
                     pr_term vars' NOBR p,
                     str "=",
-                    pr_term vars NOBR t
+                    pr_term vars NOBR t''
                   ],
                   str ";"
                 ], vars')
@@ -393,7 +397,7 @@
           in
             Pretty.chunks [
               [str ("let"), Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block,
-              [str ("in"), Pretty.fbrk, pr_term vars' NOBR t] |> Pretty.block,
+              [str ("in"), Pretty.fbrk, pr_term vars' NOBR t'] |> Pretty.block,
               str ("end")
             ] end
       | pr_term vars fxy (ICase (((td, ty), b::bs), _)) =
@@ -418,15 +422,15 @@
               :: map (pr "|") bs
             )
           end
-    and pr_app' vars c ts =
-      let
-        val p = (str o deresolv) c;
-        val ps = map (pr_term vars BR) ts;
-      in if is_cons c andalso length ts > 1 then
-        [p, Pretty.enum "," "(" ")" ps]
-      else
-        p :: ps
-      end
+    and pr_app' vars (app as ((c, (iss, ty)), ts)) =
+      if is_cons c then let
+        val k = (length o fst o CodegenThingol.unfold_fun) ty
+      in if k < 2 then 
+        (str o deresolv) c :: map (pr_term vars BR) ts
+      else if k = length ts then
+        [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
+      else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
+        (str o deresolv) c :: map (pr_term vars BR) ts
     and pr_app vars fxy (app as ((c, (iss, ty)), ts)) =
       case if is_cons c then [] else (map (pr_insts BR) o filter_out null) iss
        of [] =>
@@ -648,12 +652,16 @@
       | pr_term vars fxy (t as _ `|-> _) =
           let
             val (ts, t') = CodegenThingol.unfold_abs t;
-            val vs = fold (CodegenThingol.fold_varnames (insert (op =)) o fst) ts [];
-            val vars' = intro_vars vs vars;
+            fun pr (p, _) vars =
+              let
+                val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
+                val vars' = intro_vars vs vars;
+              in (pr_term vars' BR p, vars') end;
+            val (ps, vars') = fold_map pr ts vars;
           in
             brackify BR (
               str "\\"
-              :: map (pr_term vars' BR o fst) ts @ [
+              :: ps @ [
               str "->",
               pr_term vars' NOBR t'
             ])
@@ -710,7 +718,7 @@
               (Pretty.chunks o map pr) bs
             ]
           end
-    and pr_app' vars c ts =
+    and pr_app' vars ((c, _), ts) =
       (str o deresolv) c :: map (pr_term vars BR) ts
     and pr_app vars fxy =
       mk_app (pr_app' vars) (pr_term vars) const_syntax fxy;

--- a/src/Pure/Tools/codegen_thingol.ML	Wed Oct 11 14:51:41 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Oct 11 20:35:54 2006 +0200
@@ -174,8 +174,8 @@
     | _ => NONE);
 
 val unfold_abs = unfoldr
-  (fn (v, ty) `|-> (e as ICase (((IVar w, _), [(p, t)]), _)) =>
-        if v = w then SOME ((p, ty), t) else SOME ((IVar v, ty), t)
+  (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
+        if v = w then SOME ((p, ty), t') else SOME ((IVar v, ty), t)
     | (v, ty) `|-> t => SOME ((IVar v, ty), t)
     | _ => NONE)