# HG changeset patch
# Parent f653343d16ba8595910d5275e1bc460069aac216
debug printing

diff -r f653343d16ba src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Fri Nov 21 19:58:22 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML	Sat Nov 22 21:00:16 2014 +0100
@@ -62,7 +62,7 @@
 structure Overload_Data = Generic_Data
 (
   type T =
-    {variants : (term * typ) list Symtab.table,
+    {variants : (term * typ) list Symtab.table, (*store type to avoid repeated "fastyp_of"*)
      oconsts : string Termtab.table};
   val empty = {variants = Symtab.empty, oconsts = Termtab.empty};
   val extend = I;
@@ -92,6 +92,8 @@
   if is_overloaded (Context.proof_of context) oconst then context
   else map_tables (Symtab.update (oconst, [])) I context;
 
+val untype = map_types (K dummyT)
+
 fun generic_remove_overloaded oconst context =
   let
     fun remove_oconst_and_variants context oconst =
@@ -99,7 +101,7 @@
         val remove_variants =
           (case get_variants (Context.proof_of context) oconst of
             NONE => I
-          | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs);
+          | SOME vs => fold (Termtab.remove (op =) o rpair oconst o untype o fst) vs);
       in map_tables (Symtab.delete_safe oconst) remove_variants context end;
   in
     if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst
@@ -112,7 +114,7 @@
       val ctxt = Context.proof_of context;
       val _ = if is_overloaded ctxt oconst then () else err_not_overloaded oconst;
       val T = t |> fastype_of;
-      val t' = Term.map_types (K dummyT) t;
+      val t' = untype t;
     in
       if add then
         let
@@ -121,15 +123,15 @@
               NONE => ()
             | SOME oconst' => err_duplicate_variant oconst');
         in
-          map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t', oconst)) context
+          map_tables (Symtab.cons_list (oconst, (t, T))) (Termtab.update (t', oconst)) context
         end
       else
         let
           val _ =
-            if member variants_eq (the (get_variants ctxt oconst)) (t', T) then ()
+            if member variants_eq (the (get_variants ctxt oconst)) (t, T) then ()
             else err_not_a_variant oconst;
         in
-          map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T)))
+          map_tables (Symtab.map_entry oconst (remove1 variants_eq (t, T)))
             (Termtab.delete_safe t') context
           |> (fn context =>
             (case get_variants (Context.proof_of context) oconst of
@@ -147,16 +149,25 @@
 
 fun unifiable_with thy T1 T2 =
   let
+    val _ = writeln ("oconst type: " ^ Syntax.string_of_typ (Proof_Context.init_global thy) T1)
+    val _ = writeln ("variant type: " ^ Syntax.string_of_typ (Proof_Context.init_global thy) T2)
     val maxidx1 = Term.maxidx_of_typ T1;
-    val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
-    val maxidx2 = Term.maxidx_typ T2' maxidx1;
-  in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end;
+    (*val T1' = Logic.incr_tvar (maxidx2 + 1) T1;*)
+    val maxidx2 = Term.maxidx_typ T2 maxidx1;
+  in try (Sign.typ_unify thy (T1, T2)) (Vartab.empty, maxidx2) end;
 
 fun get_candidates ctxt (c, T) =
   get_variants ctxt c
   |> Option.map (map_filter (fn (t, T') =>
-    if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t
-    else NONE));
+    (case unifiable_with (Proof_Context.theory_of ctxt) T T' of
+      SOME (tyenv, _) =>
+        let
+          val _ = @{print} ("unifier:", tyenv);
+          val t' = Envir.subst_term_types tyenv t
+          val _ = @{print} ("candidate term:", t)
+          val _ = @{print} ("after unification:", t')
+       in SOME t' end
+    | NONE => NONE)));
 
 fun insert_variants ctxt t (oconst as Const (c, T)) =
       (case get_candidates ctxt (c, T) of