In addition to lifting many
to work with symbolic values, Rosette also lifts Racket’s
As in Racket, a structure is an instance of a structure type—a
record datatype with zero or more fields.
Structure types are defined using the struct syntax. Defining a
structure type in this way also defines the necessary procedures for
creating instances of that type and for accessing their fields.
|> (struct point (x y) #:transparent)|
|; immutable transparent type|
|> (struct pt (x y))|
|; opaque immutable type|
|> (struct pnt (x y) #:mutable #:transparent)|
|; mutable transparent type|
Rosette structures can be concrete or symbolic. Their semantics matches that of Racket,
with one important exception: immutable transparent structures are treated as values
rather than references. This means that two such structures are
eq? if they belong to the same type and their corresponding field values are eq?.
Structures of opaque or mutable types are treated as references. Two such structures are
eq? only if the point to the same instance of the same type.
|> (eq? (point 1 2) (point 1 2)) ; point structures are values|
|> (eq? (pt 1 2) (pt 1 2)) ; pt structures are references|
|> (eq? (pnt 1 2) (pnt 1 2)) ; pnt structures are references|
Like unsolvable built-in datatypes,
symbolic structures cannot be created using define-symbolic. Instead,
they are created implicitly, by, for example, using an if expression
together with a symbolic value.
As well as lifting the struct
syntax, Rosette also lifts the following structure
properties, generic interfaces, and facilities for defining new properties and interfaces:
Lifted generics work as expected with symbolic values: