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

[PVS-Help] Semantic attachments for evaluating quantifiers


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?


Best wishes,