[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Typechecking confused by a LET expression?
Piotr Trojanek <piotr.trojanek@xxxxxxxxx> wrote:
> Hi PVS experts,
> the attached example fails to type check, but I do not understand why.
> It seems that the typechecker is somehow confused by a LET expression
> (see comments in file).
> Can you help?
> Piotr Trojanek
This is a bug. I'm including a patch for it below. Add it to your
~/.pvs.lisp file (create it if necessary) and restart PVS.
(defun make-recursive-tcc-decl (name arguments)
(when (null arguments)
"Recursive definition occurrence ~a must have arguments" name))
(multiple-value-bind (dfmls dacts thinst)
(declare (ignore dacts))
(let* ((*generate-tccs* 'none)
(cth (module cdecl))
(tccdecl (mk-termination-tcc id nil dfmls))
(meas (measure cdecl))
(or (when (ordering cdecl)
(copy (ordering cdecl)))
(appl1 (make!-recursive-application meas (outer-arguments cdecl)))
(appl2 (make!-recursive-application meas arguments))
(typecheck* (mk-application ordering appl2 appl1)
*boolean* nil nil)))
(true-conc? (or (member relterm
(let ((*assert-typepreds* nil))
(form (unless true-conc?
(uform (cond ((or true-conc? (tcc-evaluates-to-true form))
(not (or *in-checker* *in-evaluator*)))
(t (beta-reduce form))))
(suform (if thinst
(subst-mod-params uform thinst cth cdecl))
(unless (tc-eq uform *true*)
(when (and *false-tcc-error-flag*
(tc-eq suform *false*))
"Termination TCC for this expression simplifies to false:~2% ~a"
(setf (definition tccdecl) suform)
(typecheck* tccdecl nil nil nil)))))