;; patch for coproducts 18.6.03

(in-package :pvs)

(defun change-application-class-if-needed (ex)
  (let ((operator (operator ex)))
    (cond ((and (typep operator 'name-expr)
		(boolean-op? operator '(NOT AND & OR IMPLIES => IFF <=> WHEN)))
	   (change-to-propositional-class ex))
	  ((and (typep operator 'name-expr)
		(eq (id operator) '=)
		(eq (id (module-instance operator)) '|equalities|))
	   (change-to-propositional-class ex))
	  ((and (typep operator 'name-expr)
		(eq (id operator) '/=)
		(eq (id (module-instance operator)) '|notequal|))
	   (change-to-propositional-class ex))
	  ((and (typep operator 'name-expr)
		(eq (id operator) 'IF)
		(eq (id (module-instance operator)) '|if_def|)
		(not (typep ex 'branch)))
	   (change-class ex 'branch)
	   (unless (tuple-expr? (argument ex))
	     (setf (argument ex)
		   (make!-projected-arg-tuple-expr*
		    (make-projections (argument ex))))))
	  ((typep operator 'injection-expr)
	   (change-class ex 'injection-application
			 'index (index operator)
			 'id (index operator)))
	  ((typep operator 'injection?-expr)
	   (change-class ex 'injection?-application
			 'index (index operator)
			 'id (id operator))))))


(defmethod accessor? ((fn injection-expr))
  nil)

(defmethod translate-to-prove ((expr injection-expr))
  (let* ((id (make-new-variable '|x| expr))
	 (cotuptype (find-supertype (range (find-supertype (type expr)))))
	 (bd (make-bind-decl id (domain (find-supertype (type expr)))))
	 (varex (make-variable-expr bd)))
    (translate-to-prove
     (make!-lambda-expr (list bd)
       (make!-injection-application (index expr) varex cotuptype)))))



;; patches for #752 (unstable proofs), #756 (invisible lemma) 30.3.03


(defun copy-subst-mod-params-cache ()
  (let ((new-hash (make-hash-table
		   :hash-function 'pvs-sxhash
		   :test 'strong-tc-eq
		   :size (floor (hash-table-size *all-subst-mod-params-caches*)
				1.5384616))))
    (maphash #'(lambda (modname hashes)
		 (setf (gethash modname new-hash)
		       (cons (copy (car hashes)) (copy (cdr hashes)))))
	     *all-subst-mod-params-caches*)
    new-hash))

(defun filter-equality-resolutions* (reses &optional result)
  (if (null reses)
      (nreverse result)
      (multiple-value-bind (creses nreses)
	  (split-on #'(lambda (res)
			(strict-compatible? (type res) (type (car reses))))
		    reses)
	(filter-equality-resolutions*
	 nreses
	 (if (null creses)
	     (cons (car reses) result)
	     (cons (let ((ctype (reduce #'compatible-type creses :key #'type)))
		     (or (find-if #'(lambda (res) (tc-eq (type res) ctype))
			   creses)
			 (make-resolution (declaration (car reses))
			   (copy (module-instance (car reses))
			     'actuals (list (mk-actual ctype))))))
		   result))))))

;; patches for #748 (auto-rewrite decls) 16.03.03

(defmethod typecheck* ((decl auto-rewrite-decl) expected kind arguments)
  (declare (ignore expected kind arguments))
  (unless (typechecked? decl)
    (typecheck* (rewrite-names decl) nil nil nil))
  (add-auto-rewrite-to-context decl)
  decl)

(defun add-auto-rewrite-to-context (decl)
  (pushnew decl (auto-rewrites *current-context*))
  (let ((new-disabled
	 (mapcar #'(lambda (disabled)
		     (remove-enabled-rewrites disabled (rewrite-names decl)))
	   (disabled-auto-rewrites *current-context*))))
    (unless (equal new-disabled (disabled-auto-rewrites *current-context*))
      (setf (disabled-auto-rewrites *current-context*) new-disabled))))  

(defun remove-enabled-rewrites (disabled names)
  (let ((diff (remove-if #'(lambda (rname)
			     (member rname names :test #'tc-eq))
		  (rewrite-names disabled))))
    (if (eq diff (rewrite-names disabled))
	disabled
	(copy disabled 'rewrite-names diff))))

(defun decl-context (decl &optional include?)
  (let* ((*generate-tccs* 'none)
	 (theory (module decl))
	 (all-decls (reverse (all-decls theory)))
	 (pdecls (or (memq decl all-decls) (cons decl all-decls)))
	 (prev-decls (if include?
			 pdecls
			 (cdr pdecls)))
	 (prev-imp (find-if #'mod-or-using? prev-decls))
	 (rem-decls (if (and prev-imp (saved-context prev-imp))
			(ldiff prev-decls (memq prev-imp prev-decls))
			prev-decls))
	 (*current-theory* theory)
	 (*current-context*
	  (if (or (not prev-imp) (saved-context prev-imp))
	      (copy-context (cond (prev-imp
				   (saved-context prev-imp))
				  ((from-prelude? decl)
				   (let ((prevp
					  (cadr (memq theory
						      (reverse
						       *prelude-theories*)))))
				     (saved-context
				      (if (datatype? prevp)
					  (or (adt-reduce-theory prevp)
					      (adt-map-theory prevp)
					      (adt-theory prevp))
					  prevp))))
				  (t (or *prelude-library-context*
					 *prelude-context*)))
			    theory
			    (reverse rem-decls)
			    (or (car rem-decls) decl))
	      (make-new-context theory))))
    ;;; Need to clear this hash or the known-subtypes table won't get
    ;;; updated properly - see add-to-known-subtypes.
    (clrhash *subtype-of-hash*)
    (dolist (d (reverse rem-decls))
      (typecase d
	(lib-decl
	 (check-for-importing-conflicts d)
	 (put-decl d (current-declarations-hash)))
	((or mod-decl theory-abbreviation-decl formal-theory-decl)
	 (put-decl d (current-declarations-hash))
	 (let* ((thname (theory-name d))
		(th (get-theory thname)))
	   (add-exporting-with-theories th thname))
	 (setf (saved-context d) (copy-context *current-context*)))
	(importing
	 (let* ((thname (theory-name d))
		(th (get-theory thname)))
	   (add-usings-to-context* th thname))
	 (setf (saved-context d) (copy-context *current-context*)))
	(subtype-judgement (add-to-known-subtypes (subtype d) (type d)))
	(judgement (add-judgement-decl d))
	(conversionminus-decl (disable-conversion d))
	(conversion-decl (push d (conversions *current-context*)))
	(auto-rewrite-minus-decl (push d (disabled-auto-rewrites
					 *current-context*)))
	(auto-rewrite-decl (add-auto-rewrite-to-context  d))
	(type-def-decl (unless (enumtype? (type-expr d))
			 (put-decl d (current-declarations-hash))))
	(declaration (put-decl d (current-declarations-hash)))
	(datatype nil)))
    (when (from-prelude? decl)
      (let* ((prevp (cadr (memq theory
				(reverse *prelude-theories*))))
	     (pths (if (datatype? prevp)
		       (delete-if #'null
			 (list (adt-theory prevp)
			       (adt-map-theory prevp)
			       (adt-reduce-theory prevp)))
		       (list prevp))))
	(dolist (pth pths)
	  (setf (gethash pth (using-hash *current-context*))
		(list (mk-modname (id pth)))))))
    (setf (declaration *current-context*) decl)
    *current-context*))

;; patch for theory instantiations 20.05.03

(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)))))