Re: Using the PVS ground evaluator

[Sam Owre <owre@csl.sri.com>]

Hi Pertti,

One of the significant changes in PVS 3.0 was a move to
case-sensitive lisp, and some of the ground evaluator functions
were not fully tested.  I'm including all the fixed functions
below.  Just add them to your ~/.pvs.lisp file (creating it if
necessary) and your examples should work.

Regards,
Sam

;;; ----- Add to ~/.pvs.lisp -------
(in-package :pvs)

(defun pvs_WHEN (x) (or (svref x 0)(not (svref x 1))))
(defun pvs_AND (x)(and (svref x 0)(svref x 1)))
(defun pvs_OR (x) (or (svref x 0)(svref x 1)))
(defun pvs_NOT (x) (not x))

(defmacro pvs__WHEN (x y) `(or (not ,y) ,x))
(defmacro pvs__AND (x y) `(and ,x ,y))
(defmacro pvs__OR (x y)  `(or ,x ,y))
(defmacro pvs__rem (y)
  (let ((xx (gentemp))
	(yy (gentemp)))
    `(function
      (lambda (x)
	(let ((,xx (the integer x))
	      (,yy (the integer ,y)))
       (if (< ,xx ,yy) ,xx (rem ,xx ,yy)))))))

(defun make-binding-ids-without-dups (bindings aux)
  (if (consp bindings)
      (let ((id (id (car bindings))))
	(if (or (memq id aux)
		(constantp id)) ; SO 2002-07-31 - lisp constants are also
					; problematic (e.g., t or nil).
	    (make-binding-ids-without-dups
	     (cdr bindings)
	     (cons (gentemp id) aux))
	    (make-binding-ids-without-dups
	     (cdr bindings)
	     (cons id aux))))
      (nreverse aux)))

(defun mk-newconstructor (id accessor-ids &optional (counter 0))
  (let* ((const-str (format nil "~a_~a" id counter))
	 (const-str? (find-symbol const-str))
	 (mk-str? (find-symbol (format nil "MAKE-~a" const-str)))
	 (rec-str? (find-symbol (format nil "~a-p" const-str)))
	 (acc-strs? (loop for acc in accessor-ids
			 thereis
			 (find-symbol (format nil "~a_~a"
					const-str
					acc)))))
    (if (or const-str? mk-str? rec-str? acc-strs?)
	(mk-newconstructor id accessor-ids (1+ counter))
	(intern const-str))))

(defun pvs2cl-constructor (constructor datatype) ;;fix multi-constructor accessors
  (cond ((enum-adt? datatype)
	 (let* ((pos (position (id constructor)
			       (constructors (adt datatype))
			       :test #'eq :key #'id))
		(decl (declaration constructor))
		(recognizer (recognizer constructor))
		(rec-decl (declaration recognizer))
		(rec-id (mk-newsymb (id recognizer)))
		(rec-defn `(defun ,rec-id (x) (eql x ,pos))))
	   (make-eval-info decl)
	   (setf (in-name decl) pos)
	   (make-eval-info rec-decl)
	   (setf (in-name rec-decl) rec-id)
	   (setf (definition (in-defn rec-decl))
		 rec-defn)
	   (eval rec-defn)
	   (compile rec-id)
	   pos))
	(t  (let* ((id (id constructor))
		   (accessors (accessors constructor))
		   (accessor-ids (mapcar #'id accessors))
		   (struct-id (mk-newconstructor id
						 accessor-ids))
		   (constructor-symbol (makesym "MAKE-~a" struct-id))
		   (defn `(defstruct (,struct-id (:constructor ,constructor-symbol 
							       ,accessor-ids))
			    ,@accessor-ids)))
	      (make-eval-info (declaration constructor))
	      (setf (definition (in-defn (declaration constructor)))
		    defn)
	      (setf (in-name (declaration constructor))
		    constructor-symbol)
	      (make-eval-info (declaration (recognizer constructor)))
	      (setf (in-name (declaration (recognizer constructor)))
		    (makesym "~a-p" struct-id))
	      (eval defn)
	      (loop for x in accessors
		    do (progn (make-eval-info (declaration x))
			      (setf (in-name (declaration x))
				    (makesym "~a-~a" struct-id (id x)))))
	      ))))

(defun pvs2cl-primitive (expr)
  (cond ((eq (id expr) 'TRUE) t)
	((eq (id expr) 'FALSE) nil)
	((eq (id expr) '|null|) nil)
	((and (eq (id expr) '-) ;;hard to distinguish unary,binary.
	      (tupletype? (domain (find-supertype (type expr)))))
	 (intern (format nil "pvs_--")))
	(t (intern (format nil "pvs_~a" (id expr))))))

(defun pvs2cl-primitive2 (expr) ;;assuming expr is an id
  (let* ((id (id expr))
	 (modinst  (module-instance expr))
	 (acts (when modinst (actuals modinst))))
    (if (and (eq id '=)
	     (eq (id modinst) '|equalities|)
	     (tc-eq  (type-value (car acts)) *number*))
	'=
	(intern (format nil "pvs__~a" id)))))