[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: bug?

Michel,

I just wanted to let you know that I have fixed this bug, and the fix will
be included in the next patch release.

Regards,

Sam Owre

> To demonstrate the problem I've extracted a few lines from my
> specification:
> 
> test[t: TYPE, c:nat]: THEORY 
> BEGIN
>   P(a:t): int
> END test
> 
> test2[t: TYPE, c:nat]: DATATYPE 
> BEGIN
>   Q(a:t): int
> END test2
> 
> I have the following question. What is the reason that when I try to
> typecheck that text, PVS (PVS 2.1 Test (patch level 2.399)) yields the
> message:
> 
>   Error: No methods applicable for generic function
>   #<STANDARD-GENERIC-FUNCTION MODULE-INSTANCE> with args (NIL) of
>   classes (NULL)
> 
> for the line:
>   Q(a:t): int
> 
> If I continue typechecking I get another message:
>   Could not determine the full theory instance for t
> 
> However, there is no problem with the theory test which has the same
> parameters and the problem disappears if I remove the constant c from
> the datatype.
> 
> Is it a bug, or my understanding of parameterized datatypes is wrong?
> 
> Thanks,
> Michal