[isabelle-dev] Order of sublocale declarations
ballarin at in.tum.de
Sat Feb 9 17:39:09 CET 2013
The failure happens while reading the locale expression, which is a
sequence of locale instances:
A s + B t + C u + ...
When reading the locale expression, we aim at achieving two conflicting goals:
- Type inference over the entire expression
- Syntax declarations of an instance are available when parsing the
next instance. That is, syntax from A s is available in t, and so on.
This is achieved by incrementally interleaved phases of parsing, type
inference and declaration activation. I suspect that when processing
the example, there is a point where the equality of the definitions
has not yet been established, and this is why the example fails.
I tend to always use qualifiers, which helps avoid the problem.
Quoting Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:
> Hi Amine,
> let's look at what happens:
> A defines the constant local.fpower as "A.fpower f"
> AB inherits it from A, i.e., we have "local.fpower == A.fpower f" (1)
> B < A "d g" produces "local.fpower == A.fpower (d g)"
> AB < B "d f" inherits this as "local.fpower == A.fpower (d (d f))" (2)
> As the locale infrastructure does not know about "d (d f) = f", it
> considers two different declarations of local.fpower from (1) and
> (2) as not being the same and therefore tries to declare both of
> them - which the local context infrastructure rejects.
> You can either use prefixes to disambiguate local.fpower like in
> sublocale AB < b!: B "d f"
> This gives you (1) and "local.b.fpower == A.fpower (d (d f))".
> Or, tell the locale infrastructure to rewrite "d (d f) = f":
> sublocale AB < B "d f" where "d (d f) == f"
> The second approach only works if you order the sublocale
> declarations like in your second case. I do not know why, but I
> believe it has technical reasons; Clemens might be able to tell you
> On 01/31/2013 02:56 PM, Amine Chaieb wrote:
>> Thanks Andreas. Does this mean that this sublocale scenario is
>> prohibited? And if so, is it due to technical reasons or is there a
>> fundamental problem here?
>> On 01/31/2013 02:04 PM, Andreas Lochbihler wrote:
>>> Hi Amine,
>>> the error message in the second case is only delayed: You get it, once
>>> you open the AB context again (context AB begin). In the first case,
>>> it shows up immediately, because the sublocale command already
>>> constructs the context AB enriched with B.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev