Email Gateway (Aug 18 2022 at 18:39): Email Gateway (Aug 18 2022 at 18:39):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
I have the following two locales:
locale node =
fixes nil :: "'node"
assumes infinite: "¬ finite (UNIV::'node set)"
begin
definition "domain f = {x :: 'node . - (f x = (nil::'node))}"
end
locale list = node +
fixes "next" :: "'node => 'node"
fixes val :: "'node => 'node"
assumes "next (nil::'node) = nil"
These locales generate error "Type unification failed". If I drop the
definition from the first locale then I do not get this message.
More generally. Is there a standard mechanism to enforce
the type 'node from the first locale to be the same as the
type node from the second locale?
Best regards,
Viorel
Email Gateway (Aug 18 2022 at 18:39):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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:
a) Do not use the locale feature of implicitly adding unmentioned parameters of
imported locales to the for clause, but state them explicitly:
locale list = node nil for nil :: "'node" + ...
The drawback is that you have to redeclare mixfix syntax if your imported locale
declares such for the parameter. If you do not plan to use syntax annotations
anyway, this is the preferred way.
b) Constrain the parameter types using "constrains":
locale list = node +
constrains nil :: "'node"
fixes "next" :: "'node => node"
...
The advantage is that constrains does not delete mixfix syntax. However, Clemens
has threatened to remove this rarely known feature in some futute release.
Moreover, this often still gives you type error messages. I found that it works
reliably if
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.
Best regards,
Andreas
Email Gateway (Aug 18 2022 at 18:39):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 18 2022 at 18:39):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Dear Andreas,
Using constrains solved my problem. Using this constrains declaration
seem like a nice solution to this problem. I don't see the reason to
remove it, but on the contrary to document it well.
I had earlier this problem and the way I solved it was by imposing
additional dummy assumptions on the imported constants.
Best regards,
Viorel
Last updated: Nov 21 2024 at 12:39 UTC