Re: Lost in translation (with SPARK user rules)

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

Le Sun, 30 May 2010 11:26:12 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> You can see why this is sensible (even if it has some drawbacks*).
> Generally the way that a user rule is written is in response to an
> unproven conclusion in a simplified VC, so the author of the rule uses
> the final form of the unproven VC to write the rule. Therefore the
> rule can only be reliably applied at the point where the VC has
> reached its final form.
Yes, I know. The nut with me, is that I try to find the best way to use  
these rules as general rules, and precisely avoid to write rules which  
would only match expressions in a given unproved VC.

The technique is evolving, it works better than at my very first attempts.  
May be I will write some french pages about it some day.

> I guess it might be possible for the Simplifier to try all the user
> rules at each stage of the process - but the developers of the tool
> have been concentrating heavily on making simplification as quick as
> possible (quite rightly in my view) and would not want to do anything
> that might slow it down without a very strong argument for the
> advantages of doing that.
I guess this is important, as I've notice the simplifier is easily slowed  
down as the number of checks increase (or may be this is the effect of my  
user rules, which I suppose, are not as much efficiently handled as the  
built-in ones).

> (Of course nothing is ever simple, for example what happens if one
> rewrite rule requires another to be applied before its sideconditions
> are satisfied - are all such rules tried repeatedly until none are
> used, or is it a once-only pass? etc...)
That is why, except with one unique single case (a rewrite rule involving  
modular types), my own rule is to not use rewrite rules at all, because it  
can easily become a one way trap only. Inference rules are more plastic  
and does not stick anything.

-- 
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 as premise.