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=unavailable autolearn_force=no version=3.4.4 X-Received: by 2002:a02:b047:: with SMTP id q7mr14860884jah.2.1558542878710; Wed, 22 May 2019 09:34:38 -0700 (PDT) X-Received: by 2002:aca:80e:: with SMTP id 14mr8233781oii.2.1558542878461; Wed, 22 May 2019 09:34:38 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!news.dns-netz.com!news.freedyn.net!newsreader4.netcologne.de!news.netcologne.de!border2.nntp.ams1.giganews.com!nntp.giganews.com!feeder1.cambriumusenet.nl!feed.tweak.nl!209.85.166.216.MISMATCH!i64no30284iti.0!news-out.google.com!l135ni51itc.0!nntp.google.com!c92no18406itd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 22 May 2019 09:34:37 -0700 (PDT) In-Reply-To: <430790a7-7d0b-4812-b40a-d781cd1dd62d@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=47.185.234.171; posting-account=zwxLlwoAAAChLBU7oraRzNDnqQYkYbpo NNTP-Posting-Host: 47.185.234.171 References: <100ad407-090e-4316-9746-a4469568b53e@googlegroups.com> <477352cf-80d0-458c-b64a-4605557fef8f@googlegroups.com> <36cf3be3-0ab0-48d4-bffa-e49c624e73ff@googlegroups.com> <430790a7-7d0b-4812-b40a-d781cd1dd62d@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <29eb5a31-64d0-45f3-8c2e-7a715ac8f02d@googlegroups.com> Subject: Re: Ada to Ada Translator ? From: Optikos Injection-Date: Wed, 22 May 2019 16:34:38 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader01.eternal-september.org comp.lang.ada:56370 Date: 2019-05-22T09:34:37-07:00 List-Id: On Wednesday, May 22, 2019 at 10:24:10 AM UTC-5, Shark8 wrote: > On Wednesday, May 22, 2019 at 6:57:05 AM UTC-6, foo wong wrote: > > Just to stick with the topic I brought up earlier, if nested subprogram= s were translated into more > > primitive Ada code, then the translator would translate any library cod= e. The only grammar that is > > required is for core Ada. > What is the use-case of the "nested subprograms" example? I just don't ge= t it...=20 Spark8, please consider the following cascading ramifications. Why do you = think that the ARG has killed off nested subprograms, lambdas, and closures= ? The implementation of named nested subprograms facilitates the implementati= on of unnamed nested subprograms (i.e., lambdas). The implementation of la= mbdas facilitates the the implementation of closures. Closures facilitate = functional programming. Functional programming facilitates correctness pro= ofs. Having another mechanism for Ada correctness proofs than SPARK facili= tates the rise of a true competitor to GNAT+SPARK. The rise of a true comp= etitor to GNAT+SPARK facilitates the rise of a true direct competitor to Ad= aCore as a company. Therefore, rewind: nip named & unnamed nested subprog= rams in the bud. Btw, this cascading-ramification sequence over in C++land could permit the = rise of a C++ correctness prover (done all wobbly on shaky C foundations, b= ut still it also could be at least =E2=80=A2marketed=E2=80=A2 as a SPARK+GN= AT competitor, even if it isn't as good). > plus, capturing the > context of those subprograms might be a bit more complex than you're thin= king: if they use local > variables, the the realization might be better as a GENERIC subprogram wi= th those very objects as > formal parameters. As much as I loathe their usage of the C++ template engine as a poor-man's = functional programming language with atrocious syntax, Boost C++ libraries = can serve as inspiration for how to implement lambdas and closures in the A= da-to-Ada code generator, especially in older Boost libraries targeting old= er C++ compilers that lack C++11-&-onward language support for lambdas and = closures. > > Based on this website: > > https://wiki.osdev.org/Ada_Bare_bones > >=20 > > These are the parts that the translator would need to translate into mo= re primitive Ada code: > >=20 > > """ > >=20 > > pragma Discard_Names; > > pragma Restrictions (No_Enumeration_Maps); > > pragma Normalize_Scalars; > > pragma Restrictions (No_Exception_Propagation); > > pragma Restrictions (No_Finalization); > > pragma Restrictions (No_Tasking); > > pragma Restrictions (No_Protected_Types); > > pragma Restrictions (No_Delay); > > pragma Restrictions (No_Recursion); > > pragma Restrictions (No_Allocators); > > pragma Restrictions (No_Dispatch); > > pragma Restrictions (No_Implicit_Dynamic_Code); > > pragma Restrictions (No_Secondary_Stack); > > """ > >=20 > > but even some of these could be skipped over. If I am the one that ends= up doing this, I will only be > > focused on hardware embedded Ada and I will focus on new targets and no= t every last corner-case > > feature > ?? >=20 > Forgive me, but I don't see how these restriction pragmas dovetail into a= n Ada-Ada translator... at all. > Could you explain how you see them doing so? Patrick is proposing that his Ada-to-Ada code generator would accept all va= lid GNAT source code. As such as GNAT-wrapper, it would need to at least p= arse & accept GNAT extensions so as to pass them through verbatim (and/or m= odified slightly if they interfere with the not-pass-through portions of th= e Ada-to-Ada code generator). What would be really cool would be for the Ada-to-Ada code generator to acc= ept Digital Ada's extensions too, especially a.app, which would permit mult= istage programming in a compile-time Ada interpreter as a rather direct com= petitor to MetaOCaml.