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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,ec6f74e58e86b38b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,CP1252
Path: 
 g2news2.google.com!postnews.google.com!m33g2000vbi.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: Lost in translation (with SPARK user rules)
Date: Thu, 27 May 2010 04:41:08 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <972f1d61-82da-4dfa-aef7-0a644234b557@m33g2000vbi.googlegroups.com>
References: <op.vda45rsfule2fv@garhos>
 <0466e131-cc80-4db4-b080-eec9aefcb1c7@z17g2000vbd.googlegroups.com>
	<op.vda7dlc2ule2fv@garhos> <op.vdcuhhymule2fv@garhos>
 <op.vdc1x3ctule2fv@garhos>
	<op.vdc3n1h0ule2fv@garhos>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1274960468 3447 127.0.0.1 (27 May 2010 11:41:08
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 27 May 2010 11:41:08 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: m33g2000vbi.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:12074
Date: 2010-05-27T04:41:08-07:00
List-Id: <comp.lang.ada>

On 27 May, 12:32, Yannick Duch=EAne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
[...]
> Ok, found. I was not correct with the way to require the type to be =A0
> integer as done in
>
> =A0 =A0 my_set(1): (X=3D0) or (X=3D1) may_be_deduced_from [ integer(X), X=
>=3D0, X<=3D1 =A0
> ].
>
> It has to be
>
> =A0 =A0 my_set(1): (X=3D0) or (X=3D1) may_be_deduced_from [ =A0
> goal(checktype(X,integer)), X>=3D0, X<=3D1 ].
>
> I've check that
>
> =A0 =A0 my_set(1): (X=3D0) or (X=3D1) may_be_deduced_from [ goal(integer(=
X)), X>=3D0, =A0
> X<=3D1 ].
>
> does not work, which lead to another question : what is the difference =
=A0
> between the two predicates =93integer(X)=94 and =93checktype(X,integer)=
=94 ? The =A0
> documentation is not clear to me about it. About =93checktype(EXPRESSION,=
 =A0
> TYPE_IDENTIFIER)=94, it says =93This predicate may be used to check that =
an =A0
> expression is of an appropriate type=94 and about =93integer(EXPRESSION)=
=94 is =A0
> says This built-in Prolog predicate succeeds if and only if its argument =
=A0
> is instantiated to an integer. So what's the difference between =A0
> =93goal(integer(X))=94 and =93goal(checktype(X,integer))=94. Does the lat=
ter =A0
> refers to root type as defined in source and the other to something else =
? =A0
> (so what?)

It's explained in the Simplifier manual section 7.2.3:
goal(integer(X)) requires X to *be* an integer, not just of integer
type (so goal(integer(42)) succeeds).

If you always use goal(checktype(X, integer)) then is works for
anything that has an integer type.

>
> Another strange thing is that the file NUMINEQS.RUL does not contains any=
 =A0
> predicate stating arguments have to be integers and there is just a =A0
> comment in heading, nothing in rules about it.
This is the documentation of a Checker rule file, so is not relevant
to the Simplifier.  In the actual rule file used by the Checker the
comment that you mention will be included in what the Checker sees, so
will be effective in restricting the application of the rule.

Cheers,

Phil