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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
