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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
