From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,6a9844368dd0a842 X-Google-Attributes: gid103376,public From: dewar@cs.nyu.edu (Robert Dewar) Subject: Re: seperate keyword and seperate compilation with Gnat? Date: 1996/07/15 Message-ID: X-Deja-AN: 169175614 references: <31D95D93.28D8D15B@jinx.sckans.edu> <4rckva$dj1@Starbase.NeoSoft.COM> organization: Courant Institute of Mathematical Sciences newsgroups: comp.lang.ada Date: 1996-07-15T00:00:00+00:00 List-Id: Jon said "As I have stated several times, I am not proposing adding this statement. Apparently you have missed my only point. Which was simply that that statement, contrary to your claim(s), is _FAR_ clearer on the subject than all the RM has to say about it. This is so OBVIOUS that to disagree with it is really to defy credulity. " No, this is not OBVIOUS, in fact, as I have tried to point out, it is obviously NOT clearer, since it would create confusion as to why subunits were being singled out. Of course I realize you are not proposing adding this statement in the sense of actually adding it (that's impossible, the RM text cannot be changed). But you do seem to be saying that if this statement *were* in the RM, it would be clearer than what is there now. I have tried to be clear about the reason for this, but since it continues to defy your credulity and is exasperating you, let's try again. First, Jon, you started this thread off with a long and incorrect attempt at exegesis on the RM to prove that it was OK for subunits to be required to be present. Let's do the opposite, and show the proof that this is wrong -- after all that's what the issue is, the clarity of that proof. First, the definition of semantic dependency in 10.1.1 26 A library_item depends semantically upon its parent declaration. A subunit depends semantically upon its parent body. A library_unit_body depends semantically upon the corresponding library_unit_declaration, if any. A compilation unit depends semantically upon each library_item mentioned in a with_clause of the compilation unit. In addition, if a given compilation unit contains an attribute_reference of a type defined in another compilation unit, then the given compilation unit depends semantically upon the other compilation unit. The semantic dependence relationship is transitive. Seems pretty clear to me, but of course one is always free to suggest improvements to wording. You didn't suggest any such clarifications anyway, so that's not an issue. Certainly there is no suggestion, nor any possible reading, under which a parent body is dependent on its subunit (the dependence in the other direction is clearly stated). Now, let's read in 10.1.4 5 When a compilation unit is compiled, all compilation units upon which it depends semantically shall already exist in the environment; the set of these compilation units shall be consistent in the sense that the new compilation unit shall not semantically depend (directly or indirectly) on two different versions of the same compilation unit, nor on an earlier version of itself. Again, seems pretty clear. Again, you could suggest clarifications to the wording of this paragraph, but you did not, so that's not an issue. So, Q.E.D. a parent does not depend on its subunits, therefore there is no requirement that the subunits be around when the parent is compiled. There is no implementation permission to modify this rule, so a requirement that subunits be around would be a restriction not justified by the RM. Now back to your OBVIOUS suggestion. You said the wording in the RM could be improved by adding a clear statement that subunits need not be around, but the reason I think that would not clarify AT ALL is that it would single out subunits (among all the other possibilities for non semantically dependent units), and suggest that there is a special rule for them. It is as though someone tried to write: x : string (1 .. 1); x := 'a'; and, being surprised that this did not work, suggest that an explicit rule be stated in the appropriate part of chapter 5 saying that something of type Character cannot be assigned to a one character String. That would be equally damaging, since of course this is just a special case of the general rule that you cannot assign things of the wrong type. Rules in reference manuals need to be stated as generally as possible, that's a critical requirement. Now what about notes, as Bob Duff pointed out, the statement you suggested as clarifying, if it were appropriate to the RM at all, would be appropriate as a note. There is one note in this area already: 10 (7) A compilation unit containing an instantiation of a separately compiled generic unit does not semantically depend on the body of the generic unit. Therefore, replacing the generic body in the environment does not result in the removal of the compilation unit containing the instantiation. This is a note because it is a (very obvious) theorem, but it is provided since the implemenation model that people may well have in mind (generic instantiation by macro substitution) might lead to an opposite conclusion. Now, is the OBVIOUS statement you proposed suitable as a note. No! That's because it does not mention the concept of semantic dependency, so it does not point out its own proof, and generally the idea of a note is to not only state a theorem, but if possible to give a clue to the proof. A possible form of the note you would like to see is A parent unit does not semantically depend on its subunits. Therefore when a parent unit is compiled, its subunits need not be present in the compilation environment. I would not object strongly to such a note, although for my own taste I prefer to absolutely minimize notes in the RM. That does not mean I don't like notes at all (for example, I suggested adding the note in 5.5: 10 (6) A loop parameter is a constant; it cannot be updated within the sequence_of_statements of the loop (see 3.3). since it seemed inappropriate to me to expect people to make the connection with the definition of constant in 3.3. But of course it would have been quite wrong to add anything *but* a note here, since this is indeed a trivial theorem, easily proved by reference to the correct section. I do not consider that the note above on needing subunits is one that is necessary, because the proof is not only obvious, but the needed paragraphs are immediately at hand, and they are the obvious ones to consult in finding the answer to the question. I am sorry if you continue to find his exasperating, but the above is definitely my opinion on the subject :-) P.S. I don't think this is a silly discussion. Learning how to read the RM involves learning the style and attitude of the presentation, which is not always obvious at first. I am certainly not saying the RM is perfect, and there are sections where things are far from clear and where the theorems are hard to state and harder to prove, but the issue at hand is a quite clear one, and a useful pedagogical example of the RM style and what notes, theorems, axioms etc are all about. Robert