[isabelle-dev] adhoc overloading

[Florian Haftmann]

Hi Christian,
> - For Overload_Data instead of Theory_Data, I should use Generic_Data
> (such that it is available in top-level theories and local theories).
> Currently that means that I do the following in the setup (where
> Adhoc_Overloading.setup is now of type "Context.generic ->
> Context.generic").
> 
>   setup {* fn thy =>
>     Adhoc_Overloading.setup (Context.Theory thy)
>     Context.theory_of *}
> 
> This looks strange, I'm sure I'm doing something wrong / non-canonical.

I think Adhoc_Overloading.setup should stay theory -> theory: this is
the installation of the necessary syntax check phases, which is done
once globally on import of the corresponding theory – unlike the dynamic
addition via add_overloaded and add_variant

Alternatively, use Context.>> directly in the body of the ML file
(which, I guess, is nowadays preferred over explicit setup in the
surrounding theory).

> - Apparently "constants" (in the sense of locally fixed variables of a
> local theory) are represented as "term"s rather than "string"s (in the
> notation command). In adhoc_overloading.ML, until now we used "string"s
> to represent top-level constants. A change (if really necessary) implies
> the following questions:

It depends how far you want to push the game.

* The simplest one I can imagine is to stay on the »constant as string«
level, but have declarations within local theories;  if these would be
morphed e.g. due to interpretation, they would only be kept if their
resulting shape is again a constant.

* Treat one component as general term appropriately (maybe the variant?).

* Treat both components as general term appropriately.

>   * How to print a "constant" represented as "term" in the error
> messages inside Overload_Data (I do not see how I could access the
> context here)

Good question.  Note that most »fully localized« data store prefer
Item_Net.T as store index, where merge always seems to prefer on branch
(I only did skim over the sources, so this conclusion might be erroneous).

>   * I also would like to add the possibility to remove overloading and
> variants again. Is that against some monotonicity requirement I'm not
> aware of?

It should work, with the usual problems on the theory level that things
deleted in one theory come up again after merge with another theory with
partly shared but different ancestry.

> - Concerning syntax, I thought about providing commands like:
> 
>   adhoc_overloading
>     bind bind_list bind_option and
>     permute permute_list permute_option
> 
> (which would declare "bind" and "permute" as ad-hoc overloaded and add
> the variants "bind_list" and "bind_option", and "permute_list" and
> "permute_option", respectively.) Maybe some punctuation between the
> overloaded constant and its variant would increase readability?

Maybe \<rightharpoonup> / => similar to existing syntax things=

> - In the check and uncheck functions I now would have to unify typed
> terms instead of mere constants. Could that be too expensive to be
> practicable?

I have no particular idea about that.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130529/fc6bf5f8/attachment.sig>