[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).

Regards,
Sam

(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)))
			    fparams))
	    (assert (every #'(lambda (fp) (eq (associated-decl fp) adecl))
			   (cdr fparams)))
	    (let* ((mi (mk-modname (id (current-theory)) nil nil nil (mk-dactuals dfmls)
				   (current-declaration)))
		   (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))
		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
> 
>   BEGIN
> 
>   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]                                                                        
>