opattr

operator attributes

In the specification of an operator using the op (and related) keyword, attributes of the operator can be specified. An <attribute-list> is a space-separate list of single attribute definitions. Currently the following attributes are supported

associative ~ specifies an associative operator, alias assoc

commutative ~ specifies a commutative operator, alias comm

itempotence ~ specifies an idempotent operator, alias idem

id: <const> ~ specifies that an identity of the operator exists and that it is <const>

prec: <int> ~ specifies the parsing precedence of the operator, an integer . Smaller precedence values designate stronger binding. See operator precedence for details of the predefined operator precedence values.

l-assoc and r-assoc ~ specifies that the operator is left-associative or right-associative

constr ~ specifies that the operator is a constructor of the coarity sort. (not evaluated at the moment)

strat: ( <int-list> ) ~ specifies the evaluation strategy. Each integer in the list refers to an argument of the operator, where 0 refers to the whole term, 1 for the first argument, etc. Evaluation proceeds in order of the <int-list>. Example:

`op if_then_else_fi : Bool Int Int -> Int { strat: (1 0) }`

In this case the first argument (the Boolean term) is tried to
be evaluated, and depending on that either the second or third.
But if the first (Boolean) argument cannot be evaluated, 
no evaluation in the subterms will appear.

Using negative values allows for lazy evaluation of the corresponding
arguments.

memo ~ tells the system to remember the results of evaluations where the operator appeared. See memo switch for details.

Remarks:

• Several operators of the same arity/coarity can be defined by using ops instead of op:

  ops f g : S -> S

  For the case of mixfix operators the underbars have to be given and the expression surrounded by parenthesis:

  ops (_+_) (_*_) : S S -> S

• Spaces can be part of the operator name, thus an operator definition of op foo op : S -> S is valid, but not advisable, as parsing needs hints.

• A single underbar cannot be an operator name.

Related: bop