Re: Ada 2012 Constraints (WRT an Ada IR)

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 16-12-09 23:41 , Randy Brukardt wrote:
> [I had to break the chain of replies as the headers got so long that the
> message wouldn't post.]
>
> "Shark8" <onewingedshark@gmail.com> wrote in message
> news:8e3b18a7-1e64-40bb-8d99-66fdeba58ace@googlegroups.com...
>> On Tuesday, December 6, 2016 at 4:23:55 PM UTC-7, Randy Brukardt wrote:
> ...
>>> You seem to be assuming that it is practical to represent all kinds of
>>> predicates as some sort of set. That's definitely not true; one of the
>>> major
>>> reasons that you can't use divide or mod in a static predicate is the
>>> difficulty of representing the set. For instance, consider:
>>>
>>>      subtype Even is new Natural with Dynamic_Predicate => Even mod 2 =
>>> 0;
>>>
>>> If Natural is a 64 bit type, Even is a set of 2**63 items, no two are
>>> contiguous. The representation of that is going to be a problem. One
>>> could
>>> imagine some special case to deal with this particular case, but then
>>> there
>>> are many other possible predicates with this property.
>>
>> Just because it's represented as a set doesn't mean that the set has to be
>> represented as a bit-mask. (The obvious breaking example for that
>> implementation here would be a string subtype constrained to contain only
>> numeric characters.)
>
> In existing Ada implementations, sets are represented as a list of ranges.
> (They come up in a number of places, including case statements and
> Ada.Strings.) That's the expected implementation for any Ada set, but that
> would take 2**63 items for Even.

Static program analyzers, at least those analysing machine code and 
aiming to understand address alignments and aliasing, tend to need and 
use not only ranges, but ranges with strides (congruence information). 
The set of Even numbers would be easy and compact to represent in such a 
model, with stride = 2. Of course, it is a coincidence that Even happens 
to fit this model, and your general argument is not affected.

> Trying to put a predicate logic prover into a compiler optimizer sounds
> challenging at best.

I'm a little surprised: I seem to remember that you have, earlier, said 
that you would like future compilers to prove all sorts of things about 
the program. But you were not thinking of predicate logic proofs?

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .