Metadata

The metadata attribute must be followed by a string (that is, by a data element in the STRING module, see Section 7.8). The metadata attribute is intended to hold data about the statement in whatever syntax the user cares to create/parse. It is like a comment that is carried around with the statement. Usual string escape conventions apply. For example, we could add the distributive law

  eq (N + M) * I = (N * I) + (M * I) [metadata "distributive law"] .

with the comment documenting that this is the distributive law.

The metadata attribute can also be associated to operator declarations. Note that, like ctor, metadata is attached to a specific operator declaration and not to the (possibly overloaded) operator itself. Thus:

• two subsorted overloaded declarations may have different metadata attributes,
• a metadata attribute is not copied by the ditto attribute (see Section 4.4.6), and
• a declaration may have a metadata attribute as well as a ditto attribute.

Under these conditions, the following ad-hoc example is therefore legal:

  fmod METADATA-EX is
    sorts Foo Bar .
    subsort Foo < Bar .
    op f : Foo -> Foo [memo metadata "f on Foos"] .
    op f : Bar -> Bar [ditto metadata "f on Bars"] .
  endfm