On Wednesday, July 17, 2013 at 13:43:34 (+0900), Christian Sternagel wrote: > > @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
Yes. I think nobody has figured out what code should be generated for the *quotients* that nominal datatypes are in general. Best wishes, Christian > > 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 > > > ---------------------------------------------------------------------- > # 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; > > > ---------------------------------------------------------------------- > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev