[isabelle-dev] adhoc overloading

[Alexander Krauss]

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