[isabelle-dev] adhoc overloading

[Christian Sternagel]

Dear all,

please find attached patches for localizing 
src/Tools/Adhoc_Overloading.thy. It should work like the previous 
version in the non-local case, besides a more convenient interface, 
i.e., instead of

   setup {*
     Adhoc_Overloading.add_overloaded @{const_name foo}
     #> Adhoc_Overloading.add_variant @{const_name foo} @{const_name bar}
   *}

it is now

   adhoc_overloading
     foo bar

where "bar" may be an arbitrary term (not just a constant). For removing 
ad-hoc overloading there is the command "no_adhoc_overloading".

I tested the local case only on toy examples. Comments are welcome.

cheers

chris

On 07/11/2013 04:36 PM, Christian Sternagel wrote:
> 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: 7402 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130712/6219e2ef/attachment-0004.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: isabelle.patch
Type: text/x-patch
Size: 13096 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130712/6219e2ef/attachment-0005.bin>