Re: Lost in translation (with SPARK user rules)

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Thu, 27 May 2010 10:13:55 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> Finally, there is a work-around: if the Simplifier expect an expression  
> which exactly match the one provided as a user rule, and there is not a  
> direct matching expression in the source, then just use Simplifier's  
> embedded rules to prove an expression is equivalent to the one the  
> Simplifier expect an exact match.
>
> That is, if there a user rule of the form
>
>     my_rule(1) Conclusion_1 may_be_deduced_from [Expression_1].
>
> and the source unfortunately contains only
>
>     Expression_2
>
> then try something like
>
>     --# check Expression_2 -> Intermediate_Expression(1);
>     --# check ...;
>     --# check ...;
>     --# check Intermediate_Expression(N) -> Expression_1;
>
> and here it is.
>

Unfortunately, I came into another trouble. I was trying this, and used  
intermediate variables to help. But Simplifier insist on using expressions  
instead of variables, so it can't find a match.

An example will be more expressive:

Here is an excerpt of a source (T is a modular type):

    ...
    --# check T'Pos (B) >= 0; -- Check #1
    --# check T'Pos (B) <= 1; -- Check #2
    --# check (T'Pos (B) = 0) or (T'Pos (B) = 1); -- Check #3
    ...

Here is a rule in a user rules file:

    my_rule(1): (X=0) or (X=1) may_be_deduced_from [ integer(X), X>=0, X<=1  
].

And Simplifier fails to prove Check #3 ; an excerpt of the *.SIV file  
shows why (conclusion associated to Check #3):

    C1:    bit__and(v, 1) = 0 or bit__and(v, 1) = 1 .

It replaces B with the source expression of the value of B and is thus  
unable to find a match with the rule. By the way, it drops Check #1 and  
Check #2, which does not appears at all in the hypotheses list (possibly  
it seems to much obvious to Simplifier).

I've tried to use an Assert instead of a Check, this did not change  
anything.

So if Simplifier requires an exact match to user rules, is there a way to  
avoid the simplifier to brake any attempt to prove an expression match a  
rule ?

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion.