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

[PVS-Help] Question on adding fields to a record

I'd like to find a way of extending records types. I couldn't find
anything in the manuals, but I'm hoping someone can help.

I have a STATE, which is a record e.g.
  [# a : typeA, 
     b : typeB #]

To STATE I'd like to add new fields such as
[#t1  : TYPE t1 #] in a uniform manner, so as to get
     [# a : typeA, 
        b : typeB, 
       t1 : typet1 #] 
without knowing the contents of STATE. (I.e. STATE would be a 
theory parameter).

The obvious solution is

[# state : STATE,
   t1 : typet1 #]

but I may do this repeatedly, resulting in something unwieldly

[# state : [# state : [# state : STATE, t1 : typet2 #], t2 : typet2 #], 
    t3 : typet3 #]

Is there anyway of creating a new, but flat, type (using STATE as a
parameter) including the contents of STATE, and my new fields? All
suggestions welcome.