Re: [Reposting again] Re: [Repost] Instantiating multiple theories simultaneously

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

Hi Michael,

I found a fix for this particular problem, but there was one other bug
that kept it from working properly.  I'm including the patches below, they
haven't been thoroughly tested; I hope you don't mind testing it for us.

Just add it to your ~/.pvs.lisp file (create it if necessary) and restart
pvs.

Let me know how it works out,
Thanks,
Sam

--------------

(in-package :pvs)

(defmethod pp* ((decl mod-decl))
  (with-slots (modname) decl
    (write 'THEORY)
    (write-char #\=)
    (write-char #\space)
    (pprint-newline :fill)
    (pp* modname)))

(defun set-type-mapping-rhs (rhs lhs modinst mappings)
  (typecase (declaration lhs)
    (type-decl
     (if (type-value rhs)
	 (set-type* (type-value rhs) nil)
	 (type-error (expr rhs) "Type expected here")))
    (mod-decl
     (let ((threses (remove-if
			(complement
			 #'(lambda (r)
			     (and (typep (declaration r)
					 '(or module mod-decl
					      formal-theory-decl))
				  (eq (id (modname (declaration lhs)))
				      (id (theory-ref (declaration r)))))))
		      (resolutions (expr rhs)))))
       (cond ((cdr threses)
	      (type-error (expr rhs)
		"Theory name ~a is ambiguous" (expr rhs)))
	     ((null threses)
	      (type-error (expr rhs)
		"No resolution for theory name ~a" (expr rhs)))
	     (t (setf (resolutions (expr rhs)) threses)
		(when (mappings (expr rhs))
		  (set-type-mappings (name-to-modname (expr rhs))))))))
    (t (let* ((mapmodinst (lcopy modinst 'mappings mappings))
	      (subst-type (subst-mod-params (type (declaration lhs))
					    mapmodinst)))
	 (set-type* (expr rhs) subst-type)))))

(defmethod theory-ref ((d module))
  d)

(defmethod theory-ref ((d mod-decl))
  (modname d))

(defmethod theory-ref ((d formal-theory-decl))
  (theory-name d))

(defmethod theory-ref ((d modname))
  d)

(defmethod theory-ref ((d name-expr))
  (theory-ref (declaration (resolution d))))

(defvar *subst-mod-free-params* nil)

(defun subst-mod-params (obj modinst &optional theory)
  (assert *current-context*)
  (assert (modname? modinst))
  (let* ((th (or theory (get-theory modinst)))
	 (formals (formals-sans-usings th))
	 (*subst-mod-free-params* nil))
    (if (or (mappings modinst)
	    (and (actuals modinst)
		 (or (some #'(lambda (ofp) (memq ofp formals))
			   (free-params obj))
		     (some #'(lambda (a)
			       (and (name-expr? (expr a))
				    (module? (declaration (expr a)))))
			   (actuals modinst)))))
	(let* ((*generate-tccs* 'none)
	       (caches (get-subst-mod-params-caches modinst))
	       (*subst-mod-params-cache* (car caches))
	       (*subst-mod-params-eq-cache* (cdr caches))
	       (*smp-mappings* (mappings modinst))
	       (bindings (make-subst-mod-params-bindings
			  modinst formals (actuals modinst)
			  (mappings modinst) nil))
	       (nobj (subst-mod-params* obj modinst bindings)))
	  #+pvsdebug (assert (or (eq obj nobj) (not (tc-eq obj nobj))))
	  #+pvsdebug (assert (equal bindings
				    (pairlis formals (actuals modinst))))
	  #+pvsdebug (assert (or (typep nobj 'modname)
				 (fully-instantiated? nobj)))
			     nobj)
	  obj)))

(defun make-subst-mod-params-bindings (modinst formals actuals mappings
					       bindings)
  (cond ((null formals)
	 (setq *subst-mod-free-params* (mapcar #'car bindings))
	 (make-subst-mod-params-map-bindings modinst mappings bindings))
	(t (let ((pred-binding (make-subst-mod-params-pred-binding
				modinst (car formals) (car actuals) bindings)))
	     (make-subst-mod-params-bindings
	      modinst
	      (cdr formals)
	      (cdr actuals)
	      mappings
	      (let ((nbindings (make-subst-mod-params-binding
				(car formals) (car actuals) bindings)))
		(if pred-binding
		    (cons pred-binding nbindings)
		    nbindings)))))))

(defmethod make-subst-mod-params-map-bindings* ((decl mod-decl) rhs bindings)
  (let* ((thname (theory-ref (expr rhs)))
	 (interpreted-theory (generated-theory decl))
	 (source-theory (get-theory (theory-name decl)))
	 (pre-bindings (make-subst-mod-params-bindings
			thname (formals-sans-usings source-theory)
			(actuals thname)
			(extended-mappings thname interpreted-theory
					   source-theory)
			nil)))
    (acons decl rhs
	   (append (mapcar #'(lambda (x)
			       (let ((interp
				      (assq (car x)
					    (mapping interpreted-theory))))
				 (if interp
				     (cons (cdr interp) (cdr x))
				     x)))
		     pre-bindings)
		   bindings))))

(defmethod subst-mod-params* :around (obj modinst bindings)
  (declare (type hash-table *subst-mod-params-cache*))
  (or (gethash obj *subst-mod-params-eq-cache*)
      (let ((hobj (gethash obj *subst-mod-params-cache*)))
	(or hobj
	    (let ((nobj (if (and (null (mappings modinst))
				 (not (some #'(lambda (b)
						(formal-theory-decl? (car b)))
					    bindings))
				 (no-matching-free-params
				  obj *subst-mod-free-params*))
			    obj
			    (call-next-method))))
	      (when (and (typep obj 'type-expr)
			 (typep nobj 'type-expr))
		(when (print-type obj)
		  (let ((pte (subst-mod-params* (print-type obj)
						modinst bindings)))
		    (setq nobj (lcopy nobj 'print-type pte))))
		(when (from-conversion obj)
		  (let ((fconv (subst-mod-params* (from-conversion obj)
						  modinst bindings)))
		    (setq nobj (lcopy nobj 'from-conversion fconv)))))
	      (if (and (null (freevars nobj))
		       (relatively-fully-instantiated? nobj))
		  (setf (gethash obj *subst-mod-params-cache*) nobj)
		  (setf (gethash obj *subst-mod-params-eq-cache*) nobj))
	      #+pvsdebug
	      (assert (every #'(lambda (fv)
				 (or (binding? fv)
				     (member fv (freevars obj)
					     :test #'same-declaration)
				     (member fv (freevars modinst)
					     :test #'same-declaration)))
			     (freevars nobj)))
	      nobj)))))

(defun no-matching-free-params (obj frees)
  (not (some #'(lambda (b) (memq b frees))
	     (free-params obj))))

(defun relatively-fully-instantiated? (obj &optional
					   (freeparms *subst-mod-free-params*))
  (let ((frees (set-difference (free-params obj) freeparms)))
    (or (null frees)
	(let ((formals (formals-sans-usings (current-theory))))
	  (every #'(lambda (fp) (memq fp formals)) frees)))))

(defun update-current-context (theory theoryname)
  (assert (saved-context theory))
  (update-known-subtypes theory theoryname)
  (update-judgements-of-current-context theory theoryname)
  (update-conversions-of-current-context theory theoryname)
  (update-auto-rewrites-of-current-context theory theoryname)
  (update-named-theories-of-current-context theory theoryname))

(defun update-named-theories-of-current-context (theory theoryname)
  (when (saved-context theory)
    (dolist (nt (named-theories (saved-context theory)))
      (pushnew nt (named-theories *current-context*)))))

(defmethod generate-xref ((a mapping-rhs))
  (if (type-value a)
      (generate-xref (type-value a))
      (if (and (name-expr? (expr a))
	       (typep (declaration (expr a))
		      '(or module mod-decl formal-theory-decl)))
	  (generate-xref (car (resolutions (expr a))))
	  (generate-xref (expr a)))))