[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Defining a strategy that takes a list as an argument and uses it with expand*


Just to clarify things a bit: strategies are not Lisp, they are
s-expressions that are evaluated by the PVS prover.  So apply is a
primitive rule, and you can see its specification by typing C-c C-h s (M-x
help-pvs-prover-strategy).  And single quotes are rarely used in PVS
strategies, except for the few commands where Lisp forms are evaluated
(the right-hand sides of let expressions and if conditions are the two
main ones).


Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

> Hi all,
> I’m trying to better understand how to create more complex strategies
> in PVS. To that end, I have the following strategy:
> (defstep expand-grind-reveal (expand-list reveal-name)
>   (then
>    (apply 'expand* expand-list)
>    (expand)
>    (reveal reveal-name)
>   )
>   "Expands, grinds, and reveals"
>   "Expanding '~a', grinding, and revealing")
> However, when I run this, the expand* strategy is definitely not
> running. If I try the apply step by itself:
> (apply 'expand* (“function_a” “function_b” “function_b2”))
> I get the following result:
> Ill-formed rule/strategy: expand*
> Can anyone give me advice on what I might be doing wrong?
> Best Regards,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx