[isabelle-dev] adhoc overloading

[Christian Sternagel]

First of all, thanks for all the useful answers and sorry for my late 
reply (I visited a conference and had some holidays ;)). As Alexander 
suggested, I first tried to modify the existing adhoc_overloading.ML in 
such a way that variants may be arbitrary terms. Please find the results 
of my attempt attached (the new adhoc_overloading.ML as well as a 
patch-file). Now I will investigate further localization.

Any comments are welcome.

cheers

chris

On 06/02/2013 08:55 AM, Alexander Krauss wrote:
> Hi Chris,
>
>> I'm currently (as of changeset e6433b34364b) investigating whether it
>> would be possible to allow adhoc overloading (implemented in
>> ~~/src/Tools/adhoc_overloading.ML) inside local contexts.
>
> Nice!
>
>> For completeness find my current adhoc_overloading.ML attached
>
> Apart from the various formalities pointed out by Makarius, here is
> another concern, which relates to Florian's earlier question about how
> local you want to be...
>
> Currently, Adhoc_Overloading replaces constants with other constants,
> which makes it global-only. Your current version tries to deal with
> Frees similarly, it's not just that. Recall the example you gave
> previously:
>
>    consts FOO :: ... (<some syntax>)
>    setup {* Adhoc_Overloading.add_overloaded @{const_name FOO} *}
>
>    locale foo =
>      fixes foo :: ...
>      assumes ...
>    begin
>
>    local_setup {*
>      Adhoc_Overloading.add_variant @{const_name FOO} @{term foo}
>    *}
>
> Now consider the following interpretation:
>
>    interpretation foo "<some term>"
>      <proof>
>
> Now, <some term> should become a variant of FOO, so at least the variant
> side of the overloading relation must be an arbitrary term. With your
> current code, the overloading would only survive interpretations where
> foo happens to be mapped to a constant.
>
> So, I guess that the overloaded constants should remain constants, since
> they are just syntactic anyway. It seems that localizing those would be
> rather artificial. But the variants must be properly localized and
> subject to the morphism.
>
> As a step towards proper localization, you could start with the global
> code, and first generalize it to accept arbitrary terms as variants.
> Note that this touches in particular the uncheck phase, which can no
> longer use Term_Subst.map_aterms_same (or Term.map_aterms), since it
> becomes general rewriting. One must resort to the more general
> Pattern.rewrite_term here. When all this is working again, the actual
> localization is then a mere formality, of which you have already
> discovered the ingredients.
>
> Makarius wrote:
>> * Same.function seems to be a let-over from the version by Alex
>> Krauss. He had that once in his function package, copied from
>> somewhere else (probably old code of mine).
>
> No, it has nothing to do with the function package, which never used any
> "Same" stuff. It just arose rather naturally from the requirement to
> return NONE when nothing changes... So it was not meant as an optimization.
>
>> There is no point to do
>> such low-level optimizations in the syntax layer.  It is for hardcore
>> kernel operations only
>
> So should I manually check the result for equality, or does the
> framework do this for me?
>
> Alex

-------------- next part --------------
(* Author: Alexander Krauss, TU Muenchen
   Author: Christian Sternagel, University of Innsbruck

Ad-hoc overloading of constants based on their types.
*)

signature ADHOC_OVERLOADING =
sig
  val add_overloaded: string -> theory -> theory
  val add_variant: string -> term -> theory -> theory

  val show_variants: bool Config.T
  val setup: theory -> theory
end

structure Adhoc_Overloading: ADHOC_OVERLOADING =
struct

val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false);


(* errors *)

fun duplicate_variant_error ext_name =
  error ("Duplicate variant of " ^ quote ext_name);

fun not_overloaded_error name =
  error ("Constant " ^ quote name ^ " is not declared as overloaded");

fun already_overloaded_error name =
  error ("Constant " ^ quote name ^ " is already 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 ^ ")");


(* theory data *)

structure Overload_Data = Theory_Data
(
  type T =
    {internalize : term list Symtab.table,
     externalize : string Termtab.table};
  val empty = {internalize = Symtab.empty, externalize = Termtab.empty};
  val extend = I;

  fun merge_ext _ (ext_name1, ext_name2) =
    if ext_name1 = ext_name2 then ext_name1
    else duplicate_variant_error ext_name1;

  fun merge
    ({internalize = int1, externalize = ext1},
     {internalize = int2, externalize = ext2}) : T =
    {internalize = Symtab.merge_list (op aconv) (int1, int2),
     externalize = Termtab.join merge_ext (ext1, ext2)};
);

fun map_tables f g =
  Overload_Data.map (fn {internalize = int, externalize = ext} =>
    {internalize = f int, externalize = g ext});

val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
val get_external = Termtab.lookup o #externalize o Overload_Data.get;

fun add_overloaded ext_name thy =
  let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_error ext_name;
  in map_tables (Symtab.update (ext_name, [])) I thy end;

fun add_variant ext_name variant thy =
  let
    val _ = is_overloaded thy ext_name orelse not_overloaded_error ext_name;
    val _ =
      (case get_external thy variant of
        NONE => ()
      | SOME gen' => duplicate_variant_error gen');
  in
    map_tables (Symtab.cons_list (ext_name, variant))
      (Termtab.update (variant, ext_name)) thy
  end


(* check / uncheck *)

fun unifiable_with ctxt T1 variant =
  let
    val T2 = fastype_of variant;
    val thy = Proof_Context.theory_of ctxt;
    val maxidx1 = Term.maxidx_of_typ T1;
    val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
    val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
  in
    (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME variant)
    handle Type.TUNIFY => NONE
  end;

fun insert_internal_same ctxt t (Const (c, T)) =
      (case map_filter (unifiable_with ctxt T)
         (Same.function (get_variants (Proof_Context.theory_of ctxt)) c) of
        [] => unresolved_overloading_error ctxt (c, T) t "no instances"
      | [variant] => variant
      | _ => raise Same.SAME)
  | insert_internal_same _ _ _ = raise Same.SAME;

fun insert_external_same ctxt variant =
  let
    val thy = Proof_Context.theory_of ctxt;
    val t' = Pattern.rewrite_term thy [] [fn t =>
      get_external thy t
      |> Option.map (fn c => Const (c, fastype_of variant))] variant;
  in if variant aconv t' then raise Same.SAME else t' end;

fun gen_check_uncheck replace ts ctxt =
  Same.capture (Same.map replace) ts
  |> Option.map (rpair ctxt);

fun check ts ctxt =
  gen_check_uncheck (fn t =>
    Term_Subst.map_aterms_same (insert_internal_same ctxt t) t) ts ctxt;

fun uncheck ts ctxt =
  if Config.get ctxt show_variants then NONE
  else gen_check_uncheck (insert_external_same ctxt) ts ctxt;

fun reject_unresolved ts ctxt =
  let
    val thy = Proof_Context.theory_of ctxt;
    fun check_unresolved t =
      (case filter (is_overloaded thy o fst) (Term.add_consts t []) of
        [] => ()
      | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t "multiple instances");
    val _ = map check_unresolved ts;
  in NONE end;


(* setup *)

val setup = Context.theory_map
  (Syntax_Phases.term_check' 0 "adhoc_overloading" check
   #> Syntax_Phases.term_check' 1 "adhoc_overloading_unresolved_check" reject_unresolved
   #> Syntax_Phases.term_uncheck' 0 "adhoc_overloading" uncheck);

end;

-------------- next part --------------
A non-text attachment was scrubbed...
Name: adhoc_overloading.ML.patch
Type: text/x-patch
Size: 4588 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130710/676e3105/attachment-0001.bin>