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
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 border1.nntp.dca3.giganews.com!backlog3.nntp.dca3.giganews.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!goblin2!goblin.stu.neva.ru!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: J Kimball <nntp@kmbll.com>
Newsgroups: comp.lang.ada
Subject: Re: Making guarantees about record components
Date: Thu, 21 Nov 2013 23:46:28 -0600
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <l6mr3m$bba$1@loke.gir.dk>
References: <l6gbro$1oc$1@loke.gir.dk>
NNTP-Posting-Host: 109.201.154.210
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit
X-Trace: loke.gir.dk 1385099190 11626 109.201.154.210 (22 Nov 2013 05:46:30
 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Fri, 22 Nov 2013 05:46:30 +0000 (UTC)
User-Agent: Mozilla/5.0 (X11; Linux x86_64;
 rv:25.0) Gecko/20100101 Thunderbird/25.0
In-Reply-To: <l6gbro$1oc$1@loke.gir.dk>
X-Original-Bytes: 2161
Xref: number.nntp.dca.giganews.com comp.lang.ada:183967
Date: 2013-11-21T23:46:28-06:00
List-Id: <comp.lang.ada>

On 11/19/2013 12:49 PM, J Kimball wrote:
> Hello
> 
> I'm trying to guarantee that two record component values map to the same
> value of another type.
> 
> type A is (...);
> type C is (...);
> 
> M : array (A) of C := (...);
> 
> type R is record
>    A1 : A;
>    A2 : A;
> end record
>    with Dynamic_Predicate => (M (R.A1) = M (R.A2) );
> 
> Is this the best solution we have as of Ada 2012?
> 
> Regards
> 

Thanks for your inputs. I understand the rules for the dynamic_predicate
as Kazakov pointed out. This is what you'd expect certainly. I was more
curious to see what solutions you might propose. My solution uses a
variant. Subtypes of A become the mapping. Static predicates make this
even more powerful. Assuming you can put up with a discriminated record,
this solution doesnt show off the power of static predicates, but
demonstrates one solution not using private types or predicates and fits
my actual problem well.

type A is (...);

subtype E is A range ...;
subtype F is A range ...;

type C is (...);

type R (One : A) is record
   case One is
      when E =>
         E_Value : E;
      when F =>
         F_Value : F;
   end case;
end record;