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

Re: [PVS-Help] Datatypes and equality

Hi Erika,

The function you need is tc-eq, which says whether two
terms (or types) are equivalent, and ignores the place
(and all other irrelevant slots).


Erika Rice <erice@cs.washington.edu> wrote:

> I have defined a datatype and written a Lisp function which extracts
> the subterms which represent something of that datatype from a
> formula.  I want to compare those subterms for equality, but I cannot
> use Lisp equals because the objects representing the datatype differ
> in the "place" field.  Is there a function defined is the PVS system
> for comparing two Lisp objects representing some instance of a
> datatype, or do I need to write it myself?
> A more concrete phrasing of the problem is below.
> Thank you,
>     Erika Rice
> *********************************************************************
> I have a datatype which looks approximately like:
>     rhodium [varid, constid:TYPE]: DATATYPE WITH SUBTYPES expr
>     BEGIN
>         ...
>         addr(e:expr): addr? : expr
>         const(cid: constid): const? : expr
>         vrbl(vid: varid): vrbl? : expr
>         ...
>     END rhodium
> And a formula that looks something like
>     ... addr(vrbl(X)) ... AND ... addr(vrbl(Y)) ... OR ... addr(vrbl(X))
> And a function which given the above formula returns a list
>     (addr(vrbl(X)) addr(vrbl(Y)) addr(vrbl(X)))
> I want to remove the duplicates, but the first and second
> addr(vrbl(X)) are not equal because they differ in the place slot of
> the object they are represented by.  I want to know if there is a
> built in way to compare objects representing datatypes for equality.