Record

"Record"s are mutable tuples consisting of a set of fields. An instantiation of the "record" type provides the name and type of each field of the "record" objects belonging to that type; there must be at least one field, and the field names must all be distinct. The case of the field names is not significant. Associated with each "record" type there is a "record" constructor that can be used to create new "record"s of the type (7.3). Each "record" type has a pair of methods for each field that allow users to read and modify the field; for a field named "A", these methods are named "A" and "set_A". Here is an example:

rt = record[a: int, b: real]  % a record type
x: rt                         % x will denote objects of this record type.
x := rt{a: 3, b: 1.1}         % construct an object
i: int := x.a( )              % read the a component
x.set_b(1.7)                  % modify the b component

In determining "record" type equality, the field names and types are significant and so is the order of the fields (3).

A "record" type "rt" has the following methods. ("st" is the related "struct" type, i.e., it has the same field names and types in the same order.)

Methods for "record" type "rt"

  a ( ) returns (T)
      % (here a is a field name and T is the corresponding type)
      % effects   returns the object stored in field a of self

  set_a (x: T)
      % (here a is a field name and T is the corresponding type)
      % modifies  self
      % effects   stores x in field a of self

  r_gets_r (x: rt)
      % modifies   self
      % effects   replaces the fields of self with the objects in the corresponding fields of x

  r_gets_s (x: st)
      % modifies   self
      % effects   replaces the fields of self with the objects in the corresponding fields of x

  to_s ( ) returns (st)
      % effects   returns an st object containing the elements of self in the corresponding fields.

  equal (x: rt) returns (bool)
      % effects   returns true if self and x are the same object else returns false.

  similar (x: rt) returns (bool)
        where all field types T of rt have similar(T) returns (bool)
      % effects   returns true if all corresponding fields of self and x are similar
      %           (using the T similar method for that field) else returns false

  copy ( ) returns (rt)
        where all field types T of rt have copy ( )  returns (T)
      % effects   returns a new record each of whose fields contains a
      %           copy of the object (obtained by calling that object's copy
      %           method) in the corresponding field of self

  unparse ( ) returns (string)
        where all field types T have unparse ( ) returns (string)
      % effects   returns a string representing the value of self.  The form is
      %           record{\tex{$n_1$}: \tex{$f_1$},...,\tex{$n_n$}: \tex{$f_n$}}, where \tex{$n_i$} is the name of the \tex{$i$}th
      %           record field and \tex{$f_i$} is obtained by calling the unparse method
      %           for the object in the corresponding field.

theta-questions@lcs.mit.edu