[isabelle-dev] adhoc overloading

[Christian Urban]

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-dev at in.tum.de
 > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

--