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.lochbih...@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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
