[isabelle-dev] Order of sublocale declarations

[Clemens Ballarin]

Hi Andreas,

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.

Clemens


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  
> more.
>
> Andreas
>
> 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?
>>
>> Amine.
>>
>> 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.
>>>
>>> Best,
>>> Andreas
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>