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

Re: [PVS-Help] args1 and strategies



Hi Erika,

The 'args1' function takes an application, and returns the first argument
to it.  I expect what you want is 'expression', which returns the
body of the forall expression ('bindings' returns the variables).  If
you use 'show' to show the form, you will see all the slots, which can
be accessed by the slot name.

Regards,
Sam

Erika Rice <erice@cs.washington.edu> wrote:

> I am trying to write a strategy and want to extract the argument of a
> formula using args1.  The relevant bit of the strategy looks like
> this:  
> 
>     (if (forall-expr? form) 
>         (let ((form1 (args1 form))) 
>           <do-something>)
>         <something-else>
>     )
> 
> When I try to run the strategy, I get the following error:
> 
>     Error: No methods applicable for generic function
>            #<standard-generic-function args1> with args
>            ((FORALL (sigma):
>                     ...
>                      ))
>            of classes (forall-expr)
> 
> Am I using args1 incorrectly?  Do I need to load something special to
> use it?  If so, what?
> 
> Thank you,
> 
>     Erika Rice