Re: Ada 2012 Constraints (WRT an Ada IR)

["Randy Brukardt" <randy@rrsoftware.com>]

[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.

...
>> Thus, your hypothetical IR would have to represent ranges as predicates,
>> rather than as some sort of set. But that would make it hard to do
>> operations on the IR (such as merging and check elimination).
>
> Would it though? Don't we have tools (and entire programming languages)
> built around predicate-logic?

(1) Hard /= impossible.
(2) I have no idea about tools or programming languages built around
predicate logic. Ada systems usually are built around simpler things, the
most complex being set operations. Trying to put a predicate logic prover
into a compiler optimizer sounds challenging at best. (Yes, I realize this
argument is somewhat circular.)

                               Randy.