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

Re: [PVS-Help] Type checking issue

Hi Jonathan,

This is indeed a bug; I'm including a patch for it below.
Simply create a <PVS>/lib/pvs-patches/ directory (where <PVS> is where you
installed PVS), and copy it there.  It will be loaded automatically on
startup (you can look in the *pvs* buffer to see that it is being loaded,
along with the nasa lib patches).


(in-package :pvs)

(defun maybe-instantiate-from-decl-formals* (reses ex)
  (when reses
    (let* ((dfmls (decl-formals (current-declaration)))
	   (fparams (when dfmls (free-params (car reses))))
	   (adecl (let ((dfml (find-if #'decl-formal-type? fparams)))
		    (when dfml (associated-decl dfml)))))
      (or (when (and fparams (length= fparams dfmls)
		     (every #'(lambda (fp)
				(and (decl-formal? fp)
				     (member fp dfmls :test #'same-id)))
	    (assert (every #'(lambda (fp) (eq (associated-decl fp) adecl))
			   (cdr fparams)))
	    (let* ((mi (mk-modname (id (current-theory)) nil nil nil (mk-dactuals dfmls)
		   (nex (subst-mod-params ex mi (current-theory) adecl)))
	      (when (fully-instantiated? nex)
		(setf (resolutions ex) (resolutions nex)
		      (actuals ex) (actuals nex)
		      (dactuals ex) (dactuals nex)
		      (free-parameters ex) 'unbound)
		(assert (fully-instantiated? ex))
	  (maybe-instantiate-from-decl-formals* (cdr reses) ex)))))
Jonathan Ostroff <jonathan@xxxxxxxx> wrote:

> The snippet below reproduces mysterious behaviour in a bigger project
> ===
> tup_small : THEORY
>   ARR [T: TYPE]: TYPE =
>   [# size    : nat
>    , content : [below(size) -> T]
>    #]
>   TUP [T: TYPE] : TYPE = [T, nat]
>   valid_bag? [T: TYPE] (a: ARR[TUP]): bool =
>     TRUE
>   END tup_small
> ===
> When trying to type check, I get at the bottom a message that says SPC-Scroll, I-ignore etc.
> There is also an Error:assertion report at the top.
> I am wondering what I did wrong? 
> Thanks,
> Jonathan
> [cid]