[isabelle-dev] adhoc overloading

[Christian Sternagel]

In the meanwhile I had a first look at the implementation of the 
"notation" command. Some things I noted w.r.t. localizing ad-hoc 
overloading (please correct me if I'm wrong):

- 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.

- 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:

   * 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)

   * 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?

- 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?

Similarly there could be

   no_adhoc_overloading
     ...

Any comments?

- 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?

Would anybody be interested in "formally" discussing and implementing 
necessary changes to the existing implementation in a dedicated 
mercurial repo on bitbucket?

cheers

chris

On 05/25/2013 03:28 AM, Makarius wrote:
> 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