[isabelle-dev] adhoc overloading

[Christian Sternagel]

Dear Florian,

On 05/30/2013 06:03 AM, Florian Haftmann wrote:
> 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
Sorry, my question should have been: how to apply a function of type 
"Generic.context -> Generic.context" in a situation where "theory -> 
theory" is expected (the former type comes from using Generic_Data, and 
the latter is what "setup" should have). In the meanwhile I found

   Context.theory_map: (Context.generic -> Context.generic) -> theory -> 
theory

>
> Alternatively, use Context.>> directly in the body of the ML file
> (which, I guess, is nowadays preferred over explicit setup in the
> surrounding theory).
Thanks for the hint. I'm now using "Context.>>" instead of a setup 
function called from a thy-file.

>
>> - 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.
My naive approach was to just turn the previous Symtabs into Termtabs, 
i.e., previously:

   internalize : (string * typ) list Symtab.table
   (*maps overloaded constants to lists of variants (together with their 
type)*)
   externalize : string Symtab.table
   (*maps variants to corresponding overloaded constants*)

(An aside: I'm leaning towards renaming those two tables and related 
functions as follows:

   internalize ~> variant_tab
   externalize ~> oconst_tab

which would make more sense to me, but maybe the old naming has a 
Isabelle-specific reason I'm not aware of?)

As a first attempt I just changed this into

   variant_tab : term list Termtab.table (*we can get the type of a term*)
   oconst_tab : term Termtab.table

But of course that is not what I intended, since types are now also 
inspected when looking up a key in a table, but at least for overloaded 
constants only their name is important. This seems to point towards one 
of your first two suggestions. The first one, would require the least 
amount of changes (and would allow to print readable error messages). 
The question is whether I'm asking for problems, when I treat "Free" 
variables (i.e., "constants" in local theories) and "Const"s both as 
strings? Any opinions?

A related question. Until now I can only register overloaded constants 
and variants via the ML interface, since the "adhoc_overloading" command 
I implemented does not seem to effect the surrounding theory. I will 
have a look at "notation" again to see how functions of type 
"local_theory -> local_theory" are able to make "non-local" changes 
persistent, i.e., update the tables in my Generic_Data. Maybe somebody 
does already have suggestions in that respect?

cheers

chris

>
>>    * 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
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>