Re: Lost in translation (with SPARK user rules)

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 27 May, 12:32, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
[...]
> Ok, found. I was not correct with the way to require the type to be  
> integer as done in
>
>     my_set(1): (X=0) or (X=1) may_be_deduced_from [ integer(X), X>=0, X<=1  
> ].
>
> It has to be
>
>     my_set(1): (X=0) or (X=1) may_be_deduced_from [  
> goal(checktype(X,integer)), X>=0, X<=1 ].
>
> I've check that
>
>     my_set(1): (X=0) or (X=1) may_be_deduced_from [ goal(integer(X)), X>=0,  
> X<=1 ].
>
> does not work, which lead to another question : what is the difference  
> between the two predicates “integer(X)” and “checktype(X,integer)” ? The  
> documentation is not clear to me about it. About “checktype(EXPRESSION,  
> TYPE_IDENTIFIER)”, it says “This predicate may be used to check that an  
> expression is of an appropriate type” and about “integer(EXPRESSION)” is  
> says This built-in Prolog predicate succeeds if and only if its argument  
> is instantiated to an integer. So what's the difference between  
> “goal(integer(X))” and “goal(checktype(X,integer))”. Does the latter  
> refers to root type as defined in source and the other to something else ?  
> (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  
> predicate stating arguments have to be integers and there is just a  
> 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