[isabelle-dev] adhoc overloading

[Christian Sternagel]

Dear all,

here is an update to my previous message. Corresponding patches are 
attached (tested with `isabelle build_doc -pa` and `isabelle afp_build -A`).

Some comments:

1) Variants are stored as terms but where all types are mapped to 
"dummyT" (which makes it easier to check for a given term, whether it is 
a variant of an overloaded constant).

2) In the table that maps overloaded constants to variants in addition 
to the "dummy-typed" variant also a type is included (where all free 
type variables are replaced by schematic ones).

3) As stated by Dmitriy in the "type unification" thread the current 
solution does not work for localization (but the corresponding change is 
trivial, I'm just avoiding it for the moment, since without localization 
I have to work with a thy, which is inconvenient to turn into a ctxt as 
required by Variable.polymorphic).

cheers

chris

On 07/10/2013 04:38 PM, Christian Sternagel wrote:
> 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 --------------
A non-text attachment was scrubbed...
Name: afp.patch
Type: text/x-patch
Size: 7743 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130711/670c8d31/attachment-0004.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: isabelle.patch
Type: text/x-patch
Size: 7975 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130711/670c8d31/attachment-0005.bin>