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

[PVS-Help] Datatypes and equality

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
        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.