From: <an...@an...> - 2013-04-16 08:42:40
|
Dear Tim Thanks for this. I don't think we should let the memory management issue force us into a position where we violate Z semantics, or have a special mode. I'm not sure whether the improvement Andrius found, and others like it, actually require that ids be the same in different schemas. I don't know whether the copying he was referring to was one that changed the ids or not. If not, maybe we can still improve memory usage without a semantic change. But if so, then perhaps there are other possible solutions? First, maybe it would be OK to copy the ZName, as long as in doing so we didn't copy any of its components? I suspect (but don't know) that the copy currently gets a new ZWord, LcAnn etc? If that wouldn't solve the problem, then perhaps we can keep some sort of id but interpret it in a way consistent with the semantics. Suppose I have x defined in schema A and then included in B. Given that its occurrence in B is, by definition of the semantics, unique, we don't actually need to assign a different id to tell us that. All we need to know is that it is a schema variable not a global one. So if the id were changed in some way to indicate the scope of the variable (global, schema, or expression-local) plus a pointer back to a declaration instance, then we could have exactly the same ZName in every schema without violating the semantics., This seems consistent with your point that ids need to be unique but actually the tools don't care - they don't care because the uniqueness to the schema is part of the language and doesn't need a separate indication. Would this reconcile the two issues, of correctness vs efficiency, do you think? (I'm writing this just before going on holiday, so please forgive the fact that I won't respond to any further discussion for a couple of weeks) All the best Anthony > On 16 April 2013 at 01:55 Tim Miller <tm...@un...> wrote: > > > 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 > > ------------------------------------------------------------------------------ > Precog is a next-generation analytics platform capable of advanced > analytics on semi-structured data. The platform includes APIs for building > apps and a phenomenal toolset for data science. Developers can use > our toolset for easy data analysis & visualization. Get a free account! > http://www2.precog.com/precogplatform/slashdotnewsletter > _______________________________________________ > CZT-Devel mailing list > CZT...@li... > https://lists.sourceforge.net/lists/listinfo/czt-devel |