;;; Fix for PVS bug 861

(pvs-message "Loading patches PVS3.2")

(defmethod copy-untyped* ((ex fieldappl))
  (with-slots (id actuals argument) ex
    (copy ex
      'id id
      'type nil
      'actuals (copy-untyped* actuals)
      'argument (copy-untyped* argument))))

;;; Fix for PVS bug 862

(defun exportable? (decl theory)
  (assert *current-context*)
  (or (eq (module decl) (current-theory))
      (from-prelude? decl)
      (from-prelude-library? decl)
      (unless (or (from-prelude? theory)
		  (from-prelude-library? theory))
	(let ((exp (exporting theory)))
	  (if (eq (module decl) theory)
	      (or (eq (kind exp) 'default)
		  (if (eq (names exp) 'all)
		      (not (member decl (but-names exp) :test #'expname-test))
		      (member decl (names exp) :test #'expname-test)))
	      (or ;;(eq (kind exp) 'default)
	       (and (rassoc (module decl) (closure exp) :test #'eq)
		    (exportable? decl (module decl)))))))))

;;; Fix for PVS bug 863

(defun get-immediate-using-ids (theory)
  (mapcan #'(lambda (d)
	      (get-immediate-using-ids* (theory-name d) theory))
    (remove-if-not #'mod-or-using? (all-decls theory))))

(defun get-immediate-using-ids* (tn theory &optional ids)
  (if (null tn)
      (nreverse ids)
      (let ((id (unless (library tn)
		   (if (eq (id tn) (id theory))
		       (if ids
			   (type-error tn
			     "Target ~a may not reference itself" (id theory))
			   (type-error tn
			     "Theory ~a may not import itself" (id theory)))
		       (id tn)))))
	(get-immediate-using-ids*
	 (target tn)
	 theory
	 (if id (cons id ids) ids)))))

(defmethod untypecheck-theory ((ex name))
  (assert (not (memq ex (list *boolean* *number*))))
  (when (next-method-p) (call-next-method))
  (untypecheck-theory (actuals ex))
  (untypecheck-theory (mappings ex))
  (untypecheck-theory (target ex))
  (setf (resolutions ex) nil))

(defmethod compare* ((old name) (new name))
  (and (compare* (mod-id old) (mod-id new))
       (compare* (library old) (library new))
       (and (or (and (null (actuals old)) (null (actuals new)))
		(and (actuals old) (actuals new)))
	    (compare* (actuals old) (actuals new)))
       (and (or (and (null (mappings old)) (null (mappings new)))
		(and (mappings old) (mappings new)))
	    (compare* (mappings old) (mappings new)))
       (and (or (and (null (target old)) (null (target new)))
		(and (target old) (target new)))
	    (compare* (target old) (target new)))
       (compare* (id old) (id new))))

;;; Fix for PVS bug 866

(defun get-interpreted-mapping (theory interpretation theory-name)
  (let* ((*subst-mod-params-map-bindings* nil)
	 (mapping (make-subst-mod-params-map-bindings
		   theory-name (mappings theory-name) nil))
	 (int-decls (when interpretation (all-decls interpretation))))
    (when interpretation
      (dolist (decl (interpretable-declarations theory))
	(unless (assq decl mapping)
	  (let ((fdecl (find decl int-decls
			     :test #'(lambda (x y)
				       (and (declaration? y)
					    (same-id x y))))))
	    (unless (eq decl fdecl)
	      (push (cons decl fdecl) mapping))))))
    #+pvsdebug (assert (every #'cdr mapping))
    mapping))

(defmethod subst-mod-params* ((expr name-expr) modinst bindings)
  (declare (ignore modinst))
  (let* ((decl (declaration expr))
	 (act (cdr (assq decl bindings))))
    (if act
	(if (declaration? act)
	    (mk-name-expr (id act) nil nil
			  (mk-resolution act
					 (mk-modname (id (module act)))
					 (type act)))
	  (expr act))
      (let ((nexpr (call-next-method)))
	(if (eq nexpr expr)
	    expr
	  (let ((ntype (type (resolution nexpr))))
	    (lcopy nexpr 'type ntype)))))))

;;; Fix for PVS bug 867

(defun get-theory-from-binfile (filename)
  (let* ((file (make-binpath filename))
	 (start-time (get-internal-real-time))
	 (*bin-theories-set* nil)
	 (vtheory (ignore-lisp-errors (fetch-object-from-file file)))
	 (load-time (get-internal-real-time)))
    (if (and (listp vtheory)
	     (integerp (car vtheory))
	     (= (car vtheory) *binfile-version*))
	(let* ((theory (cdr vtheory))
	       (*restore-object-hash* (make-hash-table :test #'eq))
	       (*restore-objects-seen* nil)
	       (*assert-if-arith-hash* (make-hash-table :test #'eq))
	       (*subtype-of-hash* (make-hash-table :test #'equal))
	       (*current-context* (prerestore-context (saved-context theory))))
	  (assert (current-theory))
	  (assert (judgement-types-hash (judgements *current-context*)))
	  (restore-object theory)
	  (assert (datatype-or-module? theory))
	  (assert (not (eq (lhash-next (declarations-hash (saved-context theory)))
			   'prelude-declarations-hash)))
	  (postrestore-context *current-context*)
	  (pvs-message
	   "Restored theory from ~a.bin in ~,2,-3fs (load part took ~,2,-3fs)"
	   filename (realtime-since start-time)
	   (floor (- load-time start-time) millisecond-factor))
	  theory)
      (progn (pvs-message "Bin file version for ~a is out of date"
			  filename)
	     (ignore-errors (delete-file file))
	     (dolist (thid *bin-theories-set*)
	       (remhash thid *pvs-modules*))
	     nil))))

;;; Fix for PVS bug 870

(defun pc-sort (decls &optional theory)
  (assert (or theory *current-context*))
  (let* ((th (or theory (current-theory)))
	 (imps (cons th (complete-importings th))))
    (assert (every #'(lambda (x)
		       (or (from-prelude? x)
			   (from-prelude-library? x)
			   (memq (module x) imps)))
		   decls))
    (sort decls
	  #'(lambda (x y)
	      (cond ((eq (module x) (module y))
		     (string< (id x) (id y)))
		    ((from-prelude? y)
		     (or (not (from-prelude? x))
			 (string< (id (module x)) (id (module y)))))
		    ((from-prelude-library? y)
		     (and (not (from-prelude? x))
			  (or (not (from-prelude-library? x))
			      (string< (id (module x)) (id (module y))))))
		    (t (and (not (from-prelude? x))
			    (memq (module y) (memq (module x) imps)))))))))

(defun complete-importings (th)
  (multiple-value-bind (imps impnames)
      (all-importings th)
    (multiple-value-call #'add-generated-interpreted-theories
			 (add-generated-adt-theories
			  (cons th imps)
			  (cons (mk-modname (id th)) impnames))
			 th)))

;;; Fix for PVS bug 872

(defun theory-formula-alist (file)
  (let* ((theories (cdr (gethash file *pvs-files*)))
	 (ce (unless theories (context-entry-of file))))
    (cond (theories
	   (mapcar #'(lambda (th)
		       (cons (id th)
			     (mapcar #'id
				     (remove-if-not #'(lambda (d)
							(provable-formula? d))
						    (all-decls th)))))
		   theories))
	  (ce
	   (mapcar #'(lambda (te)
		       (cons (te-id te)
			     (mapcar #'fe-id (te-formula-info te))))
		   (ce-theories ce))))))


;;; RWB removed bug fix 873 because it was causing problems

;;; Fix for PVS bug 878

(defmethod restore-object* :around ((obj nonempty-type-decl))
  (call-next-method)
  (set-nonempty-type (type-value obj)))

;;; Fix for PVS bug 898

(defun xt-expr (expr)
  (case (sim-term-op expr)
    (NUMBER-EXPR (xt-number-expr expr))
    (STRING-EXPR (xt-string-expr expr))
    (NAME-EXPR (xt-name-expr expr))
    (LIST-EXPR (xt-list-expr expr))
    ;;(true (xt-true expr))
    ;;(false (xt-false expr))
    (REC-EXPR (xt-rec-expr expr))
    (TUPLE-EXPR (xt-tuple-expr expr))
    (TERM-EXPR (xt-term-expr expr))
    (UNARY-TERM-EXPR (xt-unary-term-expr expr))
    (FIELDEX (xt-fieldex expr))
    (PROJEX (xt-projex expr))
    (FIELDAPPL (xt-fieldappl expr))
    (PROJAPPL (xt-projappl expr))
    ;;(intype (xt-intype expr))
    (COERCION (xt-coercion expr))
    (IF-EXPR (xt-if-expr expr))
    (APPLICATION (xt-application expr))
    (BIND-EXPR (xt-bind-expr expr))
    (NAME-BIND-EXPR (xt-name-bind-expr expr))
    (SET-EXPR (xt-set-expr expr))
    (LET-EXPR (xt-let-expr expr))
    (WHERE-EXPR (xt-where-expr expr))
    (UPDATE-EXPR (xt-update-expr expr))
    ;;(override-expr (xt-override-expr expr))
    (CASES-EXPR (xt-cases-expr expr))
    (COND-EXPR (xt-cond-expr expr))
    (TABLE-EXPR (xt-table-expr expr))
    (SKOVAR (xt-skovar expr))
    (BRACK-EXPR (xt-brack-expr expr))
    (PAREN-VBAR-EXPR (xt-paren-vbar-expr expr))
    (BRACE-VBAR-EXPR (xt-brace-vbar-expr expr))
    (t (error "Unrecognized expr - ~a" expr))))


;; ;;;BUG Fix 873 take two

;;   (defun add-tcc-bindings (expr conditions substs antes &optional bindings)
;;     (if (typep (car conditions) 'bind-decl)
;;         ;; Recurse till there are no more bindings, so we build
;;         ;;  FORALL x, y ... rather than FORALL x: FORALL y: ...
;;         (let* ((bd (car conditions))
;;   	     (nbd (or (cdr (assq bd substs)) bd)))
;;   	(add-tcc-bindings expr (cdr conditions) substs antes
;;   			  (if (or (occurs-in bd expr)
;;   				  (occurs-in bd antes)
;;   				  (occurs-in bd substs)
;;   				  (possibly-empty-type? (type bd)))
;;   			      (cons nbd bindings)
;;   			      bindings)))
;;         ;; Now we can build the universal closure
;;         (let* ((nbody (substit (if antes
;;   				(make!-implication
;;   				  (make!-conjunction* (reverse antes))
;;   				  expr)
;;   				expr)
;;   		      substs))
;;   	     (nbindings (get-tcc-closure-bindings bindings nbody))
;;   	     (nexpr (if nbindings
;;   			(make!-forall-expr nbindings nbody)
;;   			nbody)))
;;   	(add-tcc-conditions* nexpr conditions substs nil))))

;;   (defun get-tcc-closure-bindings (bindings body)
;;     (let ((fvars (freevars body)))
;;       (remove-if (complement
;;   		#'(lambda (bd)
;;   		    (or (member bd fvars :key #'declaration)
;;   			(possibly-empty-type? (type bd)))))
;;         bindings)))