Re: [isabelle] problem with locales

On Mon, 7 Nov 2011, Andreas Lochbihler wrote:

Dear Viorel,

when locales inherit from other locales, Isabelle always renames type variables of the inherited locales to 'a, 'b, 'c, etc. There are two ways to undo the renaming:

That's an old topic about locales. What you are asking for is a mechanism for "locale inheritance" in the first place, which simply does not exist at the moment. The one you have called as such above is "polymorphic locale import", which explains the most general canonical type assignment in the result. (When you refer to a polymorphic constant into a term the same happens without much surprise.)

Both solutions are not ideal and I would be glad if the locale mechanism did not rename type variable apparently randomly. However, I haven't yet been able to convince the Isabelle developpers solve this problem.

Concerning "the Isabelle developpers" the situation of locales is especially difficult. I am glad that Clemens Ballarin left things in a quite reasonably state in 2009, after the chaotic phase of 2005-2008, when too many people where trying too many things at the same time (including myself). More recently, Florian Haftmann has done some more cleanup, and I have also recommenced myself to address long-standing known problems (like the dynamic evaluation of attributes inherited from distant past).

Locales are a very delicate area of the system, and it requires extreme care to make some actual progress, without causing collateral damage to existing infrastructure.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.