[isabelle-dev] adhoc overloading

[Christian Sternagel]

Dear Makarius,

thanks for applying the patch. Here are two follow-up patches (this time 
generated by "hg export") that improve error messages for multiple 
instances (actually showing the existing instances to the user).

cheers

chris

@all: please let me know, in case anybody finds localized ad-hoc 
overloading useful.

An aside: I'm currently using localized ad-hoc overloading for a port of 
Nominal2's permutation type, where I use locales instead of type 
classes. The reason is that, if I understand correctly, when using 
Nominal datatypes I loose code generation... is that still true for 
Nominal2? For an existing term datatype of IsaFoR I want to have notions 
of "supports/set of variables" and "freshness". That is my intended 
application of the above mentioned port, to be found at

   https://bitbucket.org/csternagel/permutations

On 07/13/2013 12:00 AM, Makarius wrote:
> On Fri, 12 Jul 2013, Christian Sternagel wrote:
>
>> The patches should be ready to push (for your convenience I attached
>> them once more; the attached patches are the same as from my previous
>> e-mail). Btw, I generated the patches against Isabelle 8afb396d9178
>> and AFP 908304753f7d (but I guess this information is also included in
>> the patches ;)).
>
> This is now Isabelle/e0ff1625e96d and AFP/74746c992248.  Since you did
> not provide formal changesets, only diffs, I invented some log messages
> on the spot.  (Normally I use the "hg export" / "hg import" pair for
> small-scale patch-flow, but "hg import" was happy importing plain diffs
> like this.)
>
> I added Isabelle/fee0db8cf60d to keep the generated Proof General
> keyword tables in sync.  This is now trivial with the "isabelle
> update_keywords" tool in its fully static version.  (In the past there
> was always a full build required before applying it, or a good guess
> which sessions contribute to the keyword tables.)
>
>
>      Makarius

-------------- next part --------------
# HG changeset patch
# User Christian Sternagel
# Date 1374031154 -32400
#      Wed Jul 17 12:19:14 2013 +0900
# Node ID bfd42890e3b7bd6c475460023bcddb8723f19247
# Parent  c16f35e5a5aa3861a5f94dc1230d8859363de879
refactoring

diff -r c16f35e5a5aa -r bfd42890e3b7 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Tue Jul 16 23:34:33 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML	Wed Jul 17 12:19:14 2013 +0900
@@ -137,9 +137,12 @@
     handle Type.TUNIFY => NONE
   end;
 
+fun get_instances ctxt (c, T) =
+  Same.function (get_variants ctxt) c
+  |> map_filter (unifiable_with (Proof_Context.theory_of ctxt) T);
+
 fun insert_variants_same ctxt t (Const (c, T)) =
-      (case map_filter (unifiable_with (Proof_Context.theory_of ctxt) T)
-         (Same.function (get_variants ctxt) c) of
+      (case get_instances ctxt (c, T) of
         [] => unresolved_overloading_error ctxt (c, T) t "no instances"
       | [variant] => variant
       | _ => raise Same.SAME)
# HG changeset patch
# User Christian Sternagel
# Date 1374032519 -32400
#      Wed Jul 17 12:41:59 2013 +0900
# Node ID 2903a6e128fafc25085171880d1b63eb1cc4be02
# Parent  bfd42890e3b7bd6c475460023bcddb8723f19247
show variants in error messages; more precise error messages (give witnesses for multiple instances)

diff -r bfd42890e3b7 -r 2903a6e128fa src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Wed Jul 17 12:19:14 2013 +0900
+++ b/src/Tools/adhoc_overloading.ML	Wed Jul 17 12:41:59 2013 +0900
@@ -32,10 +32,18 @@
 fun not_overloaded_error oconst =
   error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
 
-fun unresolved_overloading_error ctxt (c, T) t reason =
-  error ("Unresolved overloading of " ^ quote c ^ " :: " ^
-    quote (Syntax.string_of_typ ctxt T) ^ " in " ^
-    quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
+fun unresolved_overloading_error ctxt (c, T) t instances =
+  let val ctxt' = Config.put show_variants true ctxt
+  in
+    cat_lines (
+      "Unresolved overloading of constant" ::
+      quote c ^ " :: " ^ quote (Syntax.string_of_typ ctxt' T) ::
+      "in term " ::
+      quote (Syntax.string_of_term ctxt' t) ::
+      (if null instances then "no instances" else "multiple instances:") ::
+    map (Syntax.string_of_term ctxt') instances)
+    |> error
+  end;
 
 (* generic data *)
 
@@ -143,7 +151,7 @@
 
 fun insert_variants_same ctxt t (Const (c, T)) =
       (case get_instances ctxt (c, T) of
-        [] => unresolved_overloading_error ctxt (c, T) t "no instances"
+        [] => unresolved_overloading_error ctxt (c, T) t []
       | [variant] => variant
       | _ => raise Same.SAME)
   | insert_variants_same _ _ _ = raise Same.SAME;
@@ -176,7 +184,7 @@
     fun check_unresolved t =
       (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of
         [] => ()
-      | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t "multiple instances");
+      | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t (get_instances ctxt (c, T)));
     val _ = map check_unresolved ts;
   in NONE end;