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

Re: [PVS-Help] Local variables and the 'LET' strategy




Florent:  The LET variables in strategies are not Lisp variables,
and there is no way to SETQ them.  Can you give me a clearer
idea of why you'd want to setq these variables?  If you're
using them as counters, you can always bind the variable to a
closure, struct, or object and apply funcall, or setf/incf to the
appropriate field. 

-Shankar

> From:    Florent Kirchner <florent.kirchner@inria.fr>
> Subject: [PVS-Help] Local variables and the 'LET' strategy
> Date:    Tue, 22 Jun 2004 00:17:27 +0200
> To:      pvs-help@csl.sri.com
> Cc:      munoz@nianet.org
> 
> [1  <text/plain; us-ascii (quoted-printable)>]
> Dear PVS users,
> 
> I am currently running PVS 3.1, and coding a number of new strategies. In most
> of them I need to define local lisp variables, and therefore to use the (LET
> ...) strategy to declare and modify these variables.
> 
> However I cannot get PVS to do the modification part: it appears that setq
> will not affect any variables declared using LET. Below is an example of this
> behaviour: 
> 
> -----------------------------------------------------------------
> 
> Rule? (let ((x 1)
>             (dy (print (format nil "x is ~D, should be 1" x))))
>         (then (let ((dy (setq x 2)))
>                 (lisp (print (format nil "x is ~D, should be 2" x))) )
>               (lisp (print (format nil "x is ~D, should be 2" x)))) 
>       )
> "x is 1, should be 1" 
> "x is 1, should be 2" 
> "x is 1, should be 2"
> 
> ex0 :  
> 
> 	|-------
> 	[1]   FORALL (x: real): x + 0 = 0 + x
> 				
> 
> -----------------------------------------------------------------
> 
> Note that I cannot use a (let ((x 2)) ...) in place of the (setq x 2 ...) on
> line 3 because this would only declare a new 'x' variable and not modify the
> 'x' declared on line 1. 
> 
> I read the Prover Guide but could not get any information on this topic. Is
> there any other way to declare and modify local variables in strategies ?
> 
> Florent.
> [2  <application/pgp-signature>]
>