Re: When a conditional expression is static, where can it be used?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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 <rm.dash-bauh...@futureapps.de>
>>> 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