[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Type checking issue
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).
(defun maybe-instantiate-from-decl-formals* (reses ex)
(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))
(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 =
> 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?