syntactic improvements and tuning names in the code generator due to Florian's code review

--- a/src/Tools/Code/code_haskell.ML	Tue Sep 20 01:32:04 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Sep 20 09:30:19 2011 +0200
@@ -85,13 +85,16 @@
                 then print_case tyvars some_thm vars fxy cases
                 else print_app tyvars some_thm vars fxy c_ts
             | NONE => print_case tyvars some_thm vars fxy cases)
-    and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, body_typ)), annotate)), ts) =
+    and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
       let
-        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ)
-        fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty]
+        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
+        val printed_const =
+          if annotate then
+            brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
+          else
+            (str o deresolve) c
       in 
-        ((if annotate then put_annotation else I)
-          ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts
+        printed_const :: map (print_term tyvars some_thm vars BR) ts
       end
     and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
     and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
@@ -234,15 +237,16 @@
                     ]
                 | SOME k =>
                     let
-                      val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *)
+                      val (c, ((_, tys), _)) = const;
                       val (vs, rhs) = (apfst o map) fst
                         (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
                       val s = if (is_some o const_syntax) c
                         then NONE else (SOME o Long_Name.base_name o deresolve) c;
                       val vars = reserved
                         |> intro_vars (map_filter I (s :: vs));
-                      val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs;
-                        (*dictionaries are not relevant at this late stage*)
+                      val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
+                        (*dictionaries are not relevant at this late stage,
+                          and these consts never need type annotations for disambiguation *)
                     in
                       semicolon [
                         print_term tyvars (SOME thm) vars NOBR lhs,
@@ -323,8 +327,7 @@
       in deriv [] tyco end;
     fun print_stmt deresolve = print_haskell_stmt labelled_name
       class_syntax tyco_syntax const_syntax (make_vars reserved)
-      deresolve
-      (if string_classes then deriving_show else K false);
+      deresolve (if string_classes then deriving_show else K false);
 
     (* print modules *)
     val import_includes_ps =

--- a/src/Tools/Code/code_ml.ML	Tue Sep 20 01:32:04 2011 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Sep 20 09:30:19 2011 +0200
@@ -117,9 +117,9 @@
                 then print_case is_pseudo_fun some_thm vars fxy cases
                 else print_app is_pseudo_fun some_thm vars fxy c_ts
             | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
-    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (function_typs, _)), _)), ts)) =
+    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (arg_tys, _)), _)), ts)) =
       if is_cons c then
-        let val k = length function_typs in
+        let val k = length arg_tys in
           if k < 2 orelse length ts = k
           then (str o deresolve) c
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)

--- a/src/Tools/Code/code_printer.ML	Tue Sep 20 01:32:04 2011 +0200
+++ b/src/Tools/Code/code_printer.ML	Tue Sep 20 09:30:19 2011 +0200
@@ -315,7 +315,7 @@
       |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
 
 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
-    (app as ((c, ((_, (function_typs, _)), _)), ts)) =
+    (app as ((c, ((_, (arg_tys, _)), _)), ts)) =
   case const_syntax c of
     NONE => brackify fxy (print_app_expr some_thm vars app)
   | SOME (Plain_const_syntax (_, s)) =>
@@ -323,7 +323,7 @@
   | SOME (Complex_const_syntax (k, print)) =>
       let
         fun print' fxy ts =
-          print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
+          print (print_term some_thm) some_thm vars fxy (ts ~~ take k arg_tys);
       in
         if k = length ts
         then print' fxy ts

--- a/src/Tools/Code/code_scala.ML	Tue Sep 20 01:32:04 2011 +0200
+++ b/src/Tools/Code/code_scala.ML	Tue Sep 20 09:30:19 2011 +0200
@@ -72,23 +72,23 @@
                 else print_app tyvars is_pat some_thm vars fxy c_ts
             | NONE => print_case tyvars some_thm vars fxy cases)
     and print_app tyvars is_pat some_thm vars fxy
-        (app as ((c, (((arg_typs, _), (function_typs, _)), _)), ts)) =
+        (app as ((c, (((tys, _), (arg_tys, _)), _)), ts)) =
       let
         val k = length ts;
-        val arg_typs' = if is_pat orelse
-          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else arg_typs;
+        val tys' = if is_pat orelse
+          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else tys;
         val (l, print') = case const_syntax c
          of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
-                  NOBR ((str o deresolve) c) arg_typs') ts)
+                  NOBR ((str o deresolve) c) tys') ts)
           | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
-                  NOBR (str s) arg_typs') ts)
+                  NOBR (str s) tys') ts)
           | SOME (Complex_const_syntax (k, print)) =>
               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
-                (ts ~~ take k function_typs))
+                (ts ~~ take k arg_tys))
       in if k = l then print' fxy ts
       else if k < l then
         print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)

--- a/src/Tools/Code/code_thingol.ML	Tue Sep 20 01:32:04 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Sep 20 09:30:19 2011 +0200
@@ -23,7 +23,7 @@
       `%% of string * itype list
     | ITyVar of vname;
   type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
-    (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
+    (* (f [T1..Tn] {dicts} (_::S1) .. (_::Sm)) :: S =^= (f, ((([T1..Tn], dicts), ([S1..Sm], S)), ambiguous)) *)
   datatype iterm =
       IConst of const
     | IVar of vname option
@@ -144,7 +144,7 @@
   | ITyVar of vname;
 
 type const = string * (((itype list * dict list list) *
-  (itype list (*types of arguments*) * itype (*body type*))) * bool (*requires type annotation*))
+  (itype list (*types of arguments*) * itype (*result type*))) * bool (*requires type annotation*))
 
 datatype iterm =
     IConst of const