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

*To*: pvs-help@csl.sri.com*Subject*: parameterized mutually recursive datatypes?*From*: Andreas Reuleaux <reuleaux@cs.tu-berlin.de>*Date*: Sun, 30 Nov 1997 10:04:52 +0100 (MET)

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

- Prev by Date:
**A question from KAIST** - Next by Date:
**questions about pvs...** - Prev by thread:
**Re: questions about pvs...** - Next by thread:
**A question from KAIST** - Index(es):