[isabelle-dev] adhoc overloading

[Makarius]

On Fri, 24 May 2013, Christian Sternagel wrote:

> Since I'm not too sure about the internals of local contexts, would that 
> make sense in principle?

Yes.  According to the "local everything approach" from 2006, locality is 
the normal situation unless there are very strong reasons against it.  In 
practice, non-locality is merely historic in most cases, and the effort to 
get things to the normal local state is called "localization".

For the declarations of Adhoc_Overloading (add_overloaded, add_variant) 
you merely need to address the usual questions what it means to transform 
them via a morphism, and then apply the result to concrete contexts in the 
applications.  A usual starting point is to look how existing similar 
mechanism do that, lets say notation that is associated with "constant" 
terms.


> A related question: what is the difference between Syntax_Phases.term_check 
> and Syntax_Phases.term_check'? Why does the latter expect a function 
> returning an option but not the former?

Syntax_Phases.term_check' allows full generality, with a functions that 
indicates a stable situation by NONE, to represent identity explicitly. 
The more common Syntax_Phases.term_check merely applies the given total 
function and compares the visible part of the result (the types/terms) to 
see if stability was achieved.

You need the "'" version in particular, when the context changes and not 
just the types/term material, e.g. setting some flags that you have "seen" 
a certain situation already.


> And another one: assume we could do
>
>  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} @{const_name foo}
>  *}
>
> would the overloading only be active inside foo or would it also have effects 
> outside of this context (that are impossible to avoid due to technical 
> reasons)? Does it make sense at all to use the locally fixed foo as a 
> constant in the call to add_overloaded?

The local_setup above is technically a 'declaration' within the local 
theory context (or other application contexts).  The morphism that 
transforms your original data from the immediate auxiliary context of the 
local definition to the application context gives you some clues about 
what to do, and when to give up the update of the context at hand. (The 
latter needs to be done gracefully, without an error.)

As a start, I recommend to imitate 'notation' to some extent.  (That is 
itself not beyond reform, but that is another story.)


 	Makarius