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,XPRIO autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Fri, 9 Dec 2016 15:41:56 -0600 Organization: JSA Research & Innovation Message-ID: NNTP-Posting-Host: rrsoftware.com X-Trace: franka.jacob-sparre.dk 1481319717 18754 24.196.82.226 (9 Dec 2016 21:41:57 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 9 Dec 2016 21:41:57 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:32702 Date: 2016-12-09T15:41:56-06:00 List-Id: [I had to break the chain of replies as the headers got so long that the message wouldn't post.] "Shark8" 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.