changing const type to pass along if typing annotations are necessary for disambigous terms

--- a/src/Tools/Code/code_haskell.ML	Wed Sep 07 11:36:39 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML	Wed Sep 07 13:51:30 2011 +0200
@@ -75,7 +75,7 @@
                 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)), ts) = case contr_classparam_typs c
+    and print_app_expr tyvars some_thm vars ((c, ((_, function_typs), _)), ts) = case contr_classparam_typs c
      of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
       | fingerprint => let
           val ts_fingerprint = ts ~~ take (length ts) fingerprint;
@@ -230,14 +230,14 @@
                     ]
                 | SOME k =>
                     let
-                      val (c, (_, tys)) = const;
+                      val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *)
                       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)) `$$ map IVar vs;
+                      val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs;
                         (*dictionaries are not relevant at this late stage*)
                     in
                       semicolon [

--- a/src/Tools/Code/code_ml.ML	Wed Sep 07 11:36:39 2011 +0200
+++ b/src/Tools/Code/code_ml.ML	Wed Sep 07 13:51:30 2011 +0200
@@ -117,7 +117,7 @@
                 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), function_typs), _)), ts)) =
       if is_cons c then
         let val k = length function_typs in
           if k < 2 orelse length ts = k
@@ -417,7 +417,7 @@
                 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), tys)), ts)) =
+    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), tys), _)), ts)) =
       if is_cons c then
         let val k = length tys in
           if length ts = k

--- a/src/Tools/Code/code_printer.ML	Wed Sep 07 11:36:39 2011 +0200
+++ b/src/Tools/Code/code_printer.ML	Wed Sep 07 13:51:30 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, ((_, function_typs), _)), ts)) =
   case const_syntax c of
     NONE => brackify fxy (print_app_expr some_thm vars app)
   | SOME (Plain_const_syntax (_, s)) =>

--- a/src/Tools/Code/code_scala.ML	Wed Sep 07 11:36:39 2011 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Sep 07 13:51:30 2011 +0200
@@ -72,7 +72,7 @@
                 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, (((arg_typs, _), function_typs), _)), ts)) =
       let
         val k = length ts;
         val arg_typs' = if is_pat orelse
@@ -265,7 +265,7 @@
           let
             val tyvars = intro_tyvars vs reserved;
             val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
-            fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
+            fun print_classparam_instance ((classparam, const as (_, ((_, tys), _))), (thm, _)) =
               let
                 val aux_tys = Name.invent_names (snd reserved) "a" tys;
                 val auxs = map fst aux_tys;

--- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 11:36:39 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:30 2011 +0200
@@ -22,7 +22,7 @@
   datatype itype =
       `%% of string * itype list
     | ITyVar of vname;
-  type const = string * ((itype list * dict list list) * itype list)
+  type const = string * (((itype list * dict list list) * itype list) * bool)
     (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
   datatype iterm =
       IConst of const
@@ -145,7 +145,8 @@
     `%% of string * itype list
   | ITyVar of vname;
 
-type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
+type const = string * (((itype list * dict list list) * itype list (*types of arguments*))
+  * bool (*requires type annotation*))
 
 datatype iterm =
     IConst of const
@@ -198,7 +199,7 @@
 fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
   | add_tycos (ITyVar _) = I;
 
-val add_tyconames = fold_constexprs (fn (_, ((tys, _), _)) => fold add_tycos tys);
+val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
 
 fun fold_varnames f =
   let
@@ -240,7 +241,7 @@
         val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
       in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
 
-fun eta_expand k (c as (name, (_, tys)), ts) =
+fun eta_expand k (c as (name, ((_, tys), _)), ts) =
   let
     val j = length ts;
     val l = k - j;
@@ -256,7 +257,7 @@
     fun cont_dict (Dict (_, d)) = cont_plain_dict d
     and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
       | cont_plain_dict (Dict_Var _) = true;
-    fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss
+    fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
       | cont_term (IVar _) = false
       | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
       | cont_term (_ `|=> t) = cont_term t
@@ -756,7 +757,8 @@
     ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
     ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
     ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
-    #>> (fn (((c, arg_typs), dss), function_typs) => IConst (c, ((arg_typs, dss), function_typs)))
+    #>> (fn (((c, arg_typs), dss), function_typs) =>
+      IConst (c, (((arg_typs, dss), function_typs), false))) (* FIXME *)
   end
 and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
   translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
@@ -801,7 +803,7 @@
         val ts_clause = nth_drop t_pos ts;
         val clauses = if null case_pats
           then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
-          else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
+          else maps (fn ((constr as IConst (_, ((_, tys), _)), n), t) =>
             mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
               (constrs ~~ ts_clause);
       in ((t, ty), clauses) end;

--- a/src/Tools/nbe.ML	Wed Sep 07 11:36:39 2011 +0200
+++ b/src/Tools/nbe.ML	Wed Sep 07 13:51:30 2011 +0200
@@ -315,7 +315,7 @@
           let
             val (t', ts) = Code_Thingol.unfold_app t
           in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
-        and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
+        and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
           | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
           | of_iapp match_cont ((v, _) `|=> t) ts =
               nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
@@ -425,7 +425,7 @@
         val params = Name.invent Name.context "d" (length names);
         fun mk (k, name) =
           (name, ([(v, [])],
-            [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
+            [([IConst (class, ((([], []), []), false)) `$$ map (IVar o SOME) params],
               IVar (SOME (nth params k)))]));
       in map_index mk names end
   | eqns_of_stmt (_, Code_Thingol.Classrel _) =
@@ -433,8 +433,8 @@
   | eqns_of_stmt (_, Code_Thingol.Classparam _) =
       []
   | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
-      [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
-        map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
+      [(inst, (arity_args, [([], IConst (class, ((([], []), []), false)) `$$
+        map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), []), false))) super_instances
         @ map (IConst o snd o fst) classparam_instances)]))];