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

parameterized mutually recursive datatypes?



Hallo,

I wonder if one can use mutually recursive datatypes in PVS in a
parameterized fashion. To illustrate what I mean let me slightly change
a well known example from the technical report "Abstract Datatypes in
PVS" by S. Owre and N. Shankar. The original example works perfectely well:

    arith: DATATYPE WITH SUBTYPES expr, term
      BEGIN
        num(n: int): num?: term         
        sum(t1: term, t2: term): sum?: term

        eq(t1: term, t2: term): eq?: expr
        ift(e: expr, t1: term, t2: term): ift?: term
      END arith

However, if I change this to

    arith[t: TYPE]: DATATYPE WITH SUBTYPES expr, term
      BEGIN
        num(n: t): num?: term         
        sum(t1: term, t2: term): sum?: term

        eq(t1: term, t2: term): eq?: expr
        ift(e: expr, t1: term, t2: term): ift?: term
      END arith

I get an error message "Could not determine the full theory instance".
To me this kind of usage seems fine and in fact I am often using it in
functional programming languages. Am I wrong, is this a bug of PVS, is
there any work-around etc. ?

Thanks in advance for the help.

    Andreas

--------------------------------
Andreas Reuleaux 
phone: +49 30 - 261 42 83   
e-mail: reuleaux@cs.tu-berlin.de