# HG changeset patch
# User bulwahn
# Date 1306756680 -7200
# Node ID c62bed03fbce3cd70992bc6614c50d6656345ece
# Parent  26774ccb1c7434be076776999be6fa3625ec15cc
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of

diff -r 26774ccb1c74 -r c62bed03fbce src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon May 30 13:57:59 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon May 30 13:58:00 2011 +0200
@@ -476,8 +476,15 @@
 fun is_case (Fun (_, (_, SOME _))) = true
   | is_case _ = false;
 
-fun contr_classparam_typs program name = case Graph.get_node program name
- of Classparam (_, class) => let
+fun lookup_classparam_instance program name = program |> Graph.get_first
+  (fn (_, (Classinst ((class, _), (_, (param_insts, _))), _)) =>
+    Option.map (fn ((const, _), _) => (class, const))
+      (find_first (fn ((_, (inst_const, _)), _) => inst_const = name) param_insts) | _ => NONE)
+
+fun contr_classparam_typs program name = 
+  let
+    fun contr_classparam_typs' (class, name) =
+      let
         val Class (_, (_, (_, params))) = Graph.get_node program class;
         val SOME ty = AList.lookup (op =) params name;
         val (tys, res_ty) = unfold_fun ty;
@@ -487,8 +494,15 @@
         then map (fn ty => if no_tyvar ty then NONE else SOME ty) tys
         else []
       end
-  | _ => [];
-
+ in 
+   case Graph.get_node program name
+   of Classparam (_, class) => contr_classparam_typs' (class, name)
+    | Fun (c, _) => (case lookup_classparam_instance program name
+      of NONE => []
+       | SOME (class, name) => the_default [] (try contr_classparam_typs' (class, name)))
+    | _ => []
+  end;
+  
 fun labelled_name thy program name =
   let val ctxt = Proof_Context.init_global thy in
     case Graph.get_node program name of