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

Re: [PVS-Help] PVS bugs 968, 948, and 978



Jerry James <Jerry.James@usu.edu> wrote:

> Could the description of the fix for PVS bug 968 be updated to include
> the definition of make-nonclashing-bindings, which does not exist in the
> PVS 4.0 source code?  Also, could the fix for bug 948 / 978 be made
> public or, failing that, be made available to me?
> 
> Thanks,
> -- 
> Jerry James, Assistant Professor        Jerry.James@usu.edu
> Computer Science Department             http://www.cs.usu.edu/~jerry/
> Utah State University

Hi Jerry,

I added the code to the bug reports for 968 and 978, and I'm including it
below.  Let me know how it works for you.

Regards,
Sam

-----------

;;; Fix for bug # 968

(defmethod replace-expr* (lhs rhs (expr binding-expr) lastopinfix?)
  (if (replace-eq lhs expr)
      (parenthesize rhs lastopinfix?)
      (let* ((*bound-variables* (append (bindings expr) *bound-variables*))
	     (nexpr (replace-expr* lhs rhs (expression expr) nil))
	     (new-bindings (unless (eq nexpr (expression expr))
			     (make-nonclashing-bindings (bindings expr) rhs)))
	     (nalist (when new-bindings
		       (substit-pairlis (bindings expr) new-bindings nil))))
	(if new-bindings
	    (lcopy expr
	      'bindings new-bindings
	      'expression (substit nexpr nalist))
	    (lcopy expr 'expression nexpr)))))

(defun make-nonclashing-bindings (bindings expr)
  (let ((free-ids (collect-free-ids expr)))
    (when (some #'(lambda (bd) (memq (id bd) free-ids)) bindings)
      (mapcar #'(lambda (bd)
		  (if (memq (id bd) free-ids)
		      (copy bd 'id (new-boundvar-id (id bd) expr))
		      bd))
	bindings))))

;;; collect-free-ids

(defun collect-free-ids (expr)
  (let ((*bound-variables* nil))
    (collect-free-ids* expr nil)))

(defmethod collect-free-ids* ((l list) fids)
  (if (null l)
      fids
      (collect-free-ids*
       (cdr l)
       (collect-free-ids* (car l) fids))))

(defmethod collect-free-ids* ((ex name-expr) fids)
  (unless (memq (declaration ex) *bound-variables*)
    (pushnew (id ex) fids)))

(defmethod collect-free-ids* ((ex number-expr) fids)
  fids)

(defmethod collect-free-ids* ((ex record-expr) fids)
  (collect-free-ids* (assignments ex) fids))

(defmethod collect-free-ids* ((ex tuple-expr) fids)
  (collect-free-ids* (exprs ex) fids))

(defmethod collect-free-ids* ((ex projection-expr) fids)
  (collect-free-ids* (actuals ex) fids))

(defmethod collect-free-ids* ((ex injection-expr) fids)
  (collect-free-ids* (actuals ex) fids))

(defmethod collect-free-ids* ((ex injection?-expr) fids)
  (collect-free-ids* (actuals ex) fids))

(defmethod collect-free-ids* ((ex extraction-expr) fids)
  (collect-free-ids* (actuals ex) fids))

(defmethod collect-free-ids* ((ex projection-application) fids)
  (collect-free-ids*
   (argument ex)
   (collect-free-ids* (actuals ex) fids)))

(defmethod collect-free-ids* ((ex injection-application) fids)
  (collect-free-ids*
   (argument ex)
   (collect-free-ids* (actuals ex) fids)))

(defmethod collect-free-ids* ((ex injection?-application) fids)
  (collect-free-ids*
   (argument ex)
   (collect-free-ids* (actuals ex) fids)))

(defmethod collect-free-ids* ((ex extraction-application) fids)
  (collect-free-ids*
   (argument ex)
   (collect-free-ids* (actuals ex) fids)))

(defmethod collect-free-ids* ((ex field-application) fids)
  (collect-free-ids* (argument ex) fids))

(defmethod collect-free-ids* ((ex application) fids)
  (collect-free-ids*
   (operator ex)
   (collect-free-ids* (argument ex) fids)))

(defmethod collect-free-ids* ((ex binding-expr) fids)
  (let ((*bound-variables* (append (bindings ex) *bound-variables*)))
    (collect-free-ids* (expression ex) fids)))

(defmethod collect-free-ids* ((ex cases-expr) fids)
  (collect-free-ids*
   (expression ex)
   (collect-free-ids*
    (selections ex)
    (collect-free-ids* (else-part ex) fids))))

(defmethod collect-free-ids* ((ex selection) fids)
  (let ((*bound-variables* (append (args ex) *bound-variables*)))
    (collect-free-ids*
     (constructor ex)
     (collect-free-ids* (expression ex) fids))))

(defmethod collect-free-ids* ((ex update-expr) fids)
  (collect-free-ids*
   (expression ex)
   (collect-free-ids* (assignments ex) fids)))

(defmethod collect-free-ids* ((ass assignment) fids)
  (collect-free-ids*
   (arguments ass)
   (collect-free-ids* (expression ass) fids)))

(defmethod collect-free-ids* ((act actual) fids)
  (if (type-value act)
      fids
      (collect-free-ids* (expr act) fids)))

;;; Fix for bug # 978

(eval-when (eval compile load)
  (fmakunbound 'get-judgement-tcc))

(defvar *possible-judgements* nil)

(defun pc-complete (decl)
  (let* ((*dependings* nil)
	 (*proved-dependings* nil)
	 (*unproved-dependings* nil)
	 (*defn-dependings* nil)
	 (*axiom-dependings* nil)
	 (*assumption-dependings* nil)
	 (*depending-chain* nil)
	 (*depending-cycles* nil)
	 (*in-checker* nil)
	 (*current-context* (context decl))
	 (*possible-judgements* (possible-judgements decl))
	 (fdecls (union (union (refers-to decl)
			       (proof-refers-to decl))
			(assuming-tccs decl)))
	 (decls (union fdecls *possible-judgements*)))
    (pc-analyze* decls)
    (mapc #'(lambda (y)
	      (cond ((typep y 'formula-decl)
		     (if (axiom? y)
			 (push y *axiom-dependings*)
			 (if (assumption? y)
			     (push y *assumption-dependings*)
			     (if (proved? y)
				 (push y *proved-dependings*)
				 (push y *unproved-dependings*)))))
		    ((and (or (typep y 'const-decl)
			      (typep y 'def-decl))
			  (definition y))
		     (push y *defn-dependings*))))
	     *dependings*)
    (cond (*depending-cycles* "circular")
	  ((and (null *unproved-dependings*)
		(proved? decl))
	   "complete")
	  (t "incomplete"))))

(defmethod pc-analyze ((decl formula-decl))
  (let* ((*dependings* nil)
	 (*proved-dependings* nil)
	 (*unproved-dependings* nil)
	 (*defn-dependings* nil)
	 (*axiom-dependings* nil)
	 (*assumption-dependings* nil)
	 (*depending-chain* nil)
	 (*depending-cycles* nil)
	 (*current-context* (context decl))
	 (*possible-judgements* (possible-judgements decl))
	 (fdecls (union (union (refers-to decl)
			       (proof-refers-to decl))
			(assuming-tccs decl)))
	 (decls (union fdecls *possible-judgements*)))
    (pc-analyze* decls)
    (mapc #'(lambda (y)
	      (cond ((typep y 'formula-decl)
		     (if (axiom? y)
			 (push y *axiom-dependings*)
			 (if (assumption? y)
			     (push y *assumption-dependings*)
			     (if (proved? y)
				 (push y *proved-dependings*)
				 (push y *unproved-dependings*)))))
		    ((and (or (typep y 'const-decl)
			      (typep y 'def-decl))
			  (definition y))
		     (push y *defn-dependings*))
		    (t)))
	  *dependings*)
    (if (axiom? decl)
	(format t "~%~a.~a is an axiom." (id (module decl)) (id decl))
	(if (proved? decl)
	    (format t "~%~a.~a has been PROVED." (id (module decl)) (id decl))
	    (format t "~%~a.~a is UNPROVED." (id (module decl)) (id decl))))
    (when *depending-cycles*
      (format t "~%~%***Warning***: The proof chain for ~a is CIRCULAR in the following:"
	(id decl))
      (loop for x in *depending-cycles*
	    do (format t "~%   ~a.~a" (id (module x))(id x))))
    (cond
      ((and (null *unproved-dependings*) (proved? decl))
       (format t "~%~%  The proof chain for ~a is COMPLETE." (id decl)))
      ((proved? decl)
       (format t "~%~%  The proof chain for ~a is INCOMPLETE.~
                  ~%  It depends on the following unproved conjectures:"
	 (id decl))
       (loop for x in (pc-sort *unproved-dependings*)
	     do
	     (format t "~%    ~a.~a" (id (module x)) (id x)))))
    (when *proved-dependings*
      (format t "~%~%  ~a depends on the following proved theorems:"
	(id decl))
      (loop for x in (pc-sort *proved-dependings*)
	     do
	     (format t "~%    ~a.~a" (id (module x)) (id x))))
    (when *axiom-dependings*
      (format t "~%~%  ~a depends on the following axioms:"
	(id decl))
      (loop for x in (pc-sort *axiom-dependings*)
	     do
	     (format t "~%    ~a.~a" (id (module x)) (id x))))
    (when *defn-dependings*
      (format t "~%~%  ~a depends on the following definitions:"
	(id decl))
      (loop for x in (pc-sort *defn-dependings*)
	     do
	     (format t "~%    ~a.~a" (id (module x)) (id x))))
    (when *assumption-dependings*
      (format t "~%~%  ~a depends on the following assumptions:"
	(id decl))
      (loop for x in (pc-sort *assumption-dependings*)
	     do
	     (format t "~%    ~a.~a" (id (module x)) (id x))))
    (when *possible-judgements*
      (format t "~%~%  ~a may depend on the following judgements:"
	(id decl))
      (loop for x in (pc-sort *possible-judgements*)
	     do
	     (format t "~%    ~a.~a" (id (module x)) (id x))))))

(defun possible-judgements (decl)
  ;;; We collect all judgements of the current context that might be
  ;;; involved in the proof of the decl.  This includes all subtype and
  ;;; number judgements, as well as any name or application judgements
  ;;; whose decl is in decls.
  ;;; [owre - 2005-09-11] Now just collect subtype judgements.
  (let ((jtccs nil))
    (dolist (jdecl (if (from-prelude? decl)
		       (judgement-declarations
			(judgements (context decl)))
		       (remove-if #'from-prelude?
			 (judgement-declarations
			  (judgements (context decl))))))
      (let ((tcc (get-judgement-tcc jdecl decl)))
	(when tcc (push tcc jtccs))))
;;     (do-all-declarations #'(lambda (decl)
;; 			     (let ((tcc (get-judgement-tcc decl decls)))
;; 			       (when tcc (push tcc jtccs)))))
    jtccs))


(defmethod get-judgement-tcc ((jdecl subtype-judgement) decl)
  ;; This one is difficult, since it is not obvious when the judgement comes
  ;; into play.  Just collect them all.
  (if (generated-by jdecl)
      (get-judgement-tcc (generated-by jdecl) decl)
      (find-if #'judgement-tcc? (generated jdecl))))

(defmethod get-judgement-tcc ((jdecl number-judgement) decl)
  ;; Similarly, don't really know when a number-judgement kicked in.
;;   (if (generated-by jdecl)
;;       (get-judgement-tcc (generated-by jdecl) decls)
;;       (find-if #'judgement-tcc? (generated jdecl)))
  )

(defmethod get-judgement-tcc ((jdecl name-judgement) decl)
  ;; Ignore it, if the associated declaration is not in decls
;;  (when (memq (declaration (name jdecl)) decls)
;;     (if (generated-by jdecl)
;; 	(get-judgement-tcc (generated-by jdecl) decls)
;; 	(when (memq (declaration (name jdecl)) decls)
;; 	  (find-if #'judgement-tcc? (generated jdecl)))))
  )

(defmethod get-judgement-tcc ((jdecl application-judgement) decl)
;;   (when (memq (declaration (name jdecl)) decls)
;;     (if (generated-by jdecl)
;; 	(get-judgement-tcc (generated-by jdecl) decls)
;; 	(find-if #'judgement-tcc? (generated jdecl))))
  )

(defmethod get-judgement-tcc ((jtcc judgement-tcc) decl)
  (get-judgement-tcc (generated-by jtcc) decl))
  
(defmethod get-judgement-tcc (decl fdecl)
  (declare (ignore decl fdecl))
  nil)

(defmethod pc-analyze* ((fdecl formula-decl))
  (let ((*depending-chain* *depending-chain*))
    (cond ((and (not (judgement-tcc? fdecl))
		(memq fdecl *depending-chain*))
	   (pushnew fdecl *depending-cycles*)
	   *dependings*)
	  ((memq fdecl *dependings*)
	   *dependings*)
	  (t (push fdecl *dependings*)
	     (push fdecl *depending-chain*)
	     (cond ((from-prelude? fdecl)
		    *dependings*)
		   ((or (axiom? fdecl)
			(assumption? fdecl))
		    ;; No need to include proof-refers-to in this case
		    (let ((decls (union (refers-to fdecl)
					(remove-if-not #'tcc?
					  (generated fdecl)))))
		      (pc-analyze* (union decls (possible-judgements fdecl)))))
		   (t (let ((decls (union (union (refers-to fdecl)
						 (proof-refers-to fdecl))
					  (remove-if-not #'tcc?
					    (generated fdecl)))))
			(pc-analyze* (union decls (possible-judgements fdecl))))))))))