[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Re: the problem "No methods applicable for genericfunction"
Hi Zheng,
I have an idea where the problem is, but I'm having difficulty recreating
it, so it's difficult to fix. I suspect that you made some edits, and the
typechecker is now confused. If you can recall what changes you made to
the file before this bug it would help ('C-h l' shows the last fifty
keystrokes, but it may be too late for that).
Do you by any chance have a ~/.pvs.lisp file that is being loaded? And if
you restart PVS do you still see the problem? What if you run 'C-u M-x
tc'?
Regards,
Sam
Zheng Bingzhou <bingzhou.zheng@gmail.com> wrote:
> --0015175cd36ec385ec04b74bc914
> Content-Type: text/plain; charset=ISO-8859-1
>
> [4c] pvs(41): :bt
> Evaluation stack:
>
> (method no-applicable-method (t)) <-
> let <- let <- let* <- let* <- let* <- :unknown <-
> update-parsed-file <- parse-file* <- (method parse-file (string)) <-
> typecheck-file <- let <- throw <- let* <- let <- catch <- eval <-
> cerror <- (method no-applicable-method (t)) <- let <- let <- let* <-
> let* <- let* <- :unknown <- update-parsed-file <- parse-file* <-
> (method parse-file (string)) <- typecheck-file <- letthrow <- ...
>
> 2012/1/24 Zheng Bingzhou <bingzhou.zheng@gmail.com>
>
> > Hi,
> >
> > When I try to define an inductive type like below:
> >
> > ivlOP : DATATYPE
> > BEGIN
> > id : id?
> > add (lop, rop: ivlOP): add?
> > sub (lop, rop: ivlOP): sub?
> > mul (lop, rop: ivlOP): mul?
> > div (lop, rop: ivlOP): div?
> > END ivlop
> >
> > I do the type-checking and get the error "No methods applicable for
> > generic function".
> >
> > I just begin to use PVS, and write this datatype based on a tutorial. I
> > wonder what's wrong with this definition? any advice
> >
> > By the way, I use PVS5.0 with the library nasalib.
> >
> > Thanks,
> > Bingzhou
> >
> >
> >
>
> --0015175cd36ec385ec04b74bc914
> Content-Type: text/html; charset=ISO-8859-1
> Content-Transfer-Encoding: quoted-printable
>
> [4c] pvs(41): :bt<br>Evaluation stack:<br><br>(method no-applicable-method =
> (t)) <-<br>=A0 let <- let <- let* <- let* <- let* <- :unk=
> nown <-<br>=A0 update-parsed-file <- parse-file* <- (method parse-=
> file (string)) <-<br>
>
> =A0 typecheck-file <- let <- throw <- let* <- let <- catch &=
> lt;- eval <-<br>=A0 cerror <- (method no-applicable-method (t)) <-=
> let <- let <- let* <-<br>=A0 let* <- let* <- :unknown <-=
> update-parsed-file <- parse-file* <-<br>
>
> =A0 (method parse-file (string)) <- typecheck-file <- letthrow <-=
> =A0 ...<br><br><div class=3D"gmail_quote">2012/1/24 Zheng Bingzhou <span di=
> r=3D"ltr"><<a href=3D"mailto:bingzhou.zheng@gmail.com";>bingzhou.zheng@gm=
> ail.com</a>></span><br>
>
> <blockquote class=3D"gmail_quote" style=3D"margin:0pt 0pt 0pt 0.8ex;border-=
> left:1px solid rgb(204,204,204);padding-left:1ex">Hi,<br><br>When I try to =
> define an inductive type like below:<br><br>=A0=A0 ivlOP :=A0 DATATYPE<br>=
> =A0=A0 BEGIN<br>
>
> =A0=A0=A0=A0=A0=A0=A0 id : id?<br>=A0=A0=A0=A0=A0=A0=A0 add (lop, rop: ivlO=
> P): add?<br>=A0=A0=A0=A0=A0=A0=A0 sub (lop, rop: ivlOP): sub?<br>=A0=A0=A0=
> =A0=A0=A0=A0 mul (lop, rop: ivlOP): mul?<br>
> =A0=A0=A0=A0=A0=A0=A0 div=A0 (lop, rop: ivlOP): div?<br>=A0=A0 END ivlop<br=
> ><br>I do the type-checking and get the error "No methods applicable f=
> or generic function". <br><br>I just begin to use PVS, and write this =
> datatype based on a tutorial. I wonder what's wrong with this definitio=
> n? any advice<br>
>
>
> <br>By the way, I use PVS5.0 with the library nasalib.<br><br>Thanks,<br>Bi=
> ngzhou<br><br><br>
> </blockquote></div><br>
>
> --0015175cd36ec385ec04b74bc914--