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

Re: [PVS-Help] Semantic attachments for evaluating quantifiers



Hi Aditya,

It's not currently possible to give an attachment to FORALL or
EXISTS, because they are not constants in PVS.  You can define
your own exists, and give an attachment to it (similar to
exists1 in the prelude).  Note, however, that exists1 cannot be
used because it refers to an uninterpreted type so it's
definition cannot be generated.  You will need to make sure the
bindings in your definition are bounded.  Also, unless your use
of exists always has the same bindings with the same types, you
will need several definitions.

As for the problem with .pvs.lisp - it is not read in the
current context, but only from your home directory (similar to
the .pvsemacs file).

Hope this helps,
Regards,
Sam Owre

Aditya Kanade <aditya@cse.iitb.ac.in> wrote:

> Hi,
> 
> I need to evaluate temporal formulae in PVS. For that firstly I've to
> give semantic attachments for quantifiers. I tried the following:
> 
> (push (mk-name '|exists| nil '|prelude|) *pvs2cl-primitives*)
> 
> ;; 2 underscores in pvs__exists as it takes more than one argument
> ;; Ref. [Evaluating, Testing, ... PVS specifications]
> 
> (defun |pvs__exists| (p type)
>   (let ((result nil))
>   (dolist (elt type result)
> 	(setq result (or (p elt) result))
> 	(when result (return t)))))
> 
> This is not working. Can anyone point out the problem (I think I don't
> know how "exists" takes its arguments) and suggest a solution?
> 
> Secondly, in the above said reference, the name of attached function
> starts with "PVS_" and the lisp code is supposed to written in
> .pvs.lisp file in current context (or home). But that too didn't work
> for me. I'd to start the name of attached function with "pvs_" and had
> to put the code in pvs-attachments file in the current context. Is
> there any change in recent implementations or is it a side effect of
> loading PVSio package?
> 
> Thanks.
> 
> Best wishes,
> Aditya.