[isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]

[Makarius]

On Sun, 7 Apr 2013, Clemens Ballarin wrote:

> The following may or may not be related: I recently spent some thought 
> on getting rid of the mandatory vs optional distinction of qualifiers. 
> In any case this will likely have considerable impact, so here's the 
> idea:
>
> Currently there is the strange feature that abbreviations are only 
> unfolded under morphisms that are the identity on term parameters.

Unfolding should always work, problems arise when folding back for printed 
output.

Here is an example:

locale foo =
   fixes xxx :: nat
begin

abbreviation "yyy == Suc xxx"

end

interpretation foo 0 .
term yyy  -- "Suc 0"

Here the unfolding is done, the folding is not done.


Adding a prefix to the interpretation should merely change name space 
accesses (IIRC, without looking at the factual situation in the sources).


> From what I see on the mailing lists this has confused users.  Instead, 
> I would propose to change the criterion to that abbreviations are only 
> unfolded under morphisms that do not change the name part (i.e. without 
> qualification).  This would mean that for an unqualified instance syntax 
> remained available while for a qualified instance syntax redeclaration 
> would be necessary.

When you say "syntax", do you mean concrete syntax (notation), abstract 
syntax (name accesses and abbreviations) or both?

I reckon that the tentative 'private' modifier would affect all that 
uniformly.


> This would, of course, require some experimentation, but for now I just 
> would like to learn whether the 'private' modifier would be related and 
> should be taken into consideration.

I think it is somewhere in the same cloud of possibilties.  Once it clears 
up a little, we should see the necessary conclusions, and what is right.


 	Makarius