Re: [CZT-Devel] Reducing memory usage: Signatures are the biggest culprit?

[Tim M. <tm...@un...>]

Hi Anthony,

You wrote:
> Can I ask a question about ids? I had understood that the id was necessary
> for distinguishing truly different instances of a name - for example x
> declared globally and x within a schema.

Yep, that's correct.

> If that's true we can't presumably
> drop ids altogether? Certainly I use them in my cross reference (as you may
> remember, we had extensive discussions about this) and I've just been
> looking at the "Go To Declaration" tool in the Eclipse IDE, which I think
> uses the word + id as the unique identifier of a name.
>
> So I wonder whether we do need to keep the id, but not to create a new id
> for every schema inclusion? If I declare x in S and then include S in T, I
> don't think we should need a new id for the x in T, for example.

It creates a new ID because it is a new variable. I did it like this 
because it is consistent with the semantics of Z. If x is declared in S 
and then S included in T, the variable x is indeed a new variable, 
because the semantics are that the definition of T is identical to the 
case that the declarations and predicate from S are "cut and paste" into 
T. So, the following:

S == [x : X];
T == [S; y : Y]

is semantically equivalent to:

S == [x : X];
T == [x : X; y : Y]

If we were to not declare a new ID for the x in the first example, then 
the two declarations of x the first example would have the same ID, 
while in the second, they would be different. I'm not comfortable with 
that inconsistency.

I'm not arguing that this is really important (I can't see that any of 
our tools would care), but this is the motivation. I would prefer to 
preserve the semantics as is currently, and just have a mode where the 
IDs are not renamed. In fact, this second mode would be nice for tracing 
variable declarations in Z state machines, as we can link included state 
variables back to their definition in a state schema quite easily. To do 
this now, we would have to pass the definitions in more detail.

> Also, there the special id deltaxi, which presumably needs to be kept or
> replaced with a different mechanism?
>
The id deltaxi was added by someone other than me (Leo I guess?) and I 
don't know what the motivation for that was, instead of e.g. just 
allocating a fresh ID.

> At the moment it also seems to be true that there are many instances of a
> ZName with the same id - that too could presumably be avoided?
>
I can't comment on that without looking further. I would assume that you 
are right because I appear to have created a method in the typechecker 
factory for copying names. One shortcut would be to just return the same 
instance for that method, but I'm not really sure. I can certainly look 
into this further once we have a consensus on how we should handle this.

Cheers,
Tim