* Preelaboration @ 2016-05-16 16:26 Simon Wright 2016-05-16 18:22 ` Preelaboration Jeffrey R. Carter 2016-05-16 20:28 ` Preelaboration Randy Brukardt 0 siblings, 2 replies; 7+ messages in thread From: Simon Wright @ 2016-05-16 16:26 UTC (permalink / raw) I (think I) need to eliminate elaboration calls in parts of my Cortex GNAT Runtime Systems project[1], and I'm left with one that I can't understand. (1) what does pragma Preelaborate actually mean? I hoped it would mean "you don't need to elaborate this package". (2) If you give Preelaborate, is it a compiler error to generate elaboration code? (the generated elaboration procedure does nothing). (3) I find ARM 10.2.1(10)[2] unclear (I got here because the problematic package body instantiates a generic). Does it mean that the instantiation won't be preelaborable unless all of 10.1 .. 10.4 are false? Or does it mean that the compiler will make these assumptions regardless of actuals? And, looking at (10.1), would you expect generic type Item is private with Preelaborable_Initialization; package Generic_Queues is to be legal? GNAT rejects it, 'aspect "Preelaborable_Initialization" not allowed for formal type declaration'. [1] https://sourceforge.net/projects/cortex-gnat-rts/ [2] http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-10-2-1.html#p10 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Preelaboration 2016-05-16 16:26 Preelaboration Simon Wright @ 2016-05-16 18:22 ` Jeffrey R. Carter 2016-05-16 19:55 ` Preelaboration Simon Wright 2016-05-16 20:28 ` Preelaboration Randy Brukardt 1 sibling, 1 reply; 7+ messages in thread From: Jeffrey R. Carter @ 2016-05-16 18:22 UTC (permalink / raw) On 05/16/2016 09:26 AM, Simon Wright wrote: > > And, looking at (10.1), would you expect > > generic > type Item is private with Preelaborable_Initialization; > package Generic_Queues is > > to be legal? GNAT rejects it, 'aspect "Preelaborable_Initialization" not > allowed for formal type declaration'. Preelaborable_Initialization is not listed as a language-defined aspect in ARM K.1. ARM 10.2.1 (11.8/2) says that pragma Preelaborable_Initialization may appear in a generic formal part, so if you replace the aspect with the pragma it should be legal. -- Jeff Carter "I'm a vicious jungle beast!" Play It Again, Sam 131 ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Preelaboration 2016-05-16 18:22 ` Preelaboration Jeffrey R. Carter @ 2016-05-16 19:55 ` Simon Wright 0 siblings, 0 replies; 7+ messages in thread From: Simon Wright @ 2016-05-16 19:55 UTC (permalink / raw) "Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> writes: > On 05/16/2016 09:26 AM, Simon Wright wrote: >> >> And, looking at (10.1), would you expect >> >> generic >> type Item is private with Preelaborable_Initialization; >> package Generic_Queues is >> >> to be legal? GNAT rejects it, 'aspect "Preelaborable_Initialization" >> not allowed for formal type declaration'. > > Preelaborable_Initialization is not listed as a language-defined > aspect in ARM K.1. ARM 10.2.1 (11.8/2) says that pragma > Preelaborable_Initialization may appear in a generic formal part, so > if you replace the aspect with the pragma it should be legal. Thanks! Solved the compilation issue, but that wasn't the cause of the original problem. I guess the fact that Preelaborable_Initialization isn't listed in K.1 was an oversight. ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Preelaboration 2016-05-16 16:26 Preelaboration Simon Wright 2016-05-16 18:22 ` Preelaboration Jeffrey R. Carter @ 2016-05-16 20:28 ` Randy Brukardt 2016-05-16 21:03 ` Preelaboration Simon Wright 1 sibling, 1 reply; 7+ messages in thread From: Randy Brukardt @ 2016-05-16 20:28 UTC (permalink / raw) "Simon Wright" <simon@pushface.org> wrote in message news:lymvnqnf3h.fsf@pushface.org... >I (think I) need to eliminate elaboration calls in parts of my Cortex > GNAT Runtime Systems project[1], and I'm left with one that I can't > understand. > > (1) what does pragma Preelaborate actually mean? I hoped it would mean > "you don't need to elaborate this package". What it says in 10.2.1, no more and no less. There is no required effect on code generation (unless Annex C is supported, and even then it is limited). > (2) If you give Preelaborate, is it a compiler error to generate > elaboration code? (the generated elaboration procedure does nothing). No, the only errors are those defined by 10.2.1. C.4 says that a subset of preelaborable packages should not generate any code. Which only applies if Annex C is implemented, and in any case is not a testable requirement (the ACATS cannot require code inspection, which is the only way to determine if C.4 is followed). C.4(12) supposedly requires documentation of cases where code is generated, but that sort of requirement is widely ignored. (And would be useless, I'd just write something like "Elaboration of a preelaborable package may execute code in all cases other than those required by C.4 to not execute any code." It's way too hard for an implementer to figure out what will and will not do something. (And this whole set of requirements is silly anyway. What implementer executes code if they don't have to?? So anything that can be done without code is done that way, and everything else executes some code, regardless of any categorization pragma.) > (3) I find ARM 10.2.1(10)[2] unclear (I got here because the problematic > package body instantiates a generic). Does it mean that the > instantiation won't be preelaborable unless all of 10.1 .. 10.4 are > false? Or does it mean that the compiler will make these assumptions > regardless of actuals? This means that the generic body would be illegal if preelaborated, unless it means the preelaboration requirements using those assumptions. The instance can't be preelaborable unless the body is. > And, looking at (10.1), would you expect > > generic > type Item is private with Preelaborable_Initialization; > package Generic_Queues is > > to be legal? GNAT rejects it, 'aspect "Preelaborable_Initialization" not > allowed for formal type declaration'. Preelaborable_Initialization is not an aspect, as it is not the same for all views of a type. We tried to come up with a model to make it an aspect and failed to come up with something that makes sense. In addition, formal types aren't allowed to have language-defined aspects, as that would add implicit contracts to the specification (and notably, would need rules for those contracts). pragma P_I isn't allowed in a formal part, either. To get a formal type that has P_I, you'd need to use a generic derived type where the ancestor has P_I. Probably not what you want. I would guess in this case that the instance in a preelaborable package should make the package illegal; the generic would need to be Preelaborable, but then it most likely would be illegal. But this area is complicated (I might be getting it all wrong) and it probably doesn't do what you want anyway (Pure/Preelaborable categorizations in general were a failure, as they can't be applied to the majority of packages). I don't really have any advice, other than if you really care, look up the old AIs on the topic. Randy. ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Preelaboration 2016-05-16 20:28 ` Preelaboration Randy Brukardt @ 2016-05-16 21:03 ` Simon Wright 2016-05-17 23:25 ` Preelaboration Randy Brukardt 0 siblings, 1 reply; 7+ messages in thread From: Simon Wright @ 2016-05-16 21:03 UTC (permalink / raw) "Randy Brukardt" <randy@rrsoftware.com> writes: > In addition, formal types aren't allowed to have language-defined aspects, > as that would add implicit contracts to the specification (and notably, > would need rules for those contracts). pragma P_I isn't allowed in a formal > part, either. But 10.2.1(10.1), (11.2) explicitly mention P_I in a formal part? > But this area is complicated (I might be getting it all wrong) and it > probably doesn't do what you want anyway (Pure/Preelaborable categorizations > in general were a failure, as they can't be applied to the majority of > packages). I don't really have any advice, other than if you really care, > look up the old AIs on the topic. Thanks for the advice. Things are clearer now, I think; anyway, it turns out it was indeed the generic that caused the package it was instantiated in to require elaboration. I expanded the generic (of which this was the only instance, huh) by hand in the caller, no more elaboration. GNAT has a program-unit restriction No_Elaboration_Code[1] which is a lot closer to what I want. I can't remember now how I got into the state where the compiler told me I couldn't use it ... [1] https://gcc.gnu.org/onlinedocs/gnat_rm/No_005fElaboration_005fCode.html ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Preelaboration 2016-05-16 21:03 ` Preelaboration Simon Wright @ 2016-05-17 23:25 ` Randy Brukardt 2016-05-18 0:05 ` Preelaboration Robert A Duff 0 siblings, 1 reply; 7+ messages in thread From: Randy Brukardt @ 2016-05-17 23:25 UTC (permalink / raw) "Simon Wright" <simon@pushface.org> wrote in message news:lya8jpoguk.fsf@pushface.org... > "Randy Brukardt" <randy@rrsoftware.com> writes: > >> In addition, formal types aren't allowed to have language-defined >> aspects, >> as that would add implicit contracts to the specification (and notably, >> would need rules for those contracts). pragma P_I isn't allowed in a >> formal >> part, either. > > But 10.2.1(10.1), (11.2) explicitly mention P_I in a formal part? These are bug, IMHO, because there are no matching rules for P_I. One could not be allowed to instantiate a generic whose formal has P_I with a type that does not have P_I. Else the assumptions of the body are violated. Besides, 10.2.1(11.6/2) says that the pragma has to appear in the visible part of a package or generic package; the formal part of a generic package is not part of the visible part. I suspect that there was an intent that this would work, but there is a lot missing that would make it work. >> But this area is complicated (I might be getting it all wrong) and it >> probably doesn't do what you want anyway (Pure/Preelaborable >> categorizations >> in general were a failure, as they can't be applied to the majority of >> packages). I don't really have any advice, other than if you really care, >> look up the old AIs on the topic. > > Thanks for the advice. Things are clearer now, I think; anyway, it turns > out it was indeed the generic that caused the package it was > instantiated in to require elaboration. I expanded the generic (of which > this was the only instance, huh) by hand in the caller, no more > elaboration. > > GNAT has a program-unit restriction No_Elaboration_Code[1] which is a > lot closer to what I want. I can't remember now how I got into the state > where the compiler told me I couldn't use it ... > > [1] > https://gcc.gnu.org/onlinedocs/gnat_rm/No_005fElaboration_005fCode.html Randy. ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Preelaboration 2016-05-17 23:25 ` Preelaboration Randy Brukardt @ 2016-05-18 0:05 ` Robert A Duff 0 siblings, 0 replies; 7+ messages in thread From: Robert A Duff @ 2016-05-18 0:05 UTC (permalink / raw) "Randy Brukardt" <randy@rrsoftware.com> writes: > Besides, 10.2.1(11.6/2) says that the pragma has to appear in the visible > part of a package or generic package; the formal part of a generic package > is not part of the visible part. But 8.2(8) says otherwise. How else could it be? The generic formals have to be visible at the instantiation, so they can be referred to in named-notation assocs. I'm not sure how this affects the P_I pragma, but for sure generic formals are visible at the instantiation. - Bob ^ permalink raw reply [flat|nested] 7+ messages in thread
end of thread, other threads:[~2016-05-18 0:05 UTC | newest] Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2016-05-16 16:26 Preelaboration Simon Wright 2016-05-16 18:22 ` Preelaboration Jeffrey R. Carter 2016-05-16 19:55 ` Preelaboration Simon Wright 2016-05-16 20:28 ` Preelaboration Randy Brukardt 2016-05-16 21:03 ` Preelaboration Simon Wright 2016-05-17 23:25 ` Preelaboration Randy Brukardt 2016-05-18 0:05 ` Preelaboration Robert A Duff
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox