[isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

>>> Let those thoughts sink further few days.  If there is no veto until Apr
>>> 7th, I would go ahead to turn the patches upstream.

You have proposed a change about which doubts were raised.  I don't  
consider it acceptable to then announce a deadline after which you  
will go ahead and push.  People simply may not be able to respond in  
time, especially in a vacation period.

Regarding interpretation vs sublocale

We are talking about user interface design, and this means choosing  
appropriate metaphors for what certain commands do.  People familiar  
with the history of locales may remember that the precursor of the  
sublocale command was

   interpretation l < e

before I changed that to sublocale in the reimplementation.  This  
change was motivated by the realisation that interpretation between  
locales essentially means changing the module hierarchy.  This is a  
remarkable feature for a module system, which deserves emphasis and  
isn't really appropriately described by 'interpretation'.  In  
contrast, interpretation in theories just interprets locales in  
theories (even though with "subscription"), there is no additional  
value.

 From this perspective (which is the perspective of the designer!) it  
seems wrong to put interpretation in locales and theories in one  
category, and local interpretation (as it might be called) in locale  
contexts and in proof contexts in the other.  Even, if this made some  
aspects of the implementation more elegant.  Let me note that, of  
course, the user interface design should not make the implementation  
unnecessarily complicated (but I believe we are far away from that).

In this light, if a version of the sublocale command seems necessary  
in context blocks, why no call it 'sublocale'?  Of course, the global  
version should remain

   sublocale l < e.

It should not be turned into

   sublocale (in l) e

because the former much more clearly indicates the change to the  
locale hierarchy.  This design has the additional benefits that users  
don't need to change existing proof documents, terminology in the  
literature remains up to date, and, most importantly, the sublocale  
command is clearly recognisable in context blocks.

There were two more aspects in the recent discussion.  I will pick  
them up in separate e-mails since this has got too long already.

Clemens