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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,9f99a33281d5072c X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news4.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!195.96.0.7.MISMATCH!newsfeed.utanet.at!newsfeed01.chello.at!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: When a conditional expression is static, where can it be used? Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <4c2b1ecb$0$7670$9b4e6d93@newsspool1.arcor-online.net> <555e3a37-c709-4b9b-995a-907da862d4b7@m40g2000prc.googlegroups.com> <12ok8wnj6k4sw$.ravumwbhfb1h$.dlg@40tude.net> <4c2ba385$0$6772$9b4e6d93@newsspool3.arcor-online.net> Date: Wed, 30 Jun 2010 22:45:19 +0200 Message-ID: <1tqq74zh1p6lw$.1jurvhtl863hq$.dlg@40tude.net> NNTP-Posting-Date: 30 Jun 2010 22:45:17 CEST NNTP-Posting-Host: e220b896.newsspool2.arcor-online.net X-Trace: DXC=W0>:LgQh1FII7\_^6>c20JA9EHlD;3YcB4Fo<]lROoRA8kF^0SV3ak:FLMNINR228`EG X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:13029 Date: 2010-06-30T22:45:17+02:00 List-Id: On Wed, 30 Jun 2010 22:05:25 +0200, Georg Bauhaus wrote: > On 30.06.10 19:35, Dmitry A. Kazakov wrote: >> On Wed, 30 Jun 2010 07:39:24 -0700 (PDT), Adam Beneschan wrote: >> >>> On Jun 30, 3:39 am, Georg Bauhaus >>> wrote: >>>> A totally meaningless example just to illustrate >>>> the question: What is it that a compiler must report >>>> for the case statement below, if anything? >>> >>> The choice "Sa" is not covered by any alternative. Other than that, I >>> don't think there's anything wrong with the CASE statement, and if you >>> had included a "when others =>" alternative I think it would be >>> legal. I'm not sure what potential problem you were trying to >>> illustrate. > > The questions I had asked myself (a little too quick, I suppose) > were along these lines: > > Is it possible to invalidate a case construct by simply > changing the value of a static constant used in determining > conditional static case values? Yes, it is possible even without > conditional expressions, but do these introduce failures that > are much more tricky to straighten out? Yep, as the example shows. > All this about static conditional expressions in case_statement_alternative > is probably a somewhat artificial argument, since a conditional > expression in such a place is something Ada programmers will > just not write. Right? Hopefully. But the problem is that static expressions are non-testable. You don't know if the expression is right until you substitute another value. This is same problem as with the C++ templates and more and more with Ada generics. This is why I don't like either and it seems that if-operators move us in wrong direction. >> Let me propose this one instead: >> >> type DOW is (Mo, Tu, We, Th, Fr, Sa, So); >> >> case D is >> when (if D = Mo then Tu else Mo) => P; >> when (if D = Tu then Tu else Mo) => Q; >> when We..So => R; >> end case; > > D: constant DOW := We; > case D is -- replace D with {We} > when (if {We} = Mo then Tu else Mo) => P; -- Mo > when (if {We} = Tu then Tu else Mo) => Q; -- Mo > when We .. So = => R; -- I should have written Su, sorry > end case; Shame on me. (A perfect illustration to the point) >> This wonderful static function can then copied and pasted everywhere you >> wanted to evaluate Gamma at compile time. Is it legal? > > Should we have "bigger" static functions? Certainly yes to solve problems like measurement units support. And also to encourage the programmer not to use these awful if-operators or at least to refactor some of them. At the same time static functions would be obviously exposed to the same problem of non-testability and utter obscureness. > The 'Constraint or invariant things being worked out for subtypes > are, I guess, potentially static. How far can one push the > compiler *and* the programmer computing or specifying conditional > expressions, resp.? > (And not have one's head spin too much, or introduce programs > that surprise when changed?) The only solution I see is requiring proofs of correctness in static contexts. I.e. if you wrote: case X is when F (...) => -- F,G are complicated user-defined static functions when G (...) => end case; then the language should require that F and G would make the case statement correct by any possible combination of their arguments, rather than by only the current one. In short, the static meta-language of Ada must be at least like SPARK. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de