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

bug?



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