[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)) &lt;-<br>=A0 let &lt;- let &lt;- let* &lt;- let* &lt;- let* &lt;- :unk=
> nown &lt;-<br>=A0 update-parsed-file &lt;- parse-file* &lt;- (method parse-=
> file (string)) &lt;-<br>
> 
> =A0 typecheck-file &lt;- let &lt;- throw &lt;- let* &lt;- let &lt;- catch &=
> lt;- eval &lt;-<br>=A0 cerror &lt;- (method no-applicable-method (t)) &lt;-=
>  let &lt;- let &lt;- let* &lt;-<br>=A0 let* &lt;- let* &lt;- :unknown &lt;-=
>  update-parsed-file &lt;- parse-file* &lt;-<br>
> 
> =A0 (method parse-file (string)) &lt;- typecheck-file &lt;- letthrow &lt;-=
> =A0 ...<br><br><div class=3D"gmail_quote">2012/1/24 Zheng Bingzhou <span di=
> r=3D"ltr">&lt;<a href=3D"mailto:bingzhou.zheng@gmail.com";>bingzhou.zheng@gm=
> ail.com</a>&gt;</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 &quot;No methods applicable f=
> or generic function&quot;. <br><br>I just begin to use PVS, and write this =
> datatype based on a tutorial. I wonder what&#39;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--